pmodule.ml

(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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 Wstdlib
open Ident
open Ty
open Term
open Decl
open Theory
open Ity
open Expr
open Pdecl

(** *)

type prog_symbol =
  | PV of pvsymbol
  | RS of rsymbol
  | OO of Srs.t

type namespace = {
  ns_ts : itysymbol   Mstr.t;  (* type symbols *)
  ns_ps : prog_symbol Mstr.t;  (* program symbols *)
  ns_xs : xsymbol     Mstr.t;  (* exception symbols *)
  ns_ns : namespace   Mstr.t;  (* inner namespaces *)
}

let empty_ns = {
  ns_ts = Mstr.empty;
  ns_ps = Mstr.empty;
  ns_xs = Mstr.empty;
  ns_ns = Mstr.empty;
}

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

let merge_ts = ns_replace its_equal
let merge_xs = ns_replace xs_equal

type overload =
  | FixedRes of ity (* t -> t -> ... -> T *)
  | SameType        (* t -> t -> ... -> t *)
  | NoOver          (* neither *)

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

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

exception IncompatibleNotation of string

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 ->
        if rs_equal r1 r2 then vo else
        if not (same_overload r1 r2) then vn else
        if ity_equal (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 ->
        if Srs.mem r2 s1 then vo else
        let r1 = Srs.choose s1 in
        if not (same_overload r1 r2) then vn else
        let ty = fsty r2 in
        let confl r = not (ity_equal (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

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 }

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

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

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_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

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

type pmodule = {
  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
  | Uclone of mod_inst
  | Umeta  of meta * meta_arg list
  | Uscope of string * mod_unit list

and mod_inst = {
  mi_mod : pmodule;
  mi_ty  : ity Mts.t;
  mi_ts  : itysymbol Mts.t;
  mi_ls  : lsymbol Mls.t;
  mi_pr  : prsymbol Mpr.t;
  mi_pk  : prop_kind Mpr.t;
  mi_pv  : pvsymbol Mvs.t;
  mi_rs  : rsymbol Mrs.t;
  mi_xs  : xsymbol Mxs.t;
  mi_df  : prop_kind;
}

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;
  mi_xs  = Mxs.empty;
  mi_df  = Plemma;
}

(** {2 Module under construction} *)

type pmodule_uc = {
  muc_theory : theory_uc;
  muc_units  : mod_unit list;
  muc_import : namespace list;
  muc_export : namespace list;
  muc_known  : known_map;
  muc_local  : Sid.t;
  muc_used   : Sid.t;
  muc_env    : Env.env;
}

let empty_module env n p = {
  muc_theory = create_theory ~path:p n;
  muc_units  = [];
  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;
               mod_units  = List.rev uc.muc_units;
               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)

let open_scope uc s = match uc.muc_import with
  | ns :: _ -> { uc with
      muc_theory = Theory.open_scope uc.muc_theory s;
      muc_units  = [Uscope (s, uc.muc_units)];
      muc_import =       ns :: uc.muc_import;
      muc_export = empty_ns :: uc.muc_export; }
  | [] -> assert false

let close_scope uc ~import =
  let th = Theory.close_scope uc.muc_theory ~import in
  match List.rev uc.muc_units, uc.muc_import, uc.muc_export with
  | [Uscope (_,ul1)], _ :: sti, _ :: ste -> (* empty scope *)
      { uc with muc_theory = th;  muc_units  = ul1;
                muc_import = sti; muc_export = ste; }
  | Uscope (s,ul1) :: ul0, _ :: i1 :: sti, e0 :: e1 :: ste ->
      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
          muc_theory = th;
          muc_units  = Uscope (s,ul0) :: ul1;
          muc_import = i1 :: sti;
          muc_export = e1 :: ste; }
  | _ -> assert false

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

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
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_theory = th;
      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; }
  | _ -> assert false

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; }

let store_path, store_module, restore_path =
  let id_to_path = Wid.create 17 in
  let store_path {muc_theory = uc} path id =
    (* this symbol already belongs to some theory *)
    if Wid.mem id_to_path id then () else
    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} =
    (* this symbol is already a module *)
    if Wid.mem id_to_path id then () else
    Wid.set id_to_path id (th.th_path, id.id_string, []) in
  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

(*
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
  let rec down mr ity = if ity.ity_imm then mr else
    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
    | Ityvar _ -> assert false
  and fields mr s tl rl =
    if s.its_private && rl = [] then mr else
    let isb = its_match_regs s tl rl in
    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
*)

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

let add_pdecl_no_logic uc d =
  let uc = { uc with
    muc_units = Udecl d :: uc.muc_units;
    muc_known = known_add_decl uc.muc_known d;
    muc_local = Sid.union uc.muc_local d.pd_news } in
  let add_rs uc s = add_symbol add_ps s.rs_name (RS s) uc in
  let add_rd uc d = add_rs uc d.rec_sym in
  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
  | PDlet (LDsym (s,_)) -> add_rs uc s
  | PDlet (LDrec l) -> List.fold_left add_rd uc l
  | PDexn xs -> add_symbol add_xs xs.xs_name xs uc
  | PDpure -> uc

let add_pdecl_raw ?(warn=true) uc d =
  let uc = add_pdecl_no_logic uc d in
  let th = List.fold_left (add_decl ~warn) uc.muc_theory d.pd_pure in
  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
  { uc with muc_theory = th }

(** {2 Builtin symbols} *)

let dummy_env = Env.create_env []

let builtin_module =
  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
  let m = close_module uc in
  { m with mod_theory = builtin_theory }

let bool_module =
  let uc = empty_module dummy_env (id_fresh "Bool") ["why3";"Bool"] in
  let uc = add_pdecl_no_logic uc pd_bool in
  let m = close_module uc in
  { m with mod_theory = bool_theory }

let highord_module =
  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
  let m = close_module uc in
  { m with mod_theory = highord_theory }

let tuple_module = Hint.memo 17 (fun n ->
  let nm = "Tuple" ^ string_of_int n in
  let uc = empty_module dummy_env (id_fresh nm) ["why3";nm] in
  let uc = add_pdecl_no_logic uc (pd_tuple n) in
  let m = close_module uc in
  { m with mod_theory = tuple_theory n })

let unit_module =
  let uc = empty_module dummy_env (id_fresh "Unit") ["why3";"Unit"] in
  let uc = use_export uc (tuple_module 0) in
  let add uc d = add_pdecl_raw ~warn:false uc d in
  let td = create_alias_decl (id_fresh "unit") [] ity_unit in
  close_module (List.fold_left add uc (create_type_decl [td]))

let create_module env ?(path=[]) n =
  let m = empty_module env n path in
  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

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

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

let add_pdecl ?(warn=true) ~vc uc d =
  let uc = add_use uc d in
  let dl = if vc then mk_vc uc d else [] in
  (* 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_raw ~warn (List.fold_left (add_pdecl_raw ~warn) uc dl) d

(** {2 Cloning} *)

type clones = {
  cl_local : Sid.t;
  mutable ty_table : ity Mts.t;
  mutable ts_table : itysymbol Mts.t;
  mutable ls_table : lsymbol Mls.t;
  mutable pr_table : prsymbol Mpr.t;
  mutable rn_table : region Mreg.t;
  mutable fd_table : pvsymbol Mpv.t;
  mutable pv_table : pvsymbol Mvs.t;
  mutable rs_table : rsymbol Mrs.t;
  mutable xs_table : xsymbol Mxs.t;
}

let empty_clones m = {
  cl_local = m.mod_local;
  ty_table = Mts.empty;
  ts_table = Mts.empty;
  ls_table = Mls.empty;
  pr_table = Mpr.empty;
  rn_table = Mreg.empty;
  fd_table = Mpv.empty;
  pv_table = Mvs.empty;
  rs_table = Mrs.empty;
  xs_table = Mxs.empty;
}

exception CloneDivergence of ident * ident

(* populate the clone structure *)

let rec sm_trans_ty tym tsm ty = match ty.ty_node with
  | Tyapp (s, tl) ->
      let tl = List.map (sm_trans_ty tym tsm) tl in
      begin match Mts.find_opt s tsm with
      | Some its -> ty_app its.its_ts tl
      | None -> begin match Mts.find_opt s tym with
      | Some ity -> ty_inst (ts_match_args s tl) (ty_of_ity ity)
      | None -> ty_app s tl
      end end
  | Tyvar _ -> ty

let clone_ty cl ty = sm_trans_ty cl.ty_table cl.ts_table ty

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

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

let rec clone_ity cl ity = match ity.ity_node with
  | Ityreg r ->
      ity_reg (clone_reg cl r)
  | Ityapp (s, tl, rl) ->
      let tl = List.map (clone_ity cl) tl in
      let rl = List.map (clone_ity cl) rl in
      begin match Mts.find_opt s.its_ts cl.ts_table with
      | Some its -> ity_app_pure its tl rl
      | None -> (* creative indentation *)
      begin match Mts.find_opt s.its_ts cl.ty_table with
      | Some ity -> ity_full_inst (its_match_regs s tl rl) ity
      | None -> ity_app_pure s tl rl
      end end
  | Ityvar _ -> ity

and clone_reg cl reg =
  (* 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.
     TODO: add to module/uc a list of locally-defined toplevel
     variables, as well as a set of imported toplevel variables. *)
  try Mreg.find reg cl.rn_table with Not_found ->
  let tl = List.map (clone_ity cl) reg.reg_args in
  let rl = List.map (clone_ity cl) reg.reg_regs in
  let r = match Mts.find_opt reg.reg_its.its_ts cl.ts_table with
    | Some its ->
        create_region (id_clone reg.reg_name) its tl rl
    | None -> (* creative indentation *)
    begin match Mts.find_opt reg.reg_its.its_ts cl.ty_table with
    | 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
        let rl = List.map (ity_full_inst sbs) r.reg_regs in
        create_region (id_clone reg.reg_name) r.reg_its tl rl
    | Some _ -> assert false
    | None ->
        create_region (id_clone reg.reg_name) reg.reg_its tl rl
    end in
  cl.rn_table <- Mreg.add reg r cl.rn_table;
  r

let cl_find_ls cl ls =
  if not (Sid.mem ls.ls_name cl.cl_local) then ls
  else Mls.find ls cl.ls_table

let clone_term cl mv t = t_gen_map (clone_ty cl) (cl_find_ls cl) mv t

let clone_fmla cl f = clone_term cl Mvs.empty f (* for closed terms *)

let cl_find_pr cl pr =
  if not (Sid.mem pr.pr_name cl.cl_local) then pr
  else Mpr.find pr cl.pr_table

let cl_find_pv cl pv =
  if not (Sid.mem pv.pv_vs.vs_name cl.cl_local) then pv
  else Mvs.find pv.pv_vs cl.pv_table

let cl_find_rs cl rs =
  if not (Sid.mem rs.rs_name cl.cl_local) then rs
  else Mrs.find rs cl.rs_table

let cl_find_xs cl xs =
  if not (Sid.mem xs.xs_name cl.cl_local) then xs
  else Mxs.find xs cl.xs_table

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 =
  let constr = ls.ls_constr in
  let id = id_clone ls.ls_name in
  let at = List.map (clone_ty cl) ls.ls_args in
  let vt = Opt.map (clone_ty cl) ls.ls_value in
  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
  | Dtype _ | Ddata _ -> assert false (* impossible *)
  | 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
  | Dparam ls ->
      let d = create_param_decl (clone_ls cl ls) in
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
  | Dlogic ldl ->
      List.iter (fun (ls,_) ->
        if Mls.mem ls inst.mi_ls then raise (CannotInstantiate ls.ls_name);
        ignore (clone_ls cl ls)) ldl;
      let get_logic (_,ld) =
        Opt.get (ls_defn_of_axiom (clone_fmla cl (ls_defn_axiom ld))) in
      let d = create_logic_decl (List.map get_logic ldl) in
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
  | Dind (s, idl) ->
      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
      let get_case (pr,f) =
        if Mpr.mem pr inst.mi_pk then raise (CannotInstantiate pr.pr_name);
        let pr' = create_prsymbol (id_clone pr.pr_name) in
        cl.pr_table <- Mpr.add pr pr' cl.pr_table;
        pr', clone_fmla cl f in
      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
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
  | Dprop (k,pr,f) ->
      let skip, k' = match k, Mpr.find_opt pr inst.mi_pk with
        | Pgoal, _ -> true, Pgoal
        | Plemma, Some Pgoal -> true, Pgoal
        | Plemma, _ -> false, Plemma
        | Paxiom, Some k -> false, k
        | Paxiom, None -> false, inst.mi_df in
      if skip then uc else
      let pr' = create_prsymbol (id_clone pr.pr_name) in
      cl.pr_table <- Mpr.add pr pr' cl.pr_table;
      let d = create_prop_decl k' pr' (clone_fmla cl f) in
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)

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

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
  | 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 *)
  end;
  match s.rs_logic, s'.rs_logic with
  | RLls s, RLls s' -> cl_save_ls cl s s'
  | RLlemma, RLlemma -> () (* TODO: update cl.pr_table? *)
  | RLnone, RLnone -> ()
  | _ -> assert false

type smap = {
  sm_vs : vsymbol Mvs.t;
  sm_pv : pvsymbol Mvs.t;
  sm_xs : xsymbol Mxs.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_xs = cl.xs_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_xs = sm.sm_xs;
  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_xs = sm.sm_xs;
  sm_rs = sm.sm_rs }

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

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

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

let clone_varl cl sm varl = List.map (fun (t,r) ->
  clone_term cl sm.sm_vs t, Opt.map (cl_find_ls cl) r) varl

let clone_cty cl sm ?(drop_decr=false) cty =
  let res = clone_ity cl cty.cty_result in
  let args = List.map (clone_pv cl) cty.cty_args in
  let sm_args = List.fold_left2 sm_save_pv sm cty.cty_args args in
  let add_old o n (sm, olds) = let o' = clone_pv cl o in
    sm_save_pv sm o o', Mpv.add o' (sm_find_pv sm_args n) olds in
  let sm_olds, olds = Mpv.fold add_old cty.cty_oldies (sm_args, Mpv.empty) in
  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
  let post = clone_invl cl sm_olds cty.cty_post in
  let xpost = Mxs.fold (fun xs fl q ->
    let xs = sm_find_xs sm xs in
    let fl = clone_invl cl sm_olds fl in
    Mxs.add xs fl q) cty.cty_xpost Mxs.empty in
  let add_read v s = Spv.add (sm_find_pv sm_args v) s in
  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
  let add_write reg fs m = (* add new mutable fields to functions effect *)
    let add_fd fd s = Spv.add (Mpv.find_def fd fd cl.fd_table) s in
    let reg' = clone_reg cl reg in
    let smf_reg' = Spv.of_list reg'.reg_its.its_mfields in
    let smf_reg = Spv.of_list reg.reg_its.its_mfields in
    let smf_ref = Spv.fold add_fd smf_reg Spv.empty in
    let smf_new = Spv.diff smf_reg' smf_ref in
    let fs = Spv.fold add_fd fs Spv.empty in
    Mreg.add reg' (Spv.union fs smf_new) m in
  let writes = Mreg.fold add_write cty.cty_effect.eff_writes Mreg.empty in
  let add_reset reg s = Sreg.add (clone_reg cl reg) s in
  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 (sm_find_xs sm xs) in
  let eff = Sxs.fold add_raise cty.cty_effect.eff_raises eff in
  let eff = if partial cty.cty_effect.eff_oneway then eff_partial eff else eff in
  let eff = if diverges cty.cty_effect.eff_oneway then eff_diverge eff else eff in
  let cty = create_cty ~mask:cty.cty_mask args pre post xpost olds eff res in
  cty_ghostify (cty_ghost cty) cty

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

let clone_ppat cl sm pp mask =
  let rec conv_pat p = match p.pat_node with
    | Term.Pwild -> PPwild
    | 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)
    | 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
  let vm, pp' = create_prog_pattern pre (clone_ity cl pp.pp_ity) mask in
  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'

let rec clone_expr cl sm e = e_attr_copy e (match e.e_node with
  | Evar v -> e_var (sm_find_pv sm v)
  | Econst c -> e_const c (clone_ity cl e.e_ity)
  | Eexec (c,_) -> e_exec (clone_cexp cl sm c)
  | 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)
  | 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)
  | Ematch (d, bl, xl) ->
      let d = clone_expr cl sm d in
      let conv_rbr (pp, e) =
        let sm, pp = clone_ppat cl sm pp d.e_mask in
        pp, clone_expr cl sm e in
      let conv_xbr xs (vl, e) m =
        let vl' = List.map (clone_pv cl) vl in
        let sm = List.fold_left2 sm_save_pv sm vl vl' in
        Mxs.add (sm_find_xs sm xs) (vl', clone_expr cl sm e) m in
      e_match d (List.map conv_rbr bl) (Mxs.fold conv_xbr xl Mxs.empty)
  | 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 (v, (f,dir,t), i, invl, e) ->
      let v' = clone_pv cl v in
      let ism = sm_save_pv sm v v' in
      let i' = if pv_equal v i then v' else clone_pv cl i in
      let ism = if pv_equal v i then ism else sm_save_pv ism i i' in
      e_for v'
        (e_var (sm_find_pv sm f)) dir (e_var (sm_find_pv sm t))
        i' (clone_invl cl ism invl) (clone_expr cl ism e)
  | Eraise (xs, e1) ->
      e_raise (sm_find_xs sm xs) (clone_expr cl sm e1) (clone_ity cl e.e_ity)
  | Eexn ({xs_name = id; xs_mask = mask; xs_ity = ity} as xs, e) ->
      let xs' = create_xsymbol (id_clone id) ~mask (clone_ity cl ity) in
      e_exn xs' (clone_expr cl (sm_save_xs sm xs xs') e)
  | Eassert (k, f) ->
      e_assert k (clone_term cl sm.sm_vs f)
  | Eghost e ->
      e_ghostify true (clone_expr cl sm e)
  | Epure t ->
      e_pure (clone_term cl sm.sm_vs t)
  | Eabsurd -> e_absurd (clone_ity cl e.e_ity))

and clone_cexp cl sm c = match c.c_node with
  | Capp (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_app (sm_find_rs sm s) vl al res
  | 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
  | 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
      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)
  | Cany ->
      c_any (clone_cty cl sm c.c_cty)

and clone_let_defn cl sm ld = match ld with
  | LDvar (v,e) ->
      let e' = clone_expr cl sm e in
      let id = id_clone v.pv_vs.vs_name in
      let ld, v' = let_var id ~ghost:v.pv_ghost e' in
      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_name = id} as rs} =
        let cty = clone_cty cl sm ~drop_decr:true rs.rs_cty in
        let rs' = create_rsymbol (id_clone id) ~ghost:(rs_ghost 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 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
        let c = c_fun ~mask:c.c_cty.cty_mask cty.cty_args
          cty.cty_pre cty.cty_post cty.cty_xpost cty.cty_oldies e in
        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

let clone_type_record cl s d s' d' =
  let id = s.its_ts.ts_name in
  let fields' = Hstr.create 16 in
  let add_field' rs' = let pj' = fd_of_rs rs' in
    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 *)
  let match_pj rs = let pj = fd_of_rs rs in
    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