dexpr.ml 61.2 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 13 14 15 16 17
(********************************************************************)

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

(** Program types *)

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

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

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

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

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

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

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

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

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

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

let dity_of_ity ity =
  let hr = Hreg.create 3 in
  let rec dity ity = match ity.ity_node with
63
    | 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 266 267 268
      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
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 276
      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
277
  | Dapp (s,tl,rl) when not s.its_mutable ->
278 279 280 281
      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
282
  | Dapp (s,tl,rl) ->
283 284 285 286
      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
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
(** Patterns *)

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

type dpattern_node =
  | DPwild
353
  | DPvar  of preid * bool
354
  | DPapp  of rsymbol * dpattern list
355
  | DPas   of dpattern * preid * bool
356
  | DPor   of dpattern * dpattern
357
  | DPcast of dpattern * dity
358 359 360 361 362

(** Specifications *)

type ghost = bool

Andrei Paskevich's avatar
Andrei Paskevich committed
363
type dbinder = preid option * ghost * dity
364

365
type register_old = string -> pvsymbol -> pvsymbol
366

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

382
type dspec = ity -> dspec_final
383 384 385 386 387
  (* 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. *)

388 389
let old_mark = "'Old"

390 391 392 393
(** Expressions *)

type dinvariant = term list

394 395 396 397
type dxsymbol =
  | DElexn of string * dity
  | DEgexn of xsymbol

398 399 400 401 402 403 404 405
type dexpr = {
  de_node : dexpr_node;
  de_dvty : dvty;
  de_loc  : Loc.position option;
}

and dexpr_node =
  | DEvar of string * dvty
406
  | DEsym of prog_symbol
407
  | DEconst of Number.constant * dity
408
  | DEapp of dexpr * dexpr
409 410
  | DEfun of dbinder list * dity * mask * dspec later * dexpr
  | DEany of dbinder list * dity * mask * dspec later
411 412
  | DElet of dlet_defn * dexpr
  | DErec of drec_defn * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
413
  | DEnot of dexpr
414 415
  | DEand of dexpr * dexpr
  | DEor of dexpr * dexpr
416
  | DEif of dexpr * dexpr * dexpr
417
  | DEcase of dexpr * dreg_branch list * dexn_branch list
418
  | DEassign of (dexpr * rsymbol * dexpr) list
419
  | DEwhile of dexpr * dinvariant later * variant list later * dexpr
420
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
421
  | DEraise of dxsymbol * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
422
  | DEghost of dexpr
423
  | DEexn of preid * dity * mask * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
424
  | DEoptexn of preid * dity * mask * dexpr
425
  | DEassert of assertion_kind * term later
426
  | DEpure of term later * dity
427
  | DEvar_pure of string * dvty
428
  | DEls_pure of lsymbol * bool
429
  | DEpv_pure of pvsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
430 431 432
  | DEabsurd
  | DEtrue
  | DEfalse
433
  | DEcast of dexpr * dity
434
  | DEmark of preid * dexpr
435 436 437
  | DEuloc of dexpr * Loc.position
  | DElabel of dexpr * Slab.t

438 439 440 441
and dreg_branch = dpattern * dexpr

and dexn_branch = dxsymbol * dpattern * dexpr

442
and dlet_defn = preid * ghost * rs_kind * dexpr
443 444 445

and drec_defn = { fds : dfun_defn list }

446 447
and dfun_defn = preid * ghost * rs_kind * dbinder list *
  dity * mask * dspec later * variant list later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
448

449 450 451 452
(** Environment *)

type denv = {
  frozen : dity list;
453
  locals : (bool * Stv.t option * dvty) Mstr.t;
454
  excpts : dxsymbol Mstr.t
455 456
}

457
let denv_names d = Mstr.domain d.locals
458

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

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

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

let free_vars frozen (argl,res) =
  let rec add s = function
475 476 477 478
    | 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
479
    | Dapp (_,tl,_) -> List.fold_left add s tl in
480 481
  List.fold_left add (add Stv.empty res) argl

482 483 484 485 486
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 =
487
  let ls = Mstr.add id.pre_name (false, None, dvty) ls in
488
  { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }
489

490
let denv_add_poly { frozen = fz; locals = ls; excpts = xs } id dvty =
491
  let ls = Mstr.add id.pre_name (false, Some (free_vars fz dvty), dvty) ls in
492
  { frozen = fz; locals = ls; excpts = xs }
493

494
let denv_add_rec_mono { frozen = fz; locals = ls; excpts = xs } id dvty =
495
  let ls = Mstr.add id.pre_name (false, Some Stv.empty, dvty) ls in
496
  { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }
497

498
let denv_add_rec_poly { frozen = fz; locals = ls; excpts = xs } fz0 id dvty =
499
  let ls = Mstr.add id.pre_name (false, Some (free_vars fz0 dvty), dvty) ls in
500
  { frozen = fz; locals = ls; excpts = xs }
501

502
let denv_add_rec denv fz0 id ((argl,res) as dvty) =
503
  let rec is_explicit = function
504 505 506
    | 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
507
    | Dutv _ -> true
508
    | Dapp (_,tl,_) -> List.for_all is_explicit tl in
509
  if List.for_all is_explicit argl && is_explicit res
510
  then denv_add_rec_poly denv fz0 id dvty
511 512 513 514
  else denv_add_rec_mono denv id dvty

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

515 516 517 518 519 520
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
521
let denv_add_let denv (id,_,_,({de_dvty = dvty} as de)) =
522 523 524
  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
525
    | DEvar _ | DEsym _ | DEls_pure _ | DEfun _ | DEany _ -> true
526 527 528 529 530
    | _ -> false in
  if is_value de
  then denv_add_poly denv id dvty
  else denv_add_mono denv id dvty

531 532
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
533
  let add s (id,_,t) = match id with
534
    | Some {pre_name = n} ->
535
        Mstr.add_new (Dterm.DuplicateVar n) n (false, None, ([],t)) s
536 537
    | None -> s in
  let s = List.fold_left add Mstr.empty bl in
538
  { frozen = l; locals = Mstr.set_union s ls; excpts = xs }
539

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

let mk_node n = function
546 547
  | _, Some tvs, dvty -> DEvar (n, specialize_scheme tvs dvty)
  | _, None,     dvty -> DEvar (n, dvty)
548 549 550 551 552 553 554

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)

555 556 557 558 559 560 561 562 563 564
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)

565 566 567 568 569 570
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

571 572 573 574 575 576 577 578 579 580 581
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
582 583 584 585
  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
586 587 588 589 590 591 592 593
  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)

594 595 596 597 598 599 600 601 602 603 604
(** 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
605 606
let dexpr_expected_type {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
607 608 609 610
  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
611 612
let dexpr_expected_type_weak {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
613 614 615 616 617 618
  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 *)

619
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
620
  dity * mask * (denv -> dspec later * variant list later * dexpr)
621 622 623 624

exception DupId of preid

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

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

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

(** Final stage *)

(** Binders *)

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

846 847 848 849
let create_assert = to_fmla

let create_invariant pl = List.map to_fmla pl

850 851
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
852

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

(** User effects *)

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