pmodule.ml 36.5 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   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_pv  : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
117 118
  mi_rs  : rsymbol Mrs.t;
  mi_xs  : xsymbol Mexn.t;
119 120 121 122
}

(** {2 Module under construction} *)

123
type pmodule_uc = {
124
  muc_theory : theory_uc;
Andrei Paskevich's avatar
Andrei Paskevich committed
125
  muc_units  : mod_unit list;
126 127 128 129 130
  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
131
  muc_env    : Env.env;
132 133 134 135
}

let empty_module env n p = {
  muc_theory = create_theory ~path:p n;
Andrei Paskevich's avatar
Andrei Paskevich committed
136
  muc_units  = [];
137 138 139 140 141 142 143 144 145 146 147 148 149
  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
150
               mod_units  = List.rev uc.muc_units;
151 152 153 154 155 156 157 158
               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)

159
let open_scope uc s = match uc.muc_import with
160
  | ns :: _ -> { uc with
161
      muc_theory = Theory.open_scope uc.muc_theory s;
Andrei Paskevich's avatar
Andrei Paskevich committed
162
      muc_units  = [Uscope (s, false, uc.muc_units)];
163 164 165 166
      muc_import =       ns :: uc.muc_import;
      muc_export = empty_ns :: uc.muc_export; }
  | [] -> assert false

167 168
let close_scope uc ~import =
  let th = Theory.close_scope uc.muc_theory ~import in
Andrei Paskevich's avatar
Andrei Paskevich committed
169
  match List.rev uc.muc_units, uc.muc_import, uc.muc_export with
Andrei Paskevich's avatar
Andrei Paskevich committed
170 171 172
  | [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
173
  | Uscope (s,_,ul1) :: ul0, _ :: i1 :: sti, e0 :: e1 :: ste ->
174 175 176 177 178
      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
179
          muc_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
180
          muc_units  = Uscope (s, import, ul0) :: ul1;
181 182
          muc_import = i1 :: sti;
          muc_export = e1 :: ste; }
Andrei Paskevich's avatar
Andrei Paskevich committed
183
  | _ -> assert false
184

Andrei Paskevich's avatar
Andrei Paskevich committed
185 186 187 188 189 190
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
191 192 193
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
194 195 196
      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; }
197 198
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
199 200 201
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; }
202

203 204
let store_path, store_module, restore_path =
  let id_to_path = Wid.create 17 in
Andrei Paskevich's avatar
Andrei Paskevich committed
205
  let store_path {muc_theory = uc} path id =
206 207
    (* this symbol already belongs to some theory *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
208 209 210
    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} =
211 212
    (* this symbol is already a module *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
213
    Wid.set id_to_path id (th.th_path, id.id_string, []) in
214 215 216 217 218 219 220 221
  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

222
(*
223 224 225 226
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
227
  let rec down mr ity = if ity.ity_imm then mr else
228 229 230
    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
231
    | Ityvar _ -> assert false
232 233 234
  and fields mr s tl rl =
    if s.its_private && rl = [] then mr else
    let isb = its_match_regs s tl rl in
235 236 237 238 239 240 241 242 243 244 245
    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
246
*)
247

248 249 250 251 252 253 254 255
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
256
let add_pdecl_no_logic uc d =
257
  let uc = { uc with
Andrei Paskevich's avatar
Andrei Paskevich committed
258
    muc_units = Udecl d :: uc.muc_units;
259
    muc_known = known_add_decl uc.muc_known d;
260
    muc_local = Sid.union uc.muc_local d.pd_news } in
261
  let add_rs uc s = add_symbol add_ps s.rs_name (RS s) uc in
262
  let add_rd uc d = add_rs uc d.rec_sym in
263 264 265 266 267 268 269 270
  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
271
  | PDlet (LDsym (s,_)) -> add_rs uc s
272
  | PDlet (LDrec l) -> List.fold_left add_rd uc l
273
  | PDexn xs -> add_symbol add_xs xs.xs_name xs uc
274
  | PDpure -> uc
275

Andrei Paskevich's avatar
Andrei Paskevich committed
276 277
let add_pdecl uc d =
  let uc = add_pdecl_no_logic uc d in
278
  let th = List.fold_left add_decl uc.muc_theory d.pd_pure in
Andrei Paskevich's avatar
Andrei Paskevich committed
279 280
  { uc with muc_theory = th }

281 282
(** {2 Builtin symbols} *)

Andrei Paskevich's avatar
Andrei Paskevich committed
283 284
let dummy_env = Env.create_env []

285
let builtin_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
286 287 288 289
  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
290 291
  let m = close_module uc in
  { m with mod_theory = builtin_theory }
292 293

let bool_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
294 295
  let uc = empty_module dummy_env (id_fresh "Bool") ["why3";"Bool"] in
  let uc = add_pdecl_no_logic uc pd_bool in
296 297
  let m = close_module uc in
  { m with mod_theory = bool_theory }
298 299

let highord_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
300 301 302
  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
303 304
  let m = close_module uc in
  { m with mod_theory = highord_theory }
305

306 307
let tuple_module = Hint.memo 17 (fun n ->
  let nm = "Tuple" ^ string_of_int n in
Andrei Paskevich's avatar
Andrei Paskevich committed
308 309
  let uc = empty_module dummy_env (id_fresh nm) ["why3";nm] in
  let uc = add_pdecl_no_logic uc (pd_tuple n) in
310 311
  let m = close_module uc in
  { m with mod_theory = tuple_theory n })
312 313

let unit_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
314
  let uc = empty_module dummy_env (id_fresh "Unit") ["why3";"Unit"] in
315
  let uc = use_export uc (tuple_module 0) in
316
  let td = create_alias_decl (id_fresh "unit") [] ity_unit in
Andrei Paskevich's avatar
Andrei Paskevich committed
317
  close_module (add_pdecl uc (create_type_decl [td]))
318 319

let create_module env ?(path=[]) n =
Andrei Paskevich's avatar
Andrei Paskevich committed
320
  let m = empty_module env n path in
321 322 323 324 325
  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
326 327 328 329 330 331 332
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

333
let add_pdecl ~vc uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
334 335
  let uc = add_use uc d in
  let dl = if vc then Vc.vc uc.muc_env uc.muc_known d else [] in
336 337 338 339 340
  (* 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. *)
  add_pdecl (List.fold_left add_pdecl uc dl) d
341

Andrei Paskevich's avatar
Andrei Paskevich committed
342 343 344 345
(** {2 Cloning} *)

type clones = {
  cl_local : Sid.t;
346 347
  mutable ty_table : ity Mts.t;
  mutable ts_table : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
348 349 350
  mutable ls_table : lsymbol Mls.t;
  mutable pr_table : prsymbol Mpr.t;
  mutable rn_table : region Mreg.t;
351
  mutable fd_table : pvsymbol Mpv.t;
352
  mutable pv_table : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
353 354 355 356
  mutable rs_table : rsymbol Mrs.t;
  mutable xs_table : xsymbol Mexn.t;
}

357 358
let empty_clones m = {
  cl_local = m.mod_local;
359
  ty_table = Mts.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
360 361 362 363
  ts_table = Mts.empty;
  ls_table = Mls.empty;
  pr_table = Mpr.empty;
  rn_table = Mreg.empty;
364
  fd_table = Mpv.empty;
365
  pv_table = Mvs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
366 367 368 369 370 371
  rs_table = Mrs.empty;
  xs_table = Mexn.empty;
}

(* populate the clone structure *)

372
let rec sm_trans_ty tym tsm ty = match ty.ty_node with
373
  | Tyapp (s, tl) ->
374
      let tl = List.map (sm_trans_ty tym tsm) tl in
375
      begin match Mts.find_opt s tsm with
376 377
      | Some its -> ty_app its.its_ts tl
      | None -> begin match Mts.find_opt s tym with
378 379
      | Some ity -> ty_inst (ts_match_args s tl) (ty_of_ity ity)
      | None -> ty_app s tl
380
      end end
381 382
  | Tyvar _ -> ty

Andrei Paskevich's avatar
Andrei Paskevich committed
383
let clone_ty cl ty = sm_trans_ty cl.ty_table cl.ts_table ty
384

385 386 387
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
388

389 390 391
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
392

Andrei Paskevich's avatar
Andrei Paskevich committed
393
let rec clone_ity cl ity = match ity.ity_node with
394
  | Ityreg r ->
Andrei Paskevich's avatar
Andrei Paskevich committed
395
      ity_reg (clone_reg cl r)
396
  | Ityapp (s, tl, rl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
397
      let tl = List.map (clone_ity cl) tl in
398
      let rl = List.map (clone_ity cl) rl in
399
      begin match Mts.find_opt s.its_ts cl.ts_table with
400 401 402
      | Some its -> ity_app_pure its tl rl
      | None -> (* creative indentation *)
      begin match Mts.find_opt s.its_ts cl.ty_table with
403
      | Some ity -> ity_full_inst (its_match_regs s tl rl) ity
404
      | None -> ity_app_pure s tl rl
405
      end end
Andrei Paskevich's avatar
Andrei Paskevich committed
406 407
  | Ityvar _ -> ity

Andrei Paskevich's avatar
Andrei Paskevich committed
408
and clone_reg cl reg =
409 410 411 412 413
  (* 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
     descending into a let_defn. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
414
  try Mreg.find reg cl.rn_table with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
415
  let tl = List.map (clone_ity cl) reg.reg_args in
416
  let rl = List.map (clone_ity cl) reg.reg_regs in
417
  let r = match Mts.find_opt reg.reg_its.its_ts cl.ts_table with
418 419
    | Some its ->
        create_region (id_clone reg.reg_name) its tl rl
420 421
    | None -> (* creative indentation *)
    begin match Mts.find_opt reg.reg_its.its_ts cl.ty_table with
422 423 424
    | 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
425
        let rl = List.map (ity_full_inst sbs) r.reg_regs in
426
        create_region (id_clone reg.reg_name) r.reg_its tl rl
427
    | Some _ -> assert false
428 429
    | None ->
        create_region (id_clone reg.reg_name) reg.reg_its tl rl
430
    end in
431 432
  cl.rn_table <- Mreg.add reg r cl.rn_table;
  r
Andrei Paskevich's avatar
Andrei Paskevich committed
433 434 435

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
442
let cl_find_pr cl pr =
Andrei Paskevich's avatar
Andrei Paskevich committed
443
  if not (Sid.mem pr.pr_name cl.cl_local) then pr
444
  else Mpr.find pr cl.pr_table
Andrei Paskevich's avatar
Andrei Paskevich committed
445

Andrei Paskevich's avatar
Andrei Paskevich committed
446
let cl_find_pv cl pv =
Andrei Paskevich's avatar
Andrei Paskevich committed
447
  if not (Sid.mem pv.pv_vs.vs_name cl.cl_local) then pv
448
  else Mvs.find pv.pv_vs cl.pv_table
Andrei Paskevich's avatar
Andrei Paskevich committed
449

Andrei Paskevich's avatar
Andrei Paskevich committed
450
let cl_find_rs cl rs =
Andrei Paskevich's avatar
Andrei Paskevich committed
451 452 453
  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
454
let cl_find_xs cl xs =
Andrei Paskevich's avatar
Andrei Paskevich committed
455 456 457
  if not (Sid.mem xs.xs_name cl.cl_local) then xs
  else Mexn.find xs cl.xs_table

Andrei Paskevich's avatar
Andrei Paskevich committed
458
let clone_ls inst cl ls =
Andrei Paskevich's avatar
Andrei Paskevich committed
459 460
  if Mls.mem ls inst.inst_ls then raise (CannotInstantiate ls.ls_name);
  let constr = ls.ls_constr in
461
  let id = id_clone ls.ls_name in
Andrei Paskevich's avatar
Andrei Paskevich committed
462 463
  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
464 465 466 467
  let ls' = create_lsymbol ~constr id at vt in
  cl.ls_table <- Mls.add ls ls' cl.ls_table;
  ls'

468
let cl_init_ty cl ({ts_name = id} as ts) ty =
469
  let its = restore_its ts and ity = ity_of_ty ty in
470 471
  if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
  let stv = Stv.of_list ts.ts_args in
472 473
  if not (Stv.subset (ity_freevars Stv.empty ity) stv &&
    its_pure its && ity_immutable ity) then raise (BadInstance id);
474 475 476 477 478
  cl.ty_table <- Mts.add ts ity cl.ty_table

let cl_init_ts cl ({ts_name = id} as ts) ts' =
  let its = restore_its ts and its' = restore_its ts' in
  if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
479 480
  if not (List.length ts.ts_args = List.length ts'.ts_args &&
    its_pure its && its_pure its') then raise (BadInstance id);
481 482 483 484
  cl.ts_table <- Mts.add its.its_ts its' cl.ts_table

let cl_init_ls cl ({ls_name = id} as ls) ls' =
  if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
Andrei Paskevich's avatar
Andrei Paskevich committed
485
  let mtch sb ty ty' = try ty_match sb ty' (clone_ty cl ty)
486
    with TypeMismatch _ -> raise (BadInstance id) in
Andrei Paskevich's avatar
Andrei Paskevich committed
487
  let sbs = match ls.ls_value,ls'.ls_value with
Andrei Paskevich's avatar
Andrei Paskevich committed
488 489
    | Some ty, Some ty' -> mtch Mtv.empty ty ty'
    | None, None -> Mtv.empty
490
    | _ -> raise (BadInstance id) in
Andrei Paskevich's avatar
Andrei Paskevich committed
491
  ignore (try List.fold_left2 mtch sbs ls.ls_args ls'.ls_args
492
    with Invalid_argument _ -> raise (BadInstance id));
Andrei Paskevich's avatar
Andrei Paskevich committed
493 494
  cl.ls_table <- Mls.add ls ls' cl.ls_table

495 496 497 498 499 500 501 502 503 504
let cl_init_pr cl {pr_name = id} _ =
  if not (Sid.mem id cl.cl_local) then raise (NonLocal id)

let cl_init m inst =
  let cl = empty_clones m in
  Mts.iter (cl_init_ty cl) inst.inst_ty;
  Mts.iter (cl_init_ts cl) inst.inst_ts;
  Mls.iter (cl_init_ls cl) inst.inst_ls;
  Mpr.iter (cl_init_pr cl) inst.inst_pr;
  cl
Andrei Paskevich's avatar
Andrei Paskevich committed
505 506 507

(* clone declarations *)

Andrei Paskevich's avatar
Andrei Paskevich committed
508
let clone_decl inst cl uc d = match d.d_node with
509
  | Dtype _ | Ddata _ -> assert false (* impossible *)
Andrei Paskevich's avatar
Andrei Paskevich committed
510
  | Dparam ls ->
511
      if Mls.mem ls inst.inst_ls then uc else
Andrei Paskevich's avatar
Andrei Paskevich committed
512
      let d = create_param_decl (clone_ls inst cl ls) in
Andrei Paskevich's avatar
Andrei Paskevich committed
513 514
      add_pdecl ~vc:false uc (create_pure_decl d)
  | Dlogic ldl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
515
      let get_ls (ls,_) = ignore (clone_ls inst cl ls) in
Andrei Paskevich's avatar
Andrei Paskevich committed
516
      let get_logic (_,ld) =
Andrei Paskevich's avatar
Andrei Paskevich committed
517
        Opt.get (ls_defn_of_axiom (clone_fmla cl (ls_defn_axiom ld))) in
Andrei Paskevich's avatar
Andrei Paskevich committed
518 519 520 521
      List.iter get_ls ldl;
      let d = create_logic_decl (List.map get_logic ldl) in
      add_pdecl ~vc:false uc (create_pure_decl d)
  | Dind (s, idl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
522
      let get_ls (ls,_) = clone_ls inst cl ls in
Andrei Paskevich's avatar
Andrei Paskevich committed
523
      let get_case (pr,f) =
524
        if Mpr.mem pr inst.inst_pr then raise (CannotInstantiate pr.pr_name);
Andrei Paskevich's avatar
Andrei Paskevich committed
525 526
        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
527
        pr', clone_fmla cl f in
Andrei Paskevich's avatar
Andrei Paskevich committed
528 529 530 531 532
      let get_ind ls (_,la) = ls, List.map get_case la in
      let lls = List.map get_ls idl in
      let d = create_ind_decl s (List.map2 get_ind lls idl) in
      add_pdecl ~vc:false uc (create_pure_decl d)
  | Dprop (k,pr,f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
533
      let skip, k' = match k, Mpr.find_opt pr inst.inst_pr with
534 535 536 537 538
        | 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
539
      if skip then uc else
Andrei Paskevich's avatar
Andrei Paskevich committed
540 541
      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
542
      let d = create_prop_decl k' pr' (clone_fmla cl f) in
Andrei Paskevich's avatar
Andrei Paskevich committed
543 544
      add_pdecl ~vc:false uc (create_pure_decl d)

545 546 547
let cl_save_ls cl s s' =
  cl.ls_table <- Mls.add_new (CannotInstantiate s.ls_name) s s' cl.ls_table

548 549 550
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
551 552 553
  | 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 *)
554 555
  end;
  match s.rs_logic, s'.rs_logic with
556
  | RLls s, RLls s' -> cl_save_ls cl s s'
557 558 559 560
  | RLlemma, RLlemma -> () (* TODO: update cl.pr_table? *)
  | RLnone, RLnone -> ()
  | _ -> assert false

561 562 563 564 565 566 567 568 569 570 571 572 573
let clone_type_decl inst cl tdl =
  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

  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
    let cloned = Mts.mem ts inst.inst_ts || Mts.mem ts inst.inst_ty in
    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 =
574 575
      List.iter2 (cl_save_rs cl) d.itd_constructors itd.itd_constructors;
      List.iter2 (cl_save_rs cl) d.itd_fields itd.itd_fields;
576 577 578 579 580 581 582 583 584 585 586 587 588
      Hits.add htd s (Some itd) in
    (* alias *)
    if s.its_def <> None then begin
      if cloned then raise (CannotInstantiate id);
      let def = conv_ity alg (Opt.get s.its_def) in
      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
    end else
    (* abstract *)
    if d.itd_fields = [] && d.itd_constructors = [] &&
                            d.itd_invariant = [] then begin
      if cloned then Hits.add htd s None else begin
589 590
        let itd = create_plain_record_decl id' ts.ts_args
          ~priv:s.its_private ~mut:s.its_mutable [] [] in
591 592 593 594 595
        cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
        save_itd itd
      end
    end else
    (* variant *)
596 597
    if not s.its_mutable && d.itd_constructors <> [] &&
                            d.itd_invariant = [] then begin
598 599 600 601 602 603 604 605 606 607 608 609 610 611
      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 ->
612
          let itd = create_plain_variant_decl id' ts.ts_args csl in
613 614 615 616 617 618 619 620 621 622
          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
623 624
        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
625
        List.map (clone_term cl mv) d.itd_invariant in
626 627
      let itd = create_plain_record_decl id' ts.ts_args
        ~priv:s.its_private ~mut:s.its_mutable fdl inv in
628 629 630 631 632 633 634
      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}
635
      | Ityapp (s,tl,_) ->
636 637 638
          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
639 640
            let s' = create_rec_itysymbol id s.its_ts.ts_args in
            cl.ts_table <- Mts.add s.its_ts s' cl.ts_table
641 642 643 644
          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
645
    clone_ity cl ity in
646 647 648 649

  Mits.iter (visit Sits.empty) def;
  Lists.map_filter (fun d -> Hits.find htd d.itd_its) tdl

650 651 652 653 654 655 656 657 658 659 660
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 }

661 662 663 664 665
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 }

666 667 668 669 670 671 672 673
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
674
  | RLls s, RLls s' -> cl_save_ls cl s s'; sm
675 676 677
  | RLpv v, RLpv v' -> sm_save_pv sm v v'
  | _ -> sm

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

681
let clone_pv cl {pv_vs = vs; pv_ity = ity; pv_ghost = ghost} =
Andrei Paskevich's avatar
Andrei Paskevich committed
682
  create_pvsymbol (id_clone vs.vs_name) ~ghost (clone_ity cl ity)
683 684

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

687
let clone_varl cl sm varl = List.map (fun (t,r) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
688
  clone_term cl sm.sm_vs t, Opt.map (cl_find_ls cl) r) varl
689 690

let clone_cty cl sm cty =
691
  let res = clone_ity cl cty.cty_result in
692
  let args = List.map (clone_pv cl) cty.cty_args in
693
  let sm_args = List.fold_left2 sm_save_pv sm cty.cty_args args in
694
  let add_old o n (sm, olds) = let o' = clone_pv cl o in
695
    sm_save_pv sm o o', Mpv.add o' (sm_find_pv sm_args n) olds in
696
  let sm_olds, olds = Mpv.fold add_old cty.cty_oldies (sm_args, Mpv.empty) in
697 698 699 700 701 702
  let pre = clone_invl cl sm_args cty.cty_pre in
  let post = clone_invl cl sm_olds cty.cty_post in
  let xpost = Mexn.fold (fun xs fl q ->
    let xs = cl_find_xs cl xs in
    let fl = clone_invl cl sm_olds fl in
    Mexn.add xs fl q) cty.cty_xpost Mexn.empty in
703
  let add_read v s = Spv.add (sm_find_pv sm_args v) s in
704 705 706
  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
707
  let add_write reg fs m =
708
    let add_fd fd s = Spv.add (Mpv.find_def fd fd cl.fd_table) s in
Andrei Paskevich's avatar
Andrei Paskevich committed
709
    Mreg.add (clone_reg cl reg) (Spv.fold add_fd fs Spv.empty) m in
710
  let writes = Mreg.fold add_write cty.cty_effect.eff_writes Mreg.empty in
Andrei Paskevich's avatar
Andrei Paskevich committed
711
  let add_reset reg s = Sreg.add (clone_reg cl reg) s in
712 713 714 715 716
  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
  let eff = Sexn.fold add_raise cty.cty_effect.eff_raises eff in
  let eff = if cty.cty_effect.eff_oneway then eff_diverge eff else eff in
717 718
  let cty = create_cty ~mask:cty.cty_mask args pre post xpost olds eff res in
  cty_ghostify (cty_ghost cty) cty
719 720 721 722 723

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' =
724 725
  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
726 727 728 729 730 731 732 733 734
  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

735
let clone_ppat cl sm pp mask =
736 737
  let rec conv_pat p = match p.pat_node with
    | Term.Pwild -> PPwild
738 739 740
    | 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)
741 742 743 744
    | 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
745
  let vm, pp' = create_prog_pattern pre (clone_ity cl pp.pp_ity) mask in
746 747 748
  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'

749
let rec clone_expr cl sm e = e_label_copy e (match e.e_node with
750
  | Evar v -> e_var (sm_find_pv sm v)
751
  | Econst c -> e_const c
752
  | Eexec (c,_) -> e_exec (clone_cexp cl sm c)
753 754 755 756
  | 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)
757 758 759 760 761
  | 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)
762
  | Ecase (d, bl) ->
763
      let d = clone_expr cl sm d in
764
      let conv_br (pp, e) =
765
        let sm, pp = clone_ppat cl sm pp d.e_mask in
766
        pp, clone_expr cl sm e in
767
      e_case d (List.map conv_br bl)
768 769 770 771 772 773 774 775 776 777
  | 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) ->
778 779 780 781 782
      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
        Mexn.add (cl_find_xs cl xs) (vl', clone_expr cl sm e) m in
      e_try (clone_expr cl sm d) (Mexn.fold conv_br xl Mexn.empty)
783
  | Eraise (xs, e) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
784
      e_raise (cl_find_xs cl xs) (clone_expr cl sm e) (clone_ity cl e.e_ity)
785
  | Eassert (k, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
786
      e_assert k (clone_term cl sm.sm_vs f)
787 788
  | Eghost e ->
      e_ghostify true (clone_expr cl sm e)
789
  | Epure t ->
Andrei Paskevich's avatar
Andrei Paskevich committed
790
      e_pure (clone_term cl sm.sm_vs t)
791
  | Eabsurd -> e_absurd (clone_ity cl e.e_ity))
792

793
and clone_cexp cl sm c = match c.c_node with
794
  | Capp (s,vl) ->
795
      let vl = List.map (fun v -> sm_find_pv sm v) vl in
Andrei Paskevich's avatar
Andrei Paskevich committed
796 797
      let al = List.map (fun v -> clone_ity cl v.pv_ity) c.c_cty.cty_args in
      let res = clone_ity cl c.c_cty.cty_result in
798
      c_app (Mrs.find_def s s sm.sm_rs) vl al res
799 800 801 802 803
  | Cpur (s,vl) ->
      let vl = List.map (fun v -> sm_find_pv sm v) vl in
      let al = List.map (fun v -> clone_ity cl v.pv_ity) c.c_cty.cty_args in
      let res = clone_ity cl c.c_cty.cty_result in
      c_pur (cl_find_ls cl s) vl al res
804 805 806 807
  | Cfun e ->
      let cty = clone_cty cl sm c.c_cty in
      let sm = sm_save_args sm c.c_cty cty in
      let sm = sm_save_olds sm c.c_cty cty in
808 809
      c_fun ~mask:cty.cty_mask cty.cty_args cty.cty_pre
        cty.cty_post cty.cty_xpost cty.cty_oldies (clone_expr cl sm e)
810
  | Cany ->
811
      c_any (clone_cty cl sm c.c_cty)
812 813 814 815

and clone_let_defn cl sm ld = match ld with
  | LDvar (v,e) ->
      let e' = clone_expr cl sm e in
816 817
      let id = id_clone v.pv_vs.vs_name in
      let ld, v' = let_var id ~ghost:v.pv_ghost e' in
818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839
      sm_save_pv sm v v', ld
  | LDsym (s,c) ->
      let c' = clone_cexp cl sm c in
      let ld, s' = let_sym (id_clone s.rs_name)
        ~ghost:(rs_ghost s) ~kind:(rs_kind s) c' in
      sm_save_rs cl sm s s', ld
  | LDrec rdl ->
      let conv_rs mrs {rec_rsym = rs} =
        let rs' = create_rsymbol (id_clone rs.rs_name)
          ~ghost:(rs_ghost rs) (clone_cty cl sm rs.rs_cty) in
        Mrs.add rs rs' mrs, rs' in
      let mrs, rsyml = Lists.map_fold_left conv_rs sm.sm_rs rdl in
      let rsm = { sm with sm_rs = mrs } in
      let conv_rd ({rec_fun = c} as rd) ({rs_cty = cty} as rs) =
        let pre = if rd.rec_varl = [] then cty.cty_pre
          else List.tl cty.cty_pre (* remove DECR *) in
        let rsm = sm_save_args rsm c.c_cty cty in
        let varl = clone_varl cl rsm rd.rec_varl in
        let rsm = sm_save_olds rsm c.c_cty cty in
        let e = match c.c_node with
          | Cfun e -> clone_expr cl rsm e
          | _ -> assert false (* can't be *) in
840 841
        let c = c_fun ~mask:c.c_cty.cty_mask cty.cty_args
          pre cty.cty_post cty.cty_xpost cty.cty_oldies e in
842 843 844 845 846 847
        rs, c, varl, rs_kind rd.rec_sym in
      let ld, rdl' = let_rec (List.map2 conv_rd rdl rsyml) in
      let sm = List.fold_left2 (fun sm d d' ->
        sm_save_rs cl sm d.rec_sym d'.rec_sym) sm rdl rdl' in
      sm, ld

Andrei Paskevich's avatar
Andrei Paskevich committed
848
let clone_pdecl inst cl uc d = match d.pd_node with
849 850 851 852
  | PDtype tdl ->
      let tdl = clone_type_decl inst cl tdl in
      if tdl = [] then uc else
      add_pdecl ~vc:false uc (create_type_decl tdl)
853 854 855 856 857 858
  | PDlet ld ->
      let reads = match ld with
        | LDvar (_,e) -> e.e_effect.eff_reads
        | LDsym (_,c) -> cty_reads c.c_cty
        | LDrec rdl -> List.fold_left (fun spv {rec_rsym = s} ->
            Spv.union spv (cty_reads s.rs_cty)) Spv.empty rdl in
859 860 861
      let frz = Spv.fold (fun v isb ->
        if Sid.mem v.pv_vs.vs_name cl.cl_local then isb
        else ity_freeze isb v.pv_ity) reads isb_empty in
862 863 864
      let frz = Mreg.map (fun ity -> match ity.ity_node with
        | Ityreg r -> r | _ -> assert false) frz.isb_reg in
      cl.rn_table <- Mreg.set_union cl.rn_table frz;
865 866
      let sm, ld = clone_let_defn cl (sm_of_cl cl) ld in
      cl.pv_table <- sm.sm_pv; cl.rs_table <- sm.sm_rs;
867
      add_pdecl ~vc:false uc (create_let_decl ld)
Andrei Paskevich's avatar
Andrei Paskevich committed
868
  | PDexn xs ->
869
      let id = id_clone xs.xs_name in
Andrei Paskevich's avatar
Andrei Paskevich committed
870
      let ity = clone_ity cl xs.xs_ity in
871
      let xs' = create_xsymbol id ~mask:xs.xs_mask ity in
Andrei Paskevich's avatar
Andrei Paskevich committed
872 873 874 875 876
      cl.xs_table <- Mexn.add xs xs' cl.xs_table;
      add_pdecl ~vc:false uc (create_exn_decl xs')
  | PDpure ->
      List.fold_left (clone_decl inst cl) uc d.pd_pure

Andrei Paskevich's avatar
Andrei Paskevich committed
877 878
let theory_add_clone = Theory.add_clone_internal ()

Andrei Paskevich's avatar
Andrei Paskevich committed
879
let add_clone uc mi =
880 881 882 883 884
  let sm = {
    sm_ty = Mts.map ty_of_ity mi.mi_ty;
    sm_ts = Mts.map (fun s -> s.its_ts) mi.mi_ts;
    sm_ls = mi.mi_ls;
    sm_pr = mi.mi_pr } in
Andrei Paskevich's avatar
Andrei Paskevich committed
885
  { uc with
886
      muc_theory = theory_add_clone uc.muc_theory mi.mi_mod.mod_theory sm;
Andrei Paskevich's avatar
Andrei Paskevich committed
887
      muc_units  = Uclone mi :: uc.muc_units }
Andrei Paskevich's avatar
Andrei Paskevich committed
888 889

let clone_export uc m inst =
890
  let cl = cl_init m inst in
Andrei Paskevich's avatar
Andrei Paskevich committed
891 892 893 894
  let<