Commit 9ddf42ab authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: admit "clone with axiom L"

parent 0affb677
...@@ -448,28 +448,17 @@ let use_export uc th = ...@@ -448,28 +448,17 @@ let use_export uc th =
(** Clone *) (** Clone *)
type th_inst = { type th_inst = {
inst_ts : tysymbol Mts.t; inst_ts : tysymbol Mts.t; (* old to new *)
inst_ls : lsymbol Mls.t; inst_ls : lsymbol Mls.t;
inst_lemma : Spr.t; inst_pr : prop_kind Mpr.t;
inst_goal : Spr.t;
} }
let empty_inst = { let empty_inst = {
inst_ts = Mts.empty; inst_ts = Mts.empty;
inst_ls = Mls.empty; inst_ls = Mls.empty;
inst_lemma = Spr.empty; inst_pr = Mpr.empty;
inst_goal = Spr.empty;
} }
let create_inst ~ts ~ls ~lemma ~goal =
let add_ts acc (tso,tsn) = Mts.add tso tsn acc in
let add_ls acc (lso,lsn) = Mls.add lso lsn acc in
let add_pr acc lem = Spr.add lem acc in {
inst_ts = List.fold_left add_ts Mts.empty ts;
inst_ls = List.fold_left add_ls Mls.empty ls;
inst_lemma = List.fold_left add_pr Spr.empty lemma;
inst_goal = List.fold_left add_pr Spr.empty goal }
exception CannotInstantiate of ident exception CannotInstantiate of ident
type clones = { type clones = {
...@@ -552,7 +541,7 @@ let cl_init_ls cl ls ls' = ...@@ -552,7 +541,7 @@ let cl_init_ls cl ls ls' =
with Invalid_argument _ -> raise (BadInstance (id, ls'.ls_name))); with Invalid_argument _ -> raise (BadInstance (id, ls'.ls_name)));
cl.ls_table <- Mls.add ls ls' cl.ls_table cl.ls_table <- Mls.add ls ls' cl.ls_table
let cl_init_pr cl pr = let cl_init_pr cl pr _ =
let id = pr.pr_name in let id = pr.pr_name in
if not (Sid.mem id cl.cl_local) then raise (NonLocal id) if not (Sid.mem id cl.cl_local) then raise (NonLocal id)
...@@ -560,8 +549,7 @@ let cl_init th inst = ...@@ -560,8 +549,7 @@ let cl_init th inst =
let cl = empty_clones th.th_local in let cl = empty_clones th.th_local in
Mts.iter (cl_init_ts cl) inst.inst_ts; Mts.iter (cl_init_ts cl) inst.inst_ts;
Mls.iter (cl_init_ls cl) inst.inst_ls; Mls.iter (cl_init_ls cl) inst.inst_ls;
Spr.iter (cl_init_pr cl) inst.inst_lemma; Mpr.iter (cl_init_pr cl) inst.inst_pr;
Spr.iter (cl_init_pr cl) inst.inst_goal;
cl cl
(* clone declarations *) (* clone declarations *)
...@@ -614,9 +602,8 @@ let cl_logic cl inst ldl = ...@@ -614,9 +602,8 @@ let cl_logic cl inst ldl =
let cl_ind cl inst (s, idl) = let cl_ind cl inst (s, idl) =
let add_case (pr,f) = let add_case (pr,f) =
if Spr.mem pr inst.inst_lemma || Spr.mem pr inst.inst_goal if Mpr.mem pr inst.inst_pr then raise (CannotInstantiate pr.pr_name);
then raise (CannotInstantiate pr.pr_name) cl_find_pr cl pr, cl_trans_fmla cl f
else cl_find_pr cl pr, cl_trans_fmla cl f
in in
let add_ind (ps,la) = let add_ind (ps,la) =
if Mls.mem ps inst.inst_ls if Mls.mem ps inst.inst_ls
...@@ -626,13 +613,15 @@ let cl_ind cl inst (s, idl) = ...@@ -626,13 +613,15 @@ let cl_ind cl inst (s, idl) =
create_ind_decl s (List.map add_ind idl) create_ind_decl s (List.map add_ind idl)
let cl_prop cl inst (k,pr,f) = let cl_prop cl inst (k,pr,f) =
let k' = match k with let k' = match k, Mpr.find_opt pr inst.inst_pr with
| Pskip | Pgoal -> Pskip | _, Some Pskip -> invalid_arg "Theory.clone_export"
| Plemma when Spr.mem pr inst.inst_goal -> Pskip | (Pskip | Pgoal), _ -> Pskip
| Paxiom when Spr.mem pr inst.inst_goal -> Pgoal | Paxiom, Some Pgoal -> Pgoal
| Paxiom when Spr.mem pr inst.inst_lemma -> Plemma | Plemma, Some Pgoal -> Pskip
| Paxiom | Plemma -> Paxiom | (Paxiom | Plemma), Some Paxiom -> Paxiom
in | (Paxiom | Plemma), Some Plemma -> Plemma
| Paxiom, None -> Paxiom (* TODO: Plemma *)
| Plemma, None -> Paxiom in
let pr' = cl_find_pr cl pr in let pr' = cl_find_pr cl pr in
let f' = cl_trans_fmla cl f in let f' = cl_trans_fmla cl f in
create_prop_decl k' pr' f' create_prop_decl k' pr' f'
......
...@@ -166,20 +166,13 @@ val use_export : theory_uc -> theory -> theory_uc ...@@ -166,20 +166,13 @@ val use_export : theory_uc -> theory -> theory_uc
(** {2 Clone} *) (** {2 Clone} *)
type th_inst = { type th_inst = {
inst_ts : tysymbol Mts.t; (* old to new *) inst_ts : tysymbol Mts.t; (* old to new *)
inst_ls : lsymbol Mls.t; inst_ls : lsymbol Mls.t;
inst_lemma : Spr.t; inst_pr : prop_kind Mpr.t;
inst_goal : Spr.t;
} }
val empty_inst : th_inst val empty_inst : th_inst
val create_inst :
ts : (tysymbol * tysymbol) list ->
ls : (lsymbol * lsymbol) list ->
lemma : prsymbol list ->
goal : prsymbol list -> th_inst
val warn_clone_not_abstract : Loc.position -> theory -> unit val warn_clone_not_abstract : Loc.position -> theory -> unit
val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
......
...@@ -518,8 +518,7 @@ let clone_decl inst cl uc d = match d.d_node with ...@@ -518,8 +518,7 @@ let clone_decl inst cl uc d = match d.d_node with
| Dind (s, idl) -> | Dind (s, idl) ->
let get_ls (ls,_) = cl_clone_ls inst cl ls in let get_ls (ls,_) = cl_clone_ls inst cl ls in
let get_case (pr,f) = let get_case (pr,f) =
if Spr.mem pr inst.inst_lemma || Spr.mem pr inst.inst_goal if Mpr.mem pr inst.inst_pr then raise (CannotInstantiate pr.pr_name);
then raise (CannotInstantiate pr.pr_name);
let pr' = create_prsymbol (id_clone pr.pr_name) in let pr' = create_prsymbol (id_clone pr.pr_name) in
cl.pr_table <- Mpr.add pr pr' cl.pr_table; cl.pr_table <- Mpr.add pr pr' cl.pr_table;
pr', cl_trans_fmla cl f in pr', cl_trans_fmla cl f in
...@@ -528,13 +527,15 @@ let clone_decl inst cl uc d = match d.d_node with ...@@ -528,13 +527,15 @@ let clone_decl inst cl uc d = match d.d_node with
let d = create_ind_decl s (List.map2 get_ind lls idl) in let d = create_ind_decl s (List.map2 get_ind lls idl) in
add_pdecl ~vc:false uc (create_pure_decl d) add_pdecl ~vc:false uc (create_pure_decl d)
| Dprop (k,pr,f) -> | Dprop (k,pr,f) ->
let k' = match k with let k' = match k, Mpr.find_opt pr inst.inst_pr with
| Pskip | Pgoal -> Pskip | _, Some Pskip -> invalid_arg "Pmodule.clone_export"
| Plemma when Spr.mem pr inst.inst_goal -> Pskip | (Pskip | Pgoal), _ -> Pskip
| Paxiom when Spr.mem pr inst.inst_goal -> Pgoal | Paxiom, Some Pgoal -> Pgoal
| Paxiom when Spr.mem pr inst.inst_lemma -> Plemma | Plemma, Some Pgoal -> Pskip
| Paxiom -> Paxiom (* TODO: Plemma *) | (Paxiom | Plemma), Some Paxiom -> Paxiom
| Plemma -> Paxiom in | (Paxiom | Plemma), Some Plemma -> Plemma
| Paxiom, None -> Paxiom (* TODO: Plemma *)
| Plemma, None -> Paxiom in
let pr' = create_prsymbol (id_clone pr.pr_name) in let pr' = create_prsymbol (id_clone pr.pr_name) in
cl.pr_table <- Mpr.add pr pr' cl.pr_table; cl.pr_table <- Mpr.add pr pr' cl.pr_table;
let d = create_prop_decl k' pr' (cl_trans_fmla cl f) in let d = create_prop_decl k' pr' (cl_trans_fmla cl f) in
...@@ -560,8 +561,7 @@ let clone_export uc m inst = ...@@ -560,8 +561,7 @@ let clone_export uc m inst =
if not (Sid.mem id m.mod_local) then raise (NonLocal id) in if not (Sid.mem id m.mod_local) then raise (NonLocal id) in
Mts.iter (fun ts _ -> check_local ts.ts_name) inst.inst_ts; Mts.iter (fun ts _ -> check_local ts.ts_name) inst.inst_ts;
Mls.iter (fun ls _ -> check_local ls.ls_name) inst.inst_ls; Mls.iter (fun ls _ -> check_local ls.ls_name) inst.inst_ls;
Spr.iter (fun pr -> check_local pr.pr_name) inst.inst_goal; Mpr.iter (fun pr _ -> check_local pr.pr_name) inst.inst_pr;
Spr.iter (fun pr -> check_local pr.pr_name) inst.inst_lemma;
let cl = empty_clones m.mod_local in let cl = empty_clones m.mod_local in
let rec add_unit uc u = match u with let rec add_unit uc u = match u with
| Udecl d -> clone_pdecl inst cl uc d | Udecl d -> clone_pdecl inst cl uc d
......
...@@ -164,7 +164,7 @@ ...@@ -164,7 +164,7 @@
%start <Pmodule.pmodule Stdlib.Mstr.t> mlw_file %start <Pmodule.pmodule Stdlib.Mstr.t> mlw_file
%% %%
(* Modules and namespaces *) (* Modules and scopes *)
mlw_file: mlw_file:
| mlw_module* EOF | mlw_module* EOF
...@@ -220,6 +220,7 @@ single_clone_subst: ...@@ -220,6 +220,7 @@ single_clone_subst:
| FUNCTION qualid EQUAL qualid { CSfsym ($2,$4) } | FUNCTION qualid EQUAL qualid { CSfsym ($2,$4) }
| PREDICATE qualid EQUAL qualid { CSpsym ($2,$4) } | PREDICATE qualid EQUAL qualid { CSpsym ($2,$4) }
| VAL qualid EQUAL qualid { CSvsym ($2,$4) } | VAL qualid EQUAL qualid { CSvsym ($2,$4) }
| AXIOM qualid { CSaxiom ($2) }
| LEMMA qualid { CSlemma ($2) } | LEMMA qualid { CSlemma ($2) }
| GOAL qualid { CSgoal ($2) } | GOAL qualid { CSgoal ($2) }
......
...@@ -209,6 +209,7 @@ type clone_subst = ...@@ -209,6 +209,7 @@ type clone_subst =
| CSfsym of qualid * qualid | CSfsym of qualid * qualid
| CSpsym of qualid * qualid | CSpsym of qualid * qualid
| CSvsym of qualid * qualid | CSvsym of qualid * qualid
| CSaxiom of qualid
| CSlemma of qualid | CSlemma of qualid
| CSgoal of qualid | CSgoal of qualid
......
...@@ -81,6 +81,7 @@ let find_prop tuc q = find_prop_ns (Theory.get_namespace tuc) q ...@@ -81,6 +81,7 @@ let find_prop tuc q = find_prop_ns (Theory.get_namespace tuc) q
let find_prop_of_kind k tuc q = let find_prop_of_kind k tuc q =
let pr = find_prop tuc q in let pr = find_prop tuc q in
match (Mid.find pr.pr_name tuc.uc_known).d_node with match (Mid.find pr.pr_name tuc.uc_known).d_node with
| Dind _ when k = Paxiom -> pr
| Dprop (l,_,_) when l = k -> pr | Dprop (l,_,_) when l = k -> pr
| _ -> Loc.errorm ~loc:(qloc q) "proposition %a is not %s" | _ -> Loc.errorm ~loc:(qloc q) "proposition %a is not %s"
print_qualid q (match k with print_qualid q (match k with
...@@ -981,43 +982,41 @@ let type_inst ({muc_theory = tuc} as muc) {mod_theory = t} s = ...@@ -981,43 +982,41 @@ let type_inst ({muc_theory = tuc} as muc) {mod_theory = t} s =
| CStsym (p,[],PTtyapp (q,[])) -> | CStsym (p,[],PTtyapp (q,[])) ->
let ts1 = find_tysymbol_ns t.th_export p in let ts1 = find_tysymbol_ns t.th_export p in
let ts2 = find_tysymbol tuc q in let ts2 = find_tysymbol tuc q in
if Mts.mem ts1 s.inst_ts then { s with inst_ts = Loc.try4 ~loc:(qloc p) Mts.add_new
Loc.error ~loc:(qloc p) (ClashSymbol ts1.ts_name.id_string); (ClashSymbol ts1.ts_name.id_string) ts1 ts2 s.inst_ts }
{ s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
| CStsym (p,tvl,pty) -> | CStsym (p,tvl,pty) ->
let ts1 = find_tysymbol_ns t.th_export p in let ts1 = find_tysymbol_ns t.th_export p in
let id = id_user (ts1.ts_name.id_string ^ "_subst") (qloc p) in let id = id_user (ts1.ts_name.id_string ^ "_subst") (qloc p) in
let tvl = List.map (fun id -> tv_of_string id.id_str) tvl in let tvl = List.map (fun id -> tv_of_string id.id_str) tvl in
let ts2 = Loc.try3 ~loc:(qloc p) let ts2 = Loc.try3 ~loc:(qloc p)
create_itysymbol_alias id tvl (ity_of_pty muc pty) in create_itysymbol_alias id tvl (ity_of_pty muc pty) in
if Mts.mem ts1 s.inst_ts then { s with inst_ts = Loc.try4 ~loc:(qloc p) Mts.add_new
Loc.error ~loc:(qloc p) (ClashSymbol ts1.ts_name.id_string); (ClashSymbol ts1.ts_name.id_string) ts1 ts2.its_ts s.inst_ts }
{ s with inst_ts = Mts.add ts1 ts2.its_ts s.inst_ts }
| CSfsym (p,q) -> | CSfsym (p,q) ->
let ls1 = find_fsymbol_ns t.th_export p in let ls1 = find_fsymbol_ns t.th_export p in
let ls2 = find_fsymbol tuc q in let ls2 = find_fsymbol tuc q in
if Mls.mem ls1 s.inst_ls then { s with inst_ls = Loc.try4 ~loc:(qloc p) Mls.add_new
Loc.error ~loc:(qloc p) (ClashSymbol ls1.ls_name.id_string); (ClashSymbol ls1.ls_name.id_string) ls1 ls2 s.inst_ls }
{ s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
| CSpsym (p,q) -> | CSpsym (p,q) ->
let ls1 = find_psymbol_ns t.th_export p in let ls1 = find_psymbol_ns t.th_export p in
let ls2 = find_psymbol tuc q in let ls2 = find_psymbol tuc q in
if Mls.mem ls1 s.inst_ls then { s with inst_ls = Loc.try4 ~loc:(qloc p) Mls.add_new
Loc.error ~loc:(qloc p) (ClashSymbol ls1.ls_name.id_string); (ClashSymbol ls1.ls_name.id_string) ls1 ls2 s.inst_ls }
{ s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
| CSvsym (p,_) -> | CSvsym (p,_) ->
Loc.errorm ~loc:(qloc p) Loc.errorm ~loc:(qloc p)
"program symbol instantiation is not supported yet" (* TODO *) "program symbol instantiation is not supported yet" (* TODO *)
| CSaxiom p ->
let pr = find_prop_ns t.th_export p in
{ s with inst_pr = Loc.try4 ~loc:(qloc p) Mpr.add_new
(ClashSymbol pr.pr_name.id_string) pr Paxiom s.inst_pr }
| CSlemma p -> | CSlemma p ->
let pr = find_prop_ns t.th_export p in let pr = find_prop_ns t.th_export p in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal then { s with inst_pr = Loc.try4 ~loc:(qloc p) Mpr.add_new
Loc.error ~loc:(qloc p) (ClashSymbol pr.pr_name.id_string); (ClashSymbol pr.pr_name.id_string) pr Plemma s.inst_pr }
{ s with inst_lemma = Spr.add pr s.inst_lemma }
| CSgoal p -> | CSgoal p ->
let pr = find_prop_ns t.th_export p in let pr = find_prop_ns t.th_export p in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal then { s with inst_pr = Loc.try4 ~loc:(qloc p) Mpr.add_new
Loc.error ~loc:(qloc p) (ClashSymbol pr.pr_name.id_string); (ClashSymbol pr.pr_name.id_string) pr Pgoal s.inst_pr }
{ s with inst_goal = Spr.add pr s.inst_goal }
in in
List.fold_left add_inst empty_inst s List.fold_left add_inst empty_inst s
......
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