dexpr.ml 65.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
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

type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
Andrei Paskevich's avatar
Andrei Paskevich committed
38
type dref = bool list * bool
39

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

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

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

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

let rec ity_of_dity = function
73 74 75 76 77 78 79 80
  | 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) []
81
        | Ityvar v -> ity_var v in
82 83 84 85
      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
86
        | Ityvar v -> Dutv v in
87 88 89 90 91 92
      let t = refresh (ity_of_dity d) in
      r := Dval (dity t); t
  | Dvar ({contents = Dreg (Dapp (s,tl,rl) as d,_)} as r) ->
      let reg = create_region (id_fresh "rho") s
        (List.map ity_of_dity tl) (List.map ity_of_dity rl) in
      r := Dval (Durg (d, reg)); ity_reg reg
93 94 95 96
  | Dvar r ->
      let v = create_tvsymbol (id_fresh "xi") in
      r := Dval (Dutv v); ity_var v
  | Dapp (s,tl,rl) ->
97
      ity_app_pure s (List.map ity_of_dity tl) (List.map ity_of_dity rl)
98 99 100 101

(** Destructive type unification *)

let rec occur_check v = function
102 103 104 105 106 107 108 109 110 111 112 113 114 115
  | Dvar {contents = (Dval d|Dpur d)} | Durg (d,_) ->
      occur_check v d
  | Dvar {contents = (Dsim (d,u)|Dreg (d,u))} ->
      if tv_equal u v then raise Exit else occur_check v d
  | Dvar {contents = Dtvs u} | Dutv u ->
      if tv_equal u v then raise Exit
  | Dapp (_,dl,_) ->
      List.iter (occur_check v) dl

let rec dity_unify_weak d1 d2 = match d1,d2 with
  | Dvar {contents = (Dval d1|Dpur d1|Dsim (d1,_)|Dreg (d1,_))}, d2
  | d1, Dvar {contents = (Dval d2|Dpur d2|Dsim (d2,_)|Dreg (d2,_))}
  | Durg (d1,_), d2 | d1, Durg (d2,_) ->
      dity_unify_weak d1 d2
116 117 118 119 120 121
  | Dvar {contents = Dtvs u},
    Dvar {contents = Dtvs v} when tv_equal u v ->
      ()
  | Dvar ({contents = Dtvs v} as r), d
  | d, Dvar ({contents = Dtvs v} as r) ->
      occur_check v d;
122
      r := Dsim (d,v)
123 124
  | Dutv u, Dutv v when tv_equal u v ->
      ()
125
  | Dapp (s1,dl1,_), Dapp (s2,dl2,_) when its_equal s1 s2 ->
126
      List.iter2 dity_unify_weak dl1 dl2
127 128
  | _ -> raise Exit

129 130 131 132 133
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
134
    | Ityvar v -> Mtv.find v mv
135 136 137 138 139 140 141
    | 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)

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

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

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

(** Built-in types *)

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

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

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

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

(* Specialization of symbols *)

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

let spec_ity hv hr frz ity =
  let rec dity ity = match ity.ity_node with
317 318 319 320 321
    | 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)
322 323 324 325
    | 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)
326
    | Ityapp (s,tl,rl) -> app_map dity s tl rl in
327 328
  dity ity

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

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

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

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

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

351 352 353
(** Patterns *)

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

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

(** Specifications *)

type ghost = bool

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

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

376
type 'a later = pvsymbol Mstr.t -> xsymbol Mstr.t -> register_old -> 'a
377 378 379 380 381 382
  (* 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;
383
  ds_post    : (pvsymbol * term) list;
384
  ds_xpost   : (pvsymbol * term) list Mxs.t;
385
  ds_reads   : pvsymbol list;
386 387
  ds_writes  : term list;
  ds_diverge : bool;
388
  ds_partial : bool;
389
  ds_checkrw : bool;
390 391
}

392
type dspec = ity -> dspec_final
393 394 395 396 397
  (* 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
398
let old_label = "'Old"
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 =
Andrei Paskevich's avatar
Andrei Paskevich committed
411
  | DEvar of string * dvty * dref
412
  | DEsym of prog_symbol
413
  | DEconst of Number.constant * dity
414
  | DEapp of dexpr * dexpr
415 416
  | DEfun of dbinder list * dity * mask * dspec later * dexpr
  | DEany of dbinder list * dity * mask * dspec later
417 418
  | DElet of dlet_defn * dexpr
  | DErec of drec_defn * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
419
  | DEnot of dexpr
420 421
  | DEand of dexpr * dexpr
  | DEor of dexpr * dexpr
422
  | DEif of dexpr * dexpr * dexpr
423
  | DEmatch of dexpr * dreg_branch list * dexn_branch list
424
  | DEassign of (dexpr * rsymbol * dexpr) list
425
  | DEwhile of dexpr * dinvariant later * variant list later * dexpr
426
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
427
  | DEraise of dxsymbol * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
428
  | DEghost of dexpr
429
  | DEexn of preid * dity * mask * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
430
  | DEoptexn of preid * dity * mask * dexpr
431
  | DEassert of assertion_kind * term later
432
  | DEpure of term later * dity
Andrei Paskevich's avatar
Andrei Paskevich committed
433
  | DEvar_pure of string * dvty * dref
434
  | DEls_pure of lsymbol * bool
435
  | DEpv_pure of pvsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
436 437 438
  | DEabsurd
  | DEtrue
  | DEfalse
Andrei Paskevich's avatar
Andrei Paskevich committed
439
  | DElabel of preid * dexpr
440
  | DEcast of dexpr * dity
441
  | DEuloc of dexpr * Loc.position
Andrei Paskevich's avatar
Andrei Paskevich committed
442
  | DEattr of dexpr * Sattr.t
443

444 445 446 447
and dreg_branch = dpattern * dexpr

and dexn_branch = dxsymbol * dpattern * dexpr

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

and drec_defn = { fds : dfun_defn list }

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

455 456 457 458 459 460
(** 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))

Andrei Paskevich's avatar
Andrei Paskevich committed
461 462 463 464 465
let dvar_expected_type {pre_loc = loc} dv_dity dity =
  try dity_unify dv_dity dity with Exit -> Loc.errorm ?loc
    "This variable has type %a,@ but is expected to have type %a"
    print_dity dv_dity print_dity dity

466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482
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

483 484 485 486
(** Environment *)

type denv = {
  frozen : dity list;
Andrei Paskevich's avatar
Andrei Paskevich committed
487
  locals : (bool * Stv.t option * dvty * dref) Mstr.t;
488
  excpts : dxsymbol Mstr.t
489 490
}

491
let denv_names d = Mstr.domain d.locals
492

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

Andrei Paskevich's avatar
Andrei Paskevich committed
495 496
let is_frozen frozen v =
  try List.iter (occur_check v) frozen; false with Exit -> true
497 498 499

let freeze_dvty frozen (argl,res) =
  let rec add l = function
500 501 502
    | Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
    | Durg (d,_) -> add l d
    | Dvar {contents = Dtvs _}
503
    | Dutv _ as d -> d :: l
504
    | Dapp (_,tl,_) -> List.fold_left add l tl in
505 506 507 508
  List.fold_left add (add frozen res) argl

let free_vars frozen (argl,res) =
  let rec add s = function
509 510 511 512
    | 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
513
    | Dapp (_,tl,_) -> List.fold_left add s tl in
514 515
  List.fold_left add (add Stv.empty res) argl

Andrei Paskevich's avatar
Andrei Paskevich committed
516
let denv_add_exn {frozen = fz; locals = ls; excpts = xs} id dity =
517 518 519
  let xs = Mstr.add id.pre_name (DElexn (id.pre_name, dity)) xs in
  { frozen = freeze_dvty fz ([], dity); locals = ls; excpts = xs }

Andrei Paskevich's avatar
Andrei Paskevich committed
520 521
let denv_add_mono {frozen = fz; locals = ls; excpts = xs} id dvty dref =
  let ls = Mstr.add id.pre_name (false, None, dvty, dref) ls in
522
  { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }
523

Andrei Paskevich's avatar
Andrei Paskevich committed
524 525 526
let denv_add_poly {frozen = fz; locals = ls; excpts = xs} id dvty dref =
  let fvs = free_vars fz dvty in
  let ls = Mstr.add id.pre_name (false, Some fvs, dvty, dref) ls in
527
  { frozen = fz; locals = ls; excpts = xs }
528

Andrei Paskevich's avatar
Andrei Paskevich committed
529 530
let denv_add_rec_mono {frozen = fz; locals = ls; excpts = xs} id dvty dref =
  let ls = Mstr.add id.pre_name (false, Some Stv.empty, dvty, dref) ls in
531
  { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }
532

Andrei Paskevich's avatar
Andrei Paskevich committed
533 534 535
let denv_add_rec_poly {frozen = fz; locals = ls; excpts = xs} fz0 id dvty dref =
  let fvs = free_vars fz0 dvty in
  let ls = Mstr.add id.pre_name (false, Some fvs, dvty, dref) ls in
536
  { frozen = fz; locals = ls; excpts = xs }
537

Andrei Paskevich's avatar
Andrei Paskevich committed
538
let denv_add_rec denv fz0 id ((argl,res) as dvty) dref =
539
  let rec is_explicit = function
540 541 542
    | 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
543
    | Dutv _ -> true
544
    | Dapp (_,tl,_) -> List.for_all is_explicit tl in
545
  if List.for_all is_explicit argl && is_explicit res
Andrei Paskevich's avatar
Andrei Paskevich committed
546 547 548 549
  then denv_add_rec_poly denv fz0 id dvty dref
  else denv_add_rec_mono denv id dvty dref

let attr_dref attrs = Sattr.mem Pmodule.ref_attr attrs
550

Andrei Paskevich's avatar
Andrei Paskevich committed
551 552 553 554 555 556 557 558 559 560 561
let bl_dref bl =
  let check = function
    | Some id,_,_ -> attr_dref id.pre_attrs
    | _ -> false in
  List.map check bl

let bl_type bl = List.map (fun (_,_,t) -> t) bl

let pv_dref pv = attr_dref pv.pv_vs.vs_name.id_attrs

let id_nref {pre_loc = loc; pre_attrs = attrs} =
562 563
  if attr_dref attrs then Loc.errorm ?loc
    "reference markers are only admitted over program variables";
Andrei Paskevich's avatar
Andrei Paskevich committed
564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592
  false

let id_dref id dity =
  if attr_dref id.pre_attrs then begin
    let dity_ref = dity_reg (Dapp (its_ref, [dity_fresh ()], [])) in
    dvar_expected_type id dity dity_ref;
    true
  end else
    false

let argl_dref ({de_dvty = argl,_} as de) =
  let rec cut dr acc = match dr, acc with
    | dr, [] -> assert (List.length dr = List.length argl); dr
    | _::dr, _::acc -> cut dr acc
    | _, _ -> List.map Util.ffalse argl in
  let rec deapp acc de = match de.de_node with
    | DEvar (_,_,(dr,_)) (* no DEvar_pure|DEls_pure *) -> cut dr acc
    | DEsym (RS rs) -> cut (List.map pv_dref rs.rs_cty.cty_args) acc
    | DEfun (bl,_,_,_,_) | DEany (bl,_,_,_) -> cut (bl_dref bl) acc
    | DEapp (de,d) -> deapp (d::acc) de
    | DEuloc (de,_) | DEattr (de,_) | DEcast (de,_)
    | DElet (_,de) | DErec (_,de) | DElabel (_,de)
    | DEexn (_,_,_,de) | DEoptexn (_,_,_,de)
    | DEghost de -> deapp acc de
    | _ -> List.map Util.ffalse argl in
  deapp [] de

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

594 595
let denv_add_for_index denv id dvty =
  let dvty = [], dity_of_dvty dvty in
Andrei Paskevich's avatar
Andrei Paskevich committed
596
  let dref = [], id_dref id (snd dvty) in
597
  let { frozen = fz; locals = ls; excpts = xs } = denv in
Andrei Paskevich's avatar
Andrei Paskevich committed
598
  let ls = Mstr.add id.pre_name (true, None, dvty, dref) ls in
599 600
  { frozen = freeze_dvty fz dvty; locals = ls; excpts = xs }

Andrei Paskevich's avatar
Andrei Paskevich committed
601 602 603 604
let denv_add_let denv (id,_,_,({de_dvty = (argl,res as dvty)} as de)) =
  let dref = if argl = [] then [], id_dref id res
                else argl_dref de, id_nref id in
  if argl = [] then denv_add_mono denv id dvty dref else
605
  let rec is_value de = match de.de_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
606
    | DEghost de | DEuloc (de,_) | DEattr (de,_) -> is_value de
607
    | DEvar _ | DEsym _ | DEls_pure _ | DEfun _ | DEany _ -> true
608
    | _ -> false in
Andrei Paskevich's avatar
Andrei Paskevich committed
609 610
  if is_value de then denv_add_poly denv id dvty dref
                 else denv_add_mono denv id dvty dref
611

Andrei Paskevich's avatar
Andrei Paskevich committed
612
let denv_add_args {frozen = fz; locals = ls; excpts = xs} bl =
613
  let l = List.fold_left (fun l (_,_,t) -> t::l) fz bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
614
  let add s (id,_,t) = match id with
Andrei Paskevich's avatar
Andrei Paskevich committed
615 616 617
    | Some ({pre_name = n} as id) ->
        let dvty = [], t and dref = [], id_dref id t in
        Mstr.add_new (Dterm.DuplicateVar n) n (false, None, dvty, dref) s
618 619
    | None -> s in
  let s = List.fold_left add Mstr.empty bl in
620
  { frozen = l; locals = Mstr.set_union s ls; excpts = xs }
621

Andrei Paskevich's avatar
Andrei Paskevich committed
622
let denv_add_pat {frozen = fz; locals = ls; excpts = xs} dp dity =
623
  dpat_expected_type dp dity;
Andrei Paskevich's avatar
Andrei Paskevich committed
624 625
  let l = Mstr.fold (fun _ (t,_) l -> t::l) dp.dp_vars fz in
  let s = Mstr.map (fun (t,d) -> false, None, ([],t), ([],d)) dp.dp_vars in
626
  { frozen = l; locals = Mstr.set_union s ls; excpts = xs }
627

628 629 630 631 632 633
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)

634
let mk_node n = function
Andrei Paskevich's avatar
Andrei Paskevich committed
635 636
  | _, Some tvs, dvty, dref -> DEvar (n, specialize_scheme tvs dvty, dref)
  | _, None,     dvty, dref -> DEvar (n, dvty, dref)
637 638 639 640 641 642 643

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)

644
let mk_node_pure n = function
Andrei Paskevich's avatar
Andrei Paskevich committed
645 646
  | _, Some tvs, dvty, dref -> DEvar_pure (n, specialize_scheme tvs dvty, dref)
  | _, None,     dvty, dref -> DEvar_pure (n, dvty, dref)
647 648 649 650 651 652 653

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)

654 655 656 657 658 659
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

660 661 662 663 664 665 666 667 668 669 670
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
Andrei Paskevich's avatar
Andrei Paskevich committed
671
  let add n (idx, _, dvty, dref) =
672
    let dity = if idx then dity_int else dity_of_dvty dvty in
Andrei Paskevich's avatar
Andrei Paskevich committed
673 674 675 676 677
    let dt = Dterm.DTvar (n, fold dity) in
    if dref = ([], true) then
      let dt = Dterm.dterm Coercion.empty dt in
      Dterm.DTapp (ls_ref_proj, [dt])
    else dt in
678
  let dty = get_dty (Mstr.mapi add denv.locals) in
679 680 681 682 683 684 685 686
  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)

687 688
(** Generation of letrec blocks *)

689
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
690
  dity * mask * (denv -> dspec later * variant list later * dexpr)
691 692 693

exception DupId of preid

Andrei Paskevich's avatar
Andrei Paskevich committed
694
let drec_defn ({frozen = frz} as denv0) prel =
Andrei Paskevich's avatar
Andrei Paskevich committed
695
  if prel = [] then invalid_arg "Dexpr.drec_defn: empty function list";
696
  let add s (id,_,_,_,_,_,_) = Sstr.add_new (DupId id) id.pre_name s in
697 698
  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
699
  let add denv (id,_,_,bl,res,_,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
700
    if bl = [] then invalid_arg "Dexpr.drec_defn: empty argument list";
Andrei Paskevich's avatar
Andrei Paskevich committed
701
    denv_add_rec denv frz id (bl_type bl, res) (bl_dref bl, id_nref id) in
702
  let denv1 = List.fold_left add denv0 prel in
703
  let parse (id,gh,pk,bl,res,msk,pre) =
704
    let dsp, dvl, de = pre denv1 in
705
    dexpr_expected_type de res;
706
    (id,gh,pk,bl,res,msk,dsp,dvl,de) in
707
  let fdl = List.map parse prel in
708
  let add denv (id,_,_,bl,res,_,_,_,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
709 710
    (* in case we linked some polymorphic type var to the outer context *)
    let check tv = if is_frozen frz tv then Loc.errorm ?loc:id.pre_loc
711 712 713
      "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
Andrei Paskevich's avatar
Andrei Paskevich committed
714 715 716
    | Some (_, Some tvs, _, _) -> Stv.iter check tvs
    | Some (_, None, _, _) | None -> assert false end;
    denv_add_poly denv id (bl_type bl, res) (bl_dref bl, false) in
717 718 719 720 721 722 723 724 725 726
  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
727
    | DPvar (id,gh) ->
728
        let dity = dity_fresh () in
Andrei Paskevich's avatar
Andrei Paskevich committed
729 730
        let vars = Mstr.singleton id.pre_name (dity, id_dref id dity) in
        mk_dpat (PPvar (id,gh)) dity vars
731 732
    | DPapp ({rs_logic = RLls ls} as rs, dpl) when ls.ls_constr > 0 ->
        let argl, res = specialize_rs rs in
733 734 735 736 737
        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
738 739 740
        mk_dpat (PPapp (rs, ppl)) res vars
    | DPapp (rs,_) ->
        raise (ConstructorExpected rs);
741 742
    | DPor (dp1,dp2) ->
        dpat_expected_type dp2 dp1.dp_dity;
Andrei Paskevich's avatar
Andrei Paskevich committed
743 744 745 746
        let join n (dity1,dref1) (dity2,dref2) =
          if dref1 <> dref2 then Loc.errorm ?loc
            "Variable %s is used with different ref statuses" n;
          try dity_unify dity1 dity2; Some (dity1,dref1)
747 748 749 750 751
          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
752
    | DPas (dp, ({pre_name = n} as id), gh) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
753
        let exn = Dterm.DuplicateVar n in
754
        let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in
Andrei Paskevich's avatar
Andrei Paskevich committed
755
        let vars = Mstr.add_new exn n (dity, id_dref id dity) vars in
756
        mk_dpat (PPas (pat, id, gh)) dity vars
757 758
    | DPcast (dp, dity) ->
        dpat_expected_type dp dity;
759 760 761 762
        dp
  in
  Loc.try1 ?loc dpat node

Andrei Paskevich's avatar
Andrei Paskevich committed
763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778
let to_deref = function
  | DEvar (_,_,([],deref))
  | DEvar_pure (_,_,([],deref)) -> deref
  | DEsym (PV pv)
  | DEpv_pure pv -> pv_dref pv
  | _ -> false

let rec undereference de = match de.de_node with
  | DEuloc (de,l) -> { de with de_node = DEuloc (undereference de, l) }
  | DEattr (de,a) -> { de with de_node = DEattr (undereference de, a) }
  | DEcast (de,_) -> undereference de (* already unified *)
  | DEapp ({de_node = DEsym (RS rs)}, de)
    when rs_equal rs rs_ref_proj
      && to_deref de.de_node -> de
  | _ -> raise Not_found

779 780
let dexpr ?loc node =
  let get_dvty = function
Andrei Paskevich's avatar
Andrei Paskevich committed
781
    | DEvar (_,dvty,_) ->
782
        dvty
Andrei Paskevich's avatar
Andrei Paskevich committed
783
    | DEvar_pure (_,dvty,_) ->
784 785 786
        let dt = dity_fresh () in
        dity_unify_asym dt (dity_of_dvty dvty);
        [], dt
787
    | DEsym (PV pv) ->
788
        [], specialize_single pv.pv_ity
789
    | DEsym (RS rs) ->
790
        specialize_rs rs
791 792
    | DEsym (OO ss) ->
        let dt = dity_fresh () in
793 794 795 796 797 798 799
        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
800
    | DEls_pure (ls,_) ->
801
        specialize_ls ls
802 803
    | DEpv_pure pv ->
        [], specialize_single (ity_purify pv.pv_ity)
804
    | DEconst (_, ity) -> [],ity
805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823
    | 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
824 825
    | DEfun (bl,res,_,_,de) ->
        dexpr_expected_type de res;
Andrei Paskevich's avatar
Andrei Paskevich committed
826
        bl_type bl, res
827
    | DEany (bl,res,_,_) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
828
        bl_type bl, res
829 830
    | DElet (_,de)
    | DErec (_,de) ->
831
        de.de_dvty
832 833
    | DEnot de ->
        dexpr_expected_type de dity_bool;
834 835 836
        dvty_bool
    | DEand (de1,de2)
    | DEor (de1,de2) ->
837 838
        dexpr_expected_type de1 dity_bool;
        dexpr_expected_type de2 dity_bool;
839
        dvty_bool
840 841 842 843 844
    | 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;
845
        [], res
846 847 848
    | DEmatch (_,[],[]) ->
        invalid_arg "Dexpr.dexpr: empty branch list in DEmatch"
    | DEmatch (de,bl,xl) ->
849
        let res = dity_fresh () in
850 851 852
        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;
853
        [], res
854
    | DEassign al ->
855 856 857
        List.iter (fun (de1,rs,de2) ->
          let argl, res = specialize_rs rs in
          let ls = match rs.rs_logic with RLls ls -> ls
858 859 860
            | _ -> invalid_arg "Dexpr.dexpr: not a field" in
          dity_unify_app ls dexpr_expected_type [de1] argl;
          dexpr_expected_type_weak de2 res) al;
861 862
        dvty_unit
    | DEwhile (de1,_,_,de2) ->
863
        dexpr_expected_type de1 dity_bool;
864
        dexpr_expected_type de2 dity_unit;
865
        dvty_unit
866
    | DEfor (_,de_from,_,de_to,_,de) ->
867 868 869
        let bty = dity_fresh () in
        dexpr_expected_type de_from bty;
        dexpr_expected_type de_to bty;
870
        dexpr_expected_type de dity_unit;
871
        dvty_unit
872
    | DEraise (xs,de) ->
873
        dexpr_expected_type de (specialize_dxs xs);
874
        [], dity_fresh ()
875
    | DEexn (_,_,_,de)