Commit 08f037e6 authored by Andrei Paskevich's avatar Andrei Paskevich

clone: several bugfixes and missing checks

parent dfb52c23
...@@ -614,13 +614,40 @@ module Context = struct ...@@ -614,13 +614,40 @@ module Context = struct
| Duse _ | Dclone _ -> | Duse _ | Dclone _ ->
d :: acc d :: acc
exception NonLocal of ident
exception BadInstance of ident * ident
let clone_theory th inst = let clone_theory th inst =
let cl = empty_clones th.th_local in let cl = empty_clones th.th_local in
Mts.iter (cl_add_ts cl) inst.inst_ts; let check_ts ts ts' = let id = ts.ts_name in
Mls.iter (cl_add_ls cl) inst.inst_ls; if not (Sid.mem id th.th_local) then raise (NonLocal id);
let add = cl_add_decl cl inst in if List.length ts.ts_args <> List.length ts'.ts_args
let decls = ctxt_fold add [] th.th_ctxt in then raise (BadInstance (id, ts'.ts_name));
cl, decls cl_add_ts cl ts ts'
in
let check_ls ls ls' = let id = ls.ls_name in
if not (Sid.mem id th.th_local) then raise (NonLocal id);
let tymatch sb ty ty' =
try Ty.matching sb ty' (cl_trans_ty cl ty)
with TypeMismatch -> raise (BadInstance (id, ls'.ls_name))
in
let sb = match ls.ls_value,ls'.ls_value with
| Some ty, Some ty' -> tymatch Mid.empty ty ty'
| None, None -> Mid.empty
| _ -> raise (BadInstance (id, ls'.ls_name))
in
ignore (try List.fold_left2 tymatch sb ls.ls_args ls'.ls_args
with Invalid_argument _ -> raise (BadInstance (id, ls'.ls_name)));
cl_add_ls cl ls ls'
in
let check_pr pr = let id = pr.pr_name in
if not (Sid.mem id th.th_local) then raise (NonLocal id);
in
Mts.iter check_ts inst.inst_ts;
Mls.iter check_ls inst.inst_ls;
Spr.iter check_pr inst.inst_lemma;
Spr.iter check_pr inst.inst_goal;
cl, ctxt_fold (cl_add_decl cl inst) [] th.th_ctxt
let add_final ctxt cl = let add_final ctxt cl =
let add id id' acc = (id,id') :: acc in let add id id' acc = (id,id') :: acc in
...@@ -758,24 +785,34 @@ module Theory = struct ...@@ -758,24 +785,34 @@ module Theory = struct
assert false assert false
let clone_export uc th inst = let clone_export uc th inst =
let cl, ctxt = Context.add_clone uc.uc_ctxt th inst in let cl,ctxt = Context.add_clone uc.uc_ctxt th inst in
let f_ts n t ns = add_ts true n (Hts.find cl.Context.ts_table t) ns in
let f_ls n l ns = add_ls true n (Hls.find cl.Context.ls_table l) ns in let add_local _ id' acc =
let f_pr n p ns = add_pr true n (Hpr.find cl.Context.pr_table p) ns in if Mid.mem id' uc.uc_ctxt.ctxt_known then acc else Sid.add id' acc in
let local = Hid.fold add_local cl.Context.id_table uc.uc_local in
let rec merge_namespace acc ns =
let find_ts ts = if Sid.mem ts.ts_name th.th_local
then Hts.find cl.Context.ts_table ts else ts in
let find_ls ls = if Sid.mem ls.ls_name th.th_local
then Hls.find cl.Context.ls_table ls else ls in
let find_pr pr = if Sid.mem pr.pr_name th.th_local
then Hpr.find cl.Context.pr_table pr else pr in
let f_ts n ts ns = add_ts true n (find_ts ts) ns in
let f_ls n ls ns = add_ls true n (find_ls ls) ns in
let f_pr n pr ns = add_pr true n (find_pr pr) ns in
let rec f_ns n s = add_ns true n (merge_namespace empty_ns s)
and merge_namespace acc ns =
let acc = Mnm.fold f_ts ns.ns_ts acc in let acc = Mnm.fold f_ts ns.ns_ts acc in
let acc = Mnm.fold f_ls ns.ns_ls acc in let acc = Mnm.fold f_ls ns.ns_ls acc in
let acc = Mnm.fold f_pr ns.ns_pr acc in let acc = Mnm.fold f_pr ns.ns_pr acc in
let acc = Mnm.fold f_ns ns.ns_ns acc in acc let acc = Mnm.fold f_ns ns.ns_ns acc in acc in
and f_ns n ns acc = add_ns true n (merge_namespace empty_ns ns) acc in
let ns = merge_namespace empty_ns th.th_export in let ns = merge_namespace empty_ns th.th_export in
match uc.uc_import, uc.uc_export with match uc.uc_import, uc.uc_export with
| i0 :: sti, e0 :: ste -> { uc with | i0 :: sti, e0 :: ste -> { uc with
uc_import = merge_ns false ns i0 :: sti; uc_import = merge_ns false ns i0 :: sti;
uc_export = merge_ns true ns e0 :: ste; uc_export = merge_ns true ns e0 :: ste;
uc_local = local;
uc_ctxt = ctxt } uc_ctxt = ctxt }
| _ -> | _ ->
assert false assert false
......
...@@ -160,7 +160,10 @@ module Context : sig ...@@ -160,7 +160,10 @@ module Context : sig
exception UnknownIdent of ident exception UnknownIdent of ident
exception RedeclaredIdent of ident exception RedeclaredIdent of ident
exception NonLocal of ident
exception CannotInstantiate of ident exception CannotInstantiate of ident
exception BadInstance of ident * ident
end end
......
...@@ -1129,16 +1129,24 @@ and add_decl env th = function ...@@ -1129,16 +1129,24 @@ and add_decl env th = function
| CStsym (p,q) -> | CStsym (p,q) ->
let ts1 = find_tysymbol_ns p t.th_export in let ts1 = find_tysymbol_ns p t.th_export in
let ts2 = find_tysymbol q th in let ts2 = find_tysymbol q th in
if Mts.mem ts1 s.inst_ts
then error ~loc (Clash ts1.ts_name.id_short);
{ s with inst_ts = Mts.add ts1 ts2 s.inst_ts } { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
| CSlsym (p,q) -> | CSlsym (p,q) ->
let ls1 = find_lsymbol_ns p t.th_export in let ls1 = find_lsymbol_ns p t.th_export in
let ls2 = find_lsymbol q th in let ls2 = find_lsymbol q th in
if Mls.mem ls1 s.inst_ls
then error ~loc (Clash ls1.ls_name.id_short);
{ s with inst_ls = Mls.add ls1 ls2 s.inst_ls } { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
| CSlemma p -> | CSlemma p ->
let pr = find_prop_ns p t.th_export in let pr = find_prop_ns p t.th_export in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
then error ~loc (Clash pr.pr_name.id_short);
{ s with inst_lemma = Spr.add pr s.inst_lemma } { s with inst_lemma = Spr.add pr s.inst_lemma }
| CSgoal p -> | CSgoal p ->
let pr = find_prop_ns p t.th_export in let pr = find_prop_ns p t.th_export in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
then error ~loc (Clash pr.pr_name.id_short);
{ s with inst_goal = Spr.add pr s.inst_goal } { s with inst_goal = Spr.add pr s.inst_goal }
in in
let s = List.fold_left add_inst empty_inst s in let s = List.fold_left add_inst empty_inst s in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment