pmodule.ml

(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2019   --   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 *)

let ref_attr = Ident.create_attribute "mlw:reference_var"

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

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 has_ref r1 || has_ref r2 then vn 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
        if has_ref r2 then vn 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, restore_module_id =
  let id_to_path = Wid.create 17 in
  let id_to_pmod = 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 pmod  =
    let th = pmod.mod_theory in
    let id = th.th_name in
    (* this symbol is already a module *)
    if Wid.mem id_to_path id then () else begin
        Wid.set id_to_path id (th.th_path, id.id_string, []);
        Sid.iter (fun id -> Wid.set id_to_pmod id pmod) pmod.mod_local;
        Wid.set id_to_pmod id pmod;
      end
  in
  let restore_path id = Wid.find id_to_path id in
  let restore_module_id id = Wid.find id_to_pmod id in
  store_path, store_module, restore_path, restore_module_id

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_str 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 itd_ref =
  let tv = create_tvsymbol (id_fresh "a") in
  let pj = create_pvsymbol (id_fresh "contents") (ity_var tv) in
  create_plain_record_decl ~priv:false ~mut:true (id_fresh "ref")
                                            [tv] [true, pj] [] []

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

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

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

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

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 if id_equal id ts_ref.ts_name then
    use_export uc ref_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 (BadI 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 (BadI 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 (BadI pr.pr_name))
    | PDpure -> () in
  Mpr.iter check_pk inst.mi_pk;
  Mpr.iter (fun pr _ -> raise (BadInstance (BadI 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 (BadI 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 (BadI id)) in
      ignore (try List.fold_left2 mtch sbs ls.ls_args ls'.ls_args
        with Invalid_argument _ -> raise (BadInstance (BadI 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 attr = Sattr.remove Ident.useraxiom_attr pr.pr_name.id_attrs in
      let pr' = create_prsymbol (id_attr pr.pr_name attr) 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