diff --git a/src/core/theory.ml b/src/core/theory.ml index 69a55f43c205800865f08bee9c5b2f62dfd2b191..9f2fe45bcb5b5d3b5794860229d3a622f938c73b 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -614,13 +614,40 @@ module Context = struct | Duse _ | Dclone _ -> d :: acc + exception NonLocal of ident + exception BadInstance of ident * ident + let clone_theory th inst = let cl = empty_clones th.th_local in - Mts.iter (cl_add_ts cl) inst.inst_ts; - Mls.iter (cl_add_ls cl) inst.inst_ls; - let add = cl_add_decl cl inst in - let decls = ctxt_fold add [] th.th_ctxt in - cl, decls + let check_ts ts ts' = let id = ts.ts_name in + if not (Sid.mem id 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_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 id id' acc = (id,id') :: acc in @@ -758,24 +785,34 @@ module Theory = struct assert false let clone_export uc th inst = - 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 f_pr n p ns = add_pr true n (Hpr.find cl.Context.pr_table p) ns in - - let rec merge_namespace acc ns = + let cl,ctxt = Context.add_clone uc.uc_ctxt th inst in + + let add_local _ id' acc = + 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 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_ls ns.ns_ls 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 - - and f_ns n ns acc = add_ns true n (merge_namespace empty_ns ns) acc in - + let acc = Mnm.fold f_ns ns.ns_ns acc in acc in let ns = merge_namespace empty_ns th.th_export in + match uc.uc_import, uc.uc_export with | i0 :: sti, e0 :: ste -> { uc with uc_import = merge_ns false ns i0 :: sti; uc_export = merge_ns true ns e0 :: ste; + uc_local = local; uc_ctxt = ctxt } | _ -> assert false diff --git a/src/core/theory.mli b/src/core/theory.mli index 1015aca6c449db0c5ab5aecb9df8283a1f563e75..e6cfcd12709746233ee24f1aed06961181d8ebea 100644 --- a/src/core/theory.mli +++ b/src/core/theory.mli @@ -160,7 +160,10 @@ module Context : sig exception UnknownIdent of ident exception RedeclaredIdent of ident + + exception NonLocal of ident exception CannotInstantiate of ident + exception BadInstance of ident * ident end diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 0b83458a15f8391efba095d2401c3f651a7a872d..02519611c620d918826852c907ecea1b01828a90 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -1129,16 +1129,24 @@ and add_decl env th = function | CStsym (p,q) -> let ts1 = find_tysymbol_ns p t.th_export 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 } | CSlsym (p,q) -> let ls1 = find_lsymbol_ns p t.th_export 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 } | CSlemma p -> 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 } | CSgoal p -> 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 } in let s = List.fold_left add_inst empty_inst s in