pmodule.ml 45.1 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

(** *)

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 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
type overload =
  | UnOp    (* t -> t *)
  | BinOp   (* t -> t -> t *)
  | BinRel  (* t -> t -> bool *)
  | NoOver  (* none of the above *)

let overload_of_rs {rs_cty = cty} =
  if cty.cty_effect.eff_ghost then NoOver else
  if cty.cty_mask <> MaskVisible then NoOver else
  match cty.cty_args with
  | [a;b] when ity_equal a.pv_ity b.pv_ity &&
               ity_equal cty.cty_result ity_bool &&
               not a.pv_ghost && not b.pv_ghost -> BinRel
  | [a;b] when ity_equal a.pv_ity b.pv_ity &&
               ity_equal cty.cty_result a.pv_ity &&
               not a.pv_ghost && not b.pv_ghost -> BinOp
  | [a]   when ity_equal cty.cty_result a.pv_ity &&
               not a.pv_ghost -> UnOp
  | _ -> NoOver

exception IncompatibleNotation of string

Andrei Paskevich's avatar
Andrei Paskevich committed
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
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 *)
    | RS r1, RS r2 when not (rs_equal r1 r2) ->
        let o1 = overload_of_rs r1 in
        let o2 = overload_of_rs r2 in
        if o1 <> o2 || o2 = NoOver then vn else
        if fsty r1 == fsty r2 then vn else
        OO (Srs.add r2 (Srs.singleton r1))
    (* or add a compatible symbol to notation *)
    | OO s1, RS r2 ->
        let o1 = overload_of_rs (Srs.choose s1) in
        let o2 = overload_of_rs r2 in
        if o1 <> o2 || o2 = NoOver then vn else
        let ty = fsty r2 in
        let confl r = fsty r != ty in
        let s1 = Srs.filter confl s1 in
        if Srs.is_empty s1 then vn else
        OO (Srs.add r2 s1)
    | _ -> vn
102

103 104 105 106 107 108 109 110 111
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 }
112

113 114
let ns_add merge chk x vn m = Mstr.change (function
  | Some vo -> Some (merge chk x vo vn)
115 116
  | None    -> Some vn) x m

117 118 119 120 121 122
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 *)
123 124 125 126 127 128

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

129 130 131 132 133 134 135 136 137 138 139 140
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
141 142 143 144 145 146 147 148 149

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

150
type pmodule = {
Andrei Paskevich's avatar
Andrei Paskevich committed
151 152 153 154 155 156 157 158 159 160 161
  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
162
  | Uclone of mod_inst
Andrei Paskevich's avatar
Andrei Paskevich committed
163 164 165
  | Umeta  of meta * meta_arg list
  | Uscope of string * bool * mod_unit list

Andrei Paskevich's avatar
Andrei Paskevich committed
166
and mod_inst = {
Andrei Paskevich's avatar
Andrei Paskevich committed
167
  mi_mod : pmodule;
168 169
  mi_ty  : ity Mts.t;
  mi_ts  : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
170 171
  mi_ls  : lsymbol Mls.t;
  mi_pr  : prsymbol Mpr.t;
172
  mi_pk  : prop_kind Mpr.t;
173
  mi_pv  : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
174
  mi_rs  : rsymbol Mrs.t;
175
  mi_xs  : xsymbol Mxs.t;
176 177
}

178 179 180 181 182 183 184 185 186
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;
187
  mi_xs  = Mxs.empty;
188 189
}

190 191
(** {2 Module under construction} *)

192
type pmodule_uc = {
193
  muc_theory : theory_uc;
Andrei Paskevich's avatar
Andrei Paskevich committed
194
  muc_units  : mod_unit list;
195 196 197 198 199
  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
200
  muc_env    : Env.env;
201 202 203 204
}

let empty_module env n p = {
  muc_theory = create_theory ~path:p n;
Andrei Paskevich's avatar
Andrei Paskevich committed
205
  muc_units  = [];
206 207 208 209 210 211 212 213 214 215 216 217 218
  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
219
               mod_units  = List.rev uc.muc_units;
220 221 222 223 224 225 226 227
               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)

228
let open_scope uc s = match uc.muc_import with
229
  | ns :: _ -> { uc with
230
      muc_theory = Theory.open_scope uc.muc_theory s;
Andrei Paskevich's avatar
Andrei Paskevich committed
231
      muc_units  = [Uscope (s, false, uc.muc_units)];
232 233 234 235
      muc_import =       ns :: uc.muc_import;
      muc_export = empty_ns :: uc.muc_export; }
  | [] -> assert false

236 237
let close_scope uc ~import =
  let th = Theory.close_scope uc.muc_theory ~import in
Andrei Paskevich's avatar
Andrei Paskevich committed
238
  match List.rev uc.muc_units, uc.muc_import, uc.muc_export with
Andrei Paskevich's avatar
Andrei Paskevich committed
239 240 241
  | [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
242
  | Uscope (s,_,ul1) :: ul0, _ :: i1 :: sti, e0 :: e1 :: ste ->
243 244 245 246
      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
247
          muc_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
248
          muc_units  = Uscope (s, import, ul0) :: ul1;
249 250
          muc_import = i1 :: sti;
          muc_export = e1 :: ste; }
Andrei Paskevich's avatar
Andrei Paskevich committed
251
  | _ -> assert false
252

Andrei Paskevich's avatar
Andrei Paskevich committed
253 254 255 256 257 258
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
259 260 261
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
262 263 264
      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; }
265 266
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
267 268 269
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; }
270

271 272
let store_path, store_module, restore_path =
  let id_to_path = Wid.create 17 in
Andrei Paskevich's avatar
Andrei Paskevich committed
273
  let store_path {muc_theory = uc} path id =
274 275
    (* this symbol already belongs to some theory *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
276 277 278
    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} =
279 280
    (* this symbol is already a module *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
281
    Wid.set id_to_path id (th.th_path, id.id_string, []) in
282 283 284 285 286 287 288 289
  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

290
(*
291 292 293 294
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
295
  let rec down mr ity = if ity.ity_imm then mr else
296 297 298
    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
299
    | Ityvar _ -> assert false
300 301 302
  and fields mr s tl rl =
    if s.its_private && rl = [] then mr else
    let isb = its_match_regs s tl rl in
303 304 305 306 307 308 309 310 311 312 313
    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
314
*)
315

316 317 318 319 320 321 322 323
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
324
let add_pdecl_no_logic uc d =
325
  let uc = { uc with
Andrei Paskevich's avatar
Andrei Paskevich committed
326
    muc_units = Udecl d :: uc.muc_units;
327
    muc_known = known_add_decl uc.muc_known d;
328
    muc_local = Sid.union uc.muc_local d.pd_news } in
329
  let add_rs uc s = add_symbol add_ps s.rs_name (RS s) uc in
330
  let add_rd uc d = add_rs uc d.rec_sym in
331 332 333 334 335 336 337 338
  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
339
  | PDlet (LDsym (s,_)) -> add_rs uc s
340
  | PDlet (LDrec l) -> List.fold_left add_rd uc l
341
  | PDexn xs -> add_symbol add_xs xs.xs_name xs uc
342
  | PDpure -> uc
343

344
let add_pdecl_raw ?(warn=true) uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
345
  let uc = add_pdecl_no_logic uc d in
346
  let th = List.fold_left (add_decl ~warn) uc.muc_theory d.pd_pure in
347 348
  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
349 350
  { uc with muc_theory = th }

351 352
(** {2 Builtin symbols} *)

Andrei Paskevich's avatar
Andrei Paskevich committed
353 354
let dummy_env = Env.create_env []

355
let builtin_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
356 357 358 359
  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
360 361
  let m = close_module uc in
  { m with mod_theory = builtin_theory }
362 363

let bool_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
364 365
  let uc = empty_module dummy_env (id_fresh "Bool") ["why3";"Bool"] in
  let uc = add_pdecl_no_logic uc pd_bool in
366 367
  let m = close_module uc in
  { m with mod_theory = bool_theory }
368 369

let highord_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
370 371 372
  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
373 374
  let m = close_module uc in
  { m with mod_theory = highord_theory }
375

376 377
let tuple_module = Hint.memo 17 (fun n ->
  let nm = "Tuple" ^ string_of_int n in
Andrei Paskevich's avatar
Andrei Paskevich committed
378 379
  let uc = empty_module dummy_env (id_fresh nm) ["why3";nm] in
  let uc = add_pdecl_no_logic uc (pd_tuple n) in
380 381
  let m = close_module uc in
  { m with mod_theory = tuple_theory n })
382 383

let unit_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
384
  let uc = empty_module dummy_env (id_fresh "Unit") ["why3";"Unit"] in
385
  let uc = use_export uc (tuple_module 0) in
386
  let add uc d = add_pdecl_raw ~warn:false uc d in
387
  let td = create_alias_decl (id_fresh "unit") [] ity_unit in
388
  close_module (List.fold_left add uc (create_type_decl [td]))
389 390

let create_module env ?(path=[]) n =
Andrei Paskevich's avatar
Andrei Paskevich committed
391
  let m = empty_module env n path in
392 393 394 395 396
  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
397 398 399 400 401 402 403
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

404
let add_pdecl ?(warn=true) ~vc uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
405 406
  let uc = add_use uc d in
  let dl = if vc then Vc.vc uc.muc_env uc.muc_known d else [] in
407 408 409 410
  (* 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. *)
411
  add_pdecl_raw ~warn (List.fold_left (add_pdecl_raw ~warn) uc dl) d
412

Andrei Paskevich's avatar
Andrei Paskevich committed
413 414 415 416
(** {2 Cloning} *)

type clones = {
  cl_local : Sid.t;
417 418
  mutable ty_table : ity Mts.t;
  mutable ts_table : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
419 420 421
  mutable ls_table : lsymbol Mls.t;
  mutable pr_table : prsymbol Mpr.t;
  mutable rn_table : region Mreg.t;
422
  mutable fd_table : pvsymbol Mpv.t;
423
  mutable pv_table : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
424
  mutable rs_table : rsymbol Mrs.t;
425
  mutable xs_table : xsymbol Mxs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
426 427
}

428 429
let empty_clones m = {
  cl_local = m.mod_local;
430
  ty_table = Mts.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
431 432 433 434
  ts_table = Mts.empty;
  ls_table = Mls.empty;
  pr_table = Mpr.empty;
  rn_table = Mreg.empty;
435
  fd_table = Mpv.empty;
436
  pv_table = Mvs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
437
  rs_table = Mrs.empty;
438
  xs_table = Mxs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
439 440 441 442
}

(* populate the clone structure *)

443
let rec sm_trans_ty tym tsm ty = match ty.ty_node with
444
  | Tyapp (s, tl) ->
445
      let tl = List.map (sm_trans_ty tym tsm) tl in
446
      begin match Mts.find_opt s tsm with
447 448
      | Some its -> ty_app its.its_ts tl
      | None -> begin match Mts.find_opt s tym with
449 450
      | Some ity -> ty_inst (ts_match_args s tl) (ty_of_ity ity)
      | None -> ty_app s tl
451
      end end
452 453
  | Tyvar _ -> ty

Andrei Paskevich's avatar
Andrei Paskevich committed
454
let clone_ty cl ty = sm_trans_ty cl.ty_table cl.ts_table ty
455

456 457 458
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
459

460 461 462
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
463

Andrei Paskevich's avatar
Andrei Paskevich committed
464
let rec clone_ity cl ity = match ity.ity_node with
465
  | Ityreg r ->
Andrei Paskevich's avatar
Andrei Paskevich committed
466
      ity_reg (clone_reg cl r)
467
  | Ityapp (s, tl, rl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
468
      let tl = List.map (clone_ity cl) tl in
469
      let rl = List.map (clone_ity cl) rl in
470
      begin match Mts.find_opt s.its_ts cl.ts_table with
471 472 473
      | Some its -> ity_app_pure its tl rl
      | None -> (* creative indentation *)
      begin match Mts.find_opt s.its_ts cl.ty_table with
474
      | Some ity -> ity_full_inst (its_match_regs s tl rl) ity
475
      | None -> ity_app_pure s tl rl
476
      end end
Andrei Paskevich's avatar
Andrei Paskevich committed
477 478
  | Ityvar _ -> ity

Andrei Paskevich's avatar
Andrei Paskevich committed
479
and clone_reg cl reg =
480 481 482 483
  (* 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
484 485 486
     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
487
  try Mreg.find reg cl.rn_table with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
488
  let tl = List.map (clone_ity cl) reg.reg_args in
489
  let rl = List.map (clone_ity cl) reg.reg_regs in
490
  let r = match Mts.find_opt reg.reg_its.its_ts cl.ts_table with
491 492
    | Some its ->
        create_region (id_clone reg.reg_name) its tl rl
493 494
    | None -> (* creative indentation *)
    begin match Mts.find_opt reg.reg_its.its_ts cl.ty_table with
495 496 497
    | 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
498
        let rl = List.map (ity_full_inst sbs) r.reg_regs in
499
        create_region (id_clone reg.reg_name) r.reg_its tl rl
500
    | Some _ -> assert false
501 502
    | None ->
        create_region (id_clone reg.reg_name) reg.reg_its tl rl
503
    end in
504 505
  cl.rn_table <- Mreg.add reg r cl.rn_table;
  r
Andrei Paskevich's avatar
Andrei Paskevich committed
506 507 508

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
515
let cl_find_pr cl pr =
Andrei Paskevich's avatar
Andrei Paskevich committed
516
  if not (Sid.mem pr.pr_name cl.cl_local) then pr
517
  else Mpr.find pr cl.pr_table
Andrei Paskevich's avatar
Andrei Paskevich committed
518

Andrei Paskevich's avatar
Andrei Paskevich committed
519
let cl_find_pv cl pv =
Andrei Paskevich's avatar
Andrei Paskevich committed
520
  if not (Sid.mem pv.pv_vs.vs_name cl.cl_local) then pv
521
  else Mvs.find pv.pv_vs cl.pv_table
Andrei Paskevich's avatar
Andrei Paskevich committed
522

Andrei Paskevich's avatar
Andrei Paskevich committed
523
let cl_find_rs cl rs =
Andrei Paskevich's avatar
Andrei Paskevich committed
524 525 526
  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
527
let cl_find_xs cl xs =
Andrei Paskevich's avatar
Andrei Paskevich committed
528
  if not (Sid.mem xs.xs_name cl.cl_local) then xs
529
  else Mxs.find xs cl.xs_table
Andrei Paskevich's avatar
Andrei Paskevich committed
530

531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561
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
562
  let constr = ls.ls_constr in
563
  let id = id_clone ls.ls_name in
Andrei Paskevich's avatar
Andrei Paskevich committed
564 565
  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
566 567 568 569 570
  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
571
  | Dtype _ | Ddata _ -> assert false (* impossible *)
572 573 574 575 576 577 578 579 580 581 582 583
  | 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
584
  | Dparam ls ->
585
      let d = create_param_decl (clone_ls cl ls) in
586
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
587
  | Dlogic ldl ->
588 589 590
      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
591
      let get_logic (_,ld) =
Andrei Paskevich's avatar
Andrei Paskevich committed
592
        Opt.get (ls_defn_of_axiom (clone_fmla cl (ls_defn_axiom ld))) in
Andrei Paskevich's avatar
Andrei Paskevich committed
593
      let d = create_logic_decl (List.map get_logic ldl) in
594
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
595
  | Dind (s, idl) ->
596 597 598
      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
599
      let get_case (pr,f) =
600
        if Mpr.mem pr inst.mi_pk then raise (CannotInstantiate pr.pr_name);
Andrei Paskevich's avatar
Andrei Paskevich committed
601 602
        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
603
        pr', clone_fmla cl f in
Andrei Paskevich's avatar
Andrei Paskevich committed
604 605
      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
606
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
607
  | Dprop (k,pr,f) ->
608
      let skip, k' = match k, Mpr.find_opt pr inst.mi_pk with
609 610 611 612 613
        | 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
614
      if skip then uc else
Andrei Paskevich's avatar
Andrei Paskevich committed
615 616
      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
617
      let d = create_prop_decl k' pr' (clone_fmla cl f) in
618
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
619

620 621 622
let cl_save_ls cl s s' =
  cl.ls_table <- Mls.add_new (CannotInstantiate s.ls_name) s s' cl.ls_table

623 624 625
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
626 627 628
  | 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 *)
629 630
  end;
  match s.rs_logic, s'.rs_logic with
631
  | RLls s, RLls s' -> cl_save_ls cl s s'
632 633 634 635
  | RLlemma, RLlemma -> () (* TODO: update cl.pr_table? *)
  | RLnone, RLnone -> ()
  | _ -> assert false

Mário Pereira's avatar
Mário Pereira committed
636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672
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 }

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 }

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

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

Mário Pereira's avatar
Mário Pereira committed
673 674 675
let clone_type_record cl s d s' d' =
  let id = s.its_ts.ts_name in
  let fields' = Hstr.create 16 in
676
  let add_field' rs' = let pj' = fd_of_rs rs' in
Mário Pereira's avatar
Mário Pereira committed
677 678 679
    Hstr.add fields' pj'.pv_vs.vs_name.id_string rs' in
  List.iter add_field' d'.itd_fields;
  (* check if fields from former type are also declared in the new type *)
680
  let match_pj rs = let pj = fd_of_rs rs in
Mário Pereira's avatar
Mário Pereira committed
681 682 683 684 685
    let pj_str = pj.pv_vs.vs_name.id_string in
    let pj_ity = clone_ity cl pj.pv_ity in
    let pj_ght = pj.pv_ghost in
    let rs' = try Hstr.find fields' pj_str
      with Not_found -> raise (BadInstance id) in
686
    let pj' = fd_of_rs rs' in
Mário Pereira's avatar
Mário Pereira committed
687 688 689 690 691 692 693 694 695 696
    let pj'_ity = pj'.pv_ity in
    let pj'_ght = pj'.pv_ghost in
    if not (ity_equal pj_ity pj'_ity && (pj_ght || not pj'_ght)) then
      raise (BadInstance id);
    let ls, ls' = ls_of_rs rs, ls_of_rs rs' in
    cl.ls_table <- Mls.add ls ls' cl.ls_table;
    cl.rs_table <- Mrs.add rs rs' cl.rs_table;
    cl.fd_table <- Mpv.add pj pj' cl.fd_table in
  List.iter match_pj d.itd_fields;
  cl.ts_table <- Mts.add s.its_ts s' cl.ts_table
Mário Pereira's avatar
Mário Pereira committed
697

Mário Pereira's avatar
Mário Pereira committed
698
let clone_type_decl inst cl tdl kn =
699 700 701
  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
Mário Pereira's avatar
Mário Pereira committed
702
  let vcs = ref ([] : (itysymbol * term) list) in
703 704 705 706
  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
707
    let cloned = Mts.mem ts inst.mi_ts || Mts.mem ts inst.mi_ty in
708 709 710
    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 =
711 712
      List.iter2 (cl_save_rs cl) d.itd_constructors itd.itd_constructors;
      List.iter2 (cl_save_rs cl) d.itd_fields itd.itd_fields;
713 714
      Hits.add htd s (Some itd) in
    (* alias *)
715
    if s.its_def <> NoDef then begin
716
      if cloned then raise (CannotInstantiate id);
717 718 719 720 721
      let itd = match s.its_def with
        | Alias ty -> create_alias_decl id' ts.ts_args (conv_ity alg ty)
        | Range ir -> create_range_decl id' ir
        | Float ff -> create_float_decl id' ff
        | NoDef -> assert false (* never *) in
722 723
      cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
      save_itd itd
724
    end else
725
    (* abstract *)
726
    if s.its_private && cloned then begin
727 728 729 730
      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
731
          let pd' = Mid.find s'.its_ts.ts_name kn in
732
          let d' = match pd'.pd_node with
Mário Pereira's avatar
Mário Pereira committed
733
            | PDtype [d'] -> d'
734 735 736
            (* FIXME: we could refine with mutual types *)
            | PDtype _ -> raise (BadInstance id)
            | PDlet _ | PDexn _ | PDpure -> raise (BadInstance id) in
Mário Pereira's avatar
Mário Pereira committed
737
          clone_type_record cl s d s' d'; (* clone record fields *)
Mário Pereira's avatar
Mário Pereira committed
738
          (* generate and add VC for type invariant implication *)
739 740 741
          if d.itd_invariant <> [] then begin
            let inv = axiom_of_invariant d in
            let invl = clone_invl cl (sm_of_cl cl) [inv] in
742
            let add_vc inv = vcs := (d.itd_its, inv) :: !vcs in
743
            List.iter add_vc invl end
744
      | None -> begin match Mts.find_opt ts inst.mi_ty with
Mário Pereira's avatar
Mário Pereira committed
745
      | Some ity -> (* creative indentation *)
746 747 748
          (* TODO: clone_type_record, axiom_of_invariant *)
          (* TODO: should we only allow cloning into ity for
             private types with no fields and no invariant? *)
749 750
          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
751
                  its_pure s && ity_immutable ity) then raise (BadInstance id);
752 753
          cl.ty_table <- Mts.add ts ity cl.ty_table
      | None -> assert false end end;
754 755
      Hits.add htd s None;
      (* TODO: check typing conditions for refined record type *)
756 757
    end else
    (* variant *)
758 759
    if not s.its_mutable && d.itd_constructors <> [] &&
                            d.itd_invariant = [] then begin
760 761
      if cloned then raise (CannotInstantiate id);
      let conv_fd m fd =
762
        let v = fd_of_rs fd in Mpv.add v (conv_pj v) m in
763 764 765 766 767 768 769 770 771 772 773
      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 ->
774
          let itd = create_plain_variant_decl id' ts.ts_args csl in
775 776 777 778 779 780
          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
781
      let pjl = List.map fd_of_rs d.itd_fields in
782 783 784
      let fdl = List.map (fun v -> Spv.mem v mfld, conv_pj v) pjl in
      let inv =
        if d.itd_invariant = [] then [] else
785 786
        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
787
        List.map (clone_term cl mv) d.itd_invariant in
788 789
      let itd = create_plain_record_decl id' ts.ts_args
        ~priv:s.its_private ~mut:s.its_mutable fdl inv in
790 791 792
      cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
      save_itd itd
    end
793

794 795 796
  and conv_ity alg ity =
    let rec down ity = match ity.ity_node with
      | Ityreg {reg_its = s; reg_args = tl}
797
      | Ityapp (s,tl,_) ->
798 799 800
          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
801 802
            let s' = create_rec_itysymbol id s.its_ts.ts_args in
            cl.ts_table <- Mts.add s.its_ts s' cl.ts_table
803 804 805 806
          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
807
    clone_ity cl ity in
808 809

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

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

816
let clone_cty cl sm ?(drop_decr=false) cty =
817
  let res = clone_ity cl cty.cty_result in
818
  let args = List.map (clone_pv cl) cty.cty_args in
819
  let sm_args = List.fold_left2 sm_save_pv sm cty.cty_args args in
820
  let add_old o n (sm, olds) = let o' = clone_pv cl o in
821
    sm_save_pv sm o o', Mpv.add o' (sm_find_pv sm_args n) olds in
822
  let sm_olds, olds = Mpv.fold add_old cty.cty_oldies (sm_args, Mpv.empty) in
823 824
  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
825
  let post = clone_invl cl sm_olds cty.cty_post in
826
  let xpost = Mxs.fold (fun xs fl q ->
827 828
    let xs = cl_find_xs cl xs in
    let fl = clone_invl cl sm_olds fl in
829
    Mxs.add xs fl q) cty.cty_xpost Mxs.empty in
830
  let add_read v s = Spv.add (sm_find_pv sm_args v) s in
831 832 833
  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
Mário Pereira's avatar
Mário Pereira committed
834
  let add_write reg fs m = (* add new mutable fields to functions effect *)
835
    let add_fd fd s = Spv.add (Mpv.find_def fd fd cl.fd_table) s in
836
    let reg' = clone_reg cl reg in
Mário Pereira's avatar
Mário Pereira committed
837 838
    let smf_reg' = Spv.of_list reg'.reg_its.its_mfields in
    let smf_reg = Spv.of_list reg.reg_its.its_mfields in
839 840
    let smf_ref = Spv.fold add_fd smf_reg Spv.empty in
    let smf_new = Spv.diff smf_reg' smf_ref in
Mário Pereira's avatar
Mário Pereira committed
841
    let fs = Spv.fold add_fd fs Spv.empty in
842
    Mreg.add reg' (Spv.union fs smf_new) m in
843
  let writes = Mreg.fold add_write cty.cty_effect.eff_writes Mreg.empty in
Andrei Paskevich's avatar
Andrei Paskevich committed
844
  let add_reset reg s = Sreg.add (clone_reg cl reg) s in
845 846 847
  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
848
  let eff = Sxs.fold add_raise cty.cty_effect.eff_raises eff in
849
  let eff = if cty.cty_effect.eff_oneway then eff_diverge eff else eff in
850 851
  let cty = create_cty ~mask:cty.cty_mask args pre post xpost olds eff res in
  cty_ghostify (cty_ghost cty) cty
852 853 854 855 856

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' =
857 858
  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
859 860
  Mpv.fold add_old c.cty_oldies sm

861
let clone_ppat cl sm pp mask =
862 863
  let rec conv_pat p = match p.pat_node with
    | Term.Pwild -> PPwild
864 865 866
    | 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)
867 868 869 870
    | 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
871
  let vm, pp' = create_prog_pattern pre (clone_ity cl pp.pp_ity) mask in
872 873 874
  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'

875
let rec clone_expr cl sm e = e_label_copy e (match e.e_node with
876
  | Evar v -> e_var (sm_find_pv sm v)
877
  | Econst c -> e_const c e.e_ity
878
  | Eexec (c,_) -> e_exec (clone_cexp cl sm c)
879 880 881 882
  | 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)
883 884 885 886 887
  | 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)
888
  | Ecase (d, bl) ->
889
      let d = clone_expr cl sm d in
890
      let conv_br (pp, e) =
891
        let sm, pp = clone_ppat cl sm pp d.e_mask in
892
        pp, clone_expr cl sm e in
893
      e_case d (List.map conv_br bl)
894 895 896 897 898 899 900 901 902 903
  | 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) ->
904 905 906
      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
907 908
        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)
909
  | Eraise (xs, e) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
910
      e_raise (cl_find_xs cl xs) (clone_expr cl sm e) (clone_ity cl e.e_ity)
911
  | Eassert (k, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
912
      e_assert k (clone_term cl sm.sm_vs f)
913 914
  | Eghost e ->
      e_ghostify true (clone_expr cl sm e)