Commit c06bc445 authored by Andrei Paskevich's avatar Andrei Paskevich

cloning: instantiate type symbols into types

this removes the ugly hack of creating an ad-hoc type alias symbol
for substitutions like "clone T with type t 'a = list (int, 'a)".

If a type symbol "t1 'a 'b 'c" is instantiated into a type of the
form "t2 'a 'b 'c", then the metas that mention the type symbol "t1"
are preserved, and "t1" is replaced with "t2". Otherwise, all such
metas disappear in the cloned theory.
parent 5f055180
......@@ -420,8 +420,10 @@ let print_logic_decl = print_logic_decl true
let print_next_ind_decl = print_ind_decl Ind false
let print_ind_decl fmt s = print_ind_decl s true fmt
let print_inst_ts fmt (ts1,ts2) =
fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2
let print_inst_ts fmt (ts1,ty2) =
fprintf fmt "type %a%a = %a" print_ts ts1
(print_list_pre space print_tv) ts1.ts_args
print_ty ty2; forget_tvs ()
let print_inst_ls fmt (ls1,ls2) =
fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
......
......@@ -171,7 +171,7 @@ and tdecl_node =
| Meta of meta * meta_arg list
and symbol_map = {
sm_ts : tysymbol Mts.t;
sm_ts : ty Mts.t;
sm_ls : lsymbol Mls.t;
sm_pr : prsymbol Mpr.t;
}
......@@ -192,7 +192,7 @@ module Hstdecl = Hashcons.Make (struct
| _,_ -> false
let eq_smap sm1 sm2 =
Mts.equal ts_equal sm1.sm_ts sm2.sm_ts &&
Mts.equal ty_equal sm1.sm_ts sm2.sm_ts &&
Mls.equal ls_equal sm1.sm_ls sm2.sm_ls &&
Mpr.equal pr_equal sm1.sm_pr sm2.sm_pr
......@@ -205,7 +205,7 @@ module Hstdecl = Hashcons.Make (struct
t1 = t2 && Lists.equal eq_marg al1 al2
| _,_ -> false
let hs_cl_ts _ ts acc = Hashcons.combine acc (ts_hash ts)
let hs_cl_ty _ ty acc = Hashcons.combine acc (ty_hash ty)
let hs_cl_ls _ ls acc = Hashcons.combine acc (ls_hash ls)
let hs_cl_pr _ pr acc = Hashcons.combine acc (pr_hash pr)
......@@ -218,7 +218,7 @@ module Hstdecl = Hashcons.Make (struct
| MAint i -> Hashtbl.hash i
let hs_smap sm h =
Mts.fold hs_cl_ts sm.sm_ts
Mts.fold hs_cl_ty sm.sm_ts
(Mls.fold hs_cl_ls sm.sm_ls
(Mpr.fold hs_cl_pr sm.sm_pr h))
......@@ -308,18 +308,17 @@ let close_scope uc ~import =
(* Base constructors *)
let known_ts kn ts = match ts.ts_def with
| Some ty -> ty_s_fold (fun () ts -> known_id kn ts.ts_name) () ty
| None -> known_id kn ts.ts_name
let known_ty kn ty =
ty_s_fold (fun () ts -> known_id kn ts.ts_name) () ty
let known_clone kn sm =
Mts.iter (fun _ ts -> known_ts kn ts) sm.sm_ts;
Mts.iter (fun _ ty -> known_ty kn ty) sm.sm_ts;
Mls.iter (fun _ ls -> known_id kn ls.ls_name) sm.sm_ls;
Mpr.iter (fun _ pr -> known_id kn pr.pr_name) sm.sm_pr
let known_meta kn al =
let check = function
| MAty ty -> ty_s_fold (fun () ts -> known_id kn ts.ts_name) () ty
| MAty ty -> known_ty kn ty
| MAts ts -> known_id kn ts.ts_name
| MAls ls -> known_id kn ls.ls_name
| MApr pr -> known_id kn pr.pr_name
......@@ -403,12 +402,11 @@ let warn_dubious_axiom uc k p syms =
(fun id ->
if Sid.mem id uc.uc_local then
match (Ident.Mid.find id uc.uc_known).d_node with
| Dtype { ts_def = None } | Dparam _ ->
raise Exit
| Dtype { ts_def = None } | Dparam _ -> raise Exit
| _ -> ())
syms;
Warning.emit ?loc:p.id_loc "axiom %s does not contain any local abstract symbol"
p.id_string
Warning.emit ?loc:p.id_loc
"axiom %s does not contain any local abstract symbol" p.id_string
with Exit -> ()
let add_decl ?(warn=true) uc d =
......@@ -448,8 +446,8 @@ let use_export uc th =
(** Clone *)
type th_inst = {
inst_ts : tysymbol Mts.t; (* old to new *)
inst_ls : lsymbol Mls.t;
inst_ts : ty Mts.t; (* old to new *)
inst_ls : lsymbol Mls.t;
inst_pr : prop_kind Mpr.t;
}
......@@ -462,14 +460,14 @@ let empty_inst = {
exception CannotInstantiate of ident
type clones = {
clone_th : theory;
mutable ts_table : tysymbol Mts.t;
cl_local : Sid.t;
mutable ts_table : ty Mts.t;
mutable ls_table : lsymbol Mls.t;
mutable pr_table : prsymbol Mpr.t;
}
let empty_clones th = {
clone_th = th;
cl_local = th.th_local;
ts_table = Mts.empty;
ls_table = Mls.empty;
pr_table = Mpr.empty;
......@@ -477,24 +475,40 @@ let empty_clones th = {
(* populate the clone structure *)
let rec cl_find_ts cl ts =
if not (Sid.mem ts.ts_name cl.clone_th.th_local) then
let td = Opt.map (cl_trans_ty cl) ts.ts_def in
if Opt.equal ty_equal ts.ts_def td then ts else
create_tysymbol (id_clone ts.ts_name) ts.ts_args td
else try Mts.find ts cl.ts_table
with Not_found ->
let td' = Opt.map (cl_trans_ty cl) ts.ts_def in
let ts' = create_tysymbol (id_clone ts.ts_name) ts.ts_args td' in
cl.ts_table <- Mts.add ts ts' cl.ts_table;
ts'
and cl_trans_ty cl ty = ty_s_map (cl_find_ts cl) ty
let rec sm_trans_ty tsm ty = match ty.ty_node with
| Tyapp (ts, tyl) ->
let tyl = List.map (sm_trans_ty tsm) tyl in
begin match Mts.find_opt ts tsm with
| Some ty -> ty_inst (ts_match_args ts tyl) ty
| None -> ty_app ts tyl
end
| Tyvar _ -> ty
let cl_trans_ty cl ty = sm_trans_ty cl.ts_table ty
let sm_find_ts tsm ({ts_args = tvl} as ts) =
let check v ty = match ty.ty_node with
| Tyvar u -> tv_equal u v
| _ -> false in
match (Mts.find ts tsm).ty_node with
| Tyapp (ts, tyl) when Lists.equal check tvl tyl -> ts
| _ -> raise Not_found
let cl_find_ts cl ts =
if not (Sid.mem ts.ts_name cl.cl_local) then ts else
try sm_find_ts cl.ts_table ts with Not_found -> raise EmptyDecl
let cl_clone_ts cl ts =
(* cl_clone_ts is only called for local non-instantiated symbols *)
let td' = Opt.map (cl_trans_ty cl) ts.ts_def in
let ts' = create_tysymbol (id_clone ts.ts_name) ts.ts_args td' in
let ty' = ty_app ts' (List.map ty_var ts.ts_args) in
cl.ts_table <- Mts.add ts ty' cl.ts_table;
ts'
let cl_find_ls cl ls =
if not (Sid.mem ls.ls_name cl.clone_th.th_local) then ls
else try Mls.find ls cl.ls_table
with Not_found ->
if not (Sid.mem ls.ls_name cl.cl_local) then ls else
try Mls.find ls cl.ls_table with Not_found ->
let constr = ls.ls_constr in
let id = id_clone ls.ls_name in
let ta' = List.map (cl_trans_ty cl) ls.ls_args in
......@@ -505,46 +519,43 @@ let cl_find_ls cl ls =
let cl_trans_fmla cl f = t_s_map (cl_trans_ty cl) (cl_find_ls cl) f
let cl_find_pr cl pr =
if not (Sid.mem pr.pr_name cl.cl_local) then pr else
try Mpr.find pr cl.pr_table with Not_found -> raise EmptyDecl
let cl_clone_pr cl pr =
let pr' = create_prsymbol (id_clone pr.pr_name) in
cl.pr_table <- Mpr.add pr pr' cl.pr_table;
pr'
let cl_find_pr cl pr =
if not (Sid.mem pr.pr_name cl.clone_th.th_local) then pr else
try Mpr.find pr cl.pr_table with Not_found -> raise EmptyDecl
(* initialize the clone structure *)
exception NonLocal of ident
exception BadInstance of ident * ident
let cl_init_ts cl ts ts' =
let id = ts.ts_name in
if not (Sid.mem id cl.clone_th.th_local) then raise (NonLocal id);
if List.length ts.ts_args <> List.length ts'.ts_args
then raise (BadInstance (id, ts'.ts_name));
cl.ts_table <- Mts.add ts ts' cl.ts_table
let cl_init_ls cl ls ls' =
let id = ls.ls_name in
if not (Sid.mem id cl.clone_th.th_local) then raise (NonLocal id);
exception BadInstance of ident
let cl_init_ts cl ({ts_name = id} as ts) ty =
if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
let stv = Stv.of_list ts.ts_args in
if not (ty_v_all (fun v -> Stv.mem v stv) ty) then raise (BadInstance id);
cl.ts_table <- Mts.add ts ty cl.ts_table
let cl_init_ls cl ({ls_name = id} as ls) ls' =
if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
let mtch sb ty ty' =
try ty_match sb ty' (cl_trans_ty cl ty)
with TypeMismatch _ -> raise (BadInstance (id, ls'.ls_name))
with TypeMismatch _ -> raise (BadInstance id)
in
let sb = match ls.ls_value,ls'.ls_value with
| Some ty, Some ty' -> mtch Mtv.empty ty ty'
| None, None -> Mtv.empty
| _ -> raise (BadInstance (id, ls'.ls_name))
| _ -> raise (BadInstance id)
in
ignore (try List.fold_left2 mtch sb ls.ls_args ls'.ls_args
with Invalid_argument _ -> raise (BadInstance (id, ls'.ls_name)));
with Invalid_argument _ -> raise (BadInstance id));
cl.ls_table <- Mls.add ls ls' cl.ls_table
let cl_init_pr cl pr _ =
let id = pr.pr_name in
if not (Sid.mem id cl.clone_th.th_local) then raise (NonLocal id)
let cl_init_pr cl {pr_name = id} _ =
if not (Sid.mem id cl.cl_local) then raise (NonLocal id)
let cl_init th inst =
let cl = empty_clones th in
......@@ -559,25 +570,18 @@ let cl_type cl inst ts =
if Mts.mem ts inst.inst_ts then
if ts.ts_def = None then raise EmptyDecl
else raise (CannotInstantiate ts.ts_name);
create_ty_decl (cl_find_ts cl ts)
create_ty_decl (cl_clone_ts cl ts)
let cl_data cl inst tdl =
let add_ls ls =
if Mls.mem ls inst.inst_ls then
raise (CannotInstantiate ls.ls_name);
cl_find_ls cl ls
in
let add_constr (ls,pl) =
add_ls ls, List.map (Opt.map add_ls) pl
in
let add_type (ts,csl) =
if Mts.mem ts inst.inst_ts then
raise (CannotInstantiate ts.ts_name);
let ts' = cl_find_ts cl ts in
let td' = List.map add_constr csl in
(ts',td')
in
create_data_decl (List.map add_type tdl)
if Mls.mem ls inst.inst_ls then raise (CannotInstantiate ls.ls_name);
cl_find_ls cl ls in
let add_constr (ls,pl) = add_ls ls, List.map (Opt.map add_ls) pl in
let add_type ts' (_,csl) = ts', List.map add_constr csl in
let get_type (ts,_) =
if Mts.mem ts inst.inst_ts then raise (CannotInstantiate ts.ts_name);
cl_clone_ts cl ts in
create_data_decl (List.map2 add_type (List.map get_type tdl) tdl)
let extract_ls_defn f =
let vl,_,f = match f.t_node with
......@@ -640,7 +644,7 @@ let cl_marg cl = function
| a -> a
let cl_smap cl sm = {
sm_ts = Mts.map (cl_find_ts cl) sm.sm_ts;
sm_ts = Mts.map (cl_trans_ty cl) sm.sm_ts;
sm_ls = Mls.map (cl_find_ls cl) sm.sm_ls;
sm_pr = Mpr.map (cl_find_pr cl) sm.sm_pr}
......@@ -689,7 +693,7 @@ let clone_export uc th inst =
let f_ts p ts =
if Mid.mem ts.ts_name th.th_local then
try let ts = Mts.find ts cl.ts_table in
try let ts = sm_find_ts cl.ts_table ts in
store_path uc p ts.ts_name; Some ts
with Not_found -> None else Some ts in
let f_ls p ls =
......@@ -760,13 +764,13 @@ let add_meta uc s al = add_tdecl uc (create_meta s al)
let clone_meta tdt th sm = match tdt.td_node with
| Meta (t,al) ->
let find_ts ts = if Mid.mem ts.ts_name th.th_local
then Mts.find ts sm.sm_ts else ts in
then sm_find_ts sm.sm_ts ts else ts in
let find_ls ls = if Mid.mem ls.ls_name th.th_local
then Mls.find ls sm.sm_ls else ls in
let find_pr pr = if Mid.mem pr.pr_name th.th_local
then Mpr.find pr sm.sm_pr else pr in
let cl_marg = function
| MAty ty -> MAty (ty_s_map find_ts ty)
| MAty ty -> MAty (sm_trans_ty sm.sm_ts ty)
| MAts ts -> MAts (find_ts ts)
| MAls ls -> MAls (find_ls ls)
| MApr pr -> MApr (find_pr pr)
......@@ -842,12 +846,11 @@ let print_meta_arg_type fmt = function
let () = Exn_printer.register
begin fun fmt exn -> match exn with
| NonLocal id ->
Format.fprintf fmt "Non-local ident: %s" id.id_string
Format.fprintf fmt "Non-local symbol: %s" id.id_string
| CannotInstantiate id ->
Format.fprintf fmt "Cannot instantiate a defined ident %s" id.id_string
| BadInstance (id1, id2) ->
Format.fprintf fmt "Cannot instantiate ident %s with %s"
id1.id_string id2.id_string
Format.fprintf fmt "Cannot instantiate a defined symbol %s" id.id_string
| BadInstance id ->
Format.fprintf fmt "Illegal instantiation for symbol %s" id.id_string
| CloseTheory ->
Format.fprintf fmt "Cannot close theory: some namespaces are still open"
| NoOpenedNamespace ->
......
......@@ -102,7 +102,7 @@ and tdecl_node = private
| Meta of meta * meta_arg list
and symbol_map = private {
sm_ts : tysymbol Mts.t;
sm_ts : ty Mts.t;
sm_ls : lsymbol Mls.t;
sm_pr : prsymbol Mpr.t;
}
......@@ -166,8 +166,8 @@ val use_export : theory_uc -> theory -> theory_uc
(** {2 Clone} *)
type th_inst = {
inst_ts : tysymbol Mts.t; (* old to new *)
inst_ls : lsymbol Mls.t;
inst_ts : ty Mts.t; (* old to new *)
inst_ls : lsymbol Mls.t;
inst_pr : prop_kind Mpr.t;
}
......@@ -180,7 +180,7 @@ val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
val add_clone_internal : unit -> theory_uc -> theory ->
tysymbol Mts.t -> lsymbol Mls.t -> prsymbol Mpr.t -> theory_uc
ty Mts.t -> lsymbol Mls.t -> prsymbol Mpr.t -> theory_uc
(** {2 Meta} *)
......@@ -212,8 +212,8 @@ val add_decl_with_tuples : theory_uc -> decl -> theory_uc
(* {2 Exceptions} *)
exception NonLocal of ident
exception BadInstance of ident
exception CannotInstantiate of ident
exception BadInstance of ident * ident
exception CloseTheory
exception NoOpenedNamespace
......
......@@ -159,11 +159,13 @@ let create_tysymbol name args def =
ignore (Opt.map (ty_v_all check) def);
mk_ts name args def
let ts_match_args s tl =
try List.fold_right2 Mtv.add s.ts_args tl Mtv.empty
with Invalid_argument _ -> raise (BadTypeArity (s, List.length tl))
let ty_app s tl = match s.ts_def with
| Some ty ->
let mv = try List.fold_right2 Mtv.add s.ts_args tl Mtv.empty with
| Invalid_argument _ -> raise (BadTypeArity (s, List.length tl)) in
ty_full_inst mv ty
ty_full_inst (ts_match_args s tl) ty
| None ->
if List.length s.ts_args <> List.length tl then
raise (BadTypeArity (s, List.length tl));
......
......@@ -109,6 +109,8 @@ val ty_match : ty Mtv.t -> ty -> ty -> ty Mtv.t
exists.
*)
val ts_match_args : tysymbol -> ty list -> ty Mtv.t
val ty_inst : ty Mtv.t -> ty -> ty
val ty_freevars : Stv.t -> ty -> Stv.t
val ty_closed : ty -> bool
......
......@@ -237,6 +237,9 @@ val isb_empty : ity_subst
val ity_match : ity_subst -> ity -> ity -> ity_subst
val reg_match : ity_subst -> region -> region -> ity_subst
val its_match_args : itysymbol -> ity list -> ity_subst
val its_match_regs : itysymbol -> ity list -> region list -> ity_subst
val ity_freeze : ity_subst -> ity -> ity_subst (* self-match *)
val reg_freeze : ity_subst -> region -> ity_subst (* self-match *)
......
......@@ -109,7 +109,7 @@ and mod_unit =
and mod_inst = {
mi_mod : pmodule;
mi_ts : itysymbol Mts.t;
mi_ts : ity Mts.t;
mi_ls : lsymbol Mls.t;
mi_pr : prsymbol Mpr.t;
mi_pv : pvsymbol Mpv.t;
......@@ -344,7 +344,7 @@ let add_pdecl ~vc uc d =
type clones = {
cl_local : Sid.t;
mutable ts_table : itysymbol Mts.t;
mutable ts_table : ity Mts.t;
mutable ls_table : lsymbol Mls.t;
mutable pr_table : prsymbol Mpr.t;
mutable rn_table : region Mreg.t;
......@@ -353,8 +353,8 @@ type clones = {
mutable xs_table : xsymbol Mexn.t;
}
let empty_clones s = {
cl_local = s;
let empty_clones m = {
cl_local = m.mod_local;
ts_table = Mts.empty;
ls_table = Mls.empty;
pr_table = Mpr.empty;
......@@ -366,83 +366,77 @@ let empty_clones s = {
(* populate the clone structure *)
let rec cl_find_its cl its =
if not (Sid.mem its.its_ts.ts_name cl.cl_local) then
match its.its_def with
| Some _ -> cl_make_its_alias cl its
| None -> its
else (*try*) Mts.find its.its_ts cl.ts_table
(* with Not_found -> cl_make_its_pure cl its*)
and cl_find_ts cl ts =
if not (Sid.mem ts.ts_name cl.cl_local) then
match ts.ts_def with
| Some _ -> (cl_make_its_alias cl (restore_its ts)).its_ts
| None -> ts
else (*try*) (Mts.find ts cl.ts_table).its_ts
(* with Not_found -> (cl_make_its_pure cl (restore_its ts)).its_ts*)
(*
and cl_make_its_pure cl ({its_ts = ts} as its) =
let id = id_clone ts.ts_name in
let nts = match its.its_def with
| Some def -> create_itysymbol_alias id ts.ts_args (cl_trans_ity cl def)
| None -> create_itysymbol_pure id ts.ts_args in
cl.ts_table <- Mts.add its.its_ts nts cl.ts_table;
nts
*)
and cl_make_its_alias cl its =
let odf = Opt.get its.its_def in
let ndf = cl_trans_ity cl odf in
if ity_equal odf ndf then its else
create_itysymbol_alias (id_clone its.its_ts.ts_name) its.its_ts.ts_args ndf
and cl_trans_ity cl ity = match ity.ity_node with
| Ityreg r -> ity_reg (cl_trans_reg cl r)
| Ityapp (s,tl,rl) ->
ity_app (cl_find_its cl s) (List.map (cl_trans_ity cl) tl)
(List.map (cl_trans_reg cl) rl)
| Itypur (s,tl) ->
ity_pur (cl_find_its cl s) (List.map (cl_trans_ity cl) tl)
let rec sm_trans_ty tsm ty = match ty.ty_node with
| Tyapp (s, tl) ->
let tl = List.map (sm_trans_ty tsm) tl in
begin match Mts.find_opt s tsm with
| Some ity -> ty_inst (ts_match_args s tl) (ty_of_ity ity)
| None -> ty_app s tl
end
| Tyvar _ -> ty
let cl_trans_ty cl ty = sm_trans_ty cl.ts_table ty
let sm_find_ts tsm ({ts_args = vl} as s) =
let check v ty = match ty.ty_node with
| Tyvar u -> tv_equal u v
| _ -> false in
match (ty_of_ity (Mts.find s tsm)).ty_node with
| Tyapp (s, tl) when Lists.equal check vl tl -> s
| _ -> raise Not_found
let cl_find_ts cl s =
if not (Sid.mem s.ts_name cl.cl_local) then s else
sm_find_ts cl.ts_table s
let rec cl_trans_ity cl ity = match ity.ity_node with
| Ityreg r ->
ity_reg (cl_trans_reg cl r)
| Ityapp (s, tl, rl) ->
let tl = List.map (cl_trans_ity cl) tl in
let rl = List.map (cl_trans_reg cl) rl in
begin match Mts.find_opt s.its_ts cl.ts_table with
| Some ity -> ity_full_inst (its_match_regs s tl rl) ity
| None -> ity_app s tl rl
end
| Itypur (s, tl) ->
let tl = List.map (cl_trans_ity cl) tl in
begin match Mts.find_opt s.its_ts cl.ts_table with
| Some ity -> ity_full_inst (its_match_args s tl) (ity_purify ity)
| None -> ity_pur s tl
end
| Ityvar _ -> ity
and cl_trans_reg cl reg =
(* FIXME: what about global non-instantiated regions? *)
(* 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. *)
try Mreg.find reg cl.rn_table with Not_found ->
let r = create_region (id_clone reg.reg_name)
(cl_find_its cl reg.reg_its) (List.map (cl_trans_ity cl) reg.reg_args)
(List.map (cl_trans_reg cl) reg.reg_regs) in
cl.rn_table <- Mreg.add reg r cl.rn_table;
r
and cl_trans_ty cl ty = ty_s_map (cl_find_ts cl) ty
let tl = List.map (cl_trans_ity cl) reg.reg_args in
let rl = List.map (cl_trans_reg cl) reg.reg_regs in
let r = match Mts.find_opt reg.reg_its.its_ts cl.ts_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 (reg_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 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 (*try*) Mls.find ls cl.ls_table
(*
with Not_found ->
let constr = ls.ls_constr in
let id = id_clone ls.ls_name in
let ta' = List.map (cl_trans_ty cl) ls.ls_args in
let vt' = Opt.map (cl_trans_ty cl) ls.ls_value in
let ls' = create_lsymbol ~constr id ta' vt' in
cl.ls_table <- Mls.add ls ls' cl.ls_table;
ls'
*)
else Mls.find ls cl.ls_table
let cl_trans_fmla cl f = t_s_map (cl_trans_ty cl) (cl_find_ls cl) f
let cl_find_pr cl pr =
if not (Sid.mem pr.pr_name cl.cl_local) then pr
else (*try*) Mpr.find pr cl.pr_table
(*
with Not_found ->
let pr' = create_prsymbol (id_clone pr.pr_name) in
cl.pr_table <- Mpr.add pr pr' cl.pr_table;
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
......@@ -456,18 +450,6 @@ let cl_find_xs cl xs =
if not (Sid.mem xs.xs_name cl.cl_local) then xs
else Mexn.find xs cl.xs_table
(*
(* initialize the clone structure *)
let cl_init_ts cl ({ts_name = id} as ts) ts' =
if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
(* TODO: check later
if List.length ts.ts_args <> List.length ts'.ts_args
then raise (BadInstance (id, ts'.ts_name));
*)
cl.ts_table <- Mts.add ts (restore_its ts') cl.ts_table
*)
let cl_clone_ls inst cl ls =
if Mls.mem ls inst.inst_ls then raise (CannotInstantiate ls.ls_name);
let constr = ls.ls_constr in
......@@ -478,15 +460,15 @@ let cl_clone_ls inst cl ls =
cl.ls_table <- Mls.add ls ls' cl.ls_table;
ls'