pmodule.ml 53.6 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2020   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

12
open Wstdlib
13 14
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

(** *)

type prog_symbol =
  | PV of pvsymbol
  | RS of rsymbol
27
  | OO of Srs.t
28 29 30 31

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

let empty_ns = {
  ns_ts = Mstr.empty;
  ns_ps = Mstr.empty;
39
  ns_xs = Mstr.empty;
40 41 42 43 44
  ns_ns = Mstr.empty;
}

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

48 49
let merge_ts = ns_replace its_equal
let merge_xs = ns_replace xs_equal
50

51
type overload =
52 53 54
  | FixedRes of ity (* t -> t -> ... -> T *)
  | SameType        (* t -> t -> ... -> t *)
  | NoOver          (* neither *)
55 56 57 58

let overload_of_rs {rs_cty = cty} =
  if cty.cty_effect.eff_ghost then NoOver else
  if cty.cty_mask <> MaskVisible then NoOver else
59
  let same_type ity a = not a.pv_ghost && ity_equal a.pv_ity ity in
60
  match cty.cty_args with
61 62 63
  | a::al when not a.pv_ghost && List.for_all (same_type a.pv_ity) al ->
      let res = cty.cty_result in
      if ity_equal res a.pv_ity then SameType else
64
      if ity_closed res && res.ity_pure then FixedRes res else NoOver
65 66
  | _ -> NoOver

67 68 69 70 71 72 73
let same_overload r1 r2 =
  List.length r1.rs_cty.cty_args = List.length r2.rs_cty.cty_args &&
  match overload_of_rs r1, overload_of_rs r2 with
  | SameType, SameType -> true
  | FixedRes t1, FixedRes t2 -> ity_equal t1 t2
  | _ -> false (* two NoOver's are not the same *)

74 75 76 77 78 79
let ref_attr = Ident.create_attribute "mlw:reference_var"

let has_ref s =
  let has v = Sattr.mem ref_attr v.pv_vs.vs_name.id_attrs in
  List.exists has s.rs_cty.cty_args

80 81
exception IncompatibleNotation of string

Andrei Paskevich's avatar
Andrei Paskevich committed
82 83 84 85 86 87 88 89 90 91 92 93
let merge_ps chk x vo vn =
  let fsty rs = (List.hd rs.rs_cty.cty_args).pv_ity in
  if chk then match vo, vn with (* export namespace *)
    (* currently, we have no way to export notation *)
    | _, OO _ | OO _, _ -> assert false
    | PV v1, PV v2 when pv_equal v1 v2 -> vo
    | RS r1, RS r2 when rs_equal r1 r2 -> vo
    | _ -> raise (ClashSymbol x)
  else match vo, vn with (* import namespace *)
    (* once again, no way to export notation *)
    | _, OO _ -> assert false
    (* but we can merge two compatible symbols *)
94 95
    | RS r1, RS r2 ->
        if rs_equal r1 r2 then vo else
96
        if has_ref r1 || has_ref r2 then vn else
97 98
        if not (same_overload r1 r2) then vn else
        if ity_equal (fsty r1) (fsty r2) then vn else
Andrei Paskevich's avatar
Andrei Paskevich committed
99 100 101
        OO (Srs.add r2 (Srs.singleton r1))
    (* or add a compatible symbol to notation *)
    | OO s1, RS r2 ->
102
        if Srs.mem r2 s1 then vo else
103
        if has_ref r2 then vn else
104
        let r1 = Srs.choose s1 in
105
        if not (same_overload r1 r2) then vn else
106
        let ty = fsty r2 in
107
        let confl r = not (ity_equal (fsty r) ty) in
Andrei Paskevich's avatar
Andrei Paskevich committed
108 109 110 111
        let s1 = Srs.filter confl s1 in
        if Srs.is_empty s1 then vn else
        OO (Srs.add r2 s1)
    | _ -> vn
112

113 114 115 116 117 118 119 120 121
let rec merge_ns chk _ no nn =
  if no == nn then no else
  let union merge o n =
    let merge x vo vn = Some (merge chk x vo vn) in
    if o == n then o else Mstr.union merge o n in
  { ns_ts = union merge_ts no.ns_ts nn.ns_ts;
    ns_ps = union merge_ps no.ns_ps nn.ns_ps;
    ns_xs = union merge_xs no.ns_xs nn.ns_xs;
    ns_ns = union merge_ns no.ns_ns nn.ns_ns }
122

123 124
let ns_add merge chk x vn m = Mstr.change (function
  | Some vo -> Some (merge chk x vo vn)
125 126
  | None    -> Some vn) x m

127 128 129 130 131 132
let add_ts chk x ts ns = { ns with ns_ts = ns_add merge_ts chk x ts ns.ns_ts }
let add_ps chk x ps ns = { ns with ns_ps = ns_add merge_ps chk x ps ns.ns_ps }
let add_xs chk x xs ns = { ns with ns_xs = ns_add merge_xs chk x xs ns.ns_xs }
let add_ns chk x nn ns = { ns with ns_ns = ns_add merge_ns chk x nn ns.ns_ns }

let merge_ns chk nn no = merge_ns chk "" no nn (* swap arguments *)
133 134 135 136 137 138

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

139 140 141 142 143 144 145 146 147 148 149 150
let ns_find_its = ns_find (fun ns -> ns.ns_ts)
let ns_find_xs  = ns_find (fun ns -> ns.ns_xs)
let ns_find_ns  = ns_find (fun ns -> ns.ns_ns)

let ns_find_prog_symbol ns s =
  let ps = ns_find (fun ns -> ns.ns_ps) ns s in
  match ps with
  | RS _ | PV _ -> ps
  | OO ss ->
      let rs1 = Expr.Srs.min_elt ss in
      let rs2 = Expr.Srs.max_elt ss in
      if Expr.rs_equal rs1 rs2 then RS rs1 else ps
151 152 153 154 155 156 157 158 159

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} *)

160
type pmodule = {
Andrei Paskevich's avatar
Andrei Paskevich committed
161 162 163 164 165 166 167 168 169 170 171
  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
172
  | Uclone of mod_inst
Andrei Paskevich's avatar
Andrei Paskevich committed
173
  | Umeta  of meta * meta_arg list
174
  | Uscope of string * mod_unit list
Andrei Paskevich's avatar
Andrei Paskevich committed
175

Andrei Paskevich's avatar
Andrei Paskevich committed
176
and mod_inst = {
Andrei Paskevich's avatar
Andrei Paskevich committed
177
  mi_mod : pmodule;
178 179
  mi_ty  : ity Mts.t;
  mi_ts  : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
180 181
  mi_ls  : lsymbol Mls.t;
  mi_pr  : prsymbol Mpr.t;
182
  mi_pk  : prop_kind Mpr.t;
183
  mi_pv  : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
184
  mi_rs  : rsymbol Mrs.t;
185
  mi_xs  : xsymbol Mxs.t;
186
  mi_df  : prop_kind;
187 188
}

189 190 191 192 193 194 195 196 197
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;
198
  mi_xs  = Mxs.empty;
199
  mi_df  = Plemma;
200 201
}

202 203
(** {2 Module under construction} *)

204
type pmodule_uc = {
205
  muc_theory : theory_uc;
Andrei Paskevich's avatar
Andrei Paskevich committed
206
  muc_units  : mod_unit list;
207 208 209 210 211
  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
212
  muc_env    : Env.env;
213 214 215 216
}

let empty_module env n p = {
  muc_theory = create_theory ~path:p n;
Andrei Paskevich's avatar
Andrei Paskevich committed
217
  muc_units  = [];
218 219 220 221 222 223 224 225 226 227 228 229 230
  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
231
               mod_units  = List.rev uc.muc_units;
232 233 234 235 236 237 238 239
               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)

240
let open_scope uc s = match uc.muc_import with
241
  | ns :: _ -> { uc with
242
      muc_theory = Theory.open_scope uc.muc_theory s;
243
      muc_units  = [Uscope (s, uc.muc_units)];
244 245 246 247
      muc_import =       ns :: uc.muc_import;
      muc_export = empty_ns :: uc.muc_export; }
  | [] -> assert false

248 249
let close_scope uc ~import =
  let th = Theory.close_scope uc.muc_theory ~import in
Andrei Paskevich's avatar
Andrei Paskevich committed
250
  match List.rev uc.muc_units, uc.muc_import, uc.muc_export with
251
  | [Uscope (_,ul1)], _ :: sti, _ :: ste -> (* empty scope *)
Andrei Paskevich's avatar
Andrei Paskevich committed
252 253
      { uc with muc_theory = th;  muc_units  = ul1;
                muc_import = sti; muc_export = ste; }
254
  | Uscope (s,ul1) :: ul0, _ :: i1 :: sti, e0 :: e1 :: ste ->
255 256 257 258
      let i1 = if import then merge_ns false e0 i1 else i1 in
      let i1 = add_ns false s e0 i1 in
      let e1 = add_ns true  s e0 e1 in
      { uc with
259
          muc_theory = th;
260
          muc_units  = Uscope (s,ul0) :: ul1;
261 262
          muc_import = i1 :: sti;
          muc_export = e1 :: ste; }
Andrei Paskevich's avatar
Andrei Paskevich committed
263
  | _ -> assert false
264

265 266 267 268 269 270 271
let import_scope uc ql = match uc.muc_import with
  | i1 :: sti ->
      let th = Theory.import_scope uc.muc_theory ql in
      let i1 = merge_ns false (ns_find_ns i1 ql) i1 in
      { uc with muc_theory = th; muc_import = i1::sti }
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
272 273 274 275 276 277
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
278 279 280
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
281 282 283
      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; }
284 285
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
286 287 288
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; }
289

290
let store_path, store_module, restore_path, restore_module_id =
291
  let id_to_path = Wid.create 17 in
292
  let id_to_pmod = Wid.create 17 in
Andrei Paskevich's avatar
Andrei Paskevich committed
293
  let store_path {muc_theory = uc} path id =
294 295
    (* this symbol already belongs to some theory *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
296 297
    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
298 299 300
  let store_module pmod  =
    let th = pmod.mod_theory in
    let id = th.th_name in
301
    (* this symbol is already a module *)
302 303 304 305 306 307
    if Wid.mem id_to_path id then () else begin
        Wid.set id_to_path id (th.th_path, id.id_string, []);
        Sid.iter (fun id -> Wid.set id_to_pmod id pmod) pmod.mod_local;
        Wid.set id_to_pmod id pmod;
      end
  in
308
  let restore_path id = Wid.find id_to_path id in
309 310
  let restore_module_id id = Wid.find id_to_pmod id in
  store_path, store_module, restore_path, restore_module_id
311 312 313 314 315 316

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

317
(*
318 319 320 321
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
322
  let rec down mr ity = if ity.ity_imm then mr else
323 324 325
    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
326
    | Ityvar _ -> assert false
327 328 329
  and fields mr s tl rl =
    if s.its_private && rl = [] then mr else
    let isb = its_match_regs s tl rl in
330 331 332 333 334 335 336 337 338 339 340
    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
341
*)
342

343 344 345 346 347 348 349 350
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
351
let add_pdecl_no_logic uc d =
352
  let uc = { uc with
Andrei Paskevich's avatar
Andrei Paskevich committed
353
    muc_units = Udecl d :: uc.muc_units;
354
    muc_known = known_add_decl uc.muc_known d;
355
    muc_local = Sid.union uc.muc_local d.pd_news } in
356
  let add_rs uc s = add_symbol add_ps s.rs_name (RS s) uc in
357
  let add_rd uc d = add_rs uc d.rec_sym in
358 359 360 361 362 363 364 365
  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
366
  | PDlet (LDsym (s,_)) -> add_rs uc s
367
  | PDlet (LDrec l) -> List.fold_left add_rd uc l
368
  | PDexn xs -> add_symbol add_xs xs.xs_name xs uc
369
  | PDpure -> uc
370

371
let add_pdecl_raw ?(warn=true) uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
372
  let uc = add_pdecl_no_logic uc d in
373
  let th = List.fold_left (add_decl ~warn) uc.muc_theory d.pd_pure in
374 375
  let add_meta th (m,l) = Theory.add_meta th m l in
  let th = List.fold_left add_meta th d.pd_meta in
Andrei Paskevich's avatar
Andrei Paskevich committed
376 377
  { uc with muc_theory = th }

378 379
(** {2 Builtin symbols} *)

Andrei Paskevich's avatar
Andrei Paskevich committed
380 381
let dummy_env = Env.create_env []

382
let builtin_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
383 384 385
  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
386
  let uc = add_pdecl_no_logic uc pd_str in
Andrei Paskevich's avatar
Andrei Paskevich committed
387
  let uc = add_pdecl_no_logic uc pd_equ in
388 389
  let m = close_module uc in
  { m with mod_theory = builtin_theory }
390 391

let bool_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
392 393
  let uc = empty_module dummy_env (id_fresh "Bool") ["why3";"Bool"] in
  let uc = add_pdecl_no_logic uc pd_bool in
394 395
  let m = close_module uc in
  { m with mod_theory = bool_theory }
396 397

let highord_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
398 399 400
  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
401 402
  let m = close_module uc in
  { m with mod_theory = highord_theory }
403

404 405
let tuple_module = Hint.memo 17 (fun n ->
  let nm = "Tuple" ^ string_of_int n in
Andrei Paskevich's avatar
Andrei Paskevich committed
406 407
  let uc = empty_module dummy_env (id_fresh nm) ["why3";nm] in
  let uc = add_pdecl_no_logic uc (pd_tuple n) in
408 409
  let m = close_module uc in
  { m with mod_theory = tuple_theory n })
410 411

let unit_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
412
  let uc = empty_module dummy_env (id_fresh "Unit") ["why3";"Unit"] in
413
  let uc = use_export uc (tuple_module 0) in
414
  let add uc d = add_pdecl_raw ~warn:false uc d in
415
  let td = create_alias_decl (id_fresh "unit") [] ity_unit in
416
  close_module (List.fold_left add uc (create_type_decl [td]))
417

418 419
let itd_ref =
  let tv = create_tvsymbol (id_fresh "a") in
Sylvain Dailler's avatar
Sylvain Dailler committed
420
  let pj = create_pvsymbol (id_fresh "contents") (ity_var tv) in
421 422 423 424 425 426 427 428 429 430 431
  create_plain_record_decl ~priv:false ~mut:true (id_fresh "ref")
                                            [tv] [true, pj] [] []

let its_ref = itd_ref.itd_its
let rs_ref_cons = List.hd itd_ref.itd_constructors
let rs_ref_proj = List.hd itd_ref.itd_fields

let ts_ref = its_ref.its_ts
let ls_ref_cons = ls_of_rs rs_ref_cons
let ls_ref_proj = ls_of_rs rs_ref_proj

432 433 434 435 436
let rs_ref_ld, rs_ref =
  let cty = rs_ref_cons.rs_cty in
  let ityl = List.map (fun v -> v.pv_ity) cty.cty_args in
  let_sym (id_fresh "ref") (c_app rs_ref_cons [] ityl cty.cty_result)

437 438 439
let ref_module =
  let add uc d = add_pdecl_raw ~warn:false uc d in
  let uc = empty_module dummy_env (id_fresh "Ref") ["why3";"Ref"] in
440 441 442
  let uc = List.fold_left add uc (create_type_decl [itd_ref]) in
  let uc = use_export uc builtin_module (* needed for "=" *) in
  close_module (add uc (create_let_decl rs_ref_ld))
443

444
let create_module env ?(path=[]) n =
Andrei Paskevich's avatar
Andrei Paskevich committed
445
  let m = empty_module env n path in
446 447 448 449 450
  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
451 452 453
let add_use uc d = Sid.fold (fun id uc ->
  if id_equal id ts_func.ts_name then
    use_export uc highord_module
454 455
  else if id_equal id ts_ref.ts_name then
    use_export uc ref_module
Andrei Paskevich's avatar
Andrei Paskevich committed
456 457 458 459
  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

460 461
let mk_vc uc d = Vc.vc uc.muc_env uc.muc_known uc.muc_theory d

462
let add_pdecl ?(warn=true) ~vc uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
463
  let uc = add_use uc d in
464
  let dl = if vc then mk_vc uc d else [] in
465 466 467 468
  (* 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. *)
469
  add_pdecl_raw ~warn (List.fold_left (add_pdecl_raw ~warn) uc dl) d
470

Andrei Paskevich's avatar
Andrei Paskevich committed
471 472 473 474
(** {2 Cloning} *)

type clones = {
  cl_local : Sid.t;
475 476
  mutable ty_table : ity Mts.t;
  mutable ts_table : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
477 478 479
  mutable ls_table : lsymbol Mls.t;
  mutable pr_table : prsymbol Mpr.t;
  mutable rn_table : region Mreg.t;
480
  mutable fd_table : pvsymbol Mpv.t;
481
  mutable pv_table : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
482
  mutable rs_table : rsymbol Mrs.t;
483
  mutable xs_table : xsymbol Mxs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
484 485
}

486 487
let empty_clones m = {
  cl_local = m.mod_local;
488
  ty_table = Mts.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
489 490 491 492
  ts_table = Mts.empty;
  ls_table = Mls.empty;
  pr_table = Mpr.empty;
  rn_table = Mreg.empty;
493
  fd_table = Mpv.empty;
494
  pv_table = Mvs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
495
  rs_table = Mrs.empty;
496
  xs_table = Mxs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
497 498 499 500
}

(* populate the clone structure *)

501
let rec sm_trans_ty tym tsm ty = match ty.ty_node with
502
  | Tyapp (s, tl) ->
503
      let tl = List.map (sm_trans_ty tym tsm) tl in
504
      begin match Mts.find_opt s tsm with
505 506
      | Some its -> ty_app its.its_ts tl
      | None -> begin match Mts.find_opt s tym with
507 508
      | Some ity -> ty_inst (ts_match_args s tl) (ty_of_ity ity)
      | None -> ty_app s tl
509
      end end
510 511
  | Tyvar _ -> ty

Andrei Paskevich's avatar
Andrei Paskevich committed
512
let clone_ty cl ty = sm_trans_ty cl.ty_table cl.ts_table ty
513

514 515 516
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
517

518 519 520
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
521

Andrei Paskevich's avatar
Andrei Paskevich committed
522
let rec clone_ity cl ity = match ity.ity_node with
523
  | Ityreg r ->
Andrei Paskevich's avatar
Andrei Paskevich committed
524
      ity_reg (clone_reg cl r)
525
  | Ityapp (s, tl, rl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
526
      let tl' = List.map (clone_ity cl) tl in
527
      begin match Mts.find_opt s.its_ts cl.ts_table with
Andrei Paskevich's avatar
Andrei Paskevich committed
528
      | Some s' -> ity_app_pure s' tl' (clone_regs cl s tl rl s')
529 530
      | None -> (* creative indentation *)
      begin match Mts.find_opt s.its_ts cl.ty_table with
Andrei Paskevich's avatar
Andrei Paskevich committed
531 532
      | Some ity -> ity_full_inst (its_match_regs s tl' []) ity
      | None -> ity_app_pure s tl' (List.map (clone_ity cl) rl)
533
      end end
Andrei Paskevich's avatar
Andrei Paskevich committed
534 535
  | Ityvar _ -> ity

Andrei Paskevich's avatar
Andrei Paskevich committed
536
and clone_reg cl reg =
Andrei Paskevich's avatar
Andrei Paskevich committed
537
  try Mreg.find reg cl.rn_table with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
538 539 540 541 542
  let tl' = List.map (clone_ity cl) reg.reg_args in
  let s',rl' = match Mts.find_opt reg.reg_its.its_ts cl.ts_table with
    | Some s' -> s', clone_regs cl reg.reg_its reg.reg_args reg.reg_regs s'
    | None -> reg.reg_its, List.map (clone_ity cl) reg.reg_regs in
  let r = create_region (id_clone reg.reg_name) s' tl' rl' in
543 544
  cl.rn_table <- Mreg.add reg r cl.rn_table;
  r
Andrei Paskevich's avatar
Andrei Paskevich committed
545

Andrei Paskevich's avatar
Andrei Paskevich committed
546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566
and clone_regs cl s tl rl s' =
  if rl = [] then [] else
  let base = its_match_regs s tl rl in
  let add sbs pj =
    let ity = clone_ity cl (ity_full_inst base pj.pv_ity) in
    ity_match sbs (Mpv.find pj cl.fd_table).pv_ity ity in
  let sbs = List.fold_left add isb_empty s.its_mfields in
  let sbs = List.fold_left add sbs s.its_ofields in
  let rec inst ity =
    if ity.ity_pure then ity_full_inst sbs ity else
    match ity.ity_node with
    | Ityreg r when Mreg.mem r sbs.isb_reg ->
        Mreg.find r sbs.isb_reg
    | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl} ->
        ity_app s (List.map inst tl) (List.map inst rl)
    | Ityapp (s,tl,rl) ->
        ity_app_pure s (List.map inst tl) (List.map inst rl)
    | Ityvar v ->
        Mtv.find v sbs.isb_var in
  List.map (fun reg -> inst (ity_reg reg)) s'.its_regions

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
575
let cl_find_pr cl pr =
Andrei Paskevich's avatar
Andrei Paskevich committed
576
  if not (Sid.mem pr.pr_name cl.cl_local) then pr
577
  else Mpr.find pr cl.pr_table
Andrei Paskevich's avatar
Andrei Paskevich committed
578

Andrei Paskevich's avatar
Andrei Paskevich committed
579
let cl_find_pv cl pv =
Andrei Paskevich's avatar
Andrei Paskevich committed
580
  if not (Sid.mem pv.pv_vs.vs_name cl.cl_local) then pv
581
  else Mvs.find pv.pv_vs cl.pv_table
Andrei Paskevich's avatar
Andrei Paskevich committed
582

Andrei Paskevich's avatar
Andrei Paskevich committed
583
let cl_find_rs cl rs =
Andrei Paskevich's avatar
Andrei Paskevich committed
584 585 586
  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
587
let cl_find_xs cl xs =
Andrei Paskevich's avatar
Andrei Paskevich committed
588
  if not (Sid.mem xs.xs_name cl.cl_local) then xs
589
  else Mxs.find xs cl.xs_table
Andrei Paskevich's avatar
Andrei Paskevich committed
590

591 592 593 594 595 596 597 598
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;
599 600
    try ignore (restore_rs ls);
        raise (BadInstance (BadI_ls_rs ls))
601 602 603 604 605
    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
606
    | PDtype _ -> raise (CannotInstantiate rs.rs_name)
607 608 609 610 611 612 613
    | 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
614 615
    | PDtype _ | PDlet  _ | PDexn  _ ->
        raise (CannotInstantiate pr.pr_name)
616 617
    | PDpure -> () in
  Mpr.iter check_pk inst.mi_pk;
618 619
  Mpr.iter (fun pr _ -> (* only through bad API use *)
    raise (BadInstance (BadI pr.pr_name))) inst.mi_pr;
620 621 622 623 624
  cl

(* clone declarations *)

let clone_ls cl ls =
Andrei Paskevich's avatar
Andrei Paskevich committed
625
  let constr = ls.ls_constr in
626
  let id = id_clone ls.ls_name in
Andrei Paskevich's avatar
Andrei Paskevich committed
627 628
  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
629 630 631 632 633
  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
634
  | Dtype _ | Ddata _ -> assert false (* impossible *)
635
  | Dparam ls when Mls.mem ls inst.mi_ls ->
636
      let ls' = Mls.find ls inst.mi_ls in
637 638
      let mtch sb ty ty' = try ty_match sb ty' (clone_ty cl ty) with
        | Ty.TypeMismatch _ -> raise (BadInstance (BadI_ls_type ls)) in
639 640 641
      let sbs = match ls.ls_value,ls'.ls_value with
        | Some ty, Some ty' -> mtch Mtv.empty ty ty'
        | None, None -> Mtv.empty
642
        | _ -> raise (BadInstance (BadI_ls_kind ls)) in
643
      ignore (try List.fold_left2 mtch sbs ls.ls_args ls'.ls_args
644 645
        with Invalid_argument _ ->
          raise (BadInstance (BadI_ls_arity ls)));
646 647
      cl.ls_table <- Mls.add ls ls' cl.ls_table;
      uc
Andrei Paskevich's avatar
Andrei Paskevich committed
648
  | Dparam ls ->
649
      let d = create_param_decl (clone_ls cl ls) in
650
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
651
  | Dlogic ldl ->
652 653 654
      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
655
      let get_logic (_,ld) =
Andrei Paskevich's avatar
Andrei Paskevich committed
656
        Opt.get (ls_defn_of_axiom (clone_fmla cl (ls_defn_axiom ld))) in
Andrei Paskevich's avatar
Andrei Paskevich committed
657
      let d = create_logic_decl (List.map get_logic ldl) in
658
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
659
  | Dind (s, idl) ->
660 661 662
      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
663
      let get_case (pr,f) =
664
        if Mpr.mem pr inst.mi_pk then raise (CannotInstantiate pr.pr_name);
Andrei Paskevich's avatar
Andrei Paskevich committed
665 666
        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
667
        pr', clone_fmla cl f in
Andrei Paskevich's avatar
Andrei Paskevich committed
668 669
      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
670
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
671
  | Dprop (k,pr,f) ->
672
      let skip, k' = match k, Mpr.find_opt pr inst.mi_pk with
673 674 675 676
        | Pgoal, _ -> true, Pgoal
        | Plemma, Some Pgoal -> true, Pgoal
        | Plemma, _ -> false, Plemma
        | Paxiom, Some k -> false, k
677
        | Paxiom, None -> false, inst.mi_df in
Andrei Paskevich's avatar
Andrei Paskevich committed
678
      if skip then uc else
DIVERIO Diego's avatar
DIVERIO Diego committed
679 680
      let attr = Sattr.remove Ident.useraxiom_attr pr.pr_name.id_attrs in
      let pr' = create_prsymbol (id_attr pr.pr_name attr) in
Andrei Paskevich's avatar
Andrei Paskevich committed
681
      cl.pr_table <- Mpr.add pr pr' cl.pr_table;
Andrei Paskevich's avatar
Andrei Paskevich committed
682
      let d = create_prop_decl k' pr' (clone_fmla cl f) in
683
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
684

685 686 687
let cl_save_ls cl s s' =
  cl.ls_table <- Mls.add_new (CannotInstantiate s.ls_name) s s' cl.ls_table

688 689 690
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
691 692
  | Some v, Some v' -> cl.fd_table <- Mpv.add v v' cl.fd_table
  | None, _ -> () (* can instantiate a non-field with a field *)
693
  | _ -> raise (CannotInstantiate s.rs_name) (* but not vice versa *)
694 695
  end;
  match s.rs_logic, s'.rs_logic with
696
  | RLls s, RLls s' -> cl_save_ls cl s s'
Andrei Paskevich's avatar
Andrei Paskevich committed
697
  | RLnone, (RLnone | RLls _ | RLlemma) -> ()
698 699
  | RLlemma, RLlemma -> ()
  | _ -> raise (BadInstance (BadI_rs_kind s.rs_name))
700

Mário Pereira's avatar
Mário Pereira committed
701 702 703
type smap = {
  sm_vs : vsymbol Mvs.t;
  sm_pv : pvsymbol Mvs.t;
704
  sm_xs : xsymbol Mxs.t;
Mário Pereira's avatar
Mário Pereira committed
705 706 707 708 709 710
  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;
711
  sm_xs = cl.xs_table;
Mário Pereira's avatar
Mário Pereira committed
712 713 714 715 716
  sm_rs = cl.rs_table }

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;
717
  sm_xs = sm.sm_xs;
Mário Pereira's avatar
Mário Pereira committed
718 719 720 721 722
  sm_rs = sm.sm_rs }

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;
723
  sm_xs = sm.sm_xs;
Mário Pereira's avatar
Mário Pereira committed
724 725
  sm_rs = sm.sm_rs }

726 727 728
let sm_save_xs sm s s' =
  { sm with sm_xs = Mxs.add s s' sm.sm_xs }

Mário Pereira's avatar
Mário Pereira committed
729 730 731 732 733 734 735 736 737 738
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
  | RLls s, RLls s' -> cl_save_ls cl s s'; sm
  | RLpv v, RLpv v' -> sm_save_pv sm v v'
  | _ -> sm

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

739 740 741 742
let sm_find_xs sm xs = Mxs.find_def xs xs sm.sm_xs

let sm_find_rs sm rs = Mrs.find_def rs rs sm.sm_rs

Mário Pereira's avatar
Mário Pereira committed
743 744 745 746 747 748
let clone_pv cl {pv_vs = vs; pv_ity = ity; pv_ghost = ghost} =
  create_pvsymbol (id_clone vs.vs_name) ~ghost (clone_ity cl ity)

let clone_invl cl sm invl =
  List.map (fun t -> clone_term cl sm.sm_vs t) invl

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

752
let clone_cty cl sm ?(drop_decr=false) cty =
753
  let res = clone_ity cl cty.cty_result in
754
  let args = List.map (clone_pv cl) cty.cty_args in
755
  let sm_args = List.fold_left2 sm_save_pv sm cty.cty_args args in
756
  let add_old o n (sm, olds) = let o' = clone_pv cl o in
757
    sm_save_pv sm o o', Mpv.add o' (sm_find_pv sm_args n) olds in
758
  let sm_olds, olds = Mpv.fold add_old cty.cty_oldies (sm_args, Mpv.empty) in
759 760
  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
761
  let post = clone_invl cl sm_olds cty.cty_post in
762
  let xpost = Mxs.fold (fun xs fl q ->
763
    let xs = sm_find_xs sm xs in
764
    let fl = clone_invl cl sm_olds fl in
765
    Mxs.add xs fl q) cty.cty_xpost Mxs.empty in
766
  let add_read v s = Spv.add (sm_find_pv sm_args v) s in
767 768 769
  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
770 771 772
  let add_frz v frz = ity_frz_regs frz v.pv_ity in
  let frz = Spv.fold add_frz reads Sreg.empty in
  let add_write reg fs m =
773
    let add_fd fd s = Spv.add (Mpv.find_def fd fd cl.fd_table) s in
774 775 776 777 778
    (* add old mutable fields to the effect *)
    let fs = Spv.fold add_fd fs Spv.empty in
    (* add new mutable fields to the effect *)
    let ({reg_its = s'} as reg') = clone_reg cl reg in
    let smf_reg' = Spv.of_list s'.its_mfields in
Mário Pereira's avatar
Mário Pereira committed
779
    let smf_reg = Spv.of_list reg.reg_its.its_mfields in
780
    let smf_ref = Spv.fold add_fd smf_reg Spv.empty in
781 782 783 784 785 786 787
    let fs = Spv.union fs (Spv.diff smf_reg' smf_ref) in
    let m = if Spv.is_empty fs && not s'.its_private
            then m else Mreg.add reg' fs m in
    (* add new non-mutable fields to the effect *)
    let sof_reg' = Spv.of_list s'.its_ofields in
    let sof_reg = Spv.of_list reg.reg_its.its_ofields in
    let sof_ref = Spv.fold add_fd sof_reg Spv.empty in
788 789 790 791 792 793 794 795 796
    let rec add_ofds r ofds m = if Spv.is_empty ofds then m else
      let sbs = its_match_regs r.reg_its r.reg_args r.reg_regs in
      let add_ofd f m =
        ity_exp_fold add_ofd_reg m (ity_full_inst sbs f.pv_ity) in
      Spv.fold add_ofd ofds m
    and add_ofd_reg m r = if Sreg.mem r frz then m else
      add_ofds r (Spv.of_list r.reg_its.its_ofields)
        (Mreg.add r (Spv.of_list r.reg_its.its_mfields) m) in
    add_ofds reg' (Spv.diff sof_reg' sof_ref) m in
797
  let writes = Mreg.fold add_write cty.cty_effect.eff_writes Mreg.empty in
Andrei Paskevich's avatar
Andrei Paskevich committed
798
  let add_reset reg s = Sreg.add (clone_reg cl reg) s in
799
  let resets = Sreg.fold add_reset cty.cty_effect.eff_resets Sreg.empty in
800 801 802
  let eff = eff_reset (eff_reset_overwritten (eff_write reads writes)) resets in
  let add_spoil tv eff = eff_spoil eff (ity_var tv) in
  let eff = Stv.fold add_spoil cty.cty_effect.eff_spoils eff in
803
  let add_raise xs eff = eff_raise eff (sm_find_xs sm xs) in
804
  let eff = Sxs.fold add_raise cty.cty_effect.eff_raises eff in
805 806
  let eff = if partial cty.cty_effect.eff_oneway then eff_partial eff else eff in
  let eff = if diverges cty.cty_effect.eff_oneway then eff_diverge eff else eff in
807
  let cty = create_cty_defensive ~mask:cty.cty_mask args pre post xpost olds eff res in
808
  cty_ghostify (cty_ghost cty) cty
809 810 811 812 813

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' =
814 815
  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
816 817
  Mpv.fold add_old c.cty_oldies sm

818
let clone_ppat cl sm pp mask =
819 820
  let rec conv_pat p = match p.pat_node with
    | Term.Pwild -> PPwild
821 822 823
    | 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)
824 825 826 827
    | 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
828
  let vm, pp' = create_prog_pattern pre (clone_ity cl pp.pp_ity) mask in
829 830 831
  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'

Andrei Paskevich's avatar
Andrei Paskevich committed
832
let rec clone_expr cl sm e = e_attr_copy e (match e.e_node with
833
  | Evar v -> e_var (sm_find_pv sm v)
834
  | Econst c -> e_const c (clone_ity cl e.e_ity)
835
  | Eexec (c,_) -> e_exec (clone_cexp cl sm c)
836 837 838 839
  | 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)
840 841 842 843 844
  | 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)
845
  | Ematch (d, bl, xl) ->
846
      let d = clone_expr cl sm d in
847
      let conv_rbr (pp, e) =
848
        let sm, pp = clone_ppat cl sm pp d.e_mask in
849
        pp, clone_expr cl sm e in
850 851 852 853
      let conv_xbr 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
        Mxs.add (sm_find_xs sm xs) (vl', clone_expr cl sm e) m in
854
      e_match d (List.map conv_rbr bl) (Mxs.fold conv_xbr xl Mxs.empty)
855 856 857
  | 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)
858 859 860 861 862 863
  | Efor (v, (f,dir,t), i, invl, e) ->
      let v' = clone_pv cl v in
      let ism = sm_save_pv sm v v' in
      let i' = if pv_equal v i then v' else clone_pv cl i in
      let ism = if pv_equal v i then ism else sm_save_pv ism i i' in
      e_for v'
864
        (e_var (sm_find_pv sm f)) dir (e_var (sm_find_pv sm t))
865
        i' (clone_invl cl ism invl) (clone_expr cl ism e)
866 867
  | Eraise (xs, e1) ->
      e_raise (sm_find_xs sm xs) (clone_expr cl sm e1) (clone_ity cl e.e_ity)
868 869 870
  | Eexn ({xs_name = id; xs_mask = mask; xs_ity = ity} as xs, e) ->
      let xs' = create_xsymbol (id_clone id) ~mask (clone_ity cl ity) in
      e_exn xs' (clone_expr cl (sm_save_xs sm xs xs') e)
871
  | Eassert (k, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
872
      e_assert k (clone_term cl sm.sm_vs f)
873 874
  | Eghost e ->
      e_ghostify true (clone_expr cl sm e)