pmodule.ml 45.8 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
  | Umeta  of meta * meta_arg list
164
  | Uscope of string * mod_unit list
Andrei Paskevich's avatar
Andrei Paskevich committed
165

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;
231
      muc_units  = [Uscope (s, 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
239
  | [Uscope (_,ul1)], _ :: sti, _ :: ste -> (* empty scope *)
Andrei Paskevich's avatar
Andrei Paskevich committed
240 241
      { uc with muc_theory = th;  muc_units  = ul1;
                muc_import = sti; muc_export = ste; }
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;
248
          muc_units  = Uscope (s,ul0) :: ul1;
249 250
          muc_import = i1 :: sti;
          muc_export = e1 :: ste; }
Andrei Paskevich's avatar
Andrei Paskevich committed
251
  | _ -> assert false
252

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

Andrei Paskevich's avatar
Andrei Paskevich committed
274 275 276
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; }
277

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

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

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

351
let add_pdecl_raw ?(warn=true) uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
352
  let uc = add_pdecl_no_logic uc d in
353
  let th = List.fold_left (add_decl ~warn) uc.muc_theory d.pd_pure in
354 355
  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
356 357
  { uc with muc_theory = th }

358 359
(** {2 Builtin symbols} *)

Andrei Paskevich's avatar
Andrei Paskevich committed
360 361
let dummy_env = Env.create_env []

362
let builtin_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
363 364 365 366
  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
367 368
  let m = close_module uc in
  { m with mod_theory = builtin_theory }
369 370

let bool_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
371 372
  let uc = empty_module dummy_env (id_fresh "Bool") ["why3";"Bool"] in
  let uc = add_pdecl_no_logic uc pd_bool in
373 374
  let m = close_module uc in
  { m with mod_theory = bool_theory }
375 376

let highord_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
377 378 379
  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
380 381
  let m = close_module uc in
  { m with mod_theory = highord_theory }
382

383 384
let tuple_module = Hint.memo 17 (fun n ->
  let nm = "Tuple" ^ string_of_int n in
Andrei Paskevich's avatar
Andrei Paskevich committed
385 386
  let uc = empty_module dummy_env (id_fresh nm) ["why3";nm] in
  let uc = add_pdecl_no_logic uc (pd_tuple n) in
387 388
  let m = close_module uc in
  { m with mod_theory = tuple_theory n })
389 390

let unit_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
391
  let uc = empty_module dummy_env (id_fresh "Unit") ["why3";"Unit"] in
392
  let uc = use_export uc (tuple_module 0) in
393
  let add uc d = add_pdecl_raw ~warn:false uc d in
394
  let td = create_alias_decl (id_fresh "unit") [] ity_unit in
395
  close_module (List.fold_left add uc (create_type_decl [td]))
396 397

let create_module env ?(path=[]) n =
Andrei Paskevich's avatar
Andrei Paskevich committed
398
  let m = empty_module env n path in
399 400 401 402 403
  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
404 405 406 407 408 409 410
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

411 412
let mk_vc uc d = Vc.vc uc.muc_env uc.muc_known uc.muc_theory d

413
let add_pdecl ?(warn=true) ~vc uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
414
  let uc = add_use uc d in
415
  let dl = if vc then mk_vc uc d else [] in
416 417 418 419
  (* 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. *)
420
  add_pdecl_raw ~warn (List.fold_left (add_pdecl_raw ~warn) uc dl) d
421

Andrei Paskevich's avatar
Andrei Paskevich committed
422 423 424 425
(** {2 Cloning} *)

type clones = {
  cl_local : Sid.t;
426 427
  mutable ty_table : ity Mts.t;
  mutable ts_table : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
428 429 430
  mutable ls_table : lsymbol Mls.t;
  mutable pr_table : prsymbol Mpr.t;
  mutable rn_table : region Mreg.t;
431
  mutable fd_table : pvsymbol Mpv.t;
432
  mutable pv_table : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
433
  mutable rs_table : rsymbol Mrs.t;
434
  mutable xs_table : xsymbol Mxs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
435 436
}

437 438
let empty_clones m = {
  cl_local = m.mod_local;
439
  ty_table = Mts.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
440 441 442 443
  ts_table = Mts.empty;
  ls_table = Mls.empty;
  pr_table = Mpr.empty;
  rn_table = Mreg.empty;
444
  fd_table = Mpv.empty;
445
  pv_table = Mvs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
446
  rs_table = Mrs.empty;
447
  xs_table = Mxs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
448 449 450 451
}

(* populate the clone structure *)

452
let rec sm_trans_ty tym tsm ty = match ty.ty_node with
453
  | Tyapp (s, tl) ->
454
      let tl = List.map (sm_trans_ty tym tsm) tl in
455
      begin match Mts.find_opt s tsm with
456 457
      | Some its -> ty_app its.its_ts tl
      | None -> begin match Mts.find_opt s tym with
458 459
      | Some ity -> ty_inst (ts_match_args s tl) (ty_of_ity ity)
      | None -> ty_app s tl
460
      end end
461 462
  | Tyvar _ -> ty

Andrei Paskevich's avatar
Andrei Paskevich committed
463
let clone_ty cl ty = sm_trans_ty cl.ty_table cl.ts_table ty
464

465 466 467
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
468

469 470 471
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
472

Andrei Paskevich's avatar
Andrei Paskevich committed
473
let rec clone_ity cl ity = match ity.ity_node with
474
  | Ityreg r ->
Andrei Paskevich's avatar
Andrei Paskevich committed
475
      ity_reg (clone_reg cl r)
476
  | Ityapp (s, tl, rl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
477
      let tl = List.map (clone_ity cl) tl in
478
      let rl = List.map (clone_ity cl) rl in
479
      begin match Mts.find_opt s.its_ts cl.ts_table with
480 481 482
      | Some its -> ity_app_pure its tl rl
      | None -> (* creative indentation *)
      begin match Mts.find_opt s.its_ts cl.ty_table with
483
      | Some ity -> ity_full_inst (its_match_regs s tl rl) ity
484
      | None -> ity_app_pure s tl rl
485
      end end
Andrei Paskevich's avatar
Andrei Paskevich committed
486 487
  | Ityvar _ -> ity

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
524
let cl_find_pr cl pr =
Andrei Paskevich's avatar
Andrei Paskevich committed
525
  if not (Sid.mem pr.pr_name cl.cl_local) then pr
526
  else Mpr.find pr cl.pr_table
Andrei Paskevich's avatar
Andrei Paskevich committed
527

Andrei Paskevich's avatar
Andrei Paskevich committed
528
let cl_find_pv cl pv =
Andrei Paskevich's avatar
Andrei Paskevich committed
529
  if not (Sid.mem pv.pv_vs.vs_name cl.cl_local) then pv
530
  else Mvs.find pv.pv_vs cl.pv_table
Andrei Paskevich's avatar
Andrei Paskevich committed
531

Andrei Paskevich's avatar
Andrei Paskevich committed
532
let cl_find_rs cl rs =
Andrei Paskevich's avatar
Andrei Paskevich committed
533 534 535
  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
536
let cl_find_xs cl xs =
Andrei Paskevich's avatar
Andrei Paskevich committed
537
  if not (Sid.mem xs.xs_name cl.cl_local) then xs
538
  else Mxs.find xs cl.xs_table
Andrei Paskevich's avatar
Andrei Paskevich committed
539

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

629 630 631
let cl_save_ls cl s s' =
  cl.ls_table <- Mls.add_new (CannotInstantiate s.ls_name) s s' cl.ls_table

632 633 634
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
635 636 637
  | 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 *)
638 639
  end;
  match s.rs_logic, s'.rs_logic with
640
  | RLls s, RLls s' -> cl_save_ls cl s s'
641 642 643 644
  | RLlemma, RLlemma -> () (* TODO: update cl.pr_table? *)
  | RLnone, RLnone -> ()
  | _ -> assert false

Mário Pereira's avatar
Mário Pereira committed
645 646 647
type smap = {
  sm_vs : vsymbol Mvs.t;
  sm_pv : pvsymbol Mvs.t;
648
  sm_xs : xsymbol Mxs.t;
Mário Pereira's avatar
Mário Pereira committed
649 650 651 652 653 654
  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;
655
  sm_xs = cl.xs_table;
Mário Pereira's avatar
Mário Pereira committed
656 657 658 659 660
  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;
661
  sm_xs = sm.sm_xs;
Mário Pereira's avatar
Mário Pereira committed
662 663 664 665 666
  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;
667
  sm_xs = sm.sm_xs;
Mário Pereira's avatar
Mário Pereira committed
668 669
  sm_rs = sm.sm_rs }

670 671 672
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
673 674 675 676 677 678 679 680 681 682
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 *)

683 684 685 686
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
687 688 689 690 691 692
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
693 694 695
let clone_type_record cl s d s' d' =
  let id = s.its_ts.ts_name in
  let fields' = Hstr.create 16 in
696
  let add_field' rs' = let pj' = fd_of_rs rs' in
Mário Pereira's avatar
Mário Pereira committed
697 698 699
    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 *)
700
  let match_pj rs = let pj = fd_of_rs rs in
Mário Pereira's avatar
Mário Pereira committed
701 702 703 704 705
    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
706
    let pj' = fd_of_rs rs' in
Mário Pereira's avatar
Mário Pereira committed
707 708 709 710 711 712 713 714 715 716
    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
717

Mário Pereira's avatar
Mário Pereira committed
718
let clone_type_decl inst cl tdl kn =
719 720 721
  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
722
  let vcs = ref ([] : (itysymbol * term) list) in
723 724 725 726
  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
727
    let cloned = Mts.mem ts inst.mi_ts || Mts.mem ts inst.mi_ty in
728 729 730
    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 =
731 732
      List.iter2 (cl_save_rs cl) d.itd_constructors itd.itd_constructors;
      List.iter2 (cl_save_rs cl) d.itd_fields itd.itd_fields;
733 734
      Hits.add htd s (Some itd) in
    (* alias *)
735
    if s.its_def <> NoDef then begin
736
      if cloned then raise (CannotInstantiate id);
737 738 739 740 741
      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
742 743
      cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
      save_itd itd
744
    end else
745
    (* abstract *)
746
    if s.its_private && cloned then begin
747 748 749 750
      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
751
          let pd' = Mid.find s'.its_ts.ts_name kn in
752
          let d' = match pd'.pd_node with
Mário Pereira's avatar
Mário Pereira committed
753
            | PDtype [d'] -> d'
754 755 756
            (* 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
757
          clone_type_record cl s d s' d'; (* clone record fields *)
Mário Pereira's avatar
Mário Pereira committed
758
          (* generate and add VC for type invariant implication *)
759 760 761
          if d.itd_invariant <> [] then begin
            let inv = axiom_of_invariant d in
            let invl = clone_invl cl (sm_of_cl cl) [inv] in
762
            let add_vc inv = vcs := (d.itd_its, inv) :: !vcs in
763
            List.iter add_vc invl end
764
      | None -> begin match Mts.find_opt ts inst.mi_ty with
Mário Pereira's avatar
Mário Pereira committed
765
      | Some ity -> (* creative indentation *)
766 767 768
          (* TODO: clone_type_record, axiom_of_invariant *)
          (* TODO: should we only allow cloning into ity for
             private types with no fields and no invariant? *)
769 770
          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
771
                  its_pure s && ity_immutable ity) then raise (BadInstance id);
772 773
          cl.ty_table <- Mts.add ts ity cl.ty_table
      | None -> assert false end end;
774 775
      Hits.add htd s None;
      (* TODO: check typing conditions for refined record type *)
776 777
    end else
    (* variant *)
778 779
    if not s.its_mutable && d.itd_constructors <> [] &&
                            d.itd_invariant = [] then begin
780 781
      if cloned then raise (CannotInstantiate id);
      let conv_fd m fd =
782
        let v = fd_of_rs fd in Mpv.add v (conv_pj v) m in
783 784 785 786 787 788 789 790 791 792 793
      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 ->
794
          let itd = create_plain_variant_decl id' ts.ts_args csl in
795 796 797 798 799 800
          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
801
      let pjl = List.map fd_of_rs d.itd_fields in
802 803 804
      let fdl = List.map (fun v -> Spv.mem v mfld, conv_pj v) pjl in
      let inv =
        if d.itd_invariant = [] then [] else
805 806
        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
807
        List.map (clone_term cl mv) d.itd_invariant in
808 809
      let itd = create_plain_record_decl id' ts.ts_args
        ~priv:s.its_private ~mut:s.its_mutable fdl inv in
810 811 812
      cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
      save_itd itd
    end
813

814 815 816
  and conv_ity alg ity =
    let rec down ity = match ity.ity_node with
      | Ityreg {reg_its = s; reg_args = tl}
817
      | Ityapp (s,tl,_) ->
818 819 820
          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
821 822
            let s' = create_rec_itysymbol id s.its_ts.ts_args in
            cl.ts_table <- Mts.add s.its_ts s' cl.ts_table
823 824 825 826
          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
827
    clone_ity cl ity in
828 829

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

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

836
let clone_cty cl sm ?(drop_decr=false) cty =
837
  let res = clone_ity cl cty.cty_result in
838
  let args = List.map (clone_pv cl) cty.cty_args in
839
  let sm_args = List.fold_left2 sm_save_pv sm cty.cty_args args in
840
  let add_old o n (sm, olds) = let o' = clone_pv cl o in
841
    sm_save_pv sm o o', Mpv.add o' (sm_find_pv sm_args n) olds in
842
  let sm_olds, olds = Mpv.fold add_old cty.cty_oldies (sm_args, Mpv.empty) in
843 844
  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
845
  let post = clone_invl cl sm_olds cty.cty_post in
846
  let xpost = Mxs.fold (fun xs fl q ->
847
    let xs = sm_find_xs sm xs in
848
    let fl = clone_invl cl sm_olds fl in
849
    Mxs.add xs fl q) cty.cty_xpost Mxs.empty in
850
  let add_read v s = Spv.add (sm_find_pv sm_args v) s in
851 852 853
  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
854
  let add_write reg fs m = (* add new mutable fields to functions effect *)
855
    let add_fd fd s = Spv.add (Mpv.find_def fd fd cl.fd_table) s in
856
    let reg' = clone_reg cl reg in
Mário Pereira's avatar
Mário Pereira committed
857 858
    let smf_reg' = Spv.of_list reg'.reg_its.its_mfields in
    let smf_reg = Spv.of_list reg.reg_its.its_mfields in
859 860
    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
861
    let fs = Spv.fold add_fd fs Spv.empty in
862
    Mreg.add reg' (Spv.union fs smf_new) m in
863
  let writes = Mreg.fold add_write cty.cty_effect.eff_writes Mreg.empty in
Andrei Paskevich's avatar
Andrei Paskevich committed
864
  let add_reset reg s = Sreg.add (clone_reg cl reg) s in
865 866
  let resets = Sreg.fold add_reset cty.cty_effect.eff_resets Sreg.empty in
  let eff = eff_reset (eff_write reads writes) resets in
867
  let add_raise xs eff = eff_raise eff (sm_find_xs sm xs) in
868
  let eff = Sxs.fold add_raise cty.cty_effect.eff_raises eff in
869
  let eff = if cty.cty_effect.eff_oneway then eff_diverge eff else eff in
870 871
  let cty = create_cty ~mask:cty.cty_mask args pre post xpost olds eff res in
  cty_ghostify (cty_ghost cty) cty
872 873 874 875 876

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' =
877