dexpr.ml 61.7 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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
open Wstdlib
13 14 15 16 17
open Ident
open Ty
open Term
open Ity
open Expr
18
open Pmodule
19 20 21 22

(** Program types *)

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

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

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

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

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

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

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

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

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

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

let dity_of_ity ity =
  let hr = Hreg.create 3 in
  let rec dity ity = match ity.ity_node with
63
    | Ityvar v -> Dutv v
64 65 66 67 68
    | 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
  | 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) []
80
        | Ityvar v -> ity_var v in
81 82 83 84
      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
85
        | Ityvar v -> Dutv v in
86 87 88 89 90 91
      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
92 93 94 95
  | Dvar r ->
      let v = create_tvsymbol (id_fresh "xi") in
      r := Dval (Dutv v); ity_var v
  | Dapp (s,tl,rl) ->
96
      ity_app_pure s (List.map ity_of_dity tl) (List.map ity_of_dity rl)
97 98 99 100

(** Destructive type unification *)

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

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

141 142 143 144 145 146
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,_) ->
147
      let d = dity_app_fresh s (List.map dity_refresh dl) in
148
      if s.its_mutable then dity_reg d else d
149 150

let rec dity_unify_asym d1 d2 = match d1,d2 with
151
  | Durg _, _ -> raise Exit (* we cannot be pure then *)
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
  | 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
175 176
  | Dutv u, Dutv v when tv_equal u v ->
      ()
177 178 179 180
  | 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
181

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

(** Built-in types *)

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

229
(*
230 231
let dvty_int  = [], dity_int
let dvty_real = [], dity_real
232
*)
233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249
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

250 251 252 253 254 255 256
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 ->
257
      Pretty.print_tv fmt v
258 259 260 261 262
  | 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})}
263
  | Durg (Dapp (s,tl,rl),{reg_name = id}) ->
264 265
      Format.fprintf fmt
        (protect_on (pri > 1 && (tl <> [] || rl <> [])) "%a%a%a@ @@%s")
266
        Pretty.print_ts_qualified s.its_ts (print_args (print_dity pur 2)) tl
267 268
          (print_regs (print_dity pur 0)) rl (Ident.id_unique rprinter id)
  | Dvar {contents = Dreg _} | Durg _ -> assert false
269
  | Dapp (s,[t1;t2],[]) when its_equal s its_func ->
270
      Format.fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
271
        (print_dity pur 1) t1 (print_dity pur 0) t2
272
  | Dapp (s,tl,[]) when is_ts_tuple s.its_ts ->
273 274 275
      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")
276
        Pretty.print_ts_qualified s.its_ts (print_args (print_dity pur 2)) tl
277
  | Dapp (s,tl,rl) when not s.its_mutable ->
278 279
      Format.fprintf fmt
        (protect_on (pri > 1 && (tl <> [] || rl <> [])) "%a%a%a")
280
        Pretty.print_ts_qualified s.its_ts (print_args (print_dity pur 2)) tl
281
          (print_regs (print_dity pur 0)) rl
282
  | Dapp (s,tl,rl) ->
283 284
      Format.fprintf fmt
        (protect_on (pri > 1 && (tl <> [] || rl <> [])) "{%a}%a%a")
285
        Pretty.print_ts_qualified s.its_ts (print_args (print_dity pur 2)) tl
286
          (print_regs (print_dity pur 0)) rl
287

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

(* Specialization of symbols *)

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

let spec_ity hv hr frz ity =
  let rec dity ity = match ity.ity_node with
316 317 318 319 320
    | 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)
321 322 323 324
    | Ityvar v ->
        (try Htv.find hv v with Not_found ->
        let nd = if Mtv.mem v frz.isb_var then Dutv v else dity_fresh () in
        Htv.add hv v nd; nd)
325
    | Ityapp (s,tl,rl) -> app_map dity s tl rl in
326 327
  dity ity

328
let specialize_single ity =
329 330
  spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity

331
let specialize_rs {rs_cty = cty} =
332 333 334 335
  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

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

342 343 344 345 346 347 348 349
type dxsymbol =
  | DElexn of string * dity
  | DEgexn of xsymbol

let specialize_dxs = function
  | DEgexn xs -> specialize_single xs.xs_ity
  | DElexn (_,dity) -> dity

350 351 352
(** Patterns *)

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

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

(** Specifications *)

type ghost = bool

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

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

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

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

391
type dspec = ity -> dspec_final
392 393 394 395 396
  (* 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. *)

Andrei Paskevich's avatar
Andrei Paskevich committed
397
let old_label = "'Old"
398

399 400 401 402 403 404 405 406 407 408 409 410
(** 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
411
  | DEsym of prog_symbol
412
  | DEconst of Number.constant * dity
413
  | DEapp of dexpr * dexpr
414 415
  | DEfun of dbinder list * dity * mask * dspec later * dexpr
  | DEany of dbinder list * dity * mask * dspec later
416 417
  | DElet of dlet_defn * dexpr
  | DErec of drec_defn * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
418
  | DEnot of dexpr
419 420
  | DEand of dexpr * dexpr
  | DEor of dexpr * dexpr
421
  | DEif of dexpr * dexpr * dexpr
422
  | DEmatch of dexpr * dreg_branch list * dexn_branch list
423
  | DEassign of (dexpr * rsymbol * dexpr) list
424
  | DEwhile of dexpr * dinvariant later * variant list later * dexpr
425
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
426
  | DEraise of dxsymbol * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
427
  | DEghost of dexpr
428
  | DEexn of preid * dity * mask * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
429
  | DEoptexn of preid * dity * mask * dexpr
430
  | DEassert of assertion_kind * term later
431
  | DEpure of term later * dity
432
  | DEvar_pure of string * dvty
433
  | DEls_pure of lsymbol * bool
434
  | DEpv_pure of pvsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
435 436 437
  | DEabsurd
  | DEtrue
  | DEfalse
Andrei Paskevich's avatar
Andrei Paskevich committed
438
  | DElabel of preid * dexpr
439
  | DEcast of dexpr * dity
440
  | DEuloc of dexpr * Loc.position
Andrei Paskevich's avatar
Andrei Paskevich committed
441
  | DEattr of dexpr * Sattr.t
442

443 444 445 446
and dreg_branch = dpattern * dexpr

and dexn_branch = dxsymbol * dpattern * dexpr

447
and dlet_defn = preid * ghost * rs_kind * dexpr
448 449 450

and drec_defn = { fds : dfun_defn list }

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

454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476
(** 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 dexpr_expected_type {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
  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

let dexpr_expected_type_weak {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
  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

477 478 479 480
(** Environment *)

type denv = {
  frozen : dity list;
481
  locals : (bool * Stv.t option * dvty) Mstr.t;
482
  excpts : dxsymbol Mstr.t
483 484
}

485
let denv_names d = Mstr.domain d.locals
486

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

Andrei Paskevich's avatar
Andrei Paskevich committed
489 490
let is_frozen frozen v =
  try List.iter (occur_check v) frozen; false with Exit -> true
491 492 493

let freeze_dvty frozen (argl,res) =
  let rec add l = function
494 495 496
    | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
    | Durg (d,_) -> add l d
    | Dvar {contents = Dtvs _}
497
    | Dutv _ as d -> d :: l
498
    | Dapp (_,tl,_) -> List.fold_left add l tl in
499 500 501 502
  List.fold_left add (add frozen res) argl

let free_vars frozen (argl,res) =
  let rec add s = function
503 504 505 506
    | 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
507
    | Dapp (_,tl,_) -> List.fold_left add s tl in
508 509
  List.fold_left add (add Stv.empty res) argl

510 511 512 513 514
let denv_add_exn { frozen = fz; locals = ls; excpts = xs } id dity =
  let xs = Mstr.add id.pre_name (DElexn (id.pre_name, dity)) xs in
  { frozen = freeze_dvty fz ([], dity); locals = ls; excpts = xs }

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

518
let denv_add_poly { frozen = fz; locals = ls; excpts = xs } id dvty =
519
  let ls = Mstr.add id.pre_name (false, Some (free_vars fz dvty), dvty) ls in
520
  { frozen = fz; locals = ls; excpts = xs }
521

522
let denv_add_rec_mono { frozen = fz; locals = ls; excpts = xs } id dvty =
523
  let ls = Mstr.add id.pre_name (false, Some Stv.empty, dvty) ls in
524
  { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }
525

526
let denv_add_rec_poly { frozen = fz; locals = ls; excpts = xs } fz0 id dvty =
527
  let ls = Mstr.add id.pre_name (false, Some (free_vars fz0 dvty), dvty) ls in
528
  { frozen = fz; locals = ls; excpts = xs }
529

530
let denv_add_rec denv fz0 id ((argl,res) as dvty) =
531
  let rec is_explicit = function
532 533 534
    | 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
535
    | Dutv _ -> true
536
    | Dapp (_,tl,_) -> List.for_all is_explicit tl in
537
  if List.for_all is_explicit argl && is_explicit res
538
  then denv_add_rec_poly denv fz0 id dvty
539 540 541 542
  else denv_add_rec_mono denv id dvty

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

543 544 545 546 547 548
let denv_add_for_index denv id dvty =
  let dvty = [], dity_of_dvty dvty in
  let { frozen = fz; locals = ls; excpts = xs } = denv in
  let ls = Mstr.add id.pre_name (true, None, dvty) ls in
  { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }

Andrei Paskevich's avatar
Andrei Paskevich committed
549
let denv_add_let denv (id,_,_,({de_dvty = dvty} as de)) =
550 551
  if fst dvty = [] then denv_add_mono denv id dvty else
  let rec is_value de = match de.de_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
552
    | DEghost de | DEuloc (de,_) | DEattr (de,_) -> is_value de
553
    | DEvar _ | DEsym _ | DEls_pure _ | DEfun _ | DEany _ -> true
554 555 556 557 558
    | _ -> false in
  if is_value de
  then denv_add_poly denv id dvty
  else denv_add_mono denv id dvty

559 560
let denv_add_args { frozen = fz; locals = ls; excpts = xs } bl =
  let l = List.fold_left (fun l (_,_,t) -> t::l) fz bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
561
  let add s (id,_,t) = match id with
562
    | Some {pre_name = n} ->
563
        Mstr.add_new (Dterm.DuplicateVar n) n (false, None, ([],t)) s
564 565
    | None -> s in
  let s = List.fold_left add Mstr.empty bl in
566
  { frozen = l; locals = Mstr.set_union s ls; excpts = xs }
567

568 569
let denv_add_pat { frozen = fz; locals = ls; excpts = xs } dp dity =
  dpat_expected_type dp dity;
570
  let l = Mstr.fold (fun _ t l -> t::l) dp.dp_vars fz in
571
  let s = Mstr.map (fun t -> false, None, ([], t)) dp.dp_vars in
572
  { frozen = l; locals = Mstr.set_union s ls; excpts = xs }
573

574 575 576 577 578 579
let denv_add_expr_pat denv dp de =
  denv_add_pat denv dp (dity_of_dvty de.de_dvty)

let denv_add_exn_pat denv dp dxs =
  denv_add_pat denv dp (specialize_dxs dxs)

580
let mk_node n = function
581 582
  | _, Some tvs, dvty -> DEvar (n, specialize_scheme tvs dvty)
  | _, None,     dvty -> DEvar (n, dvty)
583 584 585 586 587 588 589

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)

590 591 592 593 594 595 596 597 598 599
let mk_node_pure n = function
  | _, Some tvs, dvty -> DEvar_pure (n, specialize_scheme tvs dvty)
  | _, None,     dvty -> DEvar_pure (n, dvty)

let denv_get_pure denv n =
  mk_node_pure n (Mstr.find_exn (Dterm.UnboundVar n) n denv.locals)

let denv_get_pure_opt denv n =
  Opt.map (mk_node_pure n) (Mstr.find_opt n denv.locals)

600 601 602 603 604 605
exception UnboundExn of string

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

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

606 607 608 609 610 611 612 613 614 615 616
let denv_pure denv get_dty =
  let ht = Htv.create 3 in
  let hi = Hint.create 3 in
  let rec fold = function
    | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
    | Durg (d,_) -> fold d
    | Dvar {contents = Dtvs v} as d ->
        begin try fst (Htv.find ht v) with Not_found ->
        let f = Dterm.dty_fresh () in Htv.add ht v (f,d); f end
    | Dapp (s,dl,_) -> Dterm.dty_app s.its_ts (List.map fold dl)
    | Dutv v -> Dterm.dty_var v in
617 618 619 620
  let add n (idx, _, dvty) =
    let dity = if idx then dity_int else dity_of_dvty dvty in
    Dterm.DTvar (n, fold dity) in
  let dty = get_dty (Mstr.mapi add denv.locals) in
621 622 623 624 625 626 627 628
  Htv.iter (fun v (f,_) ->
    try Dterm.dty_match f (ty_var v) with Exit -> ()) ht;
  let fnS s dl = dity_app_fresh (restore_its s) dl in
  let fnV v = try snd (Htv.find ht v) with Not_found -> Dutv v in
  let fnI i = try Hint.find hi i with Not_found ->
    let d = dity_fresh () in Hint.add hi i d; d in
  dity_pur (Dterm.dty_fold fnS fnV fnI dty)

629 630
(** Generation of letrec blocks *)

631
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
632
  dity * mask * (denv -> dspec later * variant list later * dexpr)
633 634 635 636

exception DupId of preid

let drec_defn denv0 prel =
Andrei Paskevich's avatar
Andrei Paskevich committed
637
  if prel = [] then invalid_arg "Dexpr.drec_defn: empty function list";
638
  let add s (id,_,_,_,_,_,_) = Sstr.add_new (DupId id) id.pre_name s in
639 640
  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
641
  let add denv (id,_,_,bl,res,_,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
642 643
    if bl = [] then invalid_arg "Dexpr.drec_defn: empty argument list";
    let argl = List.map (fun (_,_,t) -> t) bl in
644 645
    denv_add_rec denv denv0.frozen id (argl,res) in
  let denv1 = List.fold_left add denv0 prel in
646
  let parse (id,gh,pk,bl,res,msk,pre) =
647
    let dsp, dvl, de = pre denv1 in
648
    dexpr_expected_type de res;
649
    (id,gh,pk,bl,res,msk,dsp,dvl,de) in
650
  let fdl = List.map parse prel in
651
  let add denv (id,_,_,bl,res,_,_,_,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
652
    (* just in case we linked some polymorphic type var to the outer context *)
653 654 655 656
    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
657 658
    | Some (_, Some tvs, _) -> Stv.iter check tvs
    | Some (_, None, _) | None -> assert false
659
    end;
Andrei Paskevich's avatar
Andrei Paskevich committed
660
    let argl = List.map (fun (_,_,t) -> t) bl in
661
    denv_add_poly denv id (argl, res) in
662 663 664 665 666 667 668 669 670 671
  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
672
    | DPvar (id,gh) ->
673
        let dity = dity_fresh () in
674
        mk_dpat (PPvar (id,gh)) dity (Mstr.singleton id.pre_name dity)
675 676
    | DPapp ({rs_logic = RLls ls} as rs, dpl) when ls.ls_constr > 0 ->
        let argl, res = specialize_rs rs in
677 678 679 680 681
        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
682 683 684
        mk_dpat (PPapp (rs, ppl)) res vars
    | DPapp (rs,_) ->
        raise (ConstructorExpected rs);
685 686 687 688 689 690 691 692
    | 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
693
    | DPas (dp, ({pre_name = n} as id), gh) ->
694 695
        let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in
        let vars = Mstr.add_new (Dterm.DuplicateVar n) n dity vars in
696
        mk_dpat (PPas (pat, id, gh)) dity vars
697 698
    | DPcast (dp, dity) ->
        dpat_expected_type dp dity;
699 700 701 702 703 704 705
        dp
  in
  Loc.try1 ?loc dpat node

let dexpr ?loc node =
  let get_dvty = function
    | DEvar (_,dvty) ->
706
        dvty
707 708 709 710
    | DEvar_pure (_,dvty) ->
        let dt = dity_fresh () in
        dity_unify_asym dt (dity_of_dvty dvty);
        [], dt
711
    | DEsym (PV pv) ->
712
        [], specialize_single pv.pv_ity
713
    | DEsym (RS rs) ->
714
        specialize_rs rs
715 716
    | DEsym (OO ss) ->
        let dt = dity_fresh () in
717 718 719 720 721 722 723
        let rs = Srs.choose ss in
        let ot = overload_of_rs rs in
        let res = match ot with
          | SameType -> dt
          | FixedRes ity -> dity_of_ity ity
          | NoOver -> assert false (* impossible *) in
        List.map (fun _ -> dt) rs.rs_cty.cty_args, res
724
    | DEls_pure (ls,_) ->
725
        specialize_ls ls
726 727
    | DEpv_pure pv ->
        [], specialize_single (ity_purify pv.pv_ity)
728
    | DEconst (_, ity) -> [],ity
729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747
    | 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
748 749 750 751
    | DEfun (bl,res,_,_,de) ->
        dexpr_expected_type de res;
        List.map (fun (_,_,t) -> t) bl, res
    | DEany (bl,res,_,_) ->
752
        List.map (fun (_,_,t) -> t) bl, res
753 754
    | DElet (_,de)
    | DErec (_,de) ->
755
        de.de_dvty
756 757
    | DEnot de ->
        dexpr_expected_type de dity_bool;
758 759 760
        dvty_bool
    | DEand (de1,de2)
    | DEor (de1,de2) ->
761 762
        dexpr_expected_type de1 dity_bool;
        dexpr_expected_type de2 dity_bool;
763
        dvty_bool
764 765 766 767 768
    | 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;
769
        [], res
770 771 772
    | DEmatch (_,[],[]) ->
        invalid_arg "Dexpr.dexpr: empty branch list in DEmatch"
    | DEmatch (de,bl,xl) ->
773
        let res = dity_fresh () in
774 775 776
        if bl = [] then dexpr_expected_type de res;
        List.iter (fun (_,de) -> dexpr_expected_type de res) bl;
        List.iter (fun (_,_,de) -> dexpr_expected_type de res) xl;
777
        [], res
778
    | DEassign al ->
779 780 781
        List.iter (fun (de1,rs,de2) ->
          let argl, res = specialize_rs rs in
          let ls = match rs.rs_logic with RLls ls -> ls
782 783 784
            | _ -> invalid_arg "Dexpr.dexpr: not a field" in
          dity_unify_app ls dexpr_expected_type [de1] argl;
          dexpr_expected_type_weak de2 res) al;
785 786
        dvty_unit
    | DEwhile (de1,_,_,de2) ->
787
        dexpr_expected_type de1 dity_bool;
788
        dexpr_expected_type de2 dity_unit;
789
        dvty_unit
790
    | DEfor (_,de_from,_,de_to,_,de) ->
791 792 793
        let bty = dity_fresh () in
        dexpr_expected_type de_from bty;
        dexpr_expected_type de_to bty;
794
        dexpr_expected_type de dity_unit;
795
        dvty_unit
796
    | DEraise (xs,de) ->
797
        dexpr_expected_type de (specialize_dxs xs);
798
        [], dity_fresh ()
799
    | DEexn (_,_,_,de)
800
    | DEghost de ->
801
        de.de_dvty
802
    | DEassert _ ->
803
        dvty_unit
804 805
    | DEpure (_, dity) ->
        [], dity
806
    | DEabsurd ->
807
        [], dity_fresh ()
808 809
    | DEtrue
    | DEfalse ->
810
        dvty_bool
Andrei Paskevich's avatar
Andrei Paskevich committed
811 812 813
    | DEoptexn (_,dity,_,de) ->
        dexpr_expected_type de dity;
        [], dity
814
    | DEcast (de,dity) ->
815
        dexpr_expected_type de dity;
816
        de.de_dvty
Andrei Paskevich's avatar
Andrei Paskevich committed
817
    | DElabel (_,de)
818
    | DEuloc (de,_)
Andrei Paskevich's avatar
Andrei Paskevich committed
819
    | DEattr (de,_) ->
820 821 822
        de.de_dvty in
  let dvty = Loc.try1 ?loc get_dvty node in
  { de_node = node; de_dvty = dvty; de_loc = loc }
823 824 825 826 827

(** Final stage *)

(** Binders *)

828
let binders ghost bl =
829
  let sn = ref Sstr.empty in
830
  let binder (id, gh, dity) =
831 832 833 834 835 836 837
    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
838
    create_pvsymbol id ~ghost:(ghost || gh) (ity_of_dity dity) in
839 840 841 842 843 844 845 846 847
  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

848 849 850 851
let create_assert = to_fmla

let create_invariant pl = List.map to_fmla pl

852 853
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
854

855
let create_xpost xql = Mxs.mapi (fun xs ql -> create_post xs.xs_ity ql) xql
856 857 858

(** User effects *)

859 860 861 862 863 864
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
865
        | Some {rs_cty = {cty_args = [arg]; cty_result = res}} ->
866 867 868
            ity_full_inst (ity_match isb_empty arg.pv_ity ity) res
        | Some _ -> assert false
        | None -> ity in
869
      begin try match ity.ity_node, restore_rs fs with
Andrei Paskevich's avatar
Andrei Paskevich committed
870 871
        | Ityreg {reg_its = ts