Commit 8db2a355 authored by DIVERIO Diego's avatar DIVERIO Diego

Fixed issue #388:

User axioms are tagged with @useraxiom attribute, which is removed when cloning.
parent 89649de4
......@@ -151,7 +151,7 @@ type ident = {
id_attrs : Sattr.t; (* identifier attributes *)
id_loc : Loc.position option; (* optional location *)
id_tag : Weakhtbl.tag; (* unique magical tag *)
}
}
module Id = MakeMSHW (struct
type t = ident
......@@ -341,6 +341,8 @@ let sanitizer head rest n = sanitizer' head rest rest n
let proxy_attr = create_attribute "mlw:proxy_symbol"
let useraxiom_attr = create_attribute "useraxiom"
let model_projected_attr = create_attribute "model_projected"
let model_vc_post_attr = create_attribute "model_vc_post"
......
......@@ -166,7 +166,8 @@ val id_unique_attr :
the "name:" attribute to generate the name instead of id.id_string *)
val proxy_attr: attribute
val useraxiom_attr: attribute
(** {2 Attributes for handling counterexamples} *)
val model_projected_attr : attribute
......
......@@ -541,10 +541,18 @@ let sprint_pkind = function
let print_pkind fmt k = pp_print_string fmt (sprint_pkind k)
let print_axiom fmt (pr, f) =
(fprintf fmt "@[<hov 2>%a%a :@ %a@]"
print_pr pr print_id_attrs pr.pr_name print_term f;
forget_tvs ())
let print_prop_decl fmt (k,pr,f) =
fprintf fmt "@[<hov 2>%a %a%a :@ %a@]" print_pkind k
print_pr pr print_id_attrs pr.pr_name print_term f;
forget_tvs ()
if k == Paxiom && not (Sattr.exists (Ident.attr_equal Ident.useraxiom_attr) pr.pr_name.id_attrs) then
print_axiom fmt (pr, f)
else
(fprintf fmt "@[<hov 2>%a %a%a :@ %a@]" print_pkind k
print_pr pr print_id_attrs pr.pr_name print_term f;
forget_tvs ())
let print_list_next sep print fmt = function
| [] -> ()
......
......@@ -649,7 +649,8 @@ let cl_find_pr cl pr =
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
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;
pr'
......
......@@ -672,11 +672,12 @@ let clone_decl inst cl uc d = match d.d_node with
| Paxiom, Some k -> false, k
| Paxiom, None -> false, inst.mi_df in
if skip then uc else
let pr' = create_prsymbol (id_clone pr.pr_name) in
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
......
......@@ -485,7 +485,7 @@ pure_decl:
| PREDICATE predicate_decl with_logic_decl* { Dlogic ($2::$3) }
| INDUCTIVE with_list1(inductive_decl) { Dind (Decl.Ind, $2) }
| COINDUCTIVE with_list1(inductive_decl) { Dind (Decl.Coind, $2) }
| AXIOM attrs(ident_nq) COLON term { Dprop (Decl.Paxiom, $2, $4) }
| AXIOM attrs(ident_nq) COLON term { Dprop (Decl.Paxiom, { $2 with id_ats = (Ptree.ATstr Ident.useraxiom_attr)::$2.id_ats; }, $4) }
| LEMMA attrs(ident_nq) COLON term { Dprop (Decl.Plemma, $2, $4) }
| GOAL attrs(ident_nq) COLON term { Dprop (Decl.Pgoal, $2, $4) }
......
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