pmodule.ml 42.5 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11 12 13 14
(*                                                                  *)
(*  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
15
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
16
open Decl
17 18 19
open Theory
open Ity
open Expr
20
open Pdecl
21 22 23 24 25 26 27 28 29 30

(** *)

type prog_symbol =
  | PV of pvsymbol
  | RS of rsymbol

type namespace = {
  ns_ts : itysymbol   Mstr.t;  (* type symbols *)
  ns_ps : prog_symbol Mstr.t;  (* program symbols *)
31
  ns_xs : xsymbol     Mstr.t;  (* exception symbols *)
32 33 34 35 36 37
  ns_ns : namespace   Mstr.t;  (* inner namespaces *)
}

let empty_ns = {
  ns_ts = Mstr.empty;
  ns_ps = Mstr.empty;
38
  ns_xs = Mstr.empty;
39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
  ns_ns = Mstr.empty;
}

let ns_replace eq chk x vo vn =
  if not chk then vn else
  if eq vo vn then vn else
  raise (ClashSymbol x)

let psym_equal p1 p2 = match p1,p2 with
  | PV p1, PV p2 -> pv_equal p1 p2
  | RS p1, RS p2 -> rs_equal p1 p2
  | _, _ -> false

let rec merge_ns chk ns1 ns2 =
  if ns1 == ns2 then ns1 else
  let join eq x n o = Some (ns_replace eq chk x o n) in
  let ns_union eq m1 m2 =
    if m1 == m2 then m1 else Mstr.union (join eq) m1 m2 in
  let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
  { ns_ts = ns_union its_equal ns1.ns_ts ns2.ns_ts;
    ns_ps = ns_union psym_equal ns1.ns_ps ns2.ns_ps;
60
    ns_xs = ns_union xs_equal ns1.ns_xs ns2.ns_xs;
61 62 63 64 65 66 67 68 69 70
    ns_ns = Mstr.union fusion ns1.ns_ns ns2.ns_ns; }

let add_ns chk x ns m = Mstr.change (function
  | Some os -> Some (merge_ns chk ns os)
  | None    -> Some ns) x m

let ns_add eq chk x vn m = Mstr.change (function
  | Some vo -> Some (ns_replace eq chk x vo vn)
  | None    -> Some vn) x m

71
let add_xs chk x xs ns = { ns with ns_xs = ns_add xs_equal   chk x xs ns.ns_xs }
72
let add_ts chk x ts ns = { ns with ns_ts = ns_add its_equal  chk x ts ns.ns_ts }
73
let add_ps chk x ps ns = { ns with ns_ps = ns_add psym_equal chk x ps ns.ns_ps }
74 75 76 77 78 79 80 81 82
let add_ns chk x nn ns = { ns with ns_ns = add_ns            chk x nn ns.ns_ns }

let rec ns_find get_map ns = function
  | []   -> assert false
  | [a]  -> Mstr.find a (get_map ns)
  | a::l -> ns_find get_map (Mstr.find a ns.ns_ns) l

let ns_find_prog_symbol = ns_find (fun ns -> ns.ns_ps)
let ns_find_ns          = ns_find (fun ns -> ns.ns_ns)
83
let ns_find_xs          = ns_find (fun ns -> ns.ns_xs)
84 85 86 87 88 89 90 91 92 93
let ns_find_its         = ns_find (fun ns -> ns.ns_ts)

let ns_find_pv ns s = match ns_find_prog_symbol ns s with
  | PV pv -> pv | _ -> raise Not_found

let ns_find_rs ns s = match ns_find_prog_symbol ns s with
  | RS rs -> rs | _ -> raise Not_found

(** {2 Module} *)

94
type pmodule = {
Andrei Paskevich's avatar
Andrei Paskevich committed
95 96 97 98 99 100 101 102 103 104 105
  mod_theory : theory;        (* pure theory *)
  mod_units  : mod_unit list; (* module declarations *)
  mod_export : namespace;     (* exported namespace *)
  mod_known  : known_map;     (* known identifiers *)
  mod_local  : Sid.t;         (* locally declared idents *)
  mod_used   : Sid.t;         (* used modules *)
}

and mod_unit =
  | Udecl  of pdecl
  | Uuse   of pmodule
Andrei Paskevich's avatar
Andrei Paskevich committed
106
  | Uclone of mod_inst
Andrei Paskevich's avatar
Andrei Paskevich committed
107 108 109
  | Umeta  of meta * meta_arg list
  | Uscope of string * bool * mod_unit list

Andrei Paskevich's avatar
Andrei Paskevich committed
110
and mod_inst = {
Andrei Paskevich's avatar
Andrei Paskevich committed
111
  mi_mod : pmodule;
112 113
  mi_ty  : ity Mts.t;
  mi_ts  : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
114 115
  mi_ls  : lsymbol Mls.t;
  mi_pr  : prsymbol Mpr.t;
116
  mi_pk  : prop_kind Mpr.t;
117
  mi_pv  : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
118
  mi_rs  : rsymbol Mrs.t;
119
  mi_xs  : xsymbol Mxs.t;
120 121
}

122 123 124 125 126 127 128 129 130
let empty_mod_inst m = {
  mi_mod = m;
  mi_ty  = Mts.empty;
  mi_ts  = Mts.empty;
  mi_ls  = Mls.empty;
  mi_pr  = Mpr.empty;
  mi_pk  = Mpr.empty;
  mi_pv  = Mvs.empty;
  mi_rs  = Mrs.empty;
131
  mi_xs  = Mxs.empty;
132 133
}

134 135
(** {2 Module under construction} *)

136
type pmodule_uc = {
137
  muc_theory : theory_uc;
Andrei Paskevich's avatar
Andrei Paskevich committed
138
  muc_units  : mod_unit list;
139 140 141 142 143
  muc_import : namespace list;
  muc_export : namespace list;
  muc_known  : known_map;
  muc_local  : Sid.t;
  muc_used   : Sid.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
144
  muc_env    : Env.env;
145 146 147 148
}

let empty_module env n p = {
  muc_theory = create_theory ~path:p n;
Andrei Paskevich's avatar
Andrei Paskevich committed
149
  muc_units  = [];
150 151 152 153 154 155 156 157 158 159 160 161 162
  muc_import = [empty_ns];
  muc_export = [empty_ns];
  muc_known  = Mid.empty;
  muc_local  = Sid.empty;
  muc_used   = Sid.empty;
  muc_env    = env;
}

let close_module, restore_module =
  let h = Hid.create 17 in
  (fun uc ->
     let th = close_theory uc.muc_theory in (* catches errors *)
     let m = { mod_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
163
               mod_units  = List.rev uc.muc_units;
164 165 166 167 168 169 170 171
               mod_export = List.hd uc.muc_export;
               mod_known  = uc.muc_known;
               mod_local  = uc.muc_local;
               mod_used   = uc.muc_used; } in
     Hid.add h th.th_name m;
     m),
  (fun th -> Hid.find h th.th_name)

172
let open_scope uc s = match uc.muc_import with
173
  | ns :: _ -> { uc with
174
      muc_theory = Theory.open_scope uc.muc_theory s;
Andrei Paskevich's avatar
Andrei Paskevich committed
175
      muc_units  = [Uscope (s, false, uc.muc_units)];
176 177 178 179
      muc_import =       ns :: uc.muc_import;
      muc_export = empty_ns :: uc.muc_export; }
  | [] -> assert false

180 181
let close_scope uc ~import =
  let th = Theory.close_scope uc.muc_theory ~import in
Andrei Paskevich's avatar
Andrei Paskevich committed
182
  match List.rev uc.muc_units, uc.muc_import, uc.muc_export with
Andrei Paskevich's avatar
Andrei Paskevich committed
183 184 185
  | [Uscope (_,_,ul1)], _ :: sti, _ :: ste -> (* empty scope *)
      { uc with muc_theory = th;  muc_units  = ul1;
                muc_import = sti; muc_export = ste; }
Andrei Paskevich's avatar
Andrei Paskevich committed
186
  | Uscope (s,_,ul1) :: ul0, _ :: i1 :: sti, e0 :: e1 :: ste ->
187 188 189 190 191
      let i1 = if import then merge_ns false e0 i1 else i1 in
      let _  = if import then merge_ns true  e0 e1 else e1 in
      let i1 = add_ns false s e0 i1 in
      let e1 = add_ns true  s e0 e1 in
      { uc with
192
          muc_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
193
          muc_units  = Uscope (s, import, ul0) :: ul1;
194 195
          muc_import = i1 :: sti;
          muc_export = e1 :: ste; }
Andrei Paskevich's avatar
Andrei Paskevich committed
196
  | _ -> assert false
197

Andrei Paskevich's avatar
Andrei Paskevich committed
198 199 200 201 202 203
let use_export uc ({mod_theory = mth} as m) =
  let th = Theory.use_export uc.muc_theory mth in
  let uc = if Sid.mem mth.th_name uc.muc_used then uc
    else { uc with
      muc_known = merge_known uc.muc_known m.mod_known;
      muc_used  = Sid.add mth.th_name uc.muc_used } in
204 205 206
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
207 208 209
      muc_units  = Uuse m :: uc.muc_units;
      muc_import = merge_ns false m.mod_export i0 :: sti;
      muc_export = merge_ns true  m.mod_export e0 :: ste; }
210 211
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
212 213 214
let add_meta uc m al = { uc with
  muc_theory = Theory.add_meta uc.muc_theory m al;
  muc_units  = Umeta (m,al) :: uc.muc_units; }
215

216 217
let store_path, store_module, restore_path =
  let id_to_path = Wid.create 17 in
Andrei Paskevich's avatar
Andrei Paskevich committed
218
  let store_path {muc_theory = uc} path id =
219 220
    (* this symbol already belongs to some theory *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
221 222 223
    let prefix = List.rev (id.id_string :: path @ uc.uc_prefix) in
    Wid.set id_to_path id (uc.uc_path, uc.uc_name.id_string, prefix) in
  let store_module {mod_theory = {th_name = id} as th} =
224 225
    (* this symbol is already a module *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
226
    Wid.set id_to_path id (th.th_path, id.id_string, []) in
227 228 229 230 231 232 233 234
  let restore_path id = Wid.find id_to_path id in
  store_path, store_module, restore_path

let close_module uc =
  let m = close_module uc in
  store_module m;
  m

235
(*
236 237 238 239
let count_regions {muc_known = kn} {pv_ity = ity} mr =
  let add_reg r mr = Mreg.change (fun n -> Some (n <> None)) r mr in
  let meet mr1 mr2 = Mreg.union (fun _ x y -> Some (x || y)) mr1 mr2 in
  let join mr1 mr2 = Mreg.union (fun _ _ _ -> Some true) mr1 mr2 in
240
  let rec down mr ity = if ity.ity_imm then mr else
241 242 243
    match ity.ity_node with
    | Ityreg r -> fields (add_reg r mr) r.reg_its r.reg_args r.reg_regs
    | Ityapp (s,tl,rl) -> fields mr s tl rl
244
    | Ityvar _ -> assert false
245 246 247
  and fields mr s tl rl =
    if s.its_private && rl = [] then mr else
    let isb = its_match_regs s tl rl in
248 249 250 251 252 253 254 255 256 257 258
    let add_ity mr ity = down mr (ity_full_inst isb ity) in
    let add_proj mr f = add_ity mr f.rs_cty.cty_result in
    let add_field mr v = add_ity mr v.pv_ity in
    let d = find_its_defn kn s in
    if d.itd_constructors = [] then
      List.fold_left add_proj mr d.itd_fields
    else
      join mr (List.fold_left (fun mr c ->
        meet mr (List.fold_left add_field Mreg.empty c.rs_cty.cty_args))
        Mreg.empty d.itd_constructors) in
  down mr ity
259
*)
260

261 262 263 264 265 266 267 268
let add_symbol add id v uc =
  store_path uc [] id;
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_import = add false id.id_string v i0 :: sti;
      muc_export = add true  id.id_string v e0 :: ste }
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
269
let add_pdecl_no_logic uc d =
270
  let uc = { uc with
Andrei Paskevich's avatar
Andrei Paskevich committed
271
    muc_units = Udecl d :: uc.muc_units;
272
    muc_known = known_add_decl uc.muc_known d;
273
    muc_local = Sid.union uc.muc_local d.pd_news } in
274
  let add_rs uc s = add_symbol add_ps s.rs_name (RS s) uc in
275
  let add_rd uc d = add_rs uc d.rec_sym in
276 277 278 279 280 281 282 283
  match d.pd_node with
  | PDtype tdl ->
      let add uc d =
        let uc = List.fold_left add_rs uc d.itd_fields in
        let uc = List.fold_left add_rs uc d.itd_constructors in
        add_symbol add_ts d.itd_its.its_ts.ts_name d.itd_its uc in
      List.fold_left add uc tdl
  | PDlet (LDvar (v,_)) -> add_symbol add_ps v.pv_vs.vs_name (PV v) uc
284
  | PDlet (LDsym (s,_)) -> add_rs uc s
285
  | PDlet (LDrec l) -> List.fold_left add_rd uc l
286
  | PDexn xs -> add_symbol add_xs xs.xs_name xs uc
287
  | PDpure -> uc
288

289
let add_pdecl_raw ?(warn=true) uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
290
  let uc = add_pdecl_no_logic uc d in
291
  let th = List.fold_left (add_decl ~warn) uc.muc_theory d.pd_pure in
Andrei Paskevich's avatar
Andrei Paskevich committed
292 293
  { uc with muc_theory = th }

294 295
(** {2 Builtin symbols} *)

Andrei Paskevich's avatar
Andrei Paskevich committed
296 297
let dummy_env = Env.create_env []

298
let builtin_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
299 300 301 302
  let uc = empty_module dummy_env (id_fresh "BuiltIn") ["why3";"BuiltIn"] in
  let uc = add_pdecl_no_logic uc pd_int in
  let uc = add_pdecl_no_logic uc pd_real in
  let uc = add_pdecl_no_logic uc pd_equ in
303 304
  let m = close_module uc in
  { m with mod_theory = builtin_theory }
305 306

let bool_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
307 308
  let uc = empty_module dummy_env (id_fresh "Bool") ["why3";"Bool"] in
  let uc = add_pdecl_no_logic uc pd_bool in
309 310
  let m = close_module uc in
  { m with mod_theory = bool_theory }
311 312

let highord_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
313 314 315
  let uc = empty_module dummy_env (id_fresh "HighOrd") ["why3";"HighOrd"] in
  let uc = add_pdecl_no_logic uc pd_func in
  let uc = add_pdecl_no_logic uc pd_func_app in
316 317
  let m = close_module uc in
  { m with mod_theory = highord_theory }
318

319 320
let tuple_module = Hint.memo 17 (fun n ->
  let nm = "Tuple" ^ string_of_int n in
Andrei Paskevich's avatar
Andrei Paskevich committed
321 322
  let uc = empty_module dummy_env (id_fresh nm) ["why3";nm] in
  let uc = add_pdecl_no_logic uc (pd_tuple n) in
323 324
  let m = close_module uc in
  { m with mod_theory = tuple_theory n })
325 326

let unit_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
327
  let uc = empty_module dummy_env (id_fresh "Unit") ["why3";"Unit"] in
328
  let uc = use_export uc (tuple_module 0) in
329
  let td = create_alias_decl (id_fresh "unit") [] ity_unit in
330 331
  let d,metas = create_type_decl [td] in
  assert (metas = []);
332
  close_module (add_pdecl_raw ~warn:false uc d)
333 334

let create_module env ?(path=[]) n =
Andrei Paskevich's avatar
Andrei Paskevich committed
335
  let m = empty_module env n path in
336 337 338 339 340
  let m = use_export m builtin_module in
  let m = use_export m bool_module in
  let m = use_export m unit_module in
  m

Andrei Paskevich's avatar
Andrei Paskevich committed
341 342 343 344 345 346 347
let add_use uc d = Sid.fold (fun id uc ->
  if id_equal id ts_func.ts_name then
    use_export uc highord_module
  else match is_ts_tuple_id id with
  | Some n -> use_export uc (tuple_module n)
  | None -> uc) (Mid.set_diff d.pd_syms uc.muc_known) uc

348
let add_pdecl ?(warn=true) ~vc uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
349 350
  let uc = add_use uc d in
  let dl = if vc then Vc.vc uc.muc_env uc.muc_known d else [] in
351 352 353 354
  (* verification conditions must not add additional dependencies
     on built-in theories like TupleN or HighOrd. Also, we expect
     int.Int or any other library theory to be in the context:
     importing them automatically seems to be too invasive. *)
355
  add_pdecl_raw ~warn (List.fold_left (add_pdecl_raw ~warn) uc dl) d
356

Andrei Paskevich's avatar
Andrei Paskevich committed
357 358 359 360
(** {2 Cloning} *)

type clones = {
  cl_local : Sid.t;
361 362
  mutable ty_table : ity Mts.t;
  mutable ts_table : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
363 364 365
  mutable ls_table : lsymbol Mls.t;
  mutable pr_table : prsymbol Mpr.t;
  mutable rn_table : region Mreg.t;
366
  mutable fd_table : pvsymbol Mpv.t;
367
  mutable pv_table : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
368
  mutable rs_table : rsymbol Mrs.t;
369
  mutable xs_table : xsymbol Mxs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
370 371
}

372 373
let empty_clones m = {
  cl_local = m.mod_local;
374
  ty_table = Mts.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
375 376 377 378
  ts_table = Mts.empty;
  ls_table = Mls.empty;
  pr_table = Mpr.empty;
  rn_table = Mreg.empty;
379
  fd_table = Mpv.empty;
380
  pv_table = Mvs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
381
  rs_table = Mrs.empty;
382
  xs_table = Mxs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
383 384 385 386
}

(* populate the clone structure *)

387
let rec sm_trans_ty tym tsm ty = match ty.ty_node with
388
  | Tyapp (s, tl) ->
389
      let tl = List.map (sm_trans_ty tym tsm) tl in
390
      begin match Mts.find_opt s tsm with
391 392
      | Some its -> ty_app its.its_ts tl
      | None -> begin match Mts.find_opt s tym with
393 394
      | Some ity -> ty_inst (ts_match_args s tl) (ty_of_ity ity)
      | None -> ty_app s tl
395
      end end
396 397
  | Tyvar _ -> ty

Andrei Paskevich's avatar
Andrei Paskevich committed
398
let clone_ty cl ty = sm_trans_ty cl.ty_table cl.ts_table ty
399

400 401 402
let cl_find_its cl its =
  if not (Sid.mem its.its_ts.ts_name cl.cl_local) then its
  else Mts.find its.its_ts cl.ts_table
403

404 405 406
let cl_find_ts cl ts =
  if not (Sid.mem ts.ts_name cl.cl_local) then ts
  else (Mts.find ts cl.ts_table).its_ts
407

Andrei Paskevich's avatar
Andrei Paskevich committed
408
let rec clone_ity cl ity = match ity.ity_node with
409
  | Ityreg r ->
Andrei Paskevich's avatar
Andrei Paskevich committed
410
      ity_reg (clone_reg cl r)
411
  | Ityapp (s, tl, rl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
412
      let tl = List.map (clone_ity cl) tl in
413
      let rl = List.map (clone_ity cl) rl in
414
      begin match Mts.find_opt s.its_ts cl.ts_table with
415 416 417
      | Some its -> ity_app_pure its tl rl
      | None -> (* creative indentation *)
      begin match Mts.find_opt s.its_ts cl.ty_table with
418
      | Some ity -> ity_full_inst (its_match_regs s tl rl) ity
419
      | None -> ity_app_pure s tl rl
420
      end end
Andrei Paskevich's avatar
Andrei Paskevich committed
421 422
  | Ityvar _ -> ity

Andrei Paskevich's avatar
Andrei Paskevich committed
423
and clone_reg cl reg =
424 425 426 427
  (* FIXME: what about top-level non-instantiated regions?
     We cannot check in cl.cl_local to see if they are there.
     Instead, we should prefill cl.pv_table and cl.rn_table
     with all top-level pvsymbols (local or external) before
428 429 430
     descending into a let_defn.
     TODO: add to module/uc a list of locally-defined toplevel
     variables, as well as a set of imported toplevel variables. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
431
  try Mreg.find reg cl.rn_table with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
432
  let tl = List.map (clone_ity cl) reg.reg_args in
433
  let rl = List.map (clone_ity cl) reg.reg_regs in
434
  let r = match Mts.find_opt reg.reg_its.its_ts cl.ts_table with
435 436
    | Some its ->
        create_region (id_clone reg.reg_name) its tl rl
437 438
    | None -> (* creative indentation *)
    begin match Mts.find_opt reg.reg_its.its_ts cl.ty_table with
439 440 441
    | Some {ity_node = Ityreg r} ->
        let sbs = its_match_regs reg.reg_its tl rl in
        let tl = List.map (ity_full_inst sbs) r.reg_args in
442
        let rl = List.map (ity_full_inst sbs) r.reg_regs in
443
        create_region (id_clone reg.reg_name) r.reg_its tl rl
444
    | Some _ -> assert false
445 446
    | None ->
        create_region (id_clone reg.reg_name) reg.reg_its tl rl
447
    end in
448 449
  cl.rn_table <- Mreg.add reg r cl.rn_table;
  r
Andrei Paskevich's avatar
Andrei Paskevich committed
450 451 452

let cl_find_ls cl ls =
  if not (Sid.mem ls.ls_name cl.cl_local) then ls
453
  else Mls.find ls cl.ls_table
Andrei Paskevich's avatar
Andrei Paskevich committed
454

Andrei Paskevich's avatar
Andrei Paskevich committed
455
let clone_term cl mv t = t_gen_map (clone_ty cl) (cl_find_ls cl) mv t
456

Andrei Paskevich's avatar
Andrei Paskevich committed
457
let clone_fmla cl f = clone_term cl Mvs.empty f (* for closed terms *)
Andrei Paskevich's avatar
Andrei Paskevich committed
458

Andrei Paskevich's avatar
Andrei Paskevich committed
459
let cl_find_pr cl pr =
Andrei Paskevich's avatar
Andrei Paskevich committed
460
  if not (Sid.mem pr.pr_name cl.cl_local) then pr
461
  else Mpr.find pr cl.pr_table
Andrei Paskevich's avatar
Andrei Paskevich committed
462

Andrei Paskevich's avatar
Andrei Paskevich committed
463
let cl_find_pv cl pv =
Andrei Paskevich's avatar
Andrei Paskevich committed
464
  if not (Sid.mem pv.pv_vs.vs_name cl.cl_local) then pv
465
  else Mvs.find pv.pv_vs cl.pv_table
Andrei Paskevich's avatar
Andrei Paskevich committed
466

Andrei Paskevich's avatar
Andrei Paskevich committed
467
let cl_find_rs cl rs =
Andrei Paskevich's avatar
Andrei Paskevich committed
468 469 470
  if not (Sid.mem rs.rs_name cl.cl_local) then rs
  else Mrs.find rs cl.rs_table

Andrei Paskevich's avatar
Andrei Paskevich committed
471
let cl_find_xs cl xs =
Andrei Paskevich's avatar
Andrei Paskevich committed
472
  if not (Sid.mem xs.xs_name cl.cl_local) then xs
473
  else Mxs.find xs cl.xs_table
Andrei Paskevich's avatar
Andrei Paskevich committed
474

475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505
let cl_init m inst =
  let cl = empty_clones m in
  let non_local id =
    if not (Sid.mem id cl.cl_local) then raise (NonLocal id) in
  Mts.iter (fun ts _ -> non_local ts.ts_name) inst.mi_ts;
  Mts.iter (fun ts _ -> non_local ts.ts_name) inst.mi_ty;
  let check_ls ls _ =
    non_local ls.ls_name;
    try  ignore (restore_rs ls); raise (BadInstance ls.ls_name)
    with Not_found -> () in
  Mls.iter check_ls inst.mi_ls;
  let check_rs rs _ =
    non_local rs.rs_name;
    match (Mid.find rs.rs_name m.mod_known).pd_node with
    | PDtype _ -> raise (BadInstance rs.rs_name)
    | PDlet  _ | PDexn  _ | PDpure -> () in
  Mrs.iter check_rs inst.mi_rs;
  Mvs.iter (fun vs _ -> non_local vs.vs_name) inst.mi_pv;
  Mxs.iter (fun xs _ -> non_local xs.xs_name) inst.mi_xs;
  let check_pk pr _ =
    non_local pr.pr_name;
    match (Mid.find pr.pr_name m.mod_known).pd_node with
    | PDtype _ | PDlet  _ | PDexn  _ -> raise (BadInstance pr.pr_name)
    | PDpure -> () in
  Mpr.iter check_pk inst.mi_pk;
  Mpr.iter (fun pr _ -> raise (BadInstance pr.pr_name)) inst.mi_pr;
  cl

(* clone declarations *)

let clone_ls cl ls =
Andrei Paskevich's avatar
Andrei Paskevich committed
506
  let constr = ls.ls_constr in
507
  let id = id_clone ls.ls_name in
Andrei Paskevich's avatar
Andrei Paskevich committed
508 509
  let at = List.map (clone_ty cl) ls.ls_args in
  let vt = Opt.map (clone_ty cl) ls.ls_value in
Andrei Paskevich's avatar
Andrei Paskevich committed
510 511 512 513 514
  let ls' = create_lsymbol ~constr id at vt in
  cl.ls_table <- Mls.add ls ls' cl.ls_table;
  ls'

let clone_decl inst cl uc d = match d.d_node with
515
  | Dtype _ | Ddata _ -> assert false (* impossible *)
516 517 518 519 520 521 522 523 524 525 526 527
  | Dparam ({ls_name = id} as ls) when Mls.mem ls inst.mi_ls ->
      let ls' = Mls.find ls inst.mi_ls in
      let mtch sb ty ty' = try ty_match sb ty' (clone_ty cl ty)
        with TypeMismatch _ -> raise (BadInstance id) in
      let sbs = match ls.ls_value,ls'.ls_value with
        | Some ty, Some ty' -> mtch Mtv.empty ty ty'
        | None, None -> Mtv.empty
        | _ -> raise (BadInstance id) in
      ignore (try List.fold_left2 mtch sbs ls.ls_args ls'.ls_args
        with Invalid_argument _ -> raise (BadInstance id));
      cl.ls_table <- Mls.add ls ls' cl.ls_table;
      uc
Andrei Paskevich's avatar
Andrei Paskevich committed
528
  | Dparam ls ->
529
      let d = create_param_decl (clone_ls cl ls) in
530
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
531
  | Dlogic ldl ->
532 533 534
      List.iter (fun (ls,_) ->
        if Mls.mem ls inst.mi_ls then raise (CannotInstantiate ls.ls_name);
        ignore (clone_ls cl ls)) ldl;
Andrei Paskevich's avatar
Andrei Paskevich committed
535
      let get_logic (_,ld) =
Andrei Paskevich's avatar
Andrei Paskevich committed
536
        Opt.get (ls_defn_of_axiom (clone_fmla cl (ls_defn_axiom ld))) in
Andrei Paskevich's avatar
Andrei Paskevich committed
537
      let d = create_logic_decl (List.map get_logic ldl) in
538
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
539
  | Dind (s, idl) ->
540 541 542
      let lls = List.map (fun (ls,_) ->
        if Mls.mem ls inst.mi_ls then raise (CannotInstantiate ls.ls_name);
        clone_ls cl ls) idl in
Andrei Paskevich's avatar
Andrei Paskevich committed
543
      let get_case (pr,f) =
544
        if Mpr.mem pr inst.mi_pk then raise (CannotInstantiate pr.pr_name);
Andrei Paskevich's avatar
Andrei Paskevich committed
545 546
        let pr' = create_prsymbol (id_clone pr.pr_name) in
        cl.pr_table <- Mpr.add pr pr' cl.pr_table;
Andrei Paskevich's avatar
Andrei Paskevich committed
547
        pr', clone_fmla cl f in
Andrei Paskevich's avatar
Andrei Paskevich committed
548 549
      let get_ind ls (_,la) = ls, List.map get_case la in
      let d = create_ind_decl s (List.map2 get_ind lls idl) in
550
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
551
  | Dprop (k,pr,f) ->
552
      let skip, k' = match k, Mpr.find_opt pr inst.mi_pk with
553 554 555 556 557
        | Pgoal, _ -> true, Pgoal
        | Plemma, Some Pgoal -> true, Pgoal
        | Plemma, _ -> false, Plemma
        | Paxiom, Some k -> false, k
        | Paxiom, None -> false, Paxiom (* TODO: Plemma *) in
Andrei Paskevich's avatar
Andrei Paskevich committed
558
      if skip then uc else
Andrei Paskevich's avatar
Andrei Paskevich committed
559 560
      let pr' = create_prsymbol (id_clone pr.pr_name) in
      cl.pr_table <- Mpr.add pr pr' cl.pr_table;
Andrei Paskevich's avatar
Andrei Paskevich committed
561
      let d = create_prop_decl k' pr' (clone_fmla cl f) in
562
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
563

564 565 566
let cl_save_ls cl s s' =
  cl.ls_table <- Mls.add_new (CannotInstantiate s.ls_name) s s' cl.ls_table

567 568 569
let cl_save_rs cl s s' =
  cl.rs_table <- Mrs.add s s' cl.rs_table;
  begin match s.rs_field, s'.rs_field with
570 571 572
  | Some v, Some v' -> cl.fd_table <- Mpv.add v v' cl.fd_table
  | None, _ -> () (* can instantiate a non-field with a field *)
  | _ -> assert false (* but not vice versa *)
573 574
  end;
  match s.rs_logic, s'.rs_logic with
575
  | RLls s, RLls s' -> cl_save_ls cl s s'
576 577 578 579
  | RLlemma, RLlemma -> () (* TODO: update cl.pr_table? *)
  | RLnone, RLnone -> ()
  | _ -> assert false

Mário Pereira's avatar
Mário Pereira committed
580
(* Mário: recovered this commented function *)
581 582 583
let ls_of_rs rs = match rs.rs_logic with
  | RLls ls -> ls
  | _ -> assert false
Mário Pereira's avatar
Mário Pereira committed
584

Mário Pereira's avatar
Mário Pereira committed
585 586
let clone_type_record cl s d s' d' =
  let id = s.its_ts.ts_name in
587 588 589 590 591
  let fields' = Hstr.create 16 in
  let add_field' ({rs_field = pj'} as rs') =
    let pj' = Opt.get pj' in
    Hstr.add fields' pj'.pv_vs.vs_name.id_string rs' in
  List.iter add_field' d'.itd_fields;
Mário Pereira's avatar
Mário Pereira committed
592
  (* check if fields from former type are also declared in the new type *)
Mário Pereira's avatar
Mário Pereira committed
593 594
  let match_pj ({rs_field = pj} as rs) = let pj = Opt.get pj in
    let pj_str = pj.pv_vs.vs_name.id_string in
595
    let pj_ity = clone_ity cl pj.pv_ity in
Mário Pereira's avatar
Mário Pereira committed
596
    let pj_ght = pj.pv_ghost in
597 598 599 600 601 602 603
    let rs' = try Hstr.find fields' pj_str
      with Not_found -> raise (BadInstance id) in
    let pj' = Opt.get rs'.rs_field in
    let pj'_ity = pj'.pv_ity in
    let pj'_ght = pj'.pv_ghost in
    if not (ity_equal pj_ity pj'_ity && pj_ght = pj'_ght) then
      raise (BadInstance id);
Mário Pereira's avatar
Mário Pereira committed
604 605 606
    let ls, ls' = ls_of_rs rs, ls_of_rs rs' in
    cl.ls_table <- Mls.add ls ls' cl.ls_table in (* TODO? : populate rs_table *)
  List.iter match_pj d.itd_fields;
Mário Pereira's avatar
Mário Pereira committed
607 608
  cl.ts_table <- Mts.add s.its_ts s' cl.ts_table

Mário Pereira's avatar
Mário Pereira committed
609
let clone_type_decl inst cl tdl kn =
610 611 612
  let def =
    List.fold_left (fun m d -> Mits.add d.itd_its d m) Mits.empty tdl in
  let htd = Hits.create 5 in
613
  let vcs = ref ([] : (itysymbol * term) list) in
614 615 616 617
  let rec visit alg ({its_ts = {ts_name = id} as ts} as s) d =
    if not (Hits.mem htd s) then
    let alg = Sits.add s alg in
    let id' = id_clone id in
618
    let cloned = Mts.mem ts inst.mi_ts || Mts.mem ts inst.mi_ty in
619 620 621
    let conv_pj v = create_pvsymbol
      (id_clone v.pv_vs.vs_name) ~ghost:v.pv_ghost (conv_ity alg v.pv_ity) in
    let save_itd itd =
622 623
      List.iter2 (cl_save_rs cl) d.itd_constructors itd.itd_constructors;
      List.iter2 (cl_save_rs cl) d.itd_fields itd.itd_fields;
624 625
      Hits.add htd s (Some itd) in
    (* alias *)
626 627
    match s.its_def with
    | Alias ty ->
628
      if cloned then raise (CannotInstantiate id);
629
      let def = conv_ity alg ty in
630 631 632
      let itd = create_alias_decl id' ts.ts_args def in
      cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
      save_itd itd
633 634 635
    | Range _ -> assert false (* TODO *)
    | Float _ -> assert false (* TODO *)
    | NoDef ->
636
    (* abstract *)
637
    if s.its_private && cloned then begin
638 639 640
      (* FIXME: currently, we cannot refine a block of mutual types *)
      if List.length tdl <> 1 then raise (CannotInstantiate id);
        (* FIXME: better error messsage *)
641 642 643 644
      begin match Mts.find_opt ts inst.mi_ts with
      | Some s' ->
          if not (List.length ts.ts_args = List.length s'.its_ts.ts_args) then
            raise (BadInstance id);
Mário Pereira's avatar
Mário Pereira committed
645
          (* if not (its_pure s && its_pure s') then raise (BadInstance id); *)
Mário Pereira's avatar
Mário Pereira committed
646 647 648
          let pd' = Mid.find s'.its_ts.ts_name kn in
          let d' = begin match pd'.pd_node with
            | PDtype [d'] -> d'
649 650 651 652
            | PDtype _ ->
              (* FIXME: we could refine with mutual types *)
              raise (BadInstance id)
            | PDlet _ | PDexn _ | PDpure -> raise (BadInstance id)
Mário Pereira's avatar
Mário Pereira committed
653 654
          end in
          clone_type_record cl s d s' d'
655 656 657 658
      | None -> begin match Mts.find_opt ts inst.mi_ty with
      | Some ity ->
          let stv = Stv.of_list ts.ts_args in
          if not (Stv.subset (ity_freevars Stv.empty ity) stv &&
Mário Pereira's avatar
Mário Pereira committed
659
                  its_pure s && ity_immutable ity) then raise (BadInstance id);
660 661
          cl.ty_table <- Mts.add ts ity cl.ty_table
      | None -> assert false end end;
662 663 664
      Hits.add htd s None;
      (* TODO: check typing conditions for refined record type *)
      (* TODO: add a VC for invariants (if any) *)
665 666
    end else
    (* variant *)
667 668
    if not s.its_mutable && d.itd_constructors <> [] &&
                            d.itd_invariant = [] then begin
669 670 671 672 673 674 675 676 677 678 679 680 681 682
      if cloned then raise (CannotInstantiate id);
      let conv_fd m fd =
        let v = Opt.get fd.rs_field in Mpv.add v (conv_pj v) m in
      let fldm = List.fold_left conv_fd Mpv.empty d.itd_fields in
      let conv_pj pj = match Mpv.find_opt pj fldm with
        | Some pj' -> true, pj' | None -> false, conv_pj pj in
      let conv_cs cs =
        id_clone cs.rs_name, List.map conv_pj cs.rs_cty.cty_args in
      let csl = List.map conv_cs d.itd_constructors in
      match Mts.find_opt ts cl.ts_table with
      | Some s' ->
          let itd = create_rec_variant_decl s' csl in
          save_itd itd
      | None ->
683
          let itd = create_plain_variant_decl id' ts.ts_args csl in
684 685 686 687 688 689 690 691 692 693
          cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
          save_itd itd
    end else begin
    (* flat record *)
      if cloned then raise (CannotInstantiate id);
      let mfld = Spv.of_list s.its_mfields in
      let pjl = List.map (fun fd -> Opt.get fd.rs_field) d.itd_fields in
      let fdl = List.map (fun v -> Spv.mem v mfld, conv_pj v) pjl in
      let inv =
        if d.itd_invariant = [] then [] else
694 695
        let add mv u (_,v) = Mvs.add u.pv_vs v.pv_vs mv in
        let mv = List.fold_left2 add Mvs.empty pjl fdl in
Andrei Paskevich's avatar
Andrei Paskevich committed
696
        List.map (clone_term cl mv) d.itd_invariant in
697 698
      let itd = create_plain_record_decl id' ts.ts_args
        ~priv:s.its_private ~mut:s.its_mutable fdl inv in
699 700 701 702 703 704 705
      cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
      save_itd itd
    end

  and conv_ity alg ity =
    let rec down ity = match ity.ity_node with
      | Ityreg {reg_its = s; reg_args = tl}
706
      | Ityapp (s,tl,_) ->
707 708 709
          if Sits.mem s alg then begin
            if not (Mts.mem s.its_ts cl.ts_table) then
            let id = id_clone s.its_ts.ts_name in
710 711
            let s' = create_rec_itysymbol id s.its_ts.ts_args in
            cl.ts_table <- Mts.add s.its_ts s' cl.ts_table
712 713 714 715
          end else Opt.iter (visit alg s) (Mits.find_opt s def);
          List.iter down tl
      | Ityvar _ -> () in
    down ity;
Andrei Paskevich's avatar
Andrei Paskevich committed
716
    clone_ity cl ity in
717 718

  Mits.iter (visit Sits.empty) def;
719 720
  Lists.map_filter (fun d -> Hits.find htd d.itd_its) tdl,
  !vcs
721

722 723 724 725 726 727 728 729 730 731 732
type smap = {
  sm_vs : vsymbol Mvs.t;
  sm_pv : pvsymbol Mvs.t;
  sm_rs : rsymbol Mrs.t;
}

let sm_of_cl cl = {
  sm_vs = Mvs.map (fun v -> v.pv_vs) cl.pv_table;
  sm_pv = cl.pv_table;
  sm_rs = cl.rs_table }

733 734 735 736 737
let sm_save_vs sm v v' = {
  sm_vs = Mvs.add v v'.pv_vs sm.sm_vs;
  sm_pv = Mvs.add v v' sm.sm_pv;
  sm_rs = sm.sm_rs }

738 739 740 741 742 743 744 745
let sm_save_pv sm v v' = {
  sm_vs = Mvs.add v.pv_vs v'.pv_vs sm.sm_vs;
  sm_pv = Mvs.add v.pv_vs v' sm.sm_pv;
  sm_rs = sm.sm_rs }

let sm_save_rs cl sm s s' =
  let sm = { sm with sm_rs = Mrs.add s s' sm.sm_rs } in
  match s.rs_logic, s'.rs_logic with
746
  | RLls s, RLls s' -> cl_save_ls cl s s'; sm
747 748 749
  | RLpv v, RLpv v' -> sm_save_pv sm v v'
  | _ -> sm

750 751 752
let sm_find_pv sm v = Mvs.find_def v v.pv_vs sm.sm_pv
  (* non-instantiated global variables are not in sm *)

753
let clone_pv cl {pv_vs = vs; pv_ity = ity; pv_ghost = ghost} =
Andrei Paskevich's avatar
Andrei Paskevich committed
754
  create_pvsymbol (id_clone vs.vs_name) ~ghost (clone_ity cl ity)
755 756

let clone_invl cl sm invl =
Andrei Paskevich's avatar
Andrei Paskevich committed
757
  List.map (fun t -> clone_term cl sm.sm_vs t) invl
758

759
let clone_varl cl sm varl = List.map (fun (t,r) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
760
  clone_term cl sm.sm_vs t, Opt.map (cl_find_ls cl) r) varl
761

762
let clone_cty cl sm ?(drop_decr=false) cty =
763
  let res = clone_ity cl cty.cty_result in
764
  let args = List.map (clone_pv cl) cty.cty_args in
765
  let sm_args = List.fold_left2 sm_save_pv sm cty.cty_args args in
766
  let add_old o n (sm, olds) = let o' = clone_pv cl o in
767
    sm_save_pv sm o o', Mpv.add o' (sm_find_pv sm_args n) olds in
768
  let sm_olds, olds = Mpv.fold add_old cty.cty_oldies (sm_args, Mpv.empty) in
769 770
  let pre = if drop_decr then List.tl cty.cty_pre else cty.cty_pre in
  let pre = clone_invl cl sm_args pre in
771
  let post = clone_invl cl sm_olds cty.cty_post in
772
  let xpost = Mxs.fold (fun xs fl q ->
773 774
    let xs = cl_find_xs cl xs in
    let fl = clone_invl cl sm_olds fl in
775
    Mxs.add xs fl q) cty.cty_xpost Mxs.empty in
776
  let add_read v s = Spv.add (sm_find_pv sm_args v) s in
777 778 779
  let reads = Spv.fold add_read (cty_reads cty) Spv.empty in
  let reads = List.fold_right add_read cty.cty_args reads in
  let reads = Spv.union reads (Mpv.domain olds) in
780
  let add_write reg fs m =
781
    let add_fd fd s = Spv.add (Mpv.find_def fd fd cl.fd_table) s in
Mário Pereira's avatar
Mário Pereira committed
782 783 784 785 786 787
    let reg' = Mreg.find_def reg reg cl.rn_table in
    let smf_reg' = Spv.of_list reg'.reg_its.its_mfields in
    let smf_reg = Spv.of_list reg.reg_its.its_mfields in
    let smf_diff = Spv.diff smf_reg' smf_reg in
    let fs = Spv.fold add_fd fs Spv.empty in
    Mreg.add (clone_reg cl reg) (Spv.union fs smf_diff) m in
788
  let writes = Mreg.fold add_write cty.cty_effect.eff_writes Mreg.empty in
Mário Pereira's avatar
Mário Pereira committed
789 790 791
  (* Mreg.iter (fun rho spv -> Format.eprintf "rho:%a@." print_reg rho; *)
  (*             Spv.iter (fun pv -> Format.eprintf "pv:%a@." print_pv pv) spv) *)
  (*   writes; *)
Andrei Paskevich's avatar
Andrei Paskevich committed
792
  let add_reset reg s = Sreg.add (clone_reg cl reg) s in
793 794 795
  let resets = Sreg.fold add_reset cty.cty_effect.eff_resets Sreg.empty in
  let eff = eff_reset (eff_write reads writes) resets in
  let add_raise xs eff = eff_raise eff (cl_find_xs cl xs) in
796
  let eff = Sxs.fold add_raise cty.cty_effect.eff_raises eff in
797
  let eff = if cty.cty_effect.eff_oneway then eff_diverge eff else eff in
798 799
  let cty = create_cty ~mask:cty.cty_mask args pre post xpost olds eff res in
  cty_ghostify (cty_ghost cty) cty
800 801 802 803 804

let sm_save_args sm c c' =
  List.fold_left2 sm_save_pv sm c.cty_args c'.cty_args

let sm_save_olds sm c c' =
805 806
  let revs = Mpv.fold (fun o n m -> Mpv.add n o m) c'.cty_oldies Mpv.empty in
  let add_old o n sm = sm_save_pv sm o (Mpv.find (sm_find_pv sm n) revs) in
807 808 809 810 811 812 813 814 815
  Mpv.fold add_old c.cty_oldies sm

let rs_kind s = match s.rs_logic with
  | RLnone -> RKnone
  | RLpv _ -> RKlocal
  | RLls { ls_value = None } -> RKpred
  | RLls _ -> RKfunc
  | RLlemma -> RKlemma

816
let clone_ppat cl sm pp mask =
817 818
  let rec conv_pat p = match p.pat_node with
    | Term.Pwild -> PPwild
819 820 821
    | Term.Pvar v -> PPvar (id_clone v.vs_name, (restore_pv v).pv_ghost)
    | Term.Pas (p,v) ->
        PPas (conv_pat p, id_clone v.vs_name, (restore_pv v).pv_ghost)
822 823 824 825
    | Term.Por (p1,p2) -> PPor (conv_pat p1, conv_pat p2)
    | Term.Papp (s,pl) ->
        PPapp (restore_rs (cl_find_ls cl s), List.map conv_pat pl) in
  let pre = conv_pat pp.pp_pat in
826
  let vm, pp' = create_prog_pattern pre (clone_ity cl pp.pp_ity) mask in
827 828 829
  let save v sm = sm_save_vs sm v (Mstr.find v.vs_name.id_string vm) in
  Svs.fold save pp.pp_pat.pat_vars sm, pp'

830
let rec clone_expr cl sm e = e_label_copy e (match e.e_node with
831
  | Evar v -> e_var (sm_find_pv sm v)
832
  | Econst c -> e_const c
833
  | Eexec (c,_) -> e_exec (clone_cexp cl sm c)
834 835 836 837
  | Eassign asl ->
      let conv (r,f,v) =
        e_var (sm_find_pv sm r), cl_find_rs cl f, e_var (sm_find_pv sm v) in
      e_assign (List.map conv asl)
838 839 840 841 842
  | Elet (ld, e) ->
      let sm, ld = clone_let_defn cl sm ld in
      e_let ld (clone_expr cl sm e)
  | Eif (e1, e2, e3) ->
      e_if (clone_expr cl sm e1) (clone_expr cl sm e2) (clone_expr cl sm e3)
843
  | Ecase (d, bl) ->
844
      let d = clone_expr cl sm d in
845
      let conv_br (pp, e) =
846
        let sm, pp = clone_ppat cl sm pp d.e_mask in
847
        pp, clone_expr cl sm e in
848
      e_case d (List.map conv_br bl)
849 850 851 852 853 854 855 856 857 858
  | Ewhile (c,invl,varl,e) ->
      e_while (clone_expr cl sm c) (clone_invl cl sm invl)
              (clone_varl cl sm varl) (clone_expr cl sm e)
  | Efor (i, (f,dir,t), invl, e) ->
      let i' = clone_pv cl i in
      let ism = sm_save_pv sm i i' in
      e_for i'
        (e_var (sm_find_pv sm f)) dir (e_var (sm_find_pv sm t))
        (clone_invl cl ism invl) (clone_expr cl ism e)
  | Etry (d, xl) ->
859 860 861
      let conv_br xs (vl, e) m =
        let vl' = List.map (clone_pv cl) vl in
        let sm = List.fold_left2 sm_save_pv sm vl vl' in
862 863
        Mxs.add (cl_find_xs cl xs) (vl', clone_expr cl sm e) m in
      e_try (clone_expr cl sm d) (Mxs.fold conv_br xl Mxs.empty)
864
  | Eraise (xs, e) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
865
      e_raise (cl_find_xs cl xs) (clone_expr cl sm e) (clone_ity cl e.e_ity)
866
  | Eassert (k, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
867
      e_assert k (clone_term cl sm.sm_vs f)
868 869
  | Eghost e ->
      e_ghostify true (clone_expr cl sm e)
870
  | Epure t ->
Andrei Paskevich's avatar
Andrei Paskevich committed
871
      e_pure (clone_term cl sm.sm_vs t)