dexpr.ml 58.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10 11 12 13 14 15 16 17
(********************************************************************)

open Stdlib
open Ident
open Ty
open Term
open Ity
open Expr
18
open Pmodule
19 20 21 22

(** Program types *)

type dity =
Andrei Paskevich's avatar
Andrei Paskevich committed
23
  | Dvar of dvar ref          (* destructible "fresh" type variable *)
24 25
  | Dutv of tvsymbol          (* undestructible "user" type variable *)
  | Durg of dity * region     (* undestructible "user" region *)
26 27 28
  | Dapp of itysymbol * dity list * dity list

and dvar =
29 30 31 32 33
  | Dval of dity              (* i am equal to dity *)
  | Dpur of dity              (* i am equal to the purified dity *)
  | Dsim of dity * tvsymbol   (* our purified types are equal *)
  | Dreg of dity * tvsymbol   (* unassigned region *)
  | Dtvs of        tvsymbol   (* unassigned variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
34

35
(* In Dreg and Durg, the dity field is a Dapp of the region's type. *)
36 37 38

type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)

Andrei Paskevich's avatar
Andrei Paskevich committed
39
let dity_of_dvty (argl,res) =
40
  List.fold_right (fun a d -> Dapp (its_func, [a;d], [])) argl res
Andrei Paskevich's avatar
Andrei Paskevich committed
41

42 43 44 45 46 47 48 49 50 51
let dity_fresh () =
  Dvar (ref (Dtvs (create_tvsymbol (id_fresh "mu"))))

let dity_reg d =
  Dvar (ref (Dreg (d, create_tvsymbol (id_fresh "rho"))))

let rec dity_sim = function
  | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
  | Durg (d,_) -> dity_sim d
  | d -> Dvar (ref (Dsim (d, create_tvsymbol (id_fresh "eta"))))
52

53 54 55 56 57 58
let rec dity_pur = function
  | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
  | Durg (d,_) -> dity_pur d
  | d -> Dvar (ref (Dpur d))

let app_map fn s tl rl = Dapp (s, List.map fn tl, List.map fn rl)
59 60 61 62

let dity_of_ity ity =
  let hr = Hreg.create 3 in
  let rec dity ity = match ity.ity_node with
63 64 65 66 67 68 69
    | Ityvar (v,false) -> Dutv v
    | Ityvar (v,true)  -> dity_pur (Dutv v)
    | Ityapp (s,tl,rl) -> app_map dity s tl rl
    | Ityreg ({reg_its = s; reg_args = tl; reg_regs = rl} as r) ->
        try Hreg.find hr r with Not_found ->
        let d = dity_reg (app_map dity s tl rl) in
        Hreg.add hr r d; d in
70 71 72
  dity ity

let rec ity_of_dity = function
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
  | Dutv v -> ity_var v
  | Durg (_,r) -> ity_reg r
  | Dvar {contents = Dval d} -> ity_of_dity d
  | Dvar {contents = Dpur d} -> ity_purify (ity_of_dity d)
  | Dvar ({contents = Dsim (d,_)} as r) ->
      let rec refresh ity = match ity.ity_node with
        | Ityreg {reg_its = s; reg_args = tl} | Ityapp (s,tl,_) ->
            ity_app s (List.map refresh tl) []
        | Ityvar (v,_) -> ity_var v in
      let rec dity ity = match ity.ity_node with
        | Ityreg r ->
            Durg (app_map dity r.reg_its r.reg_args r.reg_regs, r)
        | Ityapp (s,tl,rl) -> app_map dity s tl rl
        | Ityvar (v,true)  -> dity_pur (Dutv v)
        | Ityvar (v,false) -> Dutv v in
      let t = refresh (ity_of_dity d) in
      r := Dval (dity t); t
  | Dvar ({contents = Dreg (Dapp (s,tl,rl) as d,_)} as r) ->
      let reg = create_region (id_fresh "rho") s
        (List.map ity_of_dity tl) (List.map ity_of_dity rl) in
      r := Dval (Durg (d, reg)); ity_reg reg
94 95 96 97
  | Dvar r ->
      let v = create_tvsymbol (id_fresh "xi") in
      r := Dval (Dutv v); ity_var v
  | Dapp (s,tl,rl) ->
98
      ity_app_pure s (List.map ity_of_dity tl) (List.map ity_of_dity rl)
99 100 101 102

(** Destructive type unification *)

let rec occur_check v = function
103 104 105 106 107 108 109 110 111 112 113 114 115 116
  | Dvar {contents = (Dval d|Dpur d)} | Durg (d,_) ->
      occur_check v d
  | Dvar {contents = (Dsim (d,u)|Dreg (d,u))} ->
      if tv_equal u v then raise Exit else occur_check v d
  | Dvar {contents = Dtvs u} | Dutv u ->
      if tv_equal u v then raise Exit
  | Dapp (_,dl,_) ->
      List.iter (occur_check v) dl

let rec dity_unify_weak d1 d2 = match d1,d2 with
  | Dvar {contents = (Dval d1|Dpur d1|Dsim (d1,_)|Dreg (d1,_))}, d2
  | d1, Dvar {contents = (Dval d2|Dpur d2|Dsim (d2,_)|Dreg (d2,_))}
  | Durg (d1,_), d2 | d1, Durg (d2,_) ->
      dity_unify_weak d1 d2
117 118 119 120 121 122
  | Dvar {contents = Dtvs u},
    Dvar {contents = Dtvs v} when tv_equal u v ->
      ()
  | Dvar ({contents = Dtvs v} as r), d
  | d, Dvar ({contents = Dtvs v} as r) ->
      occur_check v d;
123
      r := Dsim (d,v)
124 125
  | Dutv u, Dutv v when tv_equal u v ->
      ()
126
  | Dapp (s1,dl1,_), Dapp (s2,dl2,_) when its_equal s1 s2 ->
127
      List.iter2 dity_unify_weak dl1 dl2
128 129
  | _ -> raise Exit

130 131 132 133 134 135 136 137 138 139 140 141 142 143
let dity_app_fresh s dl =
  let mv = List.fold_right2 Mtv.add s.its_ts.ts_args dl Mtv.empty in
  let hr = Hreg.create 3 in
  let rec ity_inst ity = match ity.ity_node with
    | Ityreg r -> reg_inst r
    | Ityvar (v, false) -> Mtv.find v mv
    | Ityvar (v, true) -> dity_pur (Mtv.find v mv)
    | Ityapp (s,tl,rl) -> app_map ity_inst s tl rl
  and reg_inst ({reg_its = s; reg_args = tl; reg_regs = rl} as r) =
    try Hreg.find hr r with Not_found ->
    let d = dity_reg (app_map ity_inst s tl rl) in
    Hreg.replace hr r d; d in
  Dapp (s, dl, List.map reg_inst s.its_regions)

144 145 146 147 148 149
let rec dity_refresh = function
  | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
  | Durg (d,_) -> dity_refresh d
  | Dutv _ as d -> d
  | Dvar {contents = Dtvs _} -> dity_fresh ()
  | Dapp (s,dl,_) ->
150
      let d = dity_app_fresh s (List.map dity_refresh dl) in
151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
      if its_immutable s then d else dity_reg d

let rec dity_unify_asym d1 d2 = match d1,d2 with
  | Durg _, _ | Dutv _, _ -> raise Exit (* we cannot be pure then *)
  | d1, Dvar {contents = (Dval d2|Dpur d2|Dsim (d2,_)|Dreg (d2,_))}
  | d1, Durg (d2,_)
  | Dvar {contents = Dval d1}, d2 ->
      dity_unify_asym d1 d2
  | Dvar {contents = Dpur d1}, d2 ->
      dity_unify_weak d1 d2
  | Dvar ({contents = Dsim (d1,_)} as r), d2 ->
      dity_unify_weak d1 d2;
      r := Dpur d1
  | Dvar ({contents = Dreg (d1,_)} as r), d2 ->
      dity_unify_asym d1 d2;
      r := Dval d1
  | Dvar ({contents = Dtvs u} as r),
    Dvar {contents = Dtvs v} when tv_equal u v ->
      r := Dpur (dity_fresh ())
  | Dvar ({contents = Dtvs v} as r), d ->
      occur_check v d;
      r := Dpur d
  | d (* not a Dvar! *), Dvar ({contents = Dtvs v} as r) ->
      occur_check v d;
      let d2 = dity_refresh d in
      dity_unify_asym d d2;
      r := Dval d2
  | Dapp (s1,dl1,rl1), Dapp (s2,dl2,rl2) when its_equal s1 s2 ->
      List.iter2 dity_unify_asym dl1 dl2;
      List.iter2 dity_unify_asym rl1 rl2
  | _ -> raise Exit
182

183 184 185 186 187 188 189 190
let rec dity_unify d1 d2 = match d1,d2 with
  | Dvar {contents = Dval d1}, d2 | d1, Dvar {contents = Dval d2} ->
      dity_unify d1 d2
  | Dvar ({contents = Dpur d2}), d1 (* yes, it's d2 on the left *)
  | d1, Dvar ({contents = Dpur d2}) ->
      dity_unify_asym d1 d2
  | Dvar ({contents = Dsim (_,u)}),
    Dvar ({contents = Dsim (_,v)}) when tv_equal u v ->
191
      ()
192 193 194 195 196 197 198
  | Dvar ({contents = Dsim (d1,v)} as r), d
  | d, Dvar ({contents = Dsim (d1,v)} as r) ->
      occur_check v d; (* not necessary? *)
      dity_unify_weak d1 d;
      r := Dval d
  | Dvar {contents = Dreg (_,u)},
    Dvar {contents = Dreg (_,v)} when tv_equal u v ->
199
      ()
200 201 202 203 204 205
  | Dvar ({contents = Dreg (d1,v)} as r),
    ((Dapp _ as d2 | Durg (d2,_) | Dvar {contents = Dreg (d2,_)}) as d)
  | ((Dapp _ as d1 | Durg (d1,_)) as d),
    Dvar ({contents = Dreg (d2,v)} as r) ->
      occur_check v d; (* not necessary! *)
      dity_unify d1 d2;
206
      r := Dval d
207 208 209 210 211 212 213 214 215 216 217 218 219 220 221
  | Dvar ({contents = Dtvs u}),
    Dvar ({contents = Dtvs v}) when tv_equal u v ->
      ()
  | Dvar ({contents = Dtvs v} as r), d
  | d, Dvar ({contents = Dtvs v} as r) ->
      occur_check v d;
      r := Dval d
  | Dutv u, Dutv v when tv_equal u v ->
      ()
  | Durg (_,r1), Durg (_,r2) when reg_equal r1 r2 ->
      ()
  | Dapp (s1,dl1,rl1), Dapp (s2,dl2,rl2) when its_equal s1 s2 ->
      List.iter2 dity_unify dl1 dl2;
      List.iter2 dity_unify rl1 rl2
  | _ -> raise Exit
222 223 224

(** Built-in types *)

225 226 227 228
let dity_int  = Dapp (its_int,  [], [])
let dity_real = Dapp (its_real, [], [])
let dity_bool = Dapp (its_bool, [], [])
let dity_unit = Dapp (its_unit, [], [])
229

230
(*
231 232
let dvty_int  = [], dity_int
let dvty_real = [], dity_real
233
*)
234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
let dvty_bool = [], dity_bool
let dvty_unit = [], dity_unit

(** Pretty-printing *)

let rprinter =
  let sanitizer = Ident.sanitizer Ident.char_to_lalpha Ident.char_to_alnumus in
  Ident.create_ident_printer [] ~sanitizer

let print_args pr fmt tl = if tl <> [] then
  Format.fprintf fmt "@ %a" (Pp.print_list Pp.space pr) tl

let print_regs pr fmt rl = if rl <> [] then
  Format.fprintf fmt "@ <%a>" (Pp.print_list Pp.comma pr) rl

let protect_on x s = if x then "(" ^^ s ^^ ")" else s

251 252 253 254 255 256 257
let rec print_dity pur pri fmt = function
  | Dvar {contents = Dval d} ->
      print_dity pur pri fmt d
  | Dvar {contents = (Dpur d|Dsim (d,_)|Dreg (d,_))}
  | Durg (d,_) when pur ->
      print_dity pur pri fmt d
  | Dvar {contents = Dtvs v} | Dutv v ->
258
      Pretty.print_tv fmt v
259 260 261 262 263
  | Dvar {contents = Dpur d} ->
      Format.fprintf fmt "{%a}" (print_dity true 0) d
  | Dvar {contents = Dsim (d,_)} ->
      Format.fprintf fmt "[%a]" (print_dity true 0) d
  | Dvar {contents = Dreg (Dapp (s,tl,rl),{tv_name = id})}
264
  | Durg (Dapp (s,tl,rl),{reg_name = id}) ->
265 266 267 268 269
      Format.fprintf fmt
        (protect_on (pri > 1 && (tl <> [] || rl <> [])) "%a%a%a@ @@%s")
        Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl
          (print_regs (print_dity pur 0)) rl (Ident.id_unique rprinter id)
  | Dvar {contents = Dreg _} | Durg _ -> assert false
270
  | Dapp (s,[t1;t2],[]) when its_equal s its_func ->
271
      Format.fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
272
        (print_dity pur 1) t1 (print_dity pur 0) t2
273
  | Dapp (s,tl,[]) when is_ts_tuple s.its_ts ->
274 275 276 277 278 279 280 281 282
      Format.fprintf fmt "(%a)" (Pp.print_list Pp.comma (print_dity pur 0)) tl
  | Dapp (s,tl,_) when pur ->
      Format.fprintf fmt (protect_on (pri > 1 && tl <> []) "%a%a")
        Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl
  | Dapp (s,tl,rl) when its_immutable s ->
      Format.fprintf fmt
        (protect_on (pri > 1 && (tl <> [] || rl <> [])) "%a%a%a")
        Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl
          (print_regs (print_dity pur 0)) rl
283
  | Dapp (s,tl,rl) ->
284 285 286 287
      Format.fprintf fmt
        (protect_on (pri > 1 && (tl <> [] || rl <> [])) "{%a}%a%a")
        Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl
          (print_regs (print_dity pur 0)) rl
288

289
let print_dity fmt d = print_dity false 0 fmt d
290 291 292 293

(* Specialization of symbols *)

let specialize_scheme tvs (argl,res) =
294
  let hv = Htv.create 3 in
295
  let rec spec_dity = function
296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
    | Dvar {contents = Dval d} -> spec_dity d
    | Dvar {contents = Dpur d} -> dity_pur (spec_dity d)
    | Dvar {contents = Dsim (d,v)} ->
        (try Htv.find hv v with Not_found ->
        let nd = dity_sim (spec_dity d) in
        Htv.add hv v nd; nd)
    | Dvar {contents = Dreg (d,v)} ->
        (try Htv.find hv v with Not_found ->
        let nd = dity_reg (spec_dity d) in
        Htv.add hv v nd; nd)
    | Dvar {contents = Dtvs v} | Dutv v as d ->
        (try Htv.find hv v with Not_found ->
        (* even if v is frozen, it is polymorphic in its regions *)
        let nd = if Stv.mem v tvs then dity_fresh () else dity_sim d in
        Htv.add hv v nd; nd)
    | Dapp (s,dl,rl) -> app_map spec_dity s dl rl
    | Durg _ as d -> d in
313 314 315 316
  List.map spec_dity argl, spec_dity res

let spec_ity hv hr frz ity =
  let rec dity ity = match ity.ity_node with
317 318 319 320 321 322 323 324 325 326 327 328 329 330
    | Ityreg r ->
        (try Hreg.find hr r with Not_found ->
        let d = app_map dity r.reg_its r.reg_args r.reg_regs in
        let nd = if Mreg.mem r frz.isb_reg then Durg (d,r) else dity_reg d in
        Hreg.add hr r nd; nd)
    | Ityvar (v,pure) ->
        let nd = try Htv.find hv v with Not_found ->
          let nd =
            if Mtv.mem v frz.isb_var then Dutv v else
            if Mtv.mem v frz.isb_pur then dity_sim (Dutv v) else
            dity_fresh () in
          Htv.add hv v nd; nd in
        if pure then dity_pur nd else nd
    | Ityapp (s,tl,rl) -> app_map dity s tl rl in
331 332
  dity ity

Andrei Paskevich's avatar
Andrei Paskevich committed
333
let specialize_pv {pv_ity = ity} =
334 335
  spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity

Andrei Paskevich's avatar
Andrei Paskevich committed
336
let specialize_xs {xs_ity = ity} =
337 338
  spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity

339
let specialize_rs {rs_cty = cty} =
340 341 342 343
  let hv = Htv.create 3 and hr = Hreg.create 3 in
  let spec ity = spec_ity hv hr cty.cty_freeze ity in
  List.map (fun v -> spec v.pv_ity) cty.cty_args, spec cty.cty_result

344 345
let specialize_ls {ls_args = args; ls_value = res} =
  let hv = Htv.create 3 and hr = Hreg.create 3 in
346 347 348
  let spec_val _ ty = spec_ity hv hr isb_empty (ity_of_ty_pure ty) in
  let spec_arg ty = dity_sim (spec_val () ty) in
  List.map spec_arg args, Opt.fold spec_val dity_bool res
349

350 351 352
(** Patterns *)

type dpattern = {
Andrei Paskevich's avatar
Andrei Paskevich committed
353
  dp_pat  : pre_pattern;
354 355 356 357 358 359 360
  dp_dity : dity;
  dp_vars : dity Mstr.t;
  dp_loc  : Loc.position option;
}

type dpattern_node =
  | DPwild
361
  | DPvar  of preid * bool
362
  | DPapp  of rsymbol * dpattern list
363
  | DPas   of dpattern * preid * bool
364 365 366 367 368 369 370
  | DPor   of dpattern * dpattern
  | DPcast of dpattern * ity

(** Specifications *)

type ghost = bool

Andrei Paskevich's avatar
Andrei Paskevich committed
371
type dbinder = preid option * ghost * dity
372

373 374
type register_old = pvsymbol -> string -> pvsymbol

375
type 'a later = pvsymbol Mstr.t -> xsymbol Mstr.t -> register_old -> 'a
376 377 378 379 380 381
  (* specification terms are parsed and typechecked after the program
     expressions, when the types of locally bound program variables are
     already established. *)

type dspec_final = {
  ds_pre     : term list;
382
  ds_post    : (pvsymbol * term) list;
383
  ds_xpost   : (pvsymbol * term) list Mxs.t;
384
  ds_reads   : pvsymbol list;
385 386
  ds_writes  : term list;
  ds_diverge : bool;
387
  ds_checkrw : bool;
388 389
}

390
type dspec = ity -> dspec_final
391 392 393 394 395
  (* Computation specification is also parametrized by the result type.
     All vsymbols in the postcondition clauses in the [ds_post] field
     must have this type. All vsymbols in the exceptional postcondition
     clauses must have the type of the corresponding exception. *)

396 397 398
let old_mark = "'Old"
let old_mark_id = id_fresh old_mark

399 400 401 402
(** Expressions *)

type dinvariant = term list

403 404 405 406
type dxsymbol =
  | DElexn of string * dity
  | DEgexn of xsymbol

407 408 409 410 411 412 413 414
type dexpr = {
  de_node : dexpr_node;
  de_dvty : dvty;
  de_loc  : Loc.position option;
}

and dexpr_node =
  | DEvar of string * dvty
415
  | DEsym of prog_symbol
416
  | DEls of lsymbol
417
  | DEconst of Number.constant * dity
418
  | DEapp of dexpr * dexpr
419 420
  | DEfun of dbinder list * dity * mask * dspec later * dexpr
  | DEany of dbinder list * dity * mask * dspec later
421 422
  | DElet of dlet_defn * dexpr
  | DErec of drec_defn * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
423
  | DEnot of dexpr
424 425
  | DEand of dexpr * dexpr
  | DEor of dexpr * dexpr
426 427
  | DEif of dexpr * dexpr * dexpr
  | DEcase of dexpr * (dpattern * dexpr) list
428
  | DEassign of (dexpr * rsymbol * dexpr) list
429
  | DEwhile of dexpr * dinvariant later * variant list later * dexpr
430
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
431 432
  | DEtry of dexpr * (dxsymbol * dpattern * dexpr) list
  | DEraise of dxsymbol * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
433
  | DEghost of dexpr
434
  | DEexn of preid * dity * mask * dexpr
435
  | DEassert of assertion_kind * term later
436
  | DEpure of term later * dity
Andrei Paskevich's avatar
Andrei Paskevich committed
437 438 439
  | DEabsurd
  | DEtrue
  | DEfalse
440 441
  | DEcast of dexpr * dity
  | DEmark of preid * dity * dexpr
442 443 444
  | DEuloc of dexpr * Loc.position
  | DElabel of dexpr * Slab.t

445
and dlet_defn = preid * ghost * rs_kind * dexpr
446 447 448

and drec_defn = { fds : dfun_defn list }

449 450
and dfun_defn = preid * ghost * rs_kind * dbinder list *
  dity * mask * dspec later * variant list later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
451

452 453 454 455 456
(** Environment *)

type denv = {
  frozen : dity list;
  locals : (Stv.t option * dvty) Mstr.t;
457
  excpts : dxsymbol Mstr.t
458 459
}

460 461
let denv_contents d = d.locals

462
let denv_empty = { frozen = []; locals = Mstr.empty; excpts = Mstr.empty }
463

Andrei Paskevich's avatar
Andrei Paskevich committed
464 465
let is_frozen frozen v =
  try List.iter (occur_check v) frozen; false with Exit -> true
466 467 468

let freeze_dvty frozen (argl,res) =
  let rec add l = function
469 470 471
    | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
    | Durg (d,_) -> add l d
    | Dvar {contents = Dtvs _}
472
    | Dutv _ as d -> d :: l
473
    | Dapp (_,tl,_) -> List.fold_left add l tl in
474 475 476 477
  List.fold_left add (add frozen res) argl

let free_vars frozen (argl,res) =
  let rec add s = function
478 479 480 481
    | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
    | Durg (d,_) -> add s d
    | Dvar {contents = Dtvs v} | Dutv v ->
        if is_frozen frozen v then s else Stv.add v s
482
    | Dapp (_,tl,_) -> List.fold_left add s tl in
483 484
  List.fold_left add (add Stv.empty res) argl

485 486 487 488 489 490 491
let denv_add_exn { frozen = fz; locals = ls; excpts = xs } id dity =
  let xs = Mstr.add id.pre_name (DElexn (id.pre_name, dity)) xs in
  { frozen = freeze_dvty fz ([], dity); locals = ls; excpts = xs }

let denv_add_mono { frozen = fz; locals = ls; excpts = xs } id dvty =
  let ls = Mstr.add id.pre_name (None, dvty) ls in
  { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }
492

493 494 495
let denv_add_poly { frozen = fz; locals = ls; excpts = xs } id dvty =
  let ls = Mstr.add id.pre_name (Some (free_vars fz dvty), dvty) ls in
  { frozen = fz; locals = ls; excpts = xs }
496

497 498 499
let denv_add_rec_mono { frozen = fz; locals = ls; excpts = xs } id dvty =
  let ls = Mstr.add id.pre_name (Some Stv.empty, dvty) ls in
  { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }
500

501 502 503
let denv_add_rec_poly { frozen = fz; locals = ls; excpts = xs } fz0 id dvty =
  let ls = Mstr.add id.pre_name (Some (free_vars fz0 dvty), dvty) ls in
  { frozen = fz; locals = ls; excpts = xs }
504

505
let denv_add_rec denv fz0 id ((argl,res) as dvty) =
506
  let rec is_explicit = function
507 508 509
    | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
    | Durg (d,_) -> is_explicit d
    | Dvar {contents = Dtvs _} -> false
Andrei Paskevich's avatar
Andrei Paskevich committed
510
    | Dutv _ -> true
511
    | Dapp (_,tl,_) -> List.for_all is_explicit tl in
512
  if List.for_all is_explicit argl && is_explicit res
513
  then denv_add_rec_poly denv fz0 id dvty
514 515 516 517
  else denv_add_rec_mono denv id dvty

let denv_add_var denv id dity = denv_add_mono denv id ([], dity)

Andrei Paskevich's avatar
Andrei Paskevich committed
518
let denv_add_let denv (id,_,_,({de_dvty = dvty} as de)) =
519 520 521
  if fst dvty = [] then denv_add_mono denv id dvty else
  let rec is_value de = match de.de_node with
    | DEghost de | DEuloc (de,_) | DElabel (de,_) -> is_value de
522
    | DEvar _ | DEsym _ | DEls _ | DEfun _ | DEany _ -> true
523 524 525 526 527
    | _ -> false in
  if is_value de
  then denv_add_poly denv id dvty
  else denv_add_mono denv id dvty

528 529
let denv_add_args { frozen = fz; locals = ls; excpts = xs } bl =
  let l = List.fold_left (fun l (_,_,t) -> t::l) fz bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
530
  let add s (id,_,t) = match id with
531 532 533 534
    | Some {pre_name = n} ->
        Mstr.add_new (Dterm.DuplicateVar n) n (None, ([],t)) s
    | None -> s in
  let s = List.fold_left add Mstr.empty bl in
535
  { frozen = l; locals = Mstr.set_union s ls; excpts = xs }
536

537 538
let denv_add_pat { frozen = fz; locals = ls; excpts = xs } dp =
  let l = Mstr.fold (fun _ t l -> t::l) dp.dp_vars fz in
539
  let s = Mstr.map (fun t -> None, ([], t)) dp.dp_vars in
540
  { frozen = l; locals = Mstr.set_union s ls; excpts = xs }
541 542 543 544 545 546 547 548 549 550 551

let mk_node n = function
  | Some tvs, dvty -> DEvar (n, specialize_scheme tvs dvty)
  | None,     dvty -> DEvar (n, dvty)

let denv_get denv n =
  mk_node n (Mstr.find_exn (Dterm.UnboundVar n) n denv.locals)

let denv_get_opt denv n =
  Opt.map (mk_node n) (Mstr.find_opt n denv.locals)

552 553 554 555 556 557
exception UnboundExn of string

let denv_get_exn denv n = Mstr.find_exn (UnboundExn n) n denv.excpts

let denv_get_exn_opt denv n = Mstr.find_opt n denv.excpts

558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579
let denv_pure denv get_dty =
  let ht = Htv.create 3 in
  let hi = Hint.create 3 in
  let rec fold = function
    | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
    | Durg (d,_) -> fold d
    | Dvar {contents = Dtvs v} as d ->
        begin try fst (Htv.find ht v) with Not_found ->
        let f = Dterm.dty_fresh () in Htv.add ht v (f,d); f end
    | Dapp (s,dl,_) -> Dterm.dty_app s.its_ts (List.map fold dl)
    | Dutv v -> Dterm.dty_var v in
  let pure_denv = Mstr.mapi (fun n (_, dvty) ->
    Dterm.DTvar (n, fold (dity_of_dvty dvty))) denv.locals in
  let dty = get_dty pure_denv in
  Htv.iter (fun v (f,_) ->
    try Dterm.dty_match f (ty_var v) with Exit -> ()) ht;
  let fnS s dl = dity_app_fresh (restore_its s) dl in
  let fnV v = try snd (Htv.find ht v) with Not_found -> Dutv v in
  let fnI i = try Hint.find hi i with Not_found ->
    let d = dity_fresh () in Hint.add hi i d; d in
  dity_pur (Dterm.dty_fold fnS fnV fnI dty)

580 581 582 583 584 585 586 587 588 589 590
(** Unification tools *)

let dity_unify_app ls fn (l1: 'a list) (l2: dity list) =
  try List.iter2 fn l1 l2 with Invalid_argument _ ->
    raise (BadArity (ls, List.length l1))

let dpat_expected_type {dp_dity = dp_dity; dp_loc = loc} dity =
  try dity_unify dp_dity dity with Exit -> Loc.errorm ?loc
    "This pattern has type %a,@ but is expected to have type %a"
    print_dity dp_dity print_dity dity

Andrei Paskevich's avatar
Andrei Paskevich committed
591 592
let dexpr_expected_type {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
593 594 595 596
  try dity_unify res dity with Exit -> Loc.errorm ?loc
    "This expression has type %a,@ but is expected to have type %a"
    print_dity res print_dity dity

Andrei Paskevich's avatar
Andrei Paskevich committed
597 598
let dexpr_expected_type_weak {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
599 600 601 602 603 604
  try dity_unify_weak res dity with Exit -> Loc.errorm ?loc
    "This expression has type %a,@ but is expected to have type %a"
    print_dity res print_dity dity

(** Generation of letrec blocks *)

605
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
606
  dity * mask * (denv -> dspec later * variant list later * dexpr)
607 608 609 610

exception DupId of preid

let drec_defn denv0 prel =
Andrei Paskevich's avatar
Andrei Paskevich committed
611
  if prel = [] then invalid_arg "Dexpr.drec_defn: empty function list";
612
  let add s (id,_,_,_,_,_,_) = Sstr.add_new (DupId id) id.pre_name s in
613 614
  let _ = try List.fold_left add Sstr.empty prel with DupId id ->
    Loc.errorm ?loc:id.pre_loc "duplicate function name %s" id.pre_name in
615
  let add denv (id,_,_,bl,res,_,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
616 617
    if bl = [] then invalid_arg "Dexpr.drec_defn: empty argument list";
    let argl = List.map (fun (_,_,t) -> t) bl in
618 619
    denv_add_rec denv denv0.frozen id (argl,res) in
  let denv1 = List.fold_left add denv0 prel in
620
  let parse (id,gh,pk,bl,res,msk,pre) =
621
    let dsp, dvl, de = pre (denv_add_args denv1 bl) in
622
    dexpr_expected_type de res;
623
    (id,gh,pk,bl,res,msk,dsp,dvl,de) in
624
  let fdl = List.map parse prel in
625
  let add denv (id,_,_,bl,res,_,_,_,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
626
    (* just in case we linked some polymorphic type var to the outer context *)
627 628 629 630 631 632 633
    let check tv = if is_frozen denv0.frozen tv then Loc.errorm ?loc:id.pre_loc
      "This function is expected to be polymorphic in type variable %a"
      Pretty.print_tv tv in
    begin match Mstr.find_opt id.pre_name denv1.locals with
    | Some (Some tvs, _) -> Stv.iter check tvs
    | Some (None, _) | None -> assert false
    end;
Andrei Paskevich's avatar
Andrei Paskevich committed
634
    let argl = List.map (fun (_,_,t) -> t) bl in
635
    denv_add_poly denv id (argl, res) in
636 637 638 639 640 641 642 643 644 645
  List.fold_left add denv0 fdl, { fds = fdl }

(** Constructors *)

let dpattern ?loc node =
  let mk_dpat pre dity vars =
    { dp_pat = pre; dp_dity = dity; dp_vars = vars; dp_loc = loc } in
  let dpat = function
    | DPwild ->
        mk_dpat PPwild (dity_fresh ()) Mstr.empty
646
    | DPvar (id,gh) ->
647
        let dity = dity_fresh () in
648
        mk_dpat (PPvar (id,gh)) dity (Mstr.singleton id.pre_name dity)
649 650
    | DPapp ({rs_logic = RLls ls} as rs, dpl) when ls.ls_constr > 0 ->
        let argl, res = specialize_rs rs in
651 652 653 654 655
        dity_unify_app ls dpat_expected_type dpl argl;
        let join n _ _ = raise (Dterm.DuplicateVar n) in
        let add acc dp = Mstr.union join acc dp.dp_vars in
        let vars = List.fold_left add Mstr.empty dpl in
        let ppl = List.map (fun dp -> dp.dp_pat) dpl in
656 657 658
        mk_dpat (PPapp (rs, ppl)) res vars
    | DPapp (rs,_) ->
        raise (ConstructorExpected rs);
659 660 661 662 663 664 665 666
    | DPor (dp1,dp2) ->
        dpat_expected_type dp2 dp1.dp_dity;
        let join n dity1 dity2 = try dity_unify dity1 dity2; Some dity1
          with Exit -> Loc.errorm ?loc
            "Variable %s has type %a,@ but is expected to have type %a"
            n print_dity dity1 print_dity dity2 in
        let vars = Mstr.union join dp1.dp_vars dp2.dp_vars in
        mk_dpat (PPor (dp1.dp_pat, dp2.dp_pat)) dp1.dp_dity vars
667
    | DPas (dp, ({pre_name = n} as id), gh) ->
668 669
        let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in
        let vars = Mstr.add_new (Dterm.DuplicateVar n) n dity vars in
670
        mk_dpat (PPas (pat, id, gh)) dity vars
671
    | DPcast (dp, ity) ->
672
        dpat_expected_type dp (dity_of_ity ity);
673 674 675 676
        dp
  in
  Loc.try1 ?loc dpat node

677 678 679 680
let specialize_dxs = function
  | DEgexn xs -> specialize_xs xs
  | DElexn (_,dity) -> dity

681 682 683
let dexpr ?loc node =
  let get_dvty = function
    | DEvar (_,dvty) ->
684
        dvty
685
    | DEsym (PV pv) ->
686
        [], specialize_pv pv
687
    | DEsym (RS rs) ->
688
        specialize_rs rs
689 690 691 692 693 694 695 696
    | DEsym (OO ss) ->
        let dt = dity_fresh () in
        let ot = overload_of_rs (Srs.choose ss) in
        begin match ot with
        | UnOp   -> [dt], dt
        | BinOp  -> [dt;dt], dt
        | BinRel -> [dt;dt], dity_bool
        | NoOver -> assert false end
697 698
    | DEls ls ->
        specialize_ls ls
699
    | DEconst (_, ity) -> [],ity
700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718
    | DEapp ({de_dvty = (arg::argl, res)}, de2) ->
        dexpr_expected_type de2 arg;
        argl, res
    | DEapp ({de_dvty = ([],res)} as de1, de2) ->
        let f,a,r = match specialize_rs rs_func_app with
          | [f;a],r -> f,a,r | _ -> assert false in
        begin try dity_unify res f with Exit ->
          let rec down n de = match de.de_node with
            | DEapp (de,_) -> down (succ n) de
            | _ when n = 0 -> Loc.errorm ?loc:de.de_loc
                "This expression has type %a,@ it cannot be applied"
                print_dity (dity_of_dvty de.de_dvty)
            | _ -> Loc.errorm ?loc:de.de_loc
                "This expression has type %a,@ but is applied to %d arguments"
                print_dity (dity_of_dvty de.de_dvty) (succ n) in
          down 0 de1
        end;
        dexpr_expected_type de2 a;
        [], r
719 720 721 722
    | DEfun (bl,res,_,_,de) ->
        dexpr_expected_type de res;
        List.map (fun (_,_,t) -> t) bl, res
    | DEany (bl,res,_,_) ->
723
        List.map (fun (_,_,t) -> t) bl, res
724 725
    | DElet (_,de)
    | DErec (_,de) ->
726
        de.de_dvty
727 728
    | DEnot de ->
        dexpr_expected_type de dity_bool;
729 730 731
        dvty_bool
    | DEand (de1,de2)
    | DEor (de1,de2) ->
732 733
        dexpr_expected_type de1 dity_bool;
        dexpr_expected_type de2 dity_bool;
734
        dvty_bool
735 736 737 738 739
    | DEif (de1,de2,de3) ->
        let res = dity_fresh () in
        dexpr_expected_type de1 dity_bool;
        dexpr_expected_type de2 res;
        dexpr_expected_type de3 res;
740
        [], res
741
    | DEcase (_,[]) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
742
        invalid_arg "Dexpr.dexpr: empty branch list in DEcase"
743 744 745 746
    | DEcase (de,bl) ->
        let ety = dity_fresh () in
        let res = dity_fresh () in
        dexpr_expected_type de ety;
747
        List.iter (fun (dp,de) ->
748
          dpat_expected_type dp ety;
749
          dexpr_expected_type de res) bl;
750
        [], res
751
    | DEassign al ->
752 753 754
        List.iter (fun (de1,rs,de2) ->
          let argl, res = specialize_rs rs in
          let ls = match rs.rs_logic with RLls ls -> ls
755 756 757
            | _ -> invalid_arg "Dexpr.dexpr: not a field" in
          dity_unify_app ls dexpr_expected_type [de1] argl;
          dexpr_expected_type_weak de2 res) al;
758 759
        dvty_unit
    | DEwhile (de1,_,_,de2) ->
760
        dexpr_expected_type de1 dity_bool;
761
        dexpr_expected_type de2 dity_unit;
762
        dvty_unit
763 764 765 766
    | DEfor (_,de_from,_,de_to,_,de) ->
        dexpr_expected_type de_from dity_int;
        dexpr_expected_type de_to dity_int;
        dexpr_expected_type de dity_unit;
767
        dvty_unit
768
    | DEtry (_,[]) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
769
        invalid_arg "Dexpr.dexpr: empty branch list in DEtry"
770 771 772
    | DEtry (de,bl) ->
        let res = dity_fresh () in
        dexpr_expected_type de res;
773
        List.iter (fun (xs,dp,de) ->
774
          dpat_expected_type dp (specialize_dxs xs);
775
          dexpr_expected_type de res) bl;
776
        [], res
777
    | DEraise (xs,de) ->
778
        dexpr_expected_type de (specialize_dxs xs);
779
        [], dity_fresh ()
780
    | DEexn (_,_,_,de)
781
    | DEghost de ->
782
        de.de_dvty
783
    | DEassert _ ->
784
        dvty_unit
785 786
    | DEpure (_, dity) ->
        [], dity
787
    | DEabsurd ->
788
        [], dity_fresh ()
789 790
    | DEtrue
    | DEfalse ->
791
        dvty_bool
792 793 794
    | DEcast (de,dity)
    | DEmark (_,dity,de) ->
        dexpr_expected_type de dity;
795
        de.de_dvty
796 797
    | DEuloc (de,_)
    | DElabel (de,_) ->
798 799 800
        de.de_dvty in
  let dvty = Loc.try1 ?loc get_dvty node in
  { de_node = node; de_dvty = dvty; de_loc = loc }
801 802 803 804 805

(** Final stage *)

(** Binders *)

806
let binders ghost bl =
807
  let sn = ref Sstr.empty in
808
  let binder (id, gh, dity) =
809 810 811 812 813 814 815
    let id = match id with
      | Some ({pre_name = n} as id) ->
          let exn = match id.pre_loc with
            | Some loc -> Loc.Located (loc, Dterm.DuplicateVar n)
            | None -> Dterm.DuplicateVar n in
          sn := Sstr.add_new exn n !sn; id
      | None -> id_fresh "_" in
816
    create_pvsymbol id ~ghost:(ghost || gh) (ity_of_dity dity) in
817 818 819 820 821 822 823 824 825
  List.map binder bl

(** Specifications *)

let to_fmla f = match f.t_ty with
  | None -> f
  | Some ty when ty_equal ty ty_bool -> t_equ f t_bool_true
  | _ -> Loc.error ?loc:f.t_loc Dterm.FmlaExpected

826 827 828 829
let create_assert = to_fmla

let create_invariant pl = List.map to_fmla pl

830 831
let create_post ity ql = List.map (fun (v,f) ->
  ity_equal_check ity v.pv_ity; Ity.create_post v.pv_vs (to_fmla f)) ql
832

833
let create_xpost xql = Mxs.mapi (fun xs ql -> create_post xs.xs_ity ql) xql
834 835 836

(** User effects *)

837 838 839 840 841 842
let rec effect_of_term t =
  let quit () = Loc.errorm ?loc:t.t_loc "unsupported effect expression" in
  match t.t_node with
  | Tapp (fs, [ta]) ->
      let v, ity, fa = effect_of_term ta in
      let ity = match fa with
843
        | Some {rs_cty = {cty_args = [arg]; cty_result = res}} ->
844 845 846
            ity_full_inst (ity_match isb_empty arg.pv_ity ity) res
        | Some _ -> assert false
        | None -> ity in
847
      begin try match ity.ity_node, restore_rs fs with
Andrei Paskevich's avatar
Andrei Paskevich committed
848 849
        | Ityreg {reg_its = ts}, ({rs_field = Some f} as rs)
          when List.exists (pv_equal f) ts.its_mfields -> v, ity, Some rs
850
        | _, {rs_cty={cty_args=[arg]; cty_result=res; cty_freeze=frz}} ->
851 852 853 854 855 856
            v, ity_full_inst (ity_match frz arg.pv_ity ity) res, None
        | _ -> quit () with Not_found -> quit () end
  | Tvar v ->
      let v = try restore_pv v with Not_found -> quit () in
      v, v.pv_ity, None
  | _ -> quit ()
857 858

let effect_of_dspec dsp =
859
  let pvs = Spv.of_list dsp.ds_reads in
860
  let add_write (l,eff) t = match effect_of_term t with
861 862
    | v, {ity_node = Ityreg reg}, fd ->
        let fs = match fd with
863
          | Some fd -> Spv.singleton (Opt.get fd.rs_field)
864
          | None -> Spv.of_list reg.reg_its.its_mfields in
865 866
        if not reg.reg_its.its_private && Spv.is_empty fs then
          Loc.errorm ?loc:t.t_loc "mutable expression expected";
867 868 869
        let rd = Spv.singleton v and wr = Mreg.singleton reg fs in
        let e = Loc.try2 ?loc:t.t_loc eff_write rd wr in
        (e,t)::l, eff_union_par eff e
870
    | _ ->
871
        Loc.errorm ?loc:t.t_loc "mutable expression expected" in
872
  let wl, eff = List.fold_left add_write ([], eff_read pvs) dsp.ds_writes in
873
  let eff = Mxs.fold (fun xs _ eff -> eff_raise eff xs) dsp.ds_xpost eff in
874 875
  let eff = if dsp.ds_diverge then eff_diverge eff else eff in
  wl, eff
876

877 878
(* TODO: add warnings for empty postconditions (anywhere)
    and empty exceptional postconditions (toplevel). *)
879
let check_spec inr dsp ecty ({e_loc = loc} as e) =
Andrei Paskevich's avatar
Andrei Paskevich committed
880
  let bad_read  reff eff = not (Spv.subset reff.eff_reads  eff.eff_reads) in
881
  let bad_write weff eff = not (Mreg.submap (fun _ s1 s2 -> Spv.subset s1 s2)
882 883
                                           weff.eff_writes eff.eff_writes) in
  let bad_raise xeff eff = not (Sxs.subset xeff.eff_raises eff.eff_raises) in
884
  (* computed effect vs user effect *)
885
  let uwrl, ue = effect_of_dspec dsp in
886 887
  let ucty = create_cty ecty.cty_args ecty.cty_pre ecty.cty_post
    ecty.cty_xpost ecty.cty_oldies ue ecty.cty_result in
888
  let ueff = ucty.cty_effect and eeff = ecty.cty_effect in
889 890 891 892 893 894 895 896 897
  let check_ue = not inr and check_rw = dsp.ds_checkrw in
  (* check that every user effect actually happens. We omit this
     for local functions inside recursive functions because if
     they call the parent function, they may have more effects
     than we know at this point: those will only be known after
     we finish constructing the parent function. TODO: make an
     effort to only disable the check for local functions that
     actually call their parent. *)
  if check_ue && bad_read ueff eeff then Loc.errorm ?loc
898
    "variable@ %a@ does@ not@ occur@ in@ this@ expression"
899 900
    Pretty.print_vs (Spv.choose (Spv.diff ueff.eff_reads eeff.eff_reads)).pv_vs;
  if check_ue && bad_write ueff eeff then List.iter (fun (weff,t) ->
901 902
    if bad_write weff eeff then Loc.errorm ?loc:t.t_loc
      "this@ write@ effect@ does@ not@ happen@ in@ the@ expression") uwrl;
903
  if check_ue && bad_raise ueff eeff then Loc.errorm ?loc
904
    "this@ expression@ does@ not@ raise@ exception@ %a"
905
    print_xs (Sxs.choose (Sxs.diff ueff.eff_raises eeff.eff_raises));
906 907
  if check_ue && ueff.eff_oneway && not eeff.eff_oneway then Loc.errorm ?loc
      "this@ expression@ does@ not@ diverge";
908
  (* check that every computed effect is listed *)
909 910 911 912
  if check_rw && bad_read eeff ueff then Loc.er