dexpr.ml 42.9 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   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 18 19 20 21
(********************************************************************)

open Stdlib
open Ident
open Ty
open Term
open Ity
open Expr

(** Program types *)

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

and dvar =
Andrei Paskevich's avatar
Andrei Paskevich committed
30 31 32 33 34 35 36
  | Dtvs of tvsymbol          (* unassigned fresh type variable *)
  | Dval of dity              (* destructive binding *)

(* In Dapp, the second dity list only contains Dreg's and Durg's.
   In Dreg and Durg, the dity field is a Dapp of the region's type.
   In Dreg, the dvar field leads to another Dreg or Durg.
   In Durg, the ity field is an Ityreg. *)
37 38 39

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

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

43 44
let dvar_fresh n = ref (Dtvs (create_tvsymbol (id_fresh n)))

Andrei Paskevich's avatar
Andrei Paskevich committed
45
let dreg_fresh dity = Dreg (dvar_fresh "rho", dity)
46 47 48 49 50 51 52 53 54 55 56 57

let dity_of_ity ity =
  let hr = Hreg.create 3 in
  let rec dity ity = match ity.ity_node with
    | Ityapp (s,tl,rl) -> Dapp (s, List.map dity tl, List.map dreg rl)
    | Itypur (s,tl)    -> Dpur (s, List.map dity tl)
    | Ityvar v -> Dutv v
    | Ityreg r -> dreg r
  and dreg reg =
    try Hreg.find hr reg with Not_found ->
    let {reg_its = s; reg_args = tl; reg_regs = rl} = reg in
    let d = Dapp (s, List.map dity tl, List.map dreg rl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
58
    let r = dreg_fresh d in Hreg.add hr reg r; r in
59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
  dity ity

let reg_of_ity = function
  | {ity_node = Ityreg reg} -> reg
  | _ -> assert false

let rec ity_of_dity = function
  | Dvar ({contents = Dval d})
  | Dreg ({contents = Dval d}, _) ->
      ity_of_dity d
  | Dvar r ->
      let v = create_tvsymbol (id_fresh "xi") in
      r := Dval (Dutv v); ity_var v
  | Dreg (r, d) ->
      let ity = ity_of_dity d in
      r := Dval (Durg (ity, d)); ity
  | Dutv v -> ity_var v
  | Durg (ity,_) -> ity
  | Dapp (s,tl,rl) ->
      let reg_of_dity r = reg_of_ity (ity_of_dity r) in
      ity_app s (List.map ity_of_dity tl) (List.map reg_of_dity rl)
  | Dpur (s,tl) ->
      ity_pur s (List.map ity_of_dity tl)

(** Destructive type unification *)

let rec occur_check v = function
  | Dvar {contents = Dval d} | Dreg (_,d) | Durg (_,d) -> occur_check v d
  | Dvar {contents = Dtvs u} | Dutv u -> if tv_equal u v then raise Exit
  | Dapp (_,dl,_) | Dpur (_,dl) -> List.iter (occur_check v) dl

let rec dity_unify d1 d2 = match d1,d2 with
  | Dvar {contents = Dval d1}, d2
  | d1, Dvar {contents = Dval d2}
  | Durg (_,d1), Durg (_,d2) | Durg (_,d1), Dreg (_,d2)
  | Dreg (_,d1), Durg (_,d2) | Dreg (_,d1), Dreg (_,d2) ->
      dity_unify d1 d2
  | 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 ->
      ()
  |(Dapp (s1,dl1,_), Dapp (s2,dl2,_)
Andrei Paskevich's avatar
Andrei Paskevich committed
106
  | Dpur (s1,dl1),   Dpur (s2,dl2)) when its_equal s1 s2 ->
107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
      List.iter2 dity_unify dl1 dl2
  | _ -> raise Exit

(** Reunify regions *)

let dtvs_queue : dvar ref Queue.t = Queue.create ()

let unify_queue : (dity * dity) Queue.t = Queue.create ()

let dity_fresh () =
  let r = dvar_fresh "mu" in
  Queue.add r dtvs_queue;
  Dvar r

let rec dity_refresh ht = function
  | Dreg ({contents = Dtvs v},d) ->
      begin try Htv.find ht v with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
124
      let r = dreg_fresh (dity_refresh ht d) in
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 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 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255
      Htv.add ht v r; r end
  | Dreg _ -> assert false
  | Dpur (s,dl) ->    Dpur (s, List.map (dity_refresh ht) dl)
  | Dapp (s,dl,rl) -> Dapp (s, List.map (dity_refresh ht) dl,
                               List.map (dity_refresh ht) rl)
  | Dvar {contents = Dval d} -> dity_refresh (Htv.create 3) d
  |(Dvar {contents = Dtvs _} | Dutv _ | Durg _) as d -> d

let dity_refresh d = dity_refresh (Htv.create 3) d

let dity_unify_weak = dity_unify

let dity_unify d1 d2 = dity_unify d1 d2; Queue.add (d1,d2) unify_queue

let rec reunify d1 d2 = match d1,d2 with
  | Dvar {contents = Dval d1}, d2
  | d1, Dvar {contents = Dval d2}
  | Dreg ({contents = Dval d1},_), d2
  | d1, Dreg ({contents = Dval d2},_) ->
      reunify d1 d2
  | Dvar _, Dvar _ | Dutv _, Dutv _ | Durg _, Durg _ ->
      ()
  | Dreg ({contents = Dtvs u},_),
    Dreg ({contents = Dtvs v},_) when tv_equal u v ->
      ()
  | Dreg (r, d1), (Dreg (_, d2) as d)
  | Dreg (r, d1), (Durg (_, d2) as d)
  | (Durg (_, d1) as d), Dreg (r, d2) ->
      reunify d1 d2;
      r := Dval d
  | Dapp (_,dl1,rl1), Dapp (_,dl2,rl2) ->
      List.iter2 reunify dl1 dl2;
      List.iter2 reunify rl1 rl2
  | Dpur (_,dl1), Dpur (_,dl2) ->
      List.iter2 reunify dl1 dl2
  | _ -> assert false

let reunify_regions () =
  Queue.iter (fun r -> match !r with
    | Dval d -> r := Dval (dity_refresh d)
    | Dtvs _ -> ()) dtvs_queue;
  Queue.clear dtvs_queue;
  Queue.iter (fun (d1,d2) -> reunify d1 d2) unify_queue;
  Queue.clear unify_queue

(** Chainable relations *)

let rec dity_is_bool = function
  | Dvar { contents = Dval dty } -> dity_is_bool dty
  | Dpur (s,_) -> its_equal s its_bool
  | _ -> false

let dvty_is_chainable = function
  | [t1;t2],t ->
      dity_is_bool t && not (dity_is_bool t1) && not (dity_is_bool t2)
  | _ -> false

(** Built-in types *)

let dity_int  = Dpur (its_int,  [])
let dity_real = Dpur (its_real, [])
let dity_bool = Dpur (its_bool, [])
let dity_unit = Dpur (its_unit, [])

let dvty_int  = [], dity_int
let dvty_real = [], dity_real
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

let rec print_dity pri fmt = function
  | Dvar {contents = Dval d}
  | Dreg ({contents = Dval d},_) ->
      print_dity pri fmt d
  | Dvar {contents = Dtvs v}
  | Dutv v ->
      Pretty.print_tv fmt v
  | Dreg ({contents = Dtvs v},d) ->
      Format.fprintf fmt (protect_on (pri > 1) "%a@ @@%s")
        (print_dity 0) d (Ident.id_unique rprinter v.tv_name)
  | Durg (ity,d) ->
      Format.fprintf fmt (protect_on (pri > 1) "%a@ @@%s")
        (print_dity 0) d (Ident.id_unique rprinter (reg_of_ity ity).reg_name)
  | Dpur (s,[t1;t2]) when its_equal s its_func ->
      Format.fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
        (print_dity 1) t1 (print_dity 0) t2
  | Dpur (s,tl) when is_ts_tuple s.its_ts ->
      Format.fprintf fmt "(%a)" (Pp.print_list Pp.comma (print_dity 0)) tl
  | Dpur (s,tl) when s.its_mutable || s.its_regions <> [] ->
      Format.fprintf fmt (protect_on (pri > 1 && tl <> []) "{%a}%a")
        Pretty.print_ts s.its_ts (print_args (print_dity 2)) tl
  | Dpur (s,tl) ->
      Format.fprintf fmt (protect_on (pri > 1 && tl <> []) "%a%a")
        Pretty.print_ts s.its_ts (print_args (print_dity 2)) tl
  | Dapp (s,tl,rl) ->
      Format.fprintf fmt (protect_on (pri > 1) "%a%a%a")
        Pretty.print_ts s.its_ts (print_args (print_dity 2)) tl
          (print_regs (print_dity 0)) rl

let print_dity fmt d = print_dity 0 fmt d

(* Specialization of symbols *)

let specialize_scheme tvs (argl,res) =
  let hv = Htv.create 3 and hr = Htv.create 3 in
  let rec spec_dity = function
    | Durg _ as d -> d
    | Dvar {contents = Dval d} | Dreg ({contents = Dval d},_) -> spec_dity d
    | Dvar {contents = Dtvs v} | Dutv v as d -> get_tv v d
    | Dreg ({contents = Dtvs v},d) -> get_reg v d
    | Dapp (s,dl,rl) -> Dapp (s, List.map spec_dity dl, List.map spec_dity rl)
    | Dpur (s,dl)    -> Dpur (s, List.map spec_dity dl)
  and get_tv v d = try Htv.find hv v with Not_found ->
    let nd = dity_fresh () in
    (* can't return d, might differ in regions *)
    if not (Stv.mem v tvs) then dity_unify_weak nd d;
    Htv.add hv v nd; nd
  and get_reg v d = try Htv.find hr v with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
256
    let r = dreg_fresh (spec_dity d) in
257 258 259 260 261 262 263 264 265 266 267 268 269 270 271
    Htv.add hr v r; r in
  List.map spec_dity argl, spec_dity res

let spec_ity hv hr frz ity =
  let rec dity ity = match ity.ity_node with
    | Ityreg r -> dreg r
    | Ityvar v -> if Mtv.mem v frz.isb_tv then Dutv v else get_tv v
    | Ityapp (s,tl,rl) -> Dapp (s, List.map dity tl, List.map dreg rl)
    | Itypur (s,tl)    -> Dpur (s, List.map dity tl)
  and get_tv v = try Htv.find hv v with Not_found ->
    let nd = dity_fresh () in Htv.add hv v nd; nd
  and dreg reg = try Hreg.find hr reg with Not_found ->
    let {reg_its = s; reg_args = tl; reg_regs = rl} = reg in
    let d = Dapp (s, List.map dity tl, List.map dreg rl) in
    let r = if Mreg.mem reg frz.isb_reg then
Andrei Paskevich's avatar
Andrei Paskevich committed
272
      Durg (ity_reg reg, d) else dreg_fresh d in
273 274 275
    Hreg.add hr reg r; r in
  dity ity

Andrei Paskevich's avatar
Andrei Paskevich committed
276
let specialize_pv {pv_ity = ity} =
277 278
  spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity

Andrei Paskevich's avatar
Andrei Paskevich committed
279
let specialize_xs {xs_ity = ity} =
280 281
  spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity

282
let specialize_rs {rs_cty = cty} =
283 284 285 286 287 288 289
  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

(** Patterns *)

type dpattern = {
Andrei Paskevich's avatar
Andrei Paskevich committed
290
  dp_pat  : pre_pattern;
291 292 293 294 295 296 297 298
  dp_dity : dity;
  dp_vars : dity Mstr.t;
  dp_loc  : Loc.position option;
}

type dpattern_node =
  | DPwild
  | DPvar  of preid
299
  | DPapp  of rsymbol * dpattern list
300 301 302 303 304 305 306 307
  | DPor   of dpattern * dpattern
  | DPas   of dpattern * preid
  | DPcast of dpattern * ity

(** Specifications *)

type ghost = bool

Andrei Paskevich's avatar
Andrei Paskevich committed
308
type dbinder = preid option * ghost * dity
309 310 311 312 313 314 315 316 317 318 319 320 321

type 'a later = vsymbol Mstr.t -> 'a
  (* 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;
  ds_post    : (vsymbol option * term) list;
  ds_xpost   : (vsymbol option * term) list Mexn.t;
  ds_reads   : vsymbol list;
  ds_writes  : term list;
  ds_diverge : bool;
322
  ds_checkrw : bool;
323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
}

type dspec = ty -> dspec_final
  (* 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. *)

(** Expressions *)

type dinvariant = term list

type dexpr = {
  de_node : dexpr_node;
  de_dvty : dvty;
  de_loc  : Loc.position option;
}

and dexpr_node =
  | DEvar of string * dvty
343 344
  | DEpv of pvsymbol
  | DErs of rsymbol
345
  | DEconst of Number.constant
346
  | DEapp of dexpr * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
347
  | DEfun of dbinder list * dspec later * dexpr
348
  | DEany of dbinder list * dspec later * dity
349 350
  | DElet of dlet_defn * dexpr
  | DErec of drec_defn * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
351 352
  | DEnot of dexpr
  | DElazy of lazy_op * dexpr * dexpr
353 354
  | DEif of dexpr * dexpr * dexpr
  | DEcase of dexpr * (dpattern * dexpr) list
355
  | DEassign of (dexpr * rsymbol * dexpr) list
356
  | DEwhile of dexpr * dinvariant later * variant list later * dexpr
357
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
358 359 360
  | DEtry of dexpr * (xsymbol * dpattern * dexpr) list
  | DEraise of xsymbol * dexpr
  | DEghost of dexpr
361
  | DEassert of assertion_kind * term later
Andrei Paskevich's avatar
Andrei Paskevich committed
362 363 364 365
  | DEpure of term later
  | DEabsurd
  | DEtrue
  | DEfalse
366 367 368 369 370
  | DEmark of preid * dexpr
  | DEcast of dexpr * ity
  | DEuloc of dexpr * Loc.position
  | DElabel of dexpr * Slab.t

371
and dlet_defn = preid * ghost * rs_kind * dexpr
372 373 374

and drec_defn = { fds : dfun_defn list }

375
and dfun_defn = preid * ghost * rs_kind *
376
  dbinder list * dspec later * variant list later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
377

378 379 380 381 382 383 384 385 386
(** Environment *)

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
387 388
let is_frozen frozen v =
  try List.iter (occur_check v) frozen; false with Exit -> true
389 390 391

let freeze_dvty frozen (argl,res) =
  let rec add l = function
Andrei Paskevich's avatar
Andrei Paskevich committed
392
    | Dreg (_,d) | Durg (_,d)
393 394 395 396 397 398 399 400
    | Dvar { contents = Dval d } -> add l d
    | Dvar { contents = Dtvs _ } as d -> d :: l
    | Dutv _ as d -> d :: l
    | Dapp (_,tl,_) | Dpur (_,tl) -> List.fold_left add l tl in
  List.fold_left add (add frozen res) argl

let free_vars frozen (argl,res) =
  let rec add s = function
Andrei Paskevich's avatar
Andrei Paskevich committed
401
    | Dreg (_,d) | Durg (_,d)
402
    | Dvar { contents = Dval d } -> add s d
Andrei Paskevich's avatar
Andrei Paskevich committed
403 404
    | Dvar { contents = Dtvs v }
    | Dutv v -> if is_frozen frozen v then s else Stv.add v s
405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427
    | Dapp (_,tl,_) | Dpur (_,tl) -> List.fold_left add s tl in
  List.fold_left add (add Stv.empty res) argl

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

let denv_add_poly { frozen = frozen; locals = locals } id dvty =
  let ftvs = free_vars frozen dvty in
  let locals = Mstr.add id.pre_name (Some ftvs, dvty) locals in
  { frozen = frozen; locals = locals }

let denv_add_rec_mono { frozen = frozen; locals = locals } id dvty =
  let locals = Mstr.add id.pre_name (Some Stv.empty, dvty) locals in
  { frozen = freeze_dvty frozen dvty; locals = locals }

let denv_add_rec_poly { frozen = frozen; locals = locals } frozen0 id dvty =
  let ftvs = free_vars frozen0 dvty in
  let locals = Mstr.add id.pre_name (Some ftvs, dvty) locals in
  { frozen = frozen; locals = locals }

let denv_add_rec denv frozen0 id ((argl,res) as dvty) =
  let rec is_explicit = function
Andrei Paskevich's avatar
Andrei Paskevich committed
428
    | Dreg (_,d) | Durg (_,d)
429 430
    | Dvar { contents = Dval d } -> is_explicit d
    | Dvar { contents = Dtvs _ } -> false
Andrei Paskevich's avatar
Andrei Paskevich committed
431 432
    | Dutv _ -> true
    | Dapp (_,tl,_) | Dpur (_,tl) -> List.for_all is_explicit tl in
433 434 435 436 437 438
  if List.for_all is_explicit argl && is_explicit res
  then denv_add_rec_poly denv frozen0 id dvty
  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
439
let denv_add_let denv (id,_,_,({de_dvty = dvty} as de)) =
440 441 442
  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
443
    | DEvar _ | DErs _ | DEfun _ | DEany _ -> true
444 445 446 447 448 449
    | _ -> false in
  if is_value de
  then denv_add_poly denv id dvty
  else denv_add_mono denv id dvty

let denv_add_args { frozen = frozen; locals = locals } bl =
Andrei Paskevich's avatar
Andrei Paskevich committed
450 451
  let l = List.fold_left (fun l (_,_,t) -> t::l) frozen bl in
  let add s (id,_,t) = match id with
452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488
    | 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
  { frozen = l; locals = Mstr.set_union s locals }

let denv_add_pat { frozen = frozen; locals = locals } dp =
  let l = Mstr.fold (fun _ t l -> t::l) dp.dp_vars frozen in
  let s = Mstr.map (fun t -> None, ([], t)) dp.dp_vars in
  { frozen = l; locals = Mstr.set_union s locals }

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)

(** 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

let dpat_expected_type_weak {dp_dity = dp_dity; dp_loc = loc} dity =
  try dity_unify_weak 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
489 490
let dexpr_expected_type {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
491 492 493 494
  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
495 496
let dexpr_expected_type_weak {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
497 498 499 500 501 502
  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 *)

503 504
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
  dity * (denv -> dspec later * variant list later * dexpr)
505 506 507 508

exception DupId of preid

let drec_defn denv0 prel =
Andrei Paskevich's avatar
Andrei Paskevich committed
509 510
  if prel = [] then invalid_arg "Dexpr.drec_defn: empty function list";
  let add s (id,_,_,_,_,_) = Sstr.add_new (DupId id) id.pre_name s in
511 512
  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
Andrei Paskevich's avatar
Andrei Paskevich committed
513 514 515
  let add denv (id,_,_,bl,res,_) =
    if bl = [] then invalid_arg "Dexpr.drec_defn: empty argument list";
    let argl = List.map (fun (_,_,t) -> t) bl in
516 517
    denv_add_rec denv denv0.frozen id (argl,res) in
  let denv1 = List.fold_left add denv0 prel in
Andrei Paskevich's avatar
Andrei Paskevich committed
518
  let parse (id,gh,pk,bl,res,pre) =
519
    let dsp, dvl, de = pre (denv_add_args denv1 bl) in
520
    dexpr_expected_type_weak de res;
521
    (id,gh,pk,bl,dsp,dvl,de) in
522
  let fdl = List.map parse prel in
523
  let add denv (id,_,_,bl,_,_,{de_dvty = dvty}) =
Andrei Paskevich's avatar
Andrei Paskevich committed
524
    (* just in case we linked some polymorphic type var to the outer context *)
525 526 527 528 529 530 531
    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
532 533
    let argl = List.map (fun (_,_,t) -> t) bl in
    denv_add_poly denv id (argl, dity_of_dvty dvty) in
534 535 536 537 538 539 540 541 542 543 544 545 546
  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
    | DPvar id ->
        let dity = dity_fresh () in
        mk_dpat (PPvar id) dity (Mstr.singleton id.pre_name dity)
547 548
    | DPapp ({rs_logic = RLls ls} as rs, dpl) when ls.ls_constr > 0 ->
        let argl, res = specialize_rs rs in
549 550 551 552 553
        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
554 555 556
        mk_dpat (PPapp (rs, ppl)) res vars
    | DPapp (rs,_) ->
        raise (ConstructorExpected rs);
557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577
    | 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
    | DPas (dp, ({pre_name = n} as id)) ->
        let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in
        let vars = Mstr.add_new (Dterm.DuplicateVar n) n dity vars in
        mk_dpat (PPas (pat, id)) dity vars
    | DPcast (dp, ity) ->
        dpat_expected_type_weak dp (dity_of_ity ity);
        dp
  in
  Loc.try1 ?loc dpat node

let dexpr ?loc node =
  let get_dvty = function
    | DEvar (_,dvty) ->
578
        dvty
579
    | DEpv pv ->
580
        [], specialize_pv pv
581
    | DErs rs ->
582
        specialize_rs rs
583
    | DEconst (Number.ConstInt _) ->
584
        dvty_int
585
    | DEconst (Number.ConstReal _) ->
586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605
        dvty_real
    | 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
606
    | DEfun (bl,_,de) ->
607
        List.map (fun (_,_,t) -> t) bl, dity_of_dvty de.de_dvty
608
    | DEany (bl,_,res) ->
609
        List.map (fun (_,_,t) -> t) bl, res
610 611
    | DElet (_,de)
    | DErec (_,de) ->
612
        de.de_dvty
613 614
    | DEnot de ->
        dexpr_expected_type de dity_bool;
615
        de.de_dvty
616 617 618
    | DElazy (_,de1,de2) ->
        dexpr_expected_type de1 dity_bool;
        dexpr_expected_type de2 dity_bool;
619
        de1.de_dvty
620 621 622 623 624
    | 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;
625
        [], res
626
    | DEcase (_,[]) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
627
        invalid_arg "Dexpr.dexpr: empty branch list in DEcase"
628 629 630 631
    | DEcase (de,bl) ->
        let ety = dity_fresh () in
        let res = dity_fresh () in
        dexpr_expected_type de ety;
632
        List.iter (fun (dp,de) ->
633
          dpat_expected_type dp ety;
634
          dexpr_expected_type de res) bl;
635
        [], res
636
    | DEassign al ->
637 638 639
        List.iter (fun (de1,rs,de2) ->
          let argl, res = specialize_rs rs in
          let ls = match rs.rs_logic with RLls ls -> ls
640 641 642
            | _ -> invalid_arg "Dexpr.dexpr: not a field" in
          dity_unify_app ls dexpr_expected_type [de1] argl;
          dexpr_expected_type_weak de2 res) al;
643 644
        dvty_unit
    | DEwhile (de1,_,_,de2) ->
645
        dexpr_expected_type de1 dity_bool;
646
        dexpr_expected_type de2 dity_unit;
647
        de2.de_dvty
648 649 650 651
    | 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;
652
        de.de_dvty
653
    | DEtry (_,[]) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
654
        invalid_arg "Dexpr.dexpr: empty branch list in DEtry"
655 656 657
    | DEtry (de,bl) ->
        let res = dity_fresh () in
        dexpr_expected_type de res;
658 659 660
        List.iter (fun (xs,dp,de) ->
          dpat_expected_type dp (specialize_xs xs);
          dexpr_expected_type de res) bl;
661
        [], res
662 663
    | DEraise (xs,de) ->
        dexpr_expected_type de (specialize_xs xs);
664
        [], dity_fresh ()
665
    | DEghost de ->
666
        de.de_dvty
667
    | DEassert _ ->
668
        dvty_unit
669 670
    | DEpure _
    | DEabsurd ->
671
        [], dity_fresh ()
672 673
    | DEtrue
    | DEfalse ->
674
        dvty_bool
675 676
    | DEcast (de,ity) ->
        dexpr_expected_type_weak de (dity_of_ity ity);
677
        de.de_dvty
678
    | DEmark (_,de)
679 680
    | DEuloc (de,_)
    | DElabel (de,_) ->
681 682 683
        de.de_dvty in
  let dvty = Loc.try1 ?loc get_dvty node in
  { de_node = node; de_dvty = dvty; de_loc = loc }
684 685 686 687 688 689 690

(** Final stage *)

(** Binders *)

let binders bl =
  let sn = ref Sstr.empty in
691
  let binder (id, ghost, dity) =
692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708
    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
    create_pvsymbol id ~ghost (ity_of_dity dity) in
  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

709 710 711 712 713 714 715 716 717 718
let create_assert = to_fmla

let create_invariant pl = List.map to_fmla pl

let create_pre = create_invariant

let create_post ty ql = List.map (fun (v,f) ->
  let f = (*Mlw_wp.remove_old*) (to_fmla f) in match v with
    | None -> Ity.create_post (create_vsymbol (id_fresh "result") ty) f
    | Some v -> Ty.ty_equal_check ty v.vs_ty; Ity.create_post v f) ql
719 720 721 722 723 724

let create_xpost xql =
  Mexn.mapi (fun xs ql -> create_post (ty_of_ity xs.xs_ity) ql) xql

(** User effects *)

725 726 727 728 729 730
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
731
        | Some {rs_cty = {cty_args = [arg]; cty_result = res}} ->
732 733 734
            ity_full_inst (ity_match isb_empty arg.pv_ity ity) res
        | Some _ -> assert false
        | None -> ity in
735 736 737
      begin try match ity.ity_node, restore_rs fs with
        | Ityreg _, ({rs_field = Some _} as rs) -> v, ity, Some rs
        | _, {rs_cty={cty_args=[arg]; cty_result=res; cty_freeze=frz}} ->
738 739 740 741 742 743
            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 ()
744 745 746 747 748

let effect_of_dspec dsp =
  let add_raise xs _ eff = eff_raise eff xs in
  let eff = Mexn.fold add_raise dsp.ds_xpost eff_empty in
  let eff = if dsp.ds_diverge then eff_diverge eff else eff in
749 750 751 752 753 754
  let add_read s v = Spv.add (try restore_pv v with Not_found ->
    Loc.errorm "unsupported effect expression") s in
  let pvs = List.fold_left add_read Spv.empty dsp.ds_reads in
  let add_write (s,l,e) t = match effect_of_term t with
    | v, {ity_node = Ityreg reg}, fd ->
        let fs = match fd with
755
          | Some fd -> Spv.singleton (Opt.get fd.rs_field)
756
          | None -> Spv.of_list reg.reg_its.its_mfields in
757
        let wr = Loc.try3 ?loc:t.t_loc eff_write eff_empty reg fs in
758
        Spv.add v s, (wr,t)::l, eff_union e wr
759
    | _ ->
760 761
        Loc.errorm ?loc:t.t_loc "mutable expression expected" in
  List.fold_left add_write (pvs, [], eff) dsp.ds_writes
762

763 764
let e_find_eff pr e =
  try (e_find_minimal (fun e -> e.e_loc <> None && pr e.e_effect) e).e_loc
765 766
  with Not_found -> None

Andrei Paskevich's avatar
Andrei Paskevich committed
767
let check_spec dsp ecty e =
768 769 770
  let bad_write weff eff = not (Mreg.submap (fun _ s1 s2 -> Spv.subset s1 s2)
                                            weff.eff_writes eff.eff_writes) in
  let bad_raise xeff eff = not (Sexn.subset xeff.eff_raises eff.eff_raises) in
771
  (* computed effect vs user effect *)
Andrei Paskevich's avatar
Andrei Paskevich committed
772 773 774 775
  let check_rwd = dsp.ds_checkrw in
  let ur, uwrl, ue = effect_of_dspec dsp in
  let ucty = create_cty ecty.cty_args ecty.cty_pre
    ecty.cty_post ecty.cty_xpost ur ue ecty.cty_result in
776 777
  let ueff = ucty.cty_effect and urds = ucty.cty_reads in
  let eeff = ecty.cty_effect and erds = ecty.cty_reads in
778
  (* check that every user effect actually happens *)
779 780 781 782 783 784 785 786 787 788 789
  if not (Spv.subset urds erds) then Loc.errorm ?loc:e.e_loc
    "variable@ %a@ does@ not@ occur@ in@ this@ expression"
    Pretty.print_vs (Spv.choose (Spv.diff urds erds)).pv_vs;
  if bad_write ueff eeff then List.iter (fun (weff,t) ->
    if bad_write weff eeff then Loc.errorm ?loc:t.t_loc
      "this@ write@ effect@ does@ not@ happen@ in@ the@ expression") uwrl;
  if bad_raise ueff eeff then Loc.errorm ?loc:e.e_loc
    "this@ expression@ does@ not@ raise@ exception@ %a"
    print_xs (Sexn.choose (Sexn.diff ueff.eff_raises eeff.eff_raises));
  if ueff.eff_diverg && not eeff.eff_diverg then Loc.errorm ?loc:e.e_loc
    "this@ expression@ does@ not@ diverge";
790
  (* check that every computed effect is listed *)
791 792 793 794 795 796 797 798 799
  if check_rwd && not (Spv.subset erds urds) then Spv.iter (fun v ->
    Loc.errorm ?loc:e.e_loc
      "this@ expression@ depends@ on@ variable@ %a@ left@ out@ in@ \
      the@ specification" Pretty.print_vs v.pv_vs) (Spv.diff erds urds);
  if check_rwd && bad_write eeff ueff then
    Loc.errorm ?loc:(e_find_eff (fun eff -> bad_write eff ueff) e)
      "this@ expression@ produces@ an@ unlisted@ write@ effect";
  if ecty.cty_args <> [] && bad_raise eeff ueff then Sexn.iter (fun xs ->
    Loc.errorm ?loc:(e_find_eff (fun eff -> Sexn.mem xs eff.eff_raises) e)
800
      "this@ expression@ raises@ unlisted@ exception@ %a"
801 802 803 804 805
      print_xs xs) (Sexn.diff eeff.eff_raises ueff.eff_raises);
  if check_rwd && eeff.eff_diverg && not ueff.eff_diverg then
    Loc.errorm ?loc:(e_find_eff (fun eff -> eff.eff_diverg) e)
      "this@ expression@ may@ diverge,@ but@ this@ is@ not@ \
        stated@ in@ the@ specification"
806

Andrei Paskevich's avatar
Andrei Paskevich committed
807
let check_aliases recu c =
808 809 810 811
  let rds_regs = c.cty_freeze.isb_reg in
  let report r _ _ =
    if Mreg.mem r rds_regs then let spv = Spv.filter
        (fun v -> ity_r_occurs r v.pv_ity) c.cty_reads in
812
      Loc.errorm "The type of this function contains an alias with \
813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829
        external variable %a" print_pv (Spv.choose spv)
    else Loc.errorm "The type of this function contains an alias" in
  (* we allow the value in a non-recursive function to contain
     regions coming the function's arguments, but not from the
     context. It is sometimes useful to write a function around
     a constructor or a projection. For recursive functions, we
     impose the full non-alias discipline, to ensure the safety
     of region polymorphism (see add_rec_mono). We do not track
     aliases inside the type of an argument or a result, which
     may break the type inference, but we have a safety net
     type checking in Expr. *)
  let add_ity regs ity =
    let frz = ity_freeze isb_empty ity in
    Mreg.union report regs frz.isb_reg in
  let add_arg regs v = add_ity regs v.pv_ity in
  let regs = List.fold_left add_arg rds_regs c.cty_args in
  ignore (add_ity (if recu then regs else rds_regs) c.cty_result)
830

831
let check_fun rsym dsp e =
Andrei Paskevich's avatar
Andrei Paskevich committed
832 833 834 835 836 837 838 839 840
  let c,e = match e with
    | { e_node = Efun e; e_vty = VtyC c } -> c,e
    | _ -> invalid_arg "Dexpr.check_fun" in
  let c = match rsym with
    | Some s -> s.rs_cty
    | None -> c in
  check_spec dsp c e;
  check_aliases (rsym <> None) c

841 842
(** Environment *)

Andrei Paskevich's avatar
Andrei Paskevich committed
843
type env = {
844
  rsm : rsymbol Mstr.t;
845 846 847 848
  pvm : pvsymbol Mstr.t;
  vsm : vsymbol Mstr.t;
}

849
let env_empty = {
850
  rsm = Mstr.empty;
851 852 853 854
  pvm = Mstr.empty;
  vsm = Mstr.empty;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
855
let add_rsymbol ({rsm = rsm} as env) rs =
856
  let n = rs.rs_name.id_string in
Andrei Paskevich's avatar
Andrei Paskevich committed
857
  { env with rsm = Mstr.add n rs rsm }
858

Andrei Paskevich's avatar
Andrei Paskevich committed
859
let add_pvsymbol ({pvm = pvm; vsm = vsm} as env) pv =
860
  let n = pv.pv_vs.vs_name.id_string in
Andrei Paskevich's avatar
Andrei Paskevich committed
861
  { env with pvm = Mstr.add n pv pvm; vsm = Mstr.add n pv.pv_vs vsm }
862

Andrei Paskevich's avatar
Andrei Paskevich committed
863
let add_pv_map ({pvm = pvm; vsm = vsm} as env) vm =
864
  let um = Mstr.map (fun pv -> pv.pv_vs) vm in
Andrei Paskevich's avatar
Andrei Paskevich committed
865
  { env with pvm = Mstr.set_union vm pvm; vsm = Mstr.set_union um vsm }
866 867 868 869 870

let add_binders env pvl = List.fold_left add_pvsymbol env pvl

(** Abstract values *)

Andrei Paskevich's avatar
Andrei Paskevich committed
871 872 873 874 875 876 877 878 879 880 881 882
let cty_of_spec env bl dsp dity =
  let ity = ity_of_dity dity in
  let ty = ty_of_ity ity in
  let bl = binders bl in
  let env = add_binders env bl in
  let dsp = dsp env.vsm ty in
  let rds,_,eff = effect_of_dspec dsp in
  let eff = refresh_of_effect eff in
  let p = create_pre dsp.ds_pre in
  let q = create_post ty dsp.ds_post in
  let xq = create_xpost dsp.ds_xpost in
  create_cty bl p q xq rds eff ity
883

Andrei Paskevich's avatar
Andrei Paskevich committed
884
(*
885
let val_decl env (id,ghost,kind,bl,dsp,dity) =
Andrei Paskevich's avatar
Andrei Paskevich committed
886
  let ity = ity_of_dity dity in match kind with
887
  | RKlocal -> invalid_arg "Dexpr.val_decl"
888
  | _ when bl <> [] ->
Andrei Paskevich's avatar
Andrei Paskevich committed
889
      let c = cty_of_spec env bl dsp dity in
890 891
      ValS (create_rsymbol id ~ghost ~kind c)
  | _ when ity_immutable ity ->
Andrei Paskevich's avatar
Andrei Paskevich committed
892 893
      let c = cty_of_spec env bl dsp dity in
      if c.cty_pre <> [] then Loc.errorm
894 895 896
        "Top-level constants can have no preconditions";
      if not (Spv.is_empty c.cty_reads) then Loc.errorm
        "Top-level constants can have no external dependencies";
Andrei Paskevich's avatar
Andrei Paskevich committed
897 898
      if not (eff_is_empty c.cty_effect) then Loc.errorm
        "Top-level constants can produce no effects";
899 900
      ValS (create_rsymbol id ~ghost ~kind c)
  | RKnone when ity_closed ity ->
Andrei Paskevich's avatar
Andrei Paskevich committed
901
      let dsp = dsp env.vsm (ty_of_ity ity) in
902 903 904 905 906 907 908
      if dsp.ds_pre <> [] || dsp.ds_post <> [] ||
          not (Mexn.is_empty dsp.ds_xpost) || dsp.ds_reads <> [] ||
          dsp.ds_writes <> [] || dsp.ds_diverge || dsp.ds_checkrw then
        Loc.errorm "Mutable top-level variables can have no specification";
      ValV (create_pvsymbol id ~ghost ity)
  | RKnone -> Loc.errorm
      "Mutable top-level variables must have monomorphic type"
909
  | RKfunc -> Loc.errorm
910 911 912 913 914
      "Mutable top-level variables cannot be logical functions"
  | RKpred -> Loc.errorm
      "Mutable top-level variables cannot be logical predicates"
  | RKlemma -> Loc.errorm
      "Mutable top-level variables cannot be logical lemmas"
Andrei Paskevich's avatar
Andrei Paskevich committed
915
*)
916 917 918

(** Expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
919
(*
920 921
let implicit_post = Debug.register_flag "implicit_post"
  ~desc:"Generate@ a@ postcondition@ for@ pure@ functions@ without@ one."
Andrei Paskevich's avatar
Andrei Paskevich committed
922
*)
923

Andrei Paskevich's avatar
Andrei Paskevich committed
924 925 926 927 928 929
let warn_unused s loc =
  if s = "" || s.[0] <> '_' then
  Warning.emit ?loc "unused variable %s" s

let check_used_pv e pv = if not (Spv.mem pv e.e_vars) then
  warn_unused pv.pv_vs.vs_name.id_string pv.pv_vs.vs_name.id_loc
930 931 932 933 934 935 936

let rec strip uloc labs de = match de.de_node with
  | DEcast (de,_) -> strip uloc labs de
  | DEuloc (de,loc) -> strip (Some loc) labs de
  | DElabel (de,s) -> strip uloc (Slab.union labs s) de
  | _ -> uloc, labs, de

Andrei Paskevich's avatar
Andrei Paskevich committed
937 938 939 940 941 942 943
let set_loc ?(labs=Slab.empty) keep_loc loc uloc e =
  let loc = if uloc <> None then uloc else
            if keep_loc then loc else None in
  if loc = None && Slab.is_empty labs then e
  else e_label ?loc labs e

let rec expr ~keep_loc uloc env ffo ({de_loc = loc} as de) =
944
  let uloc, labs, de = strip uloc Slab.empty de in
Andrei Paskevich's avatar
Andrei Paskevich committed
945 946 947 948 949 950 951 952 953 954 955 956
  let e = Loc.try5 ?loc try_expr keep_loc uloc env ffo de in
  let e = match e.e_vty with
    | VtyC _ when ffo ->
        let dt = dity_of_dvty de.de_dvty in
        let ty = Loc.try1 ?loc ity_of_dity dt in
        let e = set_loc keep_loc loc uloc e in
        Loc.try4 ?loc e_app e [] [] ty
    | _ -> e in
  set_loc ~labs keep_loc loc uloc e

and try_expr keep_loc uloc env ffo ({de_dvty = argl,res} as de0) =
  let get env de = expr ~keep_loc uloc env true de in
957 958
  match de0.de_node with
  | DEvar (n,_) when argl = [] ->
Andrei Paskevich's avatar
Andrei Paskevich committed
959
      e_var (Mstr.find_exn (Dterm.UnboundVar n) n env.pvm)
960
  | DEvar (n,_) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
961 962 963 964 965
      e_sym (Mstr.find_exn (Dterm.UnboundVar n) n env.rsm)
  | DEpv v ->
      e_var v
  | DErs s ->
      e_sym s
966 967
  | DEconst c ->
      e_const c
968 969 970 971 972 973
  | DEapp ({de_dvty = (_::_,_)} as de1, de2) ->
      (* it should be impossible for e1 to be a mapping *)
      let rec down de el = match de.de_node with
        | DEapp (de1, de2) -> down de1 (get env de2 :: el)
        | _ -> expr ~keep_loc uloc env false de, el in
      let e, el = down de1 [get env de2] in
Andrei Paskevich's avatar
Andrei Paskevich committed
974 975 976
      if argl = [] || not ffo
        then e_app e el (List.map ity_of_dity argl) (ity_of_dity res)
        else e_app e el [] (ity_of_dity (dity_of_dvty de0.de_dvty))
977 978 979
  | DEapp ({de_dvty = ([],_)} as de1, de2) ->
      (* it should be impossible for e1 to be a computation *)
      e_app (e_sym rs_func_app) [get env de1; get env de2] [] (ity_of_dity res)
Andrei Paskevich's avatar
Andrei Paskevich committed
980
  | DEfun (bl,dsp,de) ->
981 982
      let e, dsp, _ = expr_fun ~keep_loc uloc env (binders bl) dsp de in
      check_fun None dsp e;
Andrei Paskevich's avatar
Andrei Paskevich committed
983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000
      if bl <> [] then e else
        let e = set_loc keep_loc de0.de_loc uloc e in
        e_app e [] [] (cty_of_expr e).cty_result
  | DEany (bl,dsp,dity) ->
      let e = e_any (cty_of_spec env bl dsp dity) in
      if bl <> [] then e else
        let e = set_loc keep_loc de0.de_loc uloc e in
        e_app e [] [] (cty_of_expr e).cty_result
  | DElet ((id,ghost,kind,de1),de2) ->
      let e1 = expr ~keep_loc uloc env false de1 in
      let ld = create_let_defn id ~ghost ~kind e1 in
      let env = match ld.let_sym with
        | ValS s when s.rs_ghost && not ghost -> Loc.errorm ?loc:id.pre_loc
            "Function %s must be explicitly marked ghost" id.pre_name
        | ValS s -> add_rsymbol env s
        | ValV v -> add_pvsymbol env v in
      let e2 = expr ~keep_loc uloc env ffo de2 in
      let e2 =
1001
        let e2_unit = match e2.e_vty with
Andrei Paskevich's avatar
Andrei Paskevich committed
1002
          | VtyI i -> ity_equal i ity_unit
1003
          | _ -> false in
Andrei Paskevich's avatar
Andrei Paskevich committed
1004 1005 1006
        let id_in_e2 = match ld.let_sym with
          | ValV v -> Spv.mem v e2.e_vars
          | ValS s -> Srs.mem s e2.e_syms in
1007
        if not id_in_e2 then warn_unused id.pre_name id.pre_loc;
Andrei Paskevich's avatar
Andrei Paskevich committed
1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021
        (* if e1 is a recursive call, we may not know yet its effects,
            so we have to rely on an heuristic: if the result of e1 is
            not used in e2, then it was probably called for the effect. *)
        let e1_no_eff = eff_is_pure e1.e_effect && id_in_e2 in
        if e2_unit (* e2 is unit *)
          && e2.e_ghost (* and e2 is ghost *)
          && not e1.e_ghost (* and e1 is non-ghost *)
          && not e1_no_eff (* and e1 has observable effects *)
        then
          let ld = create_let_defn (id_fresh "_") e2 in
          e_label ?loc:e2.e_loc Slab.empty (e_let ld e_void)
        else e2
      in
      e_let ld e2
1022 1023 1024 1025 1026
  | DErec (drdf,de) ->
      let rdf = expr_rec ~keep_loc uloc env drdf in
      let add env fd = add_rsymbol env fd.fun_sym in
      let env = List.fold_left add env rdf.rec_defn in
      e_rec rdf (expr ~keep_loc uloc env ffo de)
Andrei Paskevich's avatar
Andrei Paskevich committed
1027 1028 1029 1030
  | DEnot de1 ->
      e_not (get env de1)
  | DElazy (op,de1,de2) ->
      e_lazy op (get env de1) (get env de2)
1031
  | DEif (de1,de2,de3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
1032
      e_if (get env de1) (get env de2) (get env de3)
1033 1034 1035 1036 1037
  | DEcase (de1,bl) ->
      let e1 = get env de1 in
      let ity = ity_of_expr e1 in
      let ghost = e1.e_ghost in
      let branch (dp,de) =
Andrei Paskevich's avatar
Andrei Paskevich committed
1038
        let vm, pat = create_prog_pattern dp.dp_pat ~ghost ity in
1039
        let e = get (add_pv_map env vm) de in
Andrei Paskevich's avatar
Andrei Paskevich committed
1040
        Mstr.iter (fun _ v -> check_used_pv e v) vm;
1041 1042
        pat, e in
      e_case e1 (List.map branch bl)
Andrei Paskevich's avatar
Andrei Paskevich committed
1043 1044 1045
  | DEassign al ->
      let conv (de1,f,de2) = get env de1, f, get env de2 in
      e_assign (List.map conv al)
1046
  | DEwhile (de1,dinv,dvarl,de2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
1047 1048
      let e1 = get env de1 in
      let e2 = get env de2 in
1049 1050
      let inv = dinv env.vsm in
      let varl = dvarl env.vsm in
Andrei Paskevich's avatar
Andrei Paskevich committed
1051 1052 1053 1054 1055 1056 1057 1058 1059
      e_while e1 (create_invariant inv) varl e2
  | DEfor (id,de_from,dir,de_to,dinv,de) ->
      let e_from = get env de_from in
      let e_to = get env de_to in
      let v = create_pvsymbol id ity_int in
      let env = add_pvsymbol env v in
      let e = get env de in
      let inv = dinv env.vsm in
      e_for v e_from dir e_to (create_invariant inv) e
1060 1061 1062
  | DEtry (de1,bl) ->
      let e1 = get env de1 in
      let add_branch (m,l) (xs,dp,de) =
Andrei Paskevich's avatar
Andrei Paskevich committed
1063
        let vm, pat = create_prog_pattern dp.dp_pat xs.xs_ity in
1064
        let e = get (add_pv_map env vm) de in
Andrei Paskevich's avatar
Andrei Paskevich committed
1065
        Mstr.iter (fun _ v -> check_used_pv e v) vm;
1066 1067 1068 1069
        try Mexn.add xs ((pat,e) :: Mexn.find xs m) m, l
        with Not_found -> Mexn.add xs [pat,e] m, (xs::l) in
      let xsm, xsl = List.fold_left add_branch (Mexn.empty,[]) bl in
      let mk_branch xs = match Mexn.find xs xsm with
Andrei Paskevich's avatar
Andrei Paskevich committed
1070 1071 1072
        | [{ pp_pat = { pat_node = Pvar v }}, e] ->
            xs, Ity.restore_pv v, e
        | [{ pp_pat = { pat_node = Pwild }}, e] ->
1073
            xs, create_pvsymbol (id_fresh "_") xs.xs_ity, e
Andrei Paskevich's avatar
Andrei Paskevich committed
1074 1075
        | [{ pp_pat = { pat_node = Papp (fs,[]) }}, e]
          when ls_equal fs (Term.fs_tuple 0) ->
1076 1077
            xs, create_pvsymbol (id_fresh "_") xs.xs_ity, e
        | bl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
1078 1079 1080 1081 1082 1083
            let v = create_pvsymbol (id_fresh "res") xs.xs_ity in
            let pl = List.rev_map (fun (p,_) -> [p.pp_pat]) bl in
            let bl = if Pattern.is_exhaustive [t_var v.pv_vs] pl then bl
              else let _,pp = create_prog_pattern PPwild v.pv_ity in
              (pp, e_raise xs (e_var v) (ity_of_dity res)) :: bl in
            xs, v, e_case (e_var v) (List.rev bl)
1084 1085
      in
      e_try e1 (List.rev_map mk_branch xsl)
Andrei Paskevich's avatar
Andrei Paskevich committed
1086 1087 1088 1089 1090
  | DEraise (xs,de) ->
      e_raise xs (get env de) (ity_of_dity res)
  | DEghost de ->
      (* keep user ghost annotations even if redundant *)
      e_ghost (expr ~keep_loc uloc env ffo de)
1091 1092
  | DEassert (ak,f) ->
      e_assert ak (create_assert (f env.vsm))
Andrei Paskevich's avatar
Andrei Paskevich committed
1093 1094 1095 1096 1097 1098 1099 1100 1101 1102
  | DEpure t ->
      e_pure (t env.vsm)
  | DEabsurd ->
      e_absurd (ity_of_dity res)
  | DEtrue ->
      e_true
  | DEfalse ->
      e_false
  | DEmark _ -> assert false (* TODO *)
(*
1103
  | DEmark (id,de) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
1104 1105 1106 1107
      let ld,v = create_let_defn_pv id Mlw_wp.e_now in
      let env = add_pvsymbol env v in
      e_let ld (expr ~keep_loc uloc env env ffo de)
*)
1108 1109 1110 1111
  | DEcast _ | DEuloc _ | DElabel _ ->
      assert false (* already stripped *)

and expr_rec ~keep_loc uloc env {fds = dfdl} =
1112
  let step1 env (id, gh, kind, bl, dsp, dvl, ({de_dvty = dvty} as de)) =
1113
    let pvl = binders bl in
1114 1115 1116 1117
    let ity = Loc.try1 ?loc:de.de_loc ity_of_dity (dity_of_dvty dvty) in
    let cty = create_cty pvl [] [] Mexn.empty Spv.empty eff_empty ity in
    let rs = create_rsymbol id ~ghost:gh ~kind:RKnone cty in
    add_rsymbol env rs, (rs, kind, dsp, dvl, de) in
1118
  let env, fdl = Lists.map_fold_left step1 env dfdl in
1119 1120 1121 1122 1123
  let step2 ({rs_cty = c} as rs, kind, dsp, dvl, de) (fdl, dspl) =
    let lam, dsp, env = expr_fun ~keep_loc uloc env c.cty_args dsp de in
    if lam.e_ghost && not rs.rs_ghost then Loc.errorm ?loc:rs.rs_name.id_loc
      "Function %s must be explicitly marked ghost" rs.rs_name.id_string;
    (rs, lam, dvl env.vsm, kind)::fdl, dsp::dspl in
1124
  (* check for unexpected aliases in case of trouble *)
1125 1126 1127 1128
  let fdl, dspl = try List.fold_right step2 fdl ([],[]) with
    | Loc.Located (_, Ity.TypeMismatch _) | Ity.TypeMismatch _ as exn ->
        List.iter (fun ({rs_name = {id_loc = loc}} as rs,_,_,_,_) ->
          Loc.try2 ?loc check_aliases true rs.rs_cty) fdl;
1129
        raise exn in
1130 1131 1132 1133
  let rdf = try create_rec_defn fdl with
    | Loc.Located (_, Ity.TypeMismatch _) | Ity.TypeMismatch _ as exn ->
        List.iter (fun ({rs_name = {id_loc = loc}},lam,_,_) ->
          Loc.try2 ?loc check_aliases true (cty_of_expr lam)) fdl;
1134
        raise exn in
1135 1136 1137 1138
  let check {fun_rsym = rs; fun_expr = e} dsp =
    Loc.try3 ?loc:rs.rs_name.id_loc check_fun (Some rs) dsp e in
  List.iter2 check rdf.rec_defn dspl;
  rdf
1139

Andrei Paskevich's avatar
Andrei Paskevich committed
1140
and expr_fun ~keep_loc uloc env pvl dsp de =
1141
  let env = add_binders env pvl in
Andrei Paskevich's avatar
Andrei Paskevich committed
1142 1143 1144 1145 1146 1147
  let e = expr ~keep_loc uloc env true de in
  let ty = ty_of_ity (ity_of_expr e) in
  let dsp = dsp env.vsm ty in
  let p = create_pre dsp.ds_pre in
  let q = create_post ty dsp.ds_post in
  let xq = create_xpost dsp.ds_xpost in
1148
  e_fun pvl p q xq e, dsp, env
Andrei Paskevich's avatar
Andrei Paskevich committed
1149

Andrei Paskevich's avatar
Andrei Paskevich committed
1150
(*
1151
let val_decl ?(keep_loc=true) (id,_,_,_,_,_ as vald) =
1152
  ignore keep_loc;
1153
  reunify_regions ();
Andrei Paskevich's avatar
Andrei Paskevich committed
1154
  Loc.try2 ?loc:id.pre_loc val_decl env_empty vald
Andrei Paskevich's avatar
Andrei Paskevich committed
1155
*)
1156

1157
let rec_defn ?(keep_loc=true) drdf =
1158
  reunify_regions ();
1159
  expr_rec ~keep_loc None env_empty drdf
1160

1161
let expr ?(keep_loc=true) de =
1162
  reunify_regions ();
1163 1164 1165
  let e = expr ~keep_loc None env_empty false de in
  check_expr e; e

1166
let let_defn ?(keep_loc=true) (id,ghost,kind,de) =
1167 1168 1169 1170 1171
  let e = expr ~keep_loc de in
  if e.e_ghost && not ghost then Loc.errorm ?loc:id.pre_loc
    "%s %s must be explicitly marked ghost" (match kind, e.e_vty with
      | RKnone, VtyI _ -> "Variable" | _ -> "Function") id.pre_name;
  Loc.try1 ?loc:id.pre_loc (create_let_defn id ~ghost ~kind) e