dexpr.ml 50.8 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
  | Dvar of dvar ref          (* destructible "fresh" type variable *)
23 24
  | Dutv of tvsymbol          (* undestructible "user" type variable *)
  | Durg of dity * region     (* undestructible "user" region *)
25 26 27
  | Dapp of itysymbol * dity list * dity list

and dvar =
28 29 30 31 32
  | 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
33

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

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

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

41 42 43 44 45 46 47 48 49 50
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"))))
51

52 53 54 55 56 57
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)
58 59 60 61

let dity_of_ity ity =
  let hr = Hreg.create 3 in
  let rec dity ity = match ity.ity_node with
62 63 64 65 66 67 68
    | 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
69 70 71
  dity ity

let rec ity_of_dity = function
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
  | 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
93 94 95 96
  | Dvar r ->
      let v = create_tvsymbol (id_fresh "xi") in
      r := Dval (Dutv v); ity_var v
  | Dapp (s,tl,rl) ->
97
      ity_app_pure s (List.map ity_of_dity tl) (List.map ity_of_dity rl)
98 99 100 101

(** Destructive type unification *)

let rec occur_check v = function
102 103 104 105 106 107 108 109 110 111 112 113 114 115
  | 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
116 117 118 119 120 121
  | 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;
122
      r := Dsim (d,v)
123 124
  | Dutv u, Dutv v when tv_equal u v ->
      ()
125
  | Dapp (s1,dl1,_), Dapp (s2,dl2,_) when its_equal s1 s2 ->
126
      List.iter2 dity_unify_weak dl1 dl2
127 128
  | _ -> raise Exit

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
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,_) ->
      let dl = List.map dity_refresh dl in
      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
      let d = Dapp (s, dl, List.map reg_inst s.its_regions) in
      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
179

180 181 182 183 184 185 186 187
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 ->
188
      ()
189 190 191 192 193 194 195
  | 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 ->
196
      ()
197 198 199 200 201 202
  | 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;
203
      r := Dval d
204 205 206 207 208 209 210 211 212 213 214 215 216 217 218
  | 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
219 220 221

(** Built-in types *)

222 223 224 225
let dity_int  = Dapp (its_int,  [], [])
let dity_real = Dapp (its_real, [], [])
let dity_bool = Dapp (its_bool, [], [])
let dity_unit = Dapp (its_unit, [], [])
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245

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

246 247 248 249 250 251 252
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 ->
253
      Pretty.print_tv fmt v
254 255 256 257 258
  | 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})}
259
  | Durg (Dapp (s,tl,rl),{reg_name = id}) ->
260 261 262 263 264
      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
265
  | Dapp (s,[t1;t2],[]) when its_equal s its_func ->
266
      Format.fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
267
        (print_dity pur 1) t1 (print_dity pur 0) t2
268
  | Dapp (s,tl,[]) when is_ts_tuple s.its_ts ->
269 270 271 272 273 274 275 276 277
      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
278
  | Dapp (s,tl,rl) ->
279 280 281 282
      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

284
let print_dity fmt d = print_dity false 0 fmt d
285 286 287 288

(* Specialization of symbols *)

let specialize_scheme tvs (argl,res) =
289
  let hv = Htv.create 3 in
290
  let rec spec_dity = function
291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307
    | 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
308 309 310 311
  List.map spec_dity argl, spec_dity res

let spec_ity hv hr frz ity =
  let rec dity ity = match ity.ity_node with
312 313 314 315 316 317 318 319 320 321 322 323 324 325
    | 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
326 327
  dity ity

Andrei Paskevich's avatar
Andrei Paskevich committed
328
let specialize_pv {pv_ity = ity} =
329 330
  spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity

Andrei Paskevich's avatar
Andrei Paskevich committed
331
let specialize_xs {xs_ity = ity} =
332 333
  spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity

334
let specialize_rs {rs_cty = cty} =
335 336 337 338
  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

339 340
let specialize_ls {ls_args = args; ls_value = res} =
  let hv = Htv.create 3 and hr = Hreg.create 3 in
341 342 343
  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
344

345 346 347
(** Patterns *)

type dpattern = {
Andrei Paskevich's avatar
Andrei Paskevich committed
348
  dp_pat  : pre_pattern;
349 350 351 352 353 354 355
  dp_dity : dity;
  dp_vars : dity Mstr.t;
  dp_loc  : Loc.position option;
}

type dpattern_node =
  | DPwild
356
  | DPvar  of preid * bool
357
  | DPapp  of rsymbol * dpattern list
358
  | DPas   of dpattern * preid * bool
359 360 361 362 363 364 365
  | DPor   of dpattern * dpattern
  | DPcast of dpattern * ity

(** Specifications *)

type ghost = bool

Andrei Paskevich's avatar
Andrei Paskevich committed
366
type dbinder = preid option * ghost * dity
367

368 369 370
type register_old = pvsymbol -> string -> pvsymbol

type 'a later = pvsymbol Mstr.t -> register_old -> 'a
371 372 373 374 375 376
  (* 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;
377 378 379
  ds_post    : (pvsymbol * term) list;
  ds_xpost   : (pvsymbol * term) list Mexn.t;
  ds_reads   : pvsymbol list;
380 381
  ds_writes  : term list;
  ds_diverge : bool;
382
  ds_checkrw : bool;
383 384
}

385
type dspec = ity -> dspec_final
386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402
  (* 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
403 404
  | DEpv of pvsymbol
  | DErs of rsymbol
405
  | DEls of lsymbol
406
  | DEconst of Number.constant
407
  | DEapp of dexpr * dexpr
408 409
  | DEfun of dbinder list * mask * dspec later * dexpr
  | DEany of dbinder list * mask * dspec later * dity
410 411
  | DElet of dlet_defn * dexpr
  | DErec of drec_defn * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
412
  | DEnot of dexpr
413 414
  | DEand of dexpr * dexpr
  | DEor of dexpr * dexpr
415 416
  | DEif of dexpr * dexpr * dexpr
  | DEcase of dexpr * (dpattern * dexpr) list
417
  | DEassign of (dexpr * rsymbol * dexpr) list
418
  | DEwhile of dexpr * dinvariant later * variant list later * dexpr
419
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
420 421 422
  | DEtry of dexpr * (xsymbol * dpattern * dexpr) list
  | DEraise of xsymbol * dexpr
  | DEghost of dexpr
423
  | DEassert of assertion_kind * term later
Andrei Paskevich's avatar
Andrei Paskevich committed
424 425 426 427
  | DEpure of term later
  | DEabsurd
  | DEtrue
  | DEfalse
428 429 430 431 432
  | DEmark of preid * dexpr
  | DEcast of dexpr * ity
  | DEuloc of dexpr * Loc.position
  | DElabel of dexpr * Slab.t

433
and dlet_defn = preid * ghost * rs_kind * dexpr
434 435 436

and drec_defn = { fds : dfun_defn list }

437
and dfun_defn = preid * ghost * rs_kind *
438
  dbinder list * mask * dspec later * variant list later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
439

440 441 442 443 444 445 446 447 448
(** 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
449 450
let is_frozen frozen v =
  try List.iter (occur_check v) frozen; false with Exit -> true
451 452 453

let freeze_dvty frozen (argl,res) =
  let rec add l = function
454 455 456
    | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
    | Durg (d,_) -> add l d
    | Dvar {contents = Dtvs _}
457
    | Dutv _ as d -> d :: l
458
    | Dapp (_,tl,_) -> List.fold_left add l tl in
459 460 461 462
  List.fold_left add (add frozen res) argl

let free_vars frozen (argl,res) =
  let rec add s = function
463 464 465 466
    | 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
467
    | Dapp (_,tl,_) -> List.fold_left add s tl in
468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489
  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
490 491 492
    | 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
493
    | Dutv _ -> true
494
    | Dapp (_,tl,_) -> List.for_all is_explicit tl in
495 496 497 498 499 500
  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
501
let denv_add_let denv (id,_,_,({de_dvty = dvty} as de)) =
502 503 504
  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
505
    | DEvar _ | DErs _ | DEls _ | DEfun _ | DEany _ -> true
506 507 508 509 510 511
    | _ -> 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
512 513
  let l = List.fold_left (fun l (_,_,t) -> t::l) frozen bl in
  let add s (id,_,t) = match id with
514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545
    | 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

Andrei Paskevich's avatar
Andrei Paskevich committed
546 547
let dexpr_expected_type {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
548 549 550 551
  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
552 553
let dexpr_expected_type_weak {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
554 555 556 557 558 559
  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 *)

560
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
561
  dity * mask * (denv -> dspec later * variant list later * dexpr)
562 563 564 565

exception DupId of preid

let drec_defn denv0 prel =
Andrei Paskevich's avatar
Andrei Paskevich committed
566
  if prel = [] then invalid_arg "Dexpr.drec_defn: empty function list";
567
  let add s (id,_,_,_,_,_,_) = Sstr.add_new (DupId id) id.pre_name s in
568 569
  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
570
  let add denv (id,_,_,bl,res,_,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
571 572
    if bl = [] then invalid_arg "Dexpr.drec_defn: empty argument list";
    let argl = List.map (fun (_,_,t) -> t) bl in
573 574
    denv_add_rec denv denv0.frozen id (argl,res) in
  let denv1 = List.fold_left add denv0 prel in
575
  let parse (id,gh,pk,bl,res,msk,pre) =
576
    let dsp, dvl, de = pre (denv_add_args denv1 bl) in
577
    dexpr_expected_type de res;
578
    (id,gh,pk,bl,msk,dsp,dvl,de) in
579
  let fdl = List.map parse prel in
580
  let add denv (id,_,_,bl,_,_,_,{de_dvty = dvty}) =
Andrei Paskevich's avatar
Andrei Paskevich committed
581
    (* just in case we linked some polymorphic type var to the outer context *)
582 583 584 585 586 587 588
    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
589 590
    let argl = List.map (fun (_,_,t) -> t) bl in
    denv_add_poly denv id (argl, dity_of_dvty dvty) in
591 592 593 594 595 596 597 598 599 600
  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
601
    | DPvar (id,gh) ->
602
        let dity = dity_fresh () in
603
        mk_dpat (PPvar (id,gh)) dity (Mstr.singleton id.pre_name dity)
604 605
    | DPapp ({rs_logic = RLls ls} as rs, dpl) when ls.ls_constr > 0 ->
        let argl, res = specialize_rs rs in
606 607 608 609 610
        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
611 612 613
        mk_dpat (PPapp (rs, ppl)) res vars
    | DPapp (rs,_) ->
        raise (ConstructorExpected rs);
614 615 616 617 618 619 620 621
    | 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
622
    | DPas (dp, ({pre_name = n} as id), gh) ->
623 624
        let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in
        let vars = Mstr.add_new (Dterm.DuplicateVar n) n dity vars in
625
        mk_dpat (PPas (pat, id, gh)) dity vars
626
    | DPcast (dp, ity) ->
627
        dpat_expected_type dp (dity_of_ity ity);
628 629 630 631 632 633 634
        dp
  in
  Loc.try1 ?loc dpat node

let dexpr ?loc node =
  let get_dvty = function
    | DEvar (_,dvty) ->
635
        dvty
636
    | DEpv pv ->
637
        [], specialize_pv pv
638
    | DErs rs ->
639
        specialize_rs rs
640 641
    | DEls ls ->
        specialize_ls ls
642
    | DEconst (Number.ConstInt _) ->
643
        dvty_int
644
    | DEconst (Number.ConstReal _) ->
645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664
        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
665
    | DEfun (bl,_,_,de) ->
666
        List.map (fun (_,_,t) -> t) bl, dity_of_dvty de.de_dvty
667
    | DEany (bl,_,_,res) ->
668
        List.map (fun (_,_,t) -> t) bl, res
669 670
    | DElet (_,de)
    | DErec (_,de) ->
671
        de.de_dvty
672 673
    | DEnot de ->
        dexpr_expected_type de dity_bool;
674 675 676
        dvty_bool
    | DEand (de1,de2)
    | DEor (de1,de2) ->
677 678
        dexpr_expected_type de1 dity_bool;
        dexpr_expected_type de2 dity_bool;
679
        dvty_bool
680 681 682 683 684
    | 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;
685
        [], res
686
    | DEcase (_,[]) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
687
        invalid_arg "Dexpr.dexpr: empty branch list in DEcase"
688 689 690 691
    | DEcase (de,bl) ->
        let ety = dity_fresh () in
        let res = dity_fresh () in
        dexpr_expected_type de ety;
692
        List.iter (fun (dp,de) ->
693
          dpat_expected_type dp ety;
694
          dexpr_expected_type de res) bl;
695
        [], res
696
    | DEassign al ->
697 698 699
        List.iter (fun (de1,rs,de2) ->
          let argl, res = specialize_rs rs in
          let ls = match rs.rs_logic with RLls ls -> ls
700 701 702
            | _ -> invalid_arg "Dexpr.dexpr: not a field" in
          dity_unify_app ls dexpr_expected_type [de1] argl;
          dexpr_expected_type_weak de2 res) al;
703 704
        dvty_unit
    | DEwhile (de1,_,_,de2) ->
705
        dexpr_expected_type de1 dity_bool;
706
        dexpr_expected_type de2 dity_unit;
707
        dvty_unit
708 709 710 711
    | 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;
712
        dvty_unit
713
    | DEtry (_,[]) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
714
        invalid_arg "Dexpr.dexpr: empty branch list in DEtry"
715 716 717
    | DEtry (de,bl) ->
        let res = dity_fresh () in
        dexpr_expected_type de res;
718 719 720
        List.iter (fun (xs,dp,de) ->
          dpat_expected_type dp (specialize_xs xs);
          dexpr_expected_type de res) bl;
721
        [], res
722 723
    | DEraise (xs,de) ->
        dexpr_expected_type de (specialize_xs xs);
724
        [], dity_fresh ()
725
    | DEghost de ->
726
        de.de_dvty
727
    | DEassert _ ->
728
        dvty_unit
729 730
    | DEpure _
    | DEabsurd ->
731
        [], dity_fresh ()
732 733
    | DEtrue
    | DEfalse ->
734
        dvty_bool
735
    | DEcast (de,ity) ->
736
        dexpr_expected_type de (dity_of_ity ity);
737
        de.de_dvty
738
    | DEmark (_,de)
739 740
    | DEuloc (de,_)
    | DElabel (de,_) ->
741 742 743
        de.de_dvty in
  let dvty = Loc.try1 ?loc get_dvty node in
  { de_node = node; de_dvty = dvty; de_loc = loc }
744 745 746 747 748 749 750

(** Final stage *)

(** Binders *)

let binders bl =
  let sn = ref Sstr.empty in
751
  let binder (id, ghost, dity) =
752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768
    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

769 770 771 772
let create_assert = to_fmla

let create_invariant pl = List.map to_fmla pl

773 774
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
775

776
let create_xpost xql = Mexn.mapi (fun xs ql -> create_post xs.xs_ity ql) xql
777 778 779

(** User effects *)

780 781 782 783 784 785
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
786
        | Some {rs_cty = {cty_args = [arg]; cty_result = res}} ->
787 788 789
            ity_full_inst (ity_match isb_empty arg.pv_ity ity) res
        | Some _ -> assert false
        | None -> ity in
790
      begin try match ity.ity_node, restore_rs fs with
Andrei Paskevich's avatar
Andrei Paskevich committed
791 792
        | Ityreg {reg_its = ts}, ({rs_field = Some f} as rs)
          when List.exists (pv_equal f) ts.its_mfields -> v, ity, Some rs
793
        | _, {rs_cty={cty_args=[arg]; cty_result=res; cty_freeze=frz}} ->
794 795 796 797 798 799
            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 ()
800 801

let effect_of_dspec dsp =
802
  let pvs = Spv.of_list dsp.ds_reads in
803
  let add_write (l,eff) t = match effect_of_term t with
804 805
    | v, {ity_node = Ityreg reg}, fd ->
        let fs = match fd with
806
          | Some fd -> Spv.singleton (Opt.get fd.rs_field)
807
          | None -> Spv.of_list reg.reg_its.its_mfields in
808 809
        if not reg.reg_its.its_private && Spv.is_empty fs then
          Loc.errorm ?loc:t.t_loc "mutable expression expected";
810 811 812
        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
813
    | _ ->
814
        Loc.errorm ?loc:t.t_loc "mutable expression expected" in
815 816 817 818
  let wl, eff = List.fold_left add_write ([], eff_read pvs) dsp.ds_writes in
  let eff = Mexn.fold (fun xs _ eff -> eff_raise eff xs) dsp.ds_xpost eff in
  let eff = if dsp.ds_diverge then eff_diverge eff else eff in
  wl, eff
819

820 821
(* TODO: add warnings for empty postconditions (anywhere)
    and empty exceptional postconditions (toplevel). *)
Andrei Paskevich's avatar
Andrei Paskevich committed
822
let check_spec dsp ecty e =
823 824 825
  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
826
  (* computed effect vs user effect *)
827
  let check_rw = dsp.ds_checkrw in
828
  let uwrl, ue = effect_of_dspec dsp in
829 830
  let ucty = create_cty ecty.cty_args ecty.cty_pre ecty.cty_post
    ecty.cty_xpost ecty.cty_oldies ue ecty.cty_result in
831 832
  let ueff = ucty.cty_effect and eeff = ecty.cty_effect in
  let urds = ueff.eff_reads and erds = eeff.eff_reads in
833
  (* check that every user effect actually happens *)
834 835 836 837 838 839 840 841 842
  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));
843
  if ueff.eff_oneway && not eeff.eff_oneway then Loc.errorm ?loc:e.e_loc
844
    "this@ expression@ does@ not@ diverge";
845
  (* check that every computed effect is listed *)
846
  if check_rw && not (Spv.subset erds urds) then Spv.iter (fun v ->
847 848 849
    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);
850
  if check_rw && bad_write eeff ueff then
851
    Loc.errorm ?loc:(e_locate_effect (fun eff -> bad_write eff ueff) e)
852 853
      "this@ expression@ produces@ an@ unlisted@ write@ effect";
  if ecty.cty_args <> [] && bad_raise eeff ueff then Sexn.iter (fun xs ->
854
    Loc.errorm ?loc:(e_locate_effect (fun eff -> Sexn.mem xs eff.eff_raises) e)
855
      "this@ expression@ raises@ unlisted@ exception@ %a"
856
      print_xs xs) (Sexn.diff eeff.eff_raises ueff.eff_raises);
857
  if eeff.eff_oneway && not ueff.eff_oneway then
858
    Loc.errorm ?loc:(e_locate_effect (fun eff -> eff.eff_oneway) e)
859 860
      "this@ expression@ may@ diverge,@ but@ this@ is@ not@ \
        stated@ in@ the@ specification"
861

Andrei Paskevich's avatar
Andrei Paskevich committed
862
let check_aliases recu c =
863 864 865
  let rds_regs = c.cty_freeze.isb_reg in
  let report r _ _ =
    if Mreg.mem r rds_regs then let spv = Spv.filter
866
        (fun v -> ity_r_occurs r v.pv_ity) (cty_reads c) in
867
      Loc.errorm "The type of this function contains an alias with \
868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884
        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)
885

886
let check_fun rsym dsp e =
Andrei Paskevich's avatar
Andrei Paskevich committed
887
  let c,e = match e with
888
    | { c_node = Cfun e; c_cty = c } -> c,e
Andrei Paskevich's avatar
Andrei Paskevich committed
889 890 891 892 893 894 895
    | _ -> 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

896 897
(** Environment *)

Andrei Paskevich's avatar
Andrei Paskevich committed
898
type env = {
899
  rsm : rsymbol Mstr.t;
900
  pvm : pvsymbol Mstr.t;
901
  old : (pvsymbol Mstr.t * (let_defn * pvsymbol) Hpv.t) Mstr.t;
902 903
}

904
let env_empty = {
905
  rsm = Mstr.empty;
906
  pvm = Mstr.empty;
907
  old = Mstr.empty;
908 909
}

910 911 912
exception UnboundLabel of string

let find_old pvm (ovm,old) v =
913
  if v.pv_ity.ity_imm then v else
914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938
  let n = v.pv_vs.vs_name.id_string in
  (* if v is top-level, both ov and pv are None.
     If v is local, ov and pv must be equal to v.
     If they are not equal, then v is defined under the label,
     so we return v and do not register an "oldie" for it. *)
  let ov = Mstr.find_opt n ovm in
  let pv = Mstr.find_opt n pvm in
  if not (Opt.equal pv_equal ov pv) then v
  else match Hpv.find_opt old v with
    | Some (_,o) -> o
    | None ->
        let e = e_pure (t_var v.pv_vs) in
        let id = id_clone v.pv_vs.vs_name in
        let ld = let_var id ~ghost:true e in
        Hpv.add old v ld; snd ld

let register_old env v l =
  find_old env.pvm (Mstr.find_exn (UnboundLabel l) l env.old) v

let get_later env later = later env.pvm (register_old env)

let add_label ({pvm = pvm; old = old} as env) l =
  let ht = Hpv.create 3 in
  { env with old = Mstr.add l (pvm, ht) old }, ht

Andrei Paskevich's avatar
Andrei Paskevich committed
939
let rebase_old {pvm = pvm} preold old fvs =
940 941 942 943
  let rebase v (_,{pv_vs = o}) sbs =
    if not (Mvs.mem o fvs) then sbs else match preold with
      | Some preold ->
          Mvs.add o (t_var (find_old pvm preold v).pv_vs) sbs
944
      | None -> raise (UnboundLabel "0") in
945 946
  Hpv.fold rebase old Mvs.empty

Andrei Paskevich's avatar
Andrei Paskevich committed
947
let rebase_pre env preold old pl =
948 949
  let pl = List.map to_fmla pl in
  let fvs = List.fold_left t_freevars Mvs.empty pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
950
  let sbs = rebase_old env preold old fvs in
951 952
  List.map (t_subst sbs) pl

Andrei Paskevich's avatar
Andrei Paskevich committed
953
let rebase_variant env preold old varl =
954 955
  let add s (t,_) = t_freevars s t in
  let fvs = List.fold_left add Mvs.empty varl in
Andrei Paskevich's avatar
Andrei Paskevich committed
956
  let sbs = rebase_old env preold old fvs in
957 958 959
  let conv (t,rel) = t_subst sbs t, rel in
  List.map conv varl

960 961 962 963
let get_oldies old =
  Hpv.fold (fun v (_,o) sbs -> Mpv.add o v sbs) old Mpv.empty

let add_rsymbol ({rsm = rsm; pvm = pvm} as env) rs =
964
  let n = rs.rs_name.id_string in
965 966 967 968
  let pvm = match rs.rs_logic with
    | RLpv pv -> Mstr.add n pv pvm
    | _ -> pvm in
  { env with rsm = Mstr.add n rs rsm; pvm = pvm }
969

970
let add_pvsymbol ({pvm = pvm} as env) pv =
971
  let n = pv.pv_vs.vs_name.id_string in
972
  { env with pvm = Mstr.add n pv pvm }
973

974 975
let add_pv_map ({pvm = pvm} as env) vm =
  { env with pvm = Mstr.set_union vm pvm }
976 977 978 979 980

let add_binders env pvl = List.fold_left add_pvsymbol env pvl

(** Abstract values *)

981
let cty_of_spec env bl mask dsp dity =
Andrei Paskevich's avatar
Andrei Paskevich committed
982 983 984
  let ity = ity_of_dity dity in
  let bl = binders bl in
  let env = add_binders env bl in
985 986
  let preold = Mstr.find_opt "0" env.old in
  let env, old = add_label env "0" in
987
  let dsp = get_later env dsp ity in
988
  let _, eff = effect_of_dspec dsp in
989
  let eff = eff_reset_overwritten eff in
990
  let eff = eff_reset eff (ity_freeregs Sreg.empty ity) in
Andrei Paskevich's avatar
Andrei Paskevich committed
991
  let p = rebase_pre env preold old dsp.ds_pre in
992
  let q = create_post ity dsp.ds_post in
Andrei Paskevich's avatar
Andrei Paskevich committed
993
  let xq = create_xpost dsp.ds_xpost in
994
  create_cty ~mask bl p q xq (get_oldies old) eff ity
995 996 997

(** Expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
998 999 1000 1001
let warn_unused s loc =
  if s = "" || s.[0] <> '_' then
  Warning.emit ?loc "unused variable %s" s

1002
let check_used_pv e pv = if not (Spv.mem pv e.e_effect.eff_reads) then
Andrei Paskevich's avatar
Andrei Paskevich committed
1003
  warn_unused pv.pv_vs.vs_name.id_string pv.pv_vs.vs_name.id_loc
1004

1005 1006 1007 1008
let e_let_check ld e = match ld with
  | LDvar (v,_) -> check_used_pv e v; e_let ld e
  | _           -> e_let ld e

1009 1010
let rec strip uloc labs de = match de.de_node with
  | DEcast (de,_) -> strip uloc labs de
1011
  | DEuloc (de,loc) -> strip (Some (Some loc)) labs de