mlw_dexpr.ml 53.2 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

open Stdlib
open Ident
open Ty
open Term
open Mlw_ty
open Mlw_ty.T
open Mlw_expr

(** Program types *)

22 23 24 25 26
type dity =
  | Dvar of dvar ref
  | Dutv of tvsymbol
  | Dapp of itysymbol * dity list * dreg list
  | Dpur of tysymbol  * dity list
27

28 29 30
and dvar =
  | Dtvs of tvsymbol
  | Dval of dity
31

32 33 34 35 36 37 38 39
and dreg =
  | Rreg of region * dity
  | Rvar of rvar ref

and rvar =
  | Rtvs of tvsymbol * dity
  | Rval of dreg

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

42 43 44 45
let create_dreg dity =
  Rvar (ref (Rtvs (create_tvsymbol (id_fresh "rho"), dity)))

let dity_of_ity ity =
46 47
  let hreg = Hreg.create 3 in
  let rec dity ity = match ity.ity_node with
48
    | Ityvar tv -> Dutv tv
49 50 51 52 53 54 55
    | Ityapp (s,tl,rl) -> Dapp (s, List.map dity tl, List.map dreg rl)
    | Itypur (s,tl)    -> Dpur (s, List.map dity tl)
  and dreg reg =
    try Hreg.find hreg reg with Not_found ->
    let r = create_dreg (dity reg.reg_ity) in
    Hreg.add hreg reg r;
    r
56
  in
57
  dity ity
58

59
let ity_of_dity dity =
60 61 62
  let rec ity = function
    | Dvar { contents = Dval t } -> ity t
    | Dvar ref ->
63
        let tv = create_tvsymbol (id_fresh "xi") in
64
        ref := Dval (Dutv tv);
65
        ity_var tv
66 67 68 69 70 71 72 73 74 75
    | Dutv tv -> ity_var tv
    | Dapp (s,tl,rl) -> ity_app s (List.map ity tl) (List.map reg rl)
    | Dpur (s,tl)    -> ity_pur s (List.map ity tl)
  and reg = function
    | Rreg (r,_) -> r
    | Rvar { contents = Rval r } -> reg r
    | Rvar ({ contents = Rtvs (tv,t) } as ref) ->
        let r = create_region (id_clone tv.tv_name) (ity t) in
        ref := Rval (Rreg (r,t));
        r
76
  in
77
  ity dity
78

79 80 81 82 83
let dity_int  = Dpur (ts_int,  [])
let dity_real = Dpur (ts_real, [])
let dity_bool = Dpur (ts_bool, [])
let dity_unit = Dpur (ts_unit, [])

84 85 86 87 88
let dvty_int  = [], dity_int
let dvty_real = [], dity_real
let dvty_bool = [], dity_bool
let dvty_unit = [], dity_unit

89 90 91 92 93 94 95 96
(** Destructive type unification *)

let rec occur_check tv = function
  | Dvar { contents = Dval d } -> occur_check tv d
  | Dapp (_,dl,_) | Dpur (_,dl) -> List.iter (occur_check tv) dl
  | Dvar { contents = Dtvs tv' } | Dutv tv' ->
      if tv_equal tv tv' then raise Exit

97
let rec dity_unify d1 d2 = match d1,d2 with
98 99
  | Dvar { contents = Dval d1 }, d2
  | d1, Dvar { contents = Dval d2 } ->
100
      dity_unify d1 d2
101 102 103 104 105 106 107 108 109
  | Dvar { contents = Dtvs tv1 },
    Dvar { contents = Dtvs tv2 } when tv_equal tv1 tv2 ->
      ()
  | Dvar ({ contents = Dtvs tv } as r), d
  | d, Dvar ({ contents = Dtvs tv } as r) ->
      occur_check tv d;
      r := Dval d
  | Dutv tv1, Dutv tv2 when tv_equal tv1 tv2 ->
      ()
110
  | Dapp (s1,dl1,_), Dapp (s2,dl2,_) when its_equal s1 s2 ->
111
      List.iter2 dity_unify dl1 dl2
112
  | Dpur (s1,dl1), Dpur (s2,dl2) when ts_equal s1 s2 ->
113
      List.iter2 dity_unify dl1 dl2
114 115 116 117 118 119 120 121 122 123 124 125 126 127
  | _ -> raise Exit

(** Reunify regions *)

let dtvs_queue : dvar ref Queue.t = Queue.create ()

let unify_queue : (dity * dity) Queue.t = Queue.create ()

let dity_fresh () =
  let r = ref (Dtvs (create_tvsymbol (id_fresh "a"))) in
  Queue.add r dtvs_queue;
  Dvar r

let its_app_fresh s dl =
128 129
  let htv = Htv.create 3 in
  let hreg = Hreg.create 3 in
130 131 132
  let rec inst ity = match ity.ity_node with
    | Ityvar v -> Htv.find htv v
    | Ityapp (s,tl,rl) -> Dapp (s, List.map inst tl, List.map fresh rl)
133
    | Itypur (s,tl)    -> Dpur (s, List.map inst tl)
134 135 136 137 138 139 140 141 142 143 144 145 146
  and fresh r =
    try Hreg.find hreg r with Not_found ->
    let reg = create_dreg (inst r.reg_ity) in
    Hreg.add hreg r reg;
    reg in
  List.iter2 (Htv.add htv) s.its_ts.ts_args dl;
  match s.its_def with
  | None -> Dapp (s, dl, List.map fresh s.its_regs)
  | Some ity -> inst ity

let rec dity_refresh = function
  | Dvar { contents = Dval dty } -> dity_refresh dty
  | Dvar { contents = Dtvs _ } as dity -> dity
147 148
  | Dapp (s,dl,_) -> its_app_fresh s (List.map dity_refresh dl)
  | Dpur (s,dl) -> Dpur (s, List.map dity_refresh dl)
149 150
  | Dutv _ as dity -> dity

151 152 153
let dity_unify_weak = dity_unify

let dity_unify d1 d2 = dity_unify d1 d2; Queue.add (d1,d2) unify_queue
154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191

let rec reunify d1 d2 = match d1,d2 with
  | Dvar { contents = Dval d1 }, d2
  | d1, Dvar { contents = Dval d2 } -> reunify d1 d2
  | Dvar _, Dvar _ | Dutv _, Dutv _ -> ()
  | Dapp (_,dl1,rl1), Dapp (_,dl2,rl2) ->
      List.iter2 reunify dl1 dl2;
      List.iter2 unify_reg rl1 rl2
  | Dpur (_,dl1), Dpur (_,dl2) ->
      List.iter2 reunify dl1 dl2
  | _ -> assert false

and unify_reg r1 r2 = match r1,r2 with
  | Rvar { contents = Rval r1 }, r2
  | r1, Rvar { contents = Rval r2 } ->
      unify_reg r1 r2
  | Rvar { contents = Rtvs (tv1,_) },
    Rvar { contents = Rtvs (tv2,_) } when tv_equal tv1 tv2 ->
      ()
  | Rvar ({ contents = Rtvs (_,d1) } as r),
    (Rvar { contents = Rtvs (_,d2) } as d)
  | Rvar ({ contents = Rtvs (_,d1) } as r), (Rreg (_,d2) as d)
  | (Rreg (_,d1) as d), Rvar ({ contents = Rtvs (_,d2) } as r) ->
      reunify d1 d2;
      r := Rval d
  | Rreg _, Rreg _ -> ()
    (* we don't check whether the regions are the same,
       because we won't have a good location for the error.
       Let the core API raise the exception later. *)

let reunify_regions () =
  Queue.iter (fun r -> match !r with
    | Dval d -> r := Dval (dity_refresh d)
    | Dtvs _ -> ()) dtvs_queue;
  Queue.clear dtvs_queue;
  Queue.iter (fun (d1,d2) -> reunify d1 d2) unify_queue;
  Queue.clear unify_queue

192 193 194 195 196 197 198 199 200 201 202 203 204
(** Chainable relations *)

let rec dity_is_bool = function
  | Dvar { contents = Dval dty } -> dity_is_bool dty
  | Dpur (ts,_) -> ts_equal ts ts_bool
  | _ -> false

let dvty_is_chainable = function
  | [t1;t2],t ->
      dity_is_bool t && not (dity_is_bool t1) && not (dity_is_bool t2)
  | _ -> false

(** Pretty-printing *)
205 206 207 208 209 210 211 212

let debug_print_reg_types = Debug.register_info_flag "print_reg_types"
  ~desc:"Print@ types@ of@ regions@ (mutable@ fields)."

let print_dity fmt dity =
  let protect_on x s = if x then "(" ^^ s ^^ ")" else s in
  let print_rtvs fmt tv = Mlw_pretty.print_reg fmt
    (create_region (id_clone tv.tv_name) Mlw_ty.ity_unit) in
213
  let rec print_dity pri fmt = function
214 215
    | Dvar { contents = Dtvs tv }
    | Dutv tv -> Pretty.print_tv fmt tv
216 217 218 219
    | Dvar { contents = Dval dty } -> print_dity pri fmt dty
    | Dpur (s,[t1;t2]) when ts_equal s Ty.ts_func ->
        Format.fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
          (print_dity 1) t1 (print_dity 0) t2
220
    | Dpur (s,tl) when is_ts_tuple s -> Format.fprintf fmt "(%a)"
221
        (Pp.print_list Pp.comma (print_dity 0)) tl
222
    | Dpur (s,[]) -> Pretty.print_ts fmt s
223 224 225
    | Dpur (s,tl) -> Format.fprintf fmt (protect_on (pri > 1) "%a@ %a")
        Pretty.print_ts s (Pp.print_list Pp.space (print_dity 2)) tl
    | Dapp (s,[],rl) -> Format.fprintf fmt (protect_on (pri > 1) "%a@ <%a>")
226
        Mlw_pretty.print_its s (Pp.print_list Pp.comma print_dreg) rl
227
    | Dapp (s,tl,rl) -> Format.fprintf fmt (protect_on (pri > 1) "%a@ <%a>@ %a")
228
        Mlw_pretty.print_its s (Pp.print_list Pp.comma print_dreg) rl
229
          (Pp.print_list Pp.space (print_dity 2)) tl
230 231 232 233 234 235 236
  and print_dreg fmt = function
    | Rreg (r,_) when Debug.test_flag debug_print_reg_types ->
        Format.fprintf fmt "@[%a:@,%a@]" Mlw_pretty.print_reg r
          Mlw_pretty.print_ity r.reg_ity
    | Rreg (r,_) -> Mlw_pretty.print_reg fmt r
    | Rvar { contents = Rtvs (tv,dity) }
      when Debug.test_flag debug_print_reg_types ->
237
        Format.fprintf fmt "@[%a:@,%a@]" print_rtvs tv (print_dity 0) dity
238 239 240
    | Rvar { contents = Rtvs (tv,_) } -> print_rtvs fmt tv
    | Rvar { contents = Rval dreg } -> print_dreg fmt dreg
  in
241
  print_dity 0 fmt dity
242

243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258
(* Specialization of symbols *)

let specialize_scheme tvs (argl,res) =
  let htv = Htv.create 3 and hreg = Htv.create 3 in
  let rec spec_dity = function
    | Dvar { contents = Dval dity } -> spec_dity dity
    | Dvar { contents = Dtvs tv } | Dutv tv as dity -> get_tv tv dity
    | Dapp (s,dl,rl) -> Dapp (s, List.map spec_dity dl, List.map spec_reg rl)
    | Dpur (s,dl)    -> Dpur (s, List.map spec_dity dl)
  and spec_reg = function
    | Rvar { contents = Rval r } -> spec_reg r
    | Rvar { contents = Rtvs (tv,dity) } -> get_reg tv dity
    | Rreg _ as r -> r
  and get_tv tv dity = try Htv.find htv tv with Not_found ->
    let v = dity_fresh () in
    (* can't return dity, might differ in regions *)
259
    if not (Stv.mem tv tvs) then dity_unify_weak v dity;
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
    Htv.add htv tv v;
    v
  and get_reg tv dity = try Htv.find hreg tv with Not_found ->
    let r = create_dreg (spec_dity dity) in
    Htv.add hreg tv r;
    r in
  List.map spec_dity argl, spec_dity res

let spec_ity htv hreg vars ity =
  let get_tv tv =
    try Htv.find htv tv with Not_found ->
    let v = dity_fresh () in
    Htv.add htv tv v;
    v in
  let rec dity ity = match ity.ity_node with
275
    | Ityvar tv -> if Stv.mem tv vars.vars_tv then Dutv tv else get_tv tv
276 277 278 279 280 281 282 283 284 285
    | Ityapp (s,tl,rl) -> Dapp (s, List.map dity tl, List.map dreg rl)
    | Itypur (s,tl)    -> Dpur (s, List.map dity tl)
  and dreg reg = try Hreg.find hreg reg with Not_found ->
    let t = dity reg.reg_ity in
    let r = if reg_occurs reg vars then Rreg (reg,t) else create_dreg t in
    Hreg.add hreg reg r;
    r
  in
  dity ity

286 287
let specialize_pv { pv_ity = ity } =
  spec_ity (Htv.create 3) (Hreg.create 3) ity.ity_vars ity
288

289 290
let specialize_xs { xs_ity = ity } =
  spec_ity (Htv.create 3) (Hreg.create 3) ity.ity_vars ity
291

292
let specialize_ps { ps_aty = aty; ps_vars = vars } =
293 294
  let htv = Htv.create 3 and hreg = Hreg.create 3 in
  let conv pv = spec_ity htv hreg vars pv.pv_ity in
295
  let rec spec_aty a =
296 297 298
    let argl = List.map conv a.aty_args in
    let narg,res = match a.aty_result with
      | VTvalue v -> [], spec_ity htv hreg vars v
299 300 301
      | VTarrow a -> spec_aty a in
    argl @ narg, res in
  spec_aty aty
302

303
let specialize_pl pl =
304 305
  let htv = Htv.create 3 and hreg = Hreg.create 3 in
  let conv fd = spec_ity htv hreg vars_empty fd.fd_ity in
306
  List.map conv pl.pl_args, conv pl.pl_value
307 308 309 310 311 312 313 314 315 316

let dity_of_ty htv hreg vars ty =
  let rec pure ty = match ty.ty_node with
    | Tyapp (ts,tl) ->
        begin try ignore (restore_its ts); false
        with Not_found -> List.for_all pure tl end
    | Tyvar _ -> true in
  if not (pure ty) then raise Exit;
  spec_ity htv hreg vars (ity_of_ty ty)

317
let specialize_ls ls =
318 319 320 321 322
  let htv = Htv.create 3 and hreg = Hreg.create 3 in
  let conv ty = dity_of_ty htv hreg vars_empty ty in
  let ty = Opt.get_def ty_bool ls.ls_value in
  List.map conv ls.ls_args, conv ty

323 324
let specialize_ls ls =
  try specialize_ls ls with Exit ->
325 326 327
    Loc.errorm "Function symbol `%a' can only be used in specification"
      Pretty.print_ls ls

328 329 330 331 332
(** Patterns *)

type dpattern = {
  dp_pat  : pre_ppattern;
  dp_dity : dity;
333
  dp_vars : dity Mstr.t;
334 335 336 337 338 339 340 341 342 343
  dp_loc  : Loc.position option;
}

type dpattern_node =
  | DPwild
  | DPvar  of preid
  | DPlapp of lsymbol * dpattern list
  | DPpapp of plsymbol * dpattern list
  | DPor   of dpattern * dpattern
  | DPas   of dpattern * preid
344
  | DPcast of dpattern * ity
345 346 347 348 349

(** Specifications *)

type ghost = bool

350 351
type opaque = Stv.t

352
type dbinder = preid option * ghost * opaque * dity
353 354 355 356 357 358

type 'a later = vsymbol Mstr.t -> 'a
  (* specification terms are parsed and typechecked after the program
     expressions, when the types of locally bound program variables are
     already established. *)

359 360 361 362
type dspec_final = {
  ds_pre     : term list;
  ds_post    : (vsymbol option * term) list;
  ds_xpost   : (vsymbol option * term) list Mexn.t;
363 364 365
  ds_reads   : vsymbol list;
  ds_writes  : term list;
  ds_variant : variant list;
366 367
  ds_checkrw : bool;
  ds_diverge : bool;
368 369
}

370 371 372 373 374 375
type dspec = ty -> dspec_final
  (* 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. *)

376 377 378 379 380 381 382 383
type dtype_v =
  | DSpecV of dity
  | DSpecA of dbinder list * dtype_c

and dtype_c = dtype_v * dspec later

(** Expressions *)

384 385
type dinvariant = term list

386 387 388 389 390 391 392 393 394 395 396 397 398 399
type dlazy_op = DEand | DEor

type dexpr = {
  de_node : dexpr_node;
  de_dvty : dvty;
  de_loc  : Loc.position option;
}

and dexpr_node =
  | DEvar of string * dvty
  | DEgpvar of pvsymbol
  | DEgpsym of psymbol
  | DEplapp of plsymbol * dexpr list
  | DElsapp of lsymbol * dexpr list
400
  | DEapply of dexpr * dexpr
401
  | DEconst of Number.constant
402
  | DElam of dbinder list * dexpr * dspec later
403 404
  | DElet of dlet_defn * dexpr
  | DEfun of dfun_defn * dexpr
405
  | DErec of drec_defn * dexpr
406
  | DEif of dexpr * dexpr * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
407
  | DEcase of dexpr * (dpattern * dexpr) list
408 409 410 411 412 413 414
  | DEassign of plsymbol * dexpr * dexpr
  | DElazy of dlazy_op * dexpr * dexpr
  | DEnot of dexpr
  | DEtrue
  | DEfalse
  | DEraise of xsymbol * dexpr
  | DEtry of dexpr * (xsymbol * dpattern * dexpr) list
415
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
416
  | DEwhile of dexpr * (variant list * dinvariant) later * dexpr
417
  | DEloop of (variant list * dinvariant) later * dexpr
418 419 420 421 422
  | DEabsurd
  | DEassert of assertion_kind * term later
  | DEabstract of dexpr * dspec later
  | DEmark of preid * dexpr
  | DEghost of dexpr
423
  | DEany of dtype_v * dspec later option
424 425 426 427 428 429
  | DEcast of dexpr * ity
  | DEuloc of dexpr * Loc.position
  | DElabel of dexpr * Slab.t

and dlet_defn = preid * ghost * dexpr

430
and dfun_defn = preid * ghost * dbinder list * dexpr * dspec later
431

432 433
and drec_defn = { fds : dfun_defn list }

434 435
type dval_decl = preid * ghost * dtype_v

436 437 438 439 440 441 442 443 444
(** Environment *)

type denv = {
  frozen : dity list;
  locals : (Stv.t option * dvty) Mstr.t;
}

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

445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464
let is_frozen frozen tv =
  try List.iter (occur_check tv) frozen; false with Exit -> true

let freeze_dvty frozen (argl,res) =
  let rec add l = function
    | Dvar { contents = Dval d } -> add l d
    | Dvar { contents = Dtvs _ } as d -> d :: l
    | Dutv _ as d -> d :: l
    | Dapp (_,tl,_) | Dpur (_,tl) -> List.fold_left add l tl in
  List.fold_left add (add frozen res) argl

let free_vars frozen (argl,res) =
  let rec add s = function
    | Dvar { contents = Dval d } -> add s d
    | Dvar { contents = Dtvs tv }
    | Dutv tv -> if is_frozen frozen tv then s else Stv.add tv s
    | Dapp (_,tl,_) | Dpur (_,tl) -> List.fold_left add s tl in
  List.fold_left add (add Stv.empty res) argl

let denv_add_mono { frozen = frozen; locals = locals } id dvty =
465
  let locals = Mstr.add id.pre_name (None, dvty) locals in
466 467 468 469
  { frozen = freeze_dvty frozen dvty; locals = locals }

let denv_add_poly { frozen = frozen; locals = locals } id dvty =
  let ftvs = free_vars frozen dvty in
470
  let locals = Mstr.add id.pre_name (Some ftvs, dvty) locals in
471 472
  { frozen = frozen; locals = locals }

473 474 475 476 477 478
let denv_add_rec_mono { frozen = frozen; locals = locals } id dvty =
  let locals = Mstr.add id.pre_name (Some Stv.empty, dvty) locals in
  { frozen = freeze_dvty frozen dvty; locals = locals }

let denv_add_rec_poly { frozen = frozen; locals = locals } frozen0 id dvty =
  let ftvs = free_vars frozen0 dvty in
479
  let locals = Mstr.add id.pre_name (Some ftvs, dvty) locals in
480 481 482 483 484 485 486 487 488 489 490
  { frozen = frozen; locals = locals }

let denv_add_rec denv frozen0 id ((argl,res) as dvty) =
  let rec is_explicit = function
    | Dapp (_,tl,_) | Dpur (_,tl) -> List.for_all is_explicit tl
    | Dvar { contents = Dval d } -> is_explicit d
    | Dvar { contents = Dtvs _ } -> false
    | Dutv _ -> true in
  if List.for_all is_explicit argl && is_explicit res
  then denv_add_rec_poly denv frozen0 id dvty
  else denv_add_rec_mono denv id dvty
491

492
let dvty_of_dtype_v dtv =
493
  let rec dvty argl = function
Andrei Paskevich's avatar
Andrei Paskevich committed
494 495
    | DSpecA (bl,(DSpecV res,_)) ->
        List.rev_append argl (List.map (fun (_,_,_,t) -> t) bl), res
496 497
    | DSpecA (bl,(dtv,_)) ->
        dvty (List.fold_left (fun l (_,_,_,t) -> t::l) argl bl) dtv
Andrei Paskevich's avatar
Andrei Paskevich committed
498
    | DSpecV res -> List.rev argl, res in
499 500
  dvty [] dtv

Andrei Paskevich's avatar
Andrei Paskevich committed
501 502
let denv_add_var denv id dity = denv_add_mono denv id ([], dity)

503 504 505 506 507 508 509 510 511
let denv_add_let denv (id,_,({de_dvty = dvty} as de)) =
  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
    | DEvar _ | DEgpsym _ | DElam _ | DEany (_,None) -> true
    | _ -> false in
  if is_value de
  then denv_add_poly denv id dvty
  else denv_add_mono denv id dvty
512 513

let denv_add_fun denv (id,_,bl,{de_dvty = (argl,res)},_) =
514
  if bl = [] then invalid_arg "Mlw_dexpr.denv_add_fun: empty argument list";
515 516 517 518 519 520
  let argl = List.fold_right (fun (_,_,_,t) l -> t::l) bl argl in
  denv_add_poly denv id (argl, res)

let denv_add_args { frozen = frozen; locals = locals } bl =
  let l = List.fold_left (fun l (_,_,_,t) -> t::l) frozen bl in
  let add s (id,_,_,t) = match id with
521
    | Some {pre_name = n} ->
522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540
        Mstr.add_new (Dterm.DuplicateVar n) n (None, ([],t)) s
    | None -> s in
  let s = List.fold_left add Mstr.empty bl in
  { frozen = l; locals = Mstr.set_union s locals }

let denv_add_pat { frozen = frozen; locals = locals } dp =
  let l = Mstr.fold (fun _ t l -> t::l) dp.dp_vars frozen in
  let s = Mstr.map (fun t -> None, ([], t)) dp.dp_vars in
  { frozen = l; locals = Mstr.set_union s locals }

let mk_node n = function
  | Some tvs, dvty -> DEvar (n, specialize_scheme tvs dvty)
  | None,     dvty -> DEvar (n, dvty)

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

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

542 543
(** Unification tools *)

544
let dity_unify_app ls fn (l1: 'a list) (l2: dity list) =
545
  try List.iter2 fn l1 l2 with Invalid_argument _ ->
546
    raise (BadArity (ls, List.length l1))
547 548 549 550 551

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
552

553 554 555 556 557
let dpat_expected_type_weak {dp_dity = dp_dity; dp_loc = loc} dity =
  try dity_unify_weak 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

558 559 560 561 562
let dexpr_expected_type {de_dvty = (al,res); de_loc = loc} dity =
  if al <> [] then Loc.errorm ?loc "This expression is not a first-order value";
  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
563

564 565 566 567 568 569
let dexpr_expected_type_weak {de_dvty = (al,res); de_loc = loc} dity =
  if al <> [] then Loc.errorm ?loc "This expression is not a first-order value";
  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

570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602
(** Generation of letrec blocks *)

type pre_fun_defn =
  preid * ghost * dbinder list * dity * (denv -> dexpr * dspec later)

exception DupId of preid

let drec_defn denv0 prel =
  if prel = [] then invalid_arg "Mlw_dexpr.drec_defn: empty function list";
  let add s (id,_,_,_,_) = Sstr.add_new (DupId id) id.pre_name s in
  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
  let add denv (id,_,bl,res,_) =
    if bl = [] then invalid_arg "Mlw_dexpr.drec_defn: empty argument list";
    let argl = List.map (fun (_,_,_,t) -> t) bl in
    denv_add_rec denv denv0.frozen id (argl,res) in
  let denv1 = List.fold_left add denv0 prel in
  let parse (id,gh,bl,res,pre) =
    let de, dsp = pre (denv_add_args denv1 bl) in
    dexpr_expected_type_weak de res;
    (id,gh,bl,de,dsp) in
  let fdl = List.map parse prel in
  let add denv ((id,_,_,_,_) as fd) =
    let check tv = if is_frozen denv0.frozen tv then Loc.errorm ?loc:id.pre_loc
      "This function is expected to be polymorphic in type variable %a"
      Pretty.print_tv tv in
    begin match Mstr.find_opt id.pre_name denv1.locals with
    | Some (Some tvs, _) -> Stv.iter check tvs
    | Some (None, _) | None -> assert false
    end;
    denv_add_fun denv fd in
  List.fold_left add denv0 fdl, { fds = fdl }

603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643
(** 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
    | DPvar id ->
        let dity = dity_fresh () in
        mk_dpat (PPvar id) dity (Mstr.singleton id.pre_name dity)
    | DPlapp (ls,dpl) ->
        if ls.ls_constr = 0 then raise (ConstructorExpected ls);
        let argl, res = specialize_ls ls in
        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
        mk_dpat (PPlapp (ls, ppl)) res vars
    | DPpapp ({pl_ls = ls} as pl, dpl) ->
        if ls.ls_constr = 0 then raise (ConstructorExpected ls);
        let argl, res = specialize_pl pl in
        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
        mk_dpat (PPpapp (pl, ppl)) res vars
    | 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
    | DPas (dp, ({pre_name = n} as id)) ->
        let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in
        let vars = Mstr.add_new (Dterm.DuplicateVar n) n dity vars in
        mk_dpat (PPas (pat, id)) dity vars
644 645 646
    | DPcast (dp, ity) ->
        dpat_expected_type_weak dp (dity_of_ity ity);
        dp
647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665
  in
  Loc.try1 ?loc dpat node

let dexpr ?loc node =
  let get_dvty = function
    | DEvar (_,dvty) ->
        dvty
    | DEgpvar pv ->
        [], specialize_pv pv
    | DEgpsym ps ->
        specialize_ps ps
    | DEplapp (pl,del) ->
        let argl, res = specialize_pl pl in
        dity_unify_app pl.pl_ls dexpr_expected_type del argl;
        [], res
    | DElsapp (ls,del) ->
        let argl, res = specialize_ls ls in
        dity_unify_app ls dexpr_expected_type del argl;
        [], res
666 667 668
    | DEapply ({de_dvty = (dity::argl, res)}, de2) ->
        dexpr_expected_type de2 dity;
        argl, res
669 670 671 672 673 674 675
    | DEapply ({de_dvty = ([],res)} as de1, de2) ->
        let rec not_arrow = function
          | Dvar {contents = Dval dity} -> not_arrow dity
          | Dpur (ts,_) -> not (ts_equal ts Ty.ts_func)
          | Dvar _ -> false | _ -> true in
        if not_arrow res then Loc.errorm ?loc:de1.de_loc
          "This expression has type %a,@ it cannot be applied" print_dity res;
676 677 678
        let argl, res = specialize_ls fs_func_app in
        dity_unify_app fs_func_app dexpr_expected_type [de1;de2] argl;
        [], res
679
    | DEconst (Number.ConstInt _) ->
680
        dvty_int
681
    | DEconst (Number.ConstReal _) ->
682
        dvty_real
683 684
    | DEfun ((_,_,[],_,_),_) ->
        invalid_arg "Mlw_dexpr.dexpr: empty argument list in DEfun"
685 686 687 688
    | DElet (_,de)
    | DEfun (_,de)
    | DErec (_,de) ->
        de.de_dvty
689 690 691 692
    | DElam ([],_,_) ->
        invalid_arg "Mlw_dexpr.dexpr: empty argument list in DElam"
    | DElam (bl,{de_dvty = (argl,res)},_) ->
        List.fold_right (fun (_,_,_,t) l -> t::l) bl argl, res
693 694 695 696 697 698
    | 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;
        de2.de_dvty
699 700
    | DEcase (_,[]) ->
        invalid_arg "Mlw_dexpr.dexpr: empty branch list in DEcase"
Andrei Paskevich's avatar
Andrei Paskevich committed
701
    | DEcase (de,bl) ->
702 703 704 705 706 707 708 709
        let ety = dity_fresh () in
        let res = dity_fresh () in
        dexpr_expected_type de ety;
        let branch (dp,de) =
          dpat_expected_type dp ety;
          dexpr_expected_type de res in
        List.iter branch bl;
        [], res
Andrei Paskevich's avatar
Andrei Paskevich committed
710
    | DEassign (pl,de1,de2) ->
711 712
        let argl, res = specialize_pl pl in
        dity_unify_app pl.pl_ls dexpr_expected_type [de1] argl;
Andrei Paskevich's avatar
Andrei Paskevich committed
713
        dexpr_expected_type_weak de2 res;
714
        dvty_unit
715 716 717 718 719 720 721 722 723
    | DElazy (_,de1,de2) ->
        dexpr_expected_type de1 dity_bool;
        dexpr_expected_type de2 dity_bool;
        de1.de_dvty
    | DEnot de ->
        dexpr_expected_type de dity_bool;
        de.de_dvty
    | DEtrue
    | DEfalse ->
724
        dvty_bool
725 726 727
    | DEraise (xs,de) ->
        dexpr_expected_type de (specialize_xs xs);
        [], dity_fresh ()
728 729
    | DEtry (_,[]) ->
        invalid_arg "Mlw_dexpr.dexpr: empty branch list in DEtry"
730 731 732 733 734 735 736 737 738 739 740 741 742 743
    | DEtry (de,bl) ->
        let res = dity_fresh () in
        dexpr_expected_type de res;
        let branch (xs,dp,de) =
          let ety = specialize_xs xs in
          dpat_expected_type dp ety;
          dexpr_expected_type de res in
        List.iter branch bl;
        de.de_dvty
    | DEfor (_,de_from,_,de_to,_,de) ->
        dexpr_expected_type de_from dity_int;
        dexpr_expected_type de_to dity_int;
        dexpr_expected_type de dity_unit;
        de.de_dvty
744 745 746 747
    | DEwhile (de1,_,de2) ->
        dexpr_expected_type de1 dity_bool;
        dexpr_expected_type de2 dity_unit;
        de2.de_dvty
748
    | DEloop (_,de) ->
749 750 751 752 753
        dexpr_expected_type de dity_unit;
        de.de_dvty
    | DEabsurd ->
        [], dity_fresh ()
    | DEassert _ ->
754
        dvty_unit
755 756 757 758 759 760 761 762 763 764 765 766 767 768
    | DEabstract (de,_)
    | DEmark (_,de)
    | DEghost de ->
        de.de_dvty
    | DEany (dtv,_) ->
        dvty_of_dtype_v dtv
    | DEcast (de,ity) ->
        dexpr_expected_type_weak de (dity_of_ity ity);
        de.de_dvty
    | DEuloc (de,_)
    | DElabel (de,_) ->
        de.de_dvty in
  let dvty = Loc.try1 ?loc get_dvty node in
  { de_node = node; de_dvty = dvty; de_loc = loc }
769

770 771 772 773 774 775 776
let mk_dexpr loc d n = { de_node = n; de_dvty = d; de_loc = loc }

let de_void loc = mk_dexpr loc dvty_unit (DElsapp (fs_void, []))

let pat_void loc = { dp_pat = PPlapp (fs_void, []);
  dp_dity = dity_unit; dp_vars = Mstr.empty; dp_loc = loc }

777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796
(** Final stage *)

(** Binders *)

let binders bl =
  let sn = ref Sstr.empty in
  let binder (id, ghost, _, dity) =
    let id = match id with
      | Some ({pre_name = n} as id) ->
          let exn = match id.pre_loc with
            | Some loc -> Loc.Located (loc, Dterm.DuplicateVar n)
            | None -> Dterm.DuplicateVar n in
          sn := Sstr.add_new exn n !sn; id
      | None -> id_fresh "_" in
    create_pvsymbol id ~ghost (ity_of_dity dity) in
  List.map binder bl

let opaque_binders otv bl =
  List.fold_left (fun otv (_,_,s,_) -> Stv.union otv s) otv bl

Andrei Paskevich's avatar
Andrei Paskevich committed
797 798
(** Specifications *)

Andrei Paskevich's avatar
Andrei Paskevich committed
799 800 801 802
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
803

804
let create_assert f = t_label_add Split_goal.stop_split (to_fmla f)
805 806 807
let create_pre fl = t_and_simp_l (List.map create_assert fl)
let create_inv = create_pre

808 809 810 811 812 813 814 815 816
let create_post u (v,f) =
  let f = match v with
    | Some v when vs_equal u v -> f
    | Some v -> Loc.try3 ?loc:f.t_loc t_subst_single v (t_var u) f
    | None -> f in
  let f = Mlw_wp.remove_old (to_fmla f) in
  t_label_add Split_goal.stop_split f

let create_post ty ql =
817 818
  let rec get_var = function
    | [] -> create_vsymbol (id_fresh "result") ty
819
    | (Some v, _) :: _ -> Ty.ty_equal_check ty v.vs_ty; v
820
    | _ :: l -> get_var l in
821 822 823 824 825 826 827 828
  let u = get_var ql in
  let f = t_and_simp_l (List.map (create_post u) ql) in
  Mlw_ty.create_post u f

let create_xpost xql =
  Mexn.mapi (fun xs ql -> create_post (ty_of_ity xs.xs_ity) ql) xql

let spec_of_dspec eff ty dsp = {
829
  c_pre     = create_pre dsp.ds_pre;
830
  c_post    = create_post ty dsp.ds_post;
831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868
  c_xpost   = create_xpost dsp.ds_xpost;
  c_effect  = eff;
  c_variant = dsp.ds_variant;
  c_letrec  = 0;
}

(** User effects *)

let mk_field ity gh mut = {fd_ity = ity; fd_ghost = gh; fd_mut = mut}

let rec effect_of_term t = match t.t_node with
  | Tvar vs ->
      let pv = try restore_pv vs with Not_found ->
        Loc.errorm ?loc:t.t_loc "unsupported effect expression" in
      vs, mk_field pv.pv_ity pv.pv_ghost None
  | Tapp (fs,[ta]) ->
      let vs, fa = effect_of_term ta in
      let ofa,ofv = try match restore_pl fs with
        | {pl_args = [ofa]; pl_value = ofv} ->
            ofa, ofv
        | _ -> assert false
      with Not_found -> match fs with
        | {ls_args = [tya]; ls_value = Some tyv} ->
            mk_field (ity_of_ty tya) false None,
            mk_field (ity_of_ty tyv) false None
        | {ls_args = [_]; ls_value = None} ->
            Loc.errorm ?loc:t.t_loc "unsupported effect expression"
        | _ -> assert false in
      let sbs = ity_match ity_subst_empty ofa.fd_ity fa.fd_ity in
      let ity = try ity_full_inst sbs ofv.fd_ity with Not_found ->
        Loc.errorm ?loc:t.t_loc "unsupported effect expression" in
      let gh = (fa.fd_ghost && not ofa.fd_ghost) || ofv.fd_ghost in
      let mut = Opt.map (reg_full_inst sbs) ofv.fd_mut in
      vs, mk_field ity gh mut
  | _ ->
      Loc.errorm ?loc:t.t_loc "unsupported effect expression"

let effect_of_dspec dsp =
869 870
  let add_raise xs _ eff = eff_raise eff xs in
  let eff = Mexn.fold add_raise dsp.ds_xpost eff_empty in
871
  let eff = if dsp.ds_diverge then eff_diverge eff else eff in
872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893
  let svs = List.fold_right Svs.add dsp.ds_reads Svs.empty in
  let add_write (svs,mreg,eff) t =
    let vs, fd = effect_of_term t in
    match fd.fd_mut, fd.fd_ity.ity_node with
    | Some reg, _ ->
        Svs.add vs svs, Mreg.add reg t mreg,
        eff_write eff ~ghost:fd.fd_ghost reg
    | None, Ityapp ({its_ghrl = ghrl},_,(_::_ as regl)) ->
        let add_reg mreg reg = Mreg.add reg t mreg in
        let add_write eff gh reg =
          eff_write eff ~ghost:(fd.fd_ghost || gh) reg in
        Svs.add vs svs, List.fold_left add_reg mreg regl,
        List.fold_left2 add_write eff ghrl regl
    | _ ->
        Loc.errorm ?loc:t.t_loc "mutable expression expected"
  in
  List.fold_left add_write (svs,Mreg.empty,eff) dsp.ds_writes

let e_find_loc pr e =
  try (e_find (fun e -> e.e_loc <> None && pr e) e).e_loc
  with Not_found -> None

894 895
let lab_w_diverges_no = Ident.create_label "W:diverges:N"

896
let check_user_effect ?ps e spec args dsp =
897 898 899 900 901 902
  let has_write reg eff =
    Sreg.mem reg eff.eff_writes || Sreg.mem reg eff.eff_ghostw in
  let has_raise xs eff =
    Sexn.mem xs eff.eff_raises || Sexn.mem xs eff.eff_ghostx in
  (* computed effect vs user effect *)
  let eeff = spec.c_effect in
903
  let args = Spv.of_list args in
904
  let full_xpost = ps <> None in
905 906 907 908
  let usvs, mreg, ueff = effect_of_dspec dsp in
  (* check that every user effect actually happens *)
  let check_read vs =
    let pv = try restore_pv vs with Not_found ->
909 910 911 912 913
      Loc.errorm "unsupported@ effect@ expression" in
    if Spv.mem pv args then Warning.emit ?loc:e.e_loc
      "variable@ %a@ is@ a@ local@ function@ argument,@ \
        it@ does@ not@ have@ to@ be@ listed@ in@ the@ `reads'@ clause"
      Pretty.print_vs vs;
914
    if not (Spv.mem pv e.e_syms.syms_pv) then Loc.errorm ?loc:e.e_loc
915 916
      "variable@ %a@ does@ not@ occur@ in@ this@ expression"
      Pretty.print_vs vs in
917 918 919
  List.iter check_read dsp.ds_reads;
  let check_write reg = if not (has_write reg eeff)
    then let t = Mreg.find reg mreg in Loc.errorm ?loc:t.t_loc
920
      "this@ write@ effect@ does@ not@ happen@ in@ the@ expression" in
921 922 923 924
  Sreg.iter check_write ueff.eff_writes;
  Sreg.iter check_write ueff.eff_ghostw;
  let check_raise xs _ = if not (has_raise xs eeff)
    then Loc.errorm ?loc:e.e_loc
925
      "this@ expression@ does@ not@ raise@ exception@ %a"
926 927 928
      Mlw_pretty.print_xs xs in
  Mexn.iter check_raise ueff.eff_raises;
  Mexn.iter check_raise ueff.eff_ghostx;
929
  if ueff.eff_diverg && not eeff.eff_diverg then
930
    Loc.errorm ?loc:e.e_loc "this@ expression@ does@ not@ diverge";
931 932 933
  (* check that every computed effect is listed *)
  let check_read pv = if not (Svs.mem pv.pv_vs usvs) then
    Loc.errorm ?loc:(e_find_loc (fun e -> Spv.mem pv e.e_syms.syms_pv) e)
934
      "this@ expression@ depends@ on@ variable@ %a@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
935
        left@ out@ in@ the@ specification" Mlw_pretty.print_pv pv in
936 937
  let check_write reg = if not (has_write reg ueff) then
    Loc.errorm ?loc:(e_find_loc (fun e -> has_write reg e.e_effect) e)
938
      "this@ expression@ produces@ an@ unlisted@ write@ effect" in
939 940 941
  if dsp.ds_checkrw then begin
    let reads = Spv.remove Mlw_wp.pv_old e.e_syms.syms_pv in
    let reads = Spv.diff reads (spec_pvset Spv.empty spec) in
942
    Spv.iter check_read (Spv.diff reads args);
943 944 945
    Sreg.iter check_write eeff.eff_writes;
    Sreg.iter check_write eeff.eff_ghostw;
  end;
946 947
  let check_raise xs = if not (has_raise xs ueff) then
    Loc.errorm ?loc:(e_find_loc (fun e -> has_raise xs e.e_effect) e)
948
      "this@ expression@ raises@ unlisted@ exception@ %a"
949 950
      Mlw_pretty.print_xs xs in
  if full_xpost then Sexn.iter check_raise eeff.eff_raises;
951
  if full_xpost then Sexn.iter check_raise eeff.eff_ghostx;
952
  if eeff.eff_diverg && not ueff.eff_diverg then match ps with
953 954 955 956 957
    | Some {ps_name = {id_label = l}}
      when not (Slab.mem lab_w_diverges_no l) ->
        Warning.emit ?loc:(e_find_loc (fun e -> e.e_effect.eff_diverg) e)
          "this@ expression@ may@ diverge,@ \
            which@ is@ not@ stated@ in@ the@ specification"
958
    | _ -> ()
959

960
let check_lambda_effect ({fun_lambda = lam} as fd) bl dsp =
961
  let spec = fd.fun_ps.ps_aty.aty_spec in
962
  let args = fd.fun_ps.ps_aty.aty_args in
963
  check_user_effect ~ps:fd.fun_ps lam.l_expr spec args dsp;
964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004
  let optv = opaque_binders Stv.empty bl in
  let bad_comp tv _ _ = Loc.errorm
    ?loc:(e_find_loc (fun e -> Stv.mem tv e.e_effect.eff_compar) lam.l_expr)
    "type parameter %a is not opaque in this expression" Pretty.print_tv tv in
  ignore (Mtv.inter bad_comp optv spec.c_effect.eff_compar)

let check_user_ps recu ps =
  let ps_regs = ps.ps_subst.ity_subst_reg in
  let report r =
    if Mreg.mem r ps_regs then let spv = Spv.filter
        (fun pv -> reg_occurs r pv.pv_ity.ity_vars) ps.ps_pvset in
      Loc.errorm "The type of this function contains an alias with \
        external variable %a" Mlw_pretty.print_pv (Spv.choose spv)
    else
      Loc.errorm "The type of this function contains an alias"
  in
  let rec check regs ity = match ity.ity_node with
    | Ityapp (_,_,rl) ->
        let add regs r =
          if Mreg.mem r regs then report r else
          check (Mreg.add r r regs) r.reg_ity in
        let regs = List.fold_left add regs rl in
        ity_fold check regs ity
    | _ ->
        ity_fold check regs ity
  in
  let rec down regs a =
    let add regs pv = check regs pv.pv_ity in
    let regs = List.fold_left add regs a.aty_args in
    match a.aty_result with
    | VTarrow a -> down regs a
    | VTvalue v -> check (if recu then regs else ps_regs) v
    (* we allow the value in a non-recursive function to contain
       regions coming the function's arguments, but not from the
       context. It is sometimes useful to write a function around
       a constructor or a projection. For recursive functions, we
       impose the full non-alias discipline, to ensure the safety
       of region polymorphism (see add_rec_mono). *)
  in
  ignore (down ps_regs ps.ps_aty)

1005
(** Environment *)
1006

Andrei Paskevich's avatar
Andrei Paskevich committed
1007
type local_env = {
1008 1009
   kn : Mlw_decl.known_map;
  lkn : Decl.known_map;
Andrei Paskevich's avatar
Andrei Paskevich committed
1010 1011 1012 1013 1014
  psm : psymbol Mstr.t;
  pvm : pvsymbol Mstr.t;
  vsm : vsymbol Mstr.t;
}

1015 1016 1017
let env_empty lkn kn = {
   kn = kn;
  lkn = lkn;
Andrei Paskevich's avatar
Andrei Paskevich committed
1018 1019 1020 1021 1022
  psm = Mstr.empty;
  pvm = Mstr.empty;
  vsm = Mstr.empty;
}

1023
let add_psymbol ({psm = psm} as lenv) ps =
1024
  let n = ps.ps_name.id_string in
1025
  { lenv with psm = Mstr.add n ps psm }
1026

1027
let add_pvsymbol ({pvm = pvm; vsm = vsm} as lenv) pv =
1028
  let n = pv.pv_vs.vs_name.id_string in
1029
  { lenv with pvm = Mstr.add n pv pvm; vsm = Mstr.add n pv.pv_vs vsm }
Andrei Paskevich's avatar
Andrei Paskevich committed
1030

1031
let add_pv_map ({pvm = pvm; vsm = vsm} as lenv) vm =
Andrei Paskevich's avatar
Andrei Paskevich committed
1032
  let um = Mstr.map (fun pv -> pv.pv_vs) vm in
1033
  { lenv with pvm = Mstr.set_union vm pvm; vsm = Mstr.set_union um vsm }
Andrei Paskevich's avatar
Andrei Paskevich committed
1034

1035 1036 1037
let add_let_sym env = function
  | LetV pv -> add_pvsymbol env pv
  | LetA ps -> add_psymbol env ps
1038

1039 1040 1041
let add_fundef  env fd  = add_psymbol env fd.fun_ps
let add_fundefs env fdl = List.fold_left add_fundef env fdl
let add_binders env pvl = List.fold_left add_pvsymbol env pvl
1042

1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063
(** Invariant handling *)

let env_invariant {lkn = lkn; kn = kn} eff pvs =
  let regs = Sreg.union eff.eff_writes eff.eff_ghostw in
  let add_pv pv (pinv,qinv) =
    let ity = pv.pv_ity in
    let written r = reg_occurs r ity.ity_vars in
    let inv = Mlw_wp.full_invariant lkn kn pv.pv_vs ity in
    let qinv = (* we reprove invariants for modified non-reset variables *)
      if Sreg.exists written regs && not (eff_stale_region eff ity.ity_vars)
      then t_and_simp qinv inv else qinv in
    t_and_simp pinv inv, qinv
  in
  Spv.fold add_pv pvs (t_true,t_true)

let rec check_reset rvs t = match t.t_node with
  | Tvar vs when Svs.mem vs rvs ->
      Loc.errorm "Variable %s is reset and can only be used \
        under `old' in the postcondition" vs.vs_name.id_string
  | Tapp (ls,_) when ls_equal ls Mlw_wp.fs_at -> false
  | Tlet _ | Tcase _ | Teps _ | Tquant _ ->
1064
      let rvs = Mvs.set_inter rvs (t_vars t) in
1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094
      if Mvs.is_empty rvs then false else
      t_any (check_reset rvs) t
  | _ ->
      t_any (check_reset rvs) t

let post_invariant {lkn = lkn; kn = kn} rvs inv ity q =
  ignore (check_reset rvs q);
  let vs, q = open_post q in
  let res_inv = Mlw_wp.full_invariant lkn kn vs ity in
  let q = t_and_asym_simp (t_and_simp res_inv inv) q in
  Mlw_ty.create_post vs q

let reset_vars eff pvs =
  let add pv s =
    if eff_stale_region eff pv.pv_ity.ity_vars
    then Svs.add pv.pv_vs s else s in
  if Mreg.is_empty eff.eff_resets then Svs.empty else
  Spv.fold add pvs Svs.empty

let spec_invariant env pvs vty spec =
  let ity = ity_of_vty vty in
  let pvs = spec_pvset pvs spec in
  let rvs = reset_vars spec.c_effect pvs in
  let pinv,qinv = env_invariant env spec.c_effect pvs in
  let post_inv = post_invariant env rvs qinv in
  let xpost_inv xs q = post_inv xs.xs_ity q in
  { spec with c_pre   = t_and_asym_simp pinv spec.c_pre;
              c_post  = post_inv ity spec.c_post;
              c_xpost = Mexn.mapi xpost_inv spec.c_xpost }

1095 1096
(** Abstract values *)

1097
let warn_unused s loc =
1098
  if s = "" || s.[0] <> '_' then
1099 1100 1101 1102 1103 1104 1105 1106
  Warning.emit ?loc "unused variable %s" s

let check_used_pv e pv = if not (Spv.mem pv e.e_syms.syms_pv) then
  warn_unused pv.pv_vs.vs_name.id_string pv.pv_vs.vs_name.id_loc

let check_used_ps e ps = if not (Sps.mem ps e.e_syms.syms_ps) then
  warn_unused ps.ps_name.id_string ps.ps_name.id_loc

1107 1108
let rec type_c env pvs vars otv (dtyv, dsp) =
  let vty = type_v env pvs vars otv dtyv in
1109 1110
  let res = ty_of_vty vty in
  let dsp = dsp env.vsm res in
1111 1112 1113 1114 1115 1116 1117 1118 1119
  let esvs, _, eff = effect_of_dspec dsp in
  (* refresh every subregion of a modified region *)
  let writes = Sreg.union eff.eff_writes eff.eff_ghostw in
  let check u eff =
    reg_fold (fun r e -> eff_refresh e r u) u.reg_ity.ity_vars eff in
  let eff = Sreg.fold check writes eff in
  (* eff_compare every type variable not marked as opaque *)
  let eff = Stv.fold_left eff_compare eff (Stv.diff vars.vars_tv otv) in
  (* make spec *)
1120
  let spec = spec_of_dspec eff res dsp in
1121 1122 1123 1124 1125 1126 1127 1128 1129
  if spec.c_variant <> [] then Loc.errorm
    "variants are not allowed in a parameter declaration";
  (* we add a fake variant term for every external variable in effect
     expressions which also does not occur in pre/post/xpost. In this
     way, we store the variable in the specification in order to keep
     the effect from being erased by Mlw_ty.spec_filter. Variants are
     ignored outside of "let rec" definitions, so WP are not affected. *)
  let del_pv pv s = Svs.remove pv.pv_vs s in
  let esvs = Spv.fold del_pv pvs esvs in
1130
  let drop _ t s = Mvs.set_diff s (t_vars t) in
1131 1132 1133 1134 1135 1136
  let esvs = drop () spec.c_pre esvs in
  let esvs = drop () spec.c_post esvs in
  let esvs = Mexn.fold drop spec.c_xpost esvs in
  let add_vs vs varl = (t_var vs, None) :: varl in
  let varl = Svs.fold add_vs esvs spec.c_variant in
  let spec = { spec with c_variant = varl } in
1137
  spec, vty
1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149

and type_v env pvs vars otv = function
  | DSpecV v ->
      VTvalue (ity_of_dity v)
  | DSpecA (bl,tyc) ->
      let pvl = binders bl in
      let env = add_binders env pvl in
      let otv = opaque_binders otv bl in
      let add_pv pv s = vars_union pv.pv_ity.ity_vars s in
      let vars = List.fold_right add_pv pvl vars in
      let pvs = List.fold_right Spv.add pvl pvs in
      let spec, vty = type_c env pvs vars otv tyc in
1150
      let spec = spec_invariant env pvs vty spec in
1151 1152
      VTarrow (vty_arrow pvl ~spec vty)

1153 1154 1155 1156 1157
let val_decl env (id,ghost,dtyv) =
  match type_v env Spv.empty vars_empty Stv.empty dtyv with
  | VTvalue v -> LetV (create_pvsymbol id ~ghost v)
  | VTarrow a -> LetA (create_psymbol id ~ghost a)

1158 1159
(** Expressions *)

1160 1161 1162
let implicit_post = Debug.register_flag "implicit_post"
  ~desc:"Generate@ a@ postcondition@ for@ pure@ functions@ without@ one."

Andrei Paskevich's avatar
Andrei Paskevich committed
1163 1164 1165
let e_ghostify gh e =
  if gh && not e.e_ghost then e_ghost e else e

1166 1167 1168 1169 1170 1171 1172 1173
let rec strip uloc labs de = match de.de_node with
  | DEcast (de,_) -> strip uloc labs de
  | DEuloc (de,loc) -> strip (Some loc) labs de
  | DElabel (de,s) -> strip uloc (Slab.union labs s) de
  | _ -> uloc, labs, de

let rec expr ~keep_loc uloc env ({de_loc = loc} as de) =
  let uloc, labs, de = strip uloc Slab.empty de in
1174
  let e = Loc.try4 ?loc try_expr keep_loc uloc env de in
1175 1176 1177 1178 1179
  let loc = if keep_loc then loc else None in
  let loc = if uloc <> None then uloc else loc in
  if loc = None && Slab.is_empty labs then e else
  e_label ?loc labs e

1180
and try_expr keep_loc uloc env ({de_dvty = argl,res} as de0) =
1181
  let get env de = expr ~keep_loc uloc env de in
1182
  match de0.de_node with
1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196
  | DEvar (n,_) when argl = [] ->
      e_value (Mstr.find_exn (Dterm.UnboundVar n) n env.pvm)
  | DEvar (n,_) ->
      let ps = Mstr.find_exn (Dterm.UnboundVar n) n env.psm in
      e_arrow ps (List.map ity_of_dity argl) (ity_of_dity res)
  | DEgpvar pv ->
      e_value pv
  | DEgpsym ps ->
      e_arrow ps (List.map ity_of_dity argl) (ity_of_dity res)
  | DEplapp (pl,del) ->
      let get_gh fd de = e_ghostify fd.fd_ghost (get env de) in
      e_plapp pl (List.map2 get_gh pl.pl_args del) (ity_of_dity res)
  | DElsapp (ls,del) ->
      e_lapp ls (List.map (get env) del) (ity_of_dity res)
1197 1198 1199 1200 1201 1202 1203 1204
  | DEapply ({de_dvty = (_::_, _)} as de1,de2) ->
      let e1 = get env de1 in
      let gh = match e1.e_vty with
        | VTarrow {aty_args = pv::_} -> pv.pv_ghost
        | _ -> assert false in
      e_app e1 [e_ghostify gh (get env de2)]
  | DEapply (de1,de2) ->
      e_lapp fs_func_app [get env de1; get env de2] (ity_of_dity res)
1205 1206 1207 1208 1209 1210 1211
  | DEconst c ->
      e_const c
  | DElet ((id,gh,de1),de2) ->
      let e1 = get env de1 in
      let mk_expr e1 =
        let e1 = e_ghostify gh e1 in
        let ld1 = create_let_defn id e1 in
1212
        let env = add_let_sym env ld1.let_sym in
1213 1214 1215 1216
        let e2 = get env de2 in
        let e2_unit = match e2.e_vty with
          | VTvalue ity -> ity_equal ity ity_unit
          | _ -> false in
1217 1218 1219 1220
        let id_in_e2 = match ld1.let_sym with
          | LetV pv -> Spv.mem pv e2.e_syms.syms_pv
          | LetA ps -> Sps.mem ps e2.e_syms.syms_ps in
        if not id_in_e2 then warn_unused id.pre_name id.pre_loc;
1221 1222 1223
        let e1_no_eff =
          Sreg.is_empty e1.e_effect.eff_writes &&
          Sexn.is_empty e1.e_effect.eff_raises &&
1224 1225 1226 1227
          not e1.e_effect.eff_diverg &&
          (* if e1 is a recursive call, we may not know yet its effects,
             so we have to rely on an heuristic: if the result of e1 is
             not used in e2, then it was probably called for the effect. *)
1228
          id_in_e2
1229
        in
1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243
        let e2 =
          if e2_unit (* e2 is unit *)
            && e2.e_ghost (* and e2 is ghost *)
            && not e1.e_ghost (* and e1 is non-ghost *)
            && not e1_no_eff (* and e1 has observable effects *)
          then e_let (create_let_defn (id_fresh "gh") e2) e_void
          else e2 in
        e_let ld1 e2 in
      let rec flatten e1 = match e1.e_node with
        | Elet (ld,_) (* can't let a non-ghost expr escape *)
          when gh && not ld.let_expr.e_ghost -> mk_expr e1
        | Elet (ld,e1) -> e_let ld (flatten e1)
        | _ -> mk_expr e1 in
      begin match e1.e_vty with
1244
        | VTarrow _ when e1.e_ghost && not gh -> (* TODO: localize *)
1245 1246 1247 1248 1249 1250 1251 1252 1253
            Loc.errorm "%s must be a ghost function" id.pre_name
        | VTarrow _ -> flatten e1
        | VTvalue _ -> mk_expr e1
      end
  | DEif (de1,de2,de3) ->
      let e1 = get env de1 in
      let e2 = get env de2 in
      let e3 = get env de3 in
      e_if e1 e2 e3
Andrei Paskevich's avatar
Andrei Paskevich committed
1254
  | DEcase (de1,bl) ->
1255 1256 1257 1258 1259
      let e1 = get env de1 in
      let ity = ity_of_expr e1 in
      let ghost = e1.e_ghost in
      let branch (dp,de) =
        let vm, pat = make_ppattern dp.dp_pat ~ghost ity in
1260 1261 1262
        let e = get (add_pv_map env vm) de in
        Mstr.iter (fun _ pv -> check_used_pv e pv) vm;
        pat, e in
1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282
      e_case e1 (List.map branch bl)
  | DEassign (pl,de1,de2) ->
      e_assign pl (get env de1) (get env de2)
  | DElazy (DEand,de1,de2) ->
      e_lazy_and (get env de1) (get env de2)
  | DElazy (DEor,de1,de2) ->
      e_lazy_or (get env de1) (get env de2)
  | DEnot de ->
      e_not (get env de)
  | DEtrue ->
      e_true
  | DEfalse ->
      e_false
  | DEraise (xs,de) ->
      e_raise xs (get env de) (ity_of_dity res)
  | DEtry (de1,bl) ->
      let e1 = get env de1 in
      let add_branch (m,l) (xs,dp,de) =
        let vm, pat = make_ppattern dp.dp_pat xs.xs_ity in
        let e = get (add_pv_map env vm) de in
1283
        Mstr.iter (fun _ pv -> check_used_pv e pv) vm;
1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296
        try Mexn.add xs ((pat,e) :: Mexn.find xs m) m, l
        with Not_found -> Mexn.add xs [pat,e] m, (xs::l) in
      let xsm, xsl = List.fold_left add_branch (Mexn.empty,[]) bl in
      let mk_branch xs = match Mexn.find xs xsm with
        | [{ ppat_pattern = { pat_node = Pvar vs }}, e] ->
            xs, Mlw_ty.restore_pv vs, e
        | [{ ppat_pattern = { pat_node = Pwild }}, e] ->
            xs, create_pvsymbol (id_fresh "_") xs.xs_ity, e
        | [{ ppat_pattern = { pat_node = Papp (fs,[]) }}, e]
          when ls_equal fs Mlw_expr.fs_void ->
            xs, create_pvsymbol (id_fresh "_") xs.xs_ity, e
        | bl ->
            let pv = create_pvsymbol (id_fresh "res") xs.xs_ity in
1297 1298 1299 1300
            let pl = List.rev_map (fun (p,_) -> [p.ppat_pattern]) bl in
            let bl = if Pattern.is_exhaustive [t_var pv.pv_vs] pl
              then bl else let _,pp = make_ppattern PPwild pv.pv_ity in
              (pp, e_raise xs (e_value pv) (ity_of_dity res)) :: bl in
1301 1302 1303 1304 1305 1306 1307
            xs, pv, e_case (e_value pv) (List.rev bl)
      in
      e_try e1 (List.rev_map mk_branch xsl)
  | DEfor (id,de_from,dir,de_to,dinv,de) ->
      let e_from = get env de_from in
      let e_to = get env de_to in
      let pv = create_pvsymbol id ity_int in
1308
      let env = add_pvsymbol env pv in
1309 1310 1311
      let e = get env de in
      let inv = dinv env.vsm in
      e_for pv e_from dir e_to (create_inv inv) e
1312 1313 1314 1315 1316 1317 1318 1319 1320
  | DEwhile (de1,varl_inv,de2) ->
      let loc = de0.de_loc in
      let de3 = mk_dexpr loc dvty_unit
        (DEtry (mk_dexpr loc dvty_unit
          (DEloop (varl_inv, mk_dexpr loc dvty_unit
            (DEif (de1, de2, mk_dexpr loc dvty_unit
              (DEraise (Mlw_module.xs_exit, de_void loc)))))),
          [Mlw_module.xs_exit, pat_void loc, de_void loc])) in
      try_expr keep_loc uloc env de3
1321 1322 1323 1324 1325 1326 1327
  | DEloop (varl_inv,de) ->
      let e = get env de in
      let varl, inv = varl_inv env.vsm in
      e_loop (create_inv inv) varl e
  | DEabsurd ->
      e_absurd (ity_of_dity res)
  | DEassert (ak,f) ->
1328
      e_assert ak (create_assert (f env.vsm))
1329
  | DEabstract (de,dsp) ->
1330
      let e = get env de in
1331 1332
      let tyv = ty_of_vty e.e_vty in
      let dsp = dsp env.vsm tyv in
1333
      if dsp.ds_variant <> [] then Loc.errorm
1334
        "variants are not allowed in `abstract'";
1335
      let spec = spec_of_dspec e.e_effect tyv dsp in
1336
      check_user_effect e spec [] dsp;
Andrei Paskevich's avatar
Andrei Paskevich committed
1337 1338 1339
      let speci = spec_invariant env e.e_syms.syms_pv e.e_vty spec in
      (* we do not require invariants on free variables *)
      e_abstract e { speci with c_pre = spec.c_pre }