dexpr.ml 61.3 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 417
  | DEif of dexpr * dexpr * dexpr
  | DEcase of dexpr * (dpattern * dexpr) 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
  | DEtry of dexpr * bool * (dxsymbol * dpattern * dexpr) list
422
  | DEraise of dxsymbol * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
423
  | DEghost of dexpr
424
  | DEexn of preid * dity * mask * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
425
  | DEoptexn of preid * dity * mask * dexpr
426
  | DEassert of assertion_kind * term later
427
  | DEpure of term later * dity
428
  | DEvar_pure of string * dvty
429
  | DEls_pure of lsymbol * bool
430
  | DEpv_pure of pvsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
431 432 433
  | DEabsurd
  | DEtrue
  | DEfalse
434
  | DEcast of dexpr * dity
435
  | DEmark of preid * dexpr
436 437 438
  | DEuloc of dexpr * Loc.position
  | DElabel of dexpr * Slab.t

439
and dlet_defn = preid * ghost * rs_kind * dexpr
440 441 442

and drec_defn = { fds : dfun_defn list }

443 444
and dfun_defn = preid * ghost * rs_kind * dbinder list *
  dity * mask * dspec later * variant list later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
445

446 447 448 449
(** Environment *)

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

454
let denv_names d = Mstr.domain d.locals
455

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

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

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

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

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

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

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

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

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

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

512 513 514 515 516 517
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
518
let denv_add_let denv (id,_,_,({de_dvty = dvty} as de)) =
519 520 521
  if fst dvty = [] then denv_add_mono denv id dvty else
  let rec is_value de = match de.de_node with
    | DEghost de | DEuloc (de,_) | DElabel (de,_) -> is_value de
522
    | DEvar _ | DEsym _ | DEls_pure _ | DEfun _ | DEany _ -> true
523 524 525 526 527
    | _ -> false in
  if is_value de
  then denv_add_poly denv id dvty
  else denv_add_mono denv id dvty

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

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

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

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

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

552 553 554 555 556 557 558 559 560 561
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)

562 563 564 565 566 567
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

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

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

616
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
617
  dity * mask * (denv -> dspec later * variant list later * dexpr)
618 619 620 621

exception DupId of preid

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

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

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