Commit e3447b63 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

trans compute: more robust selection of rewrite rules

parent c503c7fc
......@@ -353,7 +353,12 @@ let collect_rule_decl prs e d =
| Decl.Dlogic _ -> e
| Decl.Dprop(_, pr, t) ->
if Decl.Spr.mem pr prs then
Reduction_engine.add_rule t e
try
Reduction_engine.add_rule t e
with Reduction_engine.NotARewriteRule msg ->
Warning.emit "prop %a cannot be turned into a rewrite rule: %s"
Pretty.print_pr pr msg;
e
else e
let collect_rules env km prs t =
......
......@@ -766,7 +766,20 @@ let create env km =
exception NotARewriteRule of string
let extract_rule t =
let extract_rule km t =
let check_ls ls =
try let _ = Hls.find builtins ls in
raise (NotARewriteRule "root of lhs of rule must not be a built-in symbol")
with Not_found ->
let d = Ident.Mid.find ls.ls_name km in
match d.Decl.d_node with
| Decl.Dtype _ | Decl.Dprop _ -> assert false
| Decl.Dlogic _ ->
raise (NotARewriteRule "root of lhs of rule must not be defined symbol")
| Decl.Ddata _ ->
raise (NotARewriteRule "root of lhs of rule must not be a constructor nor a projection")
| Decl.Dparam _ | Decl.Dind _ -> ()
in
let rec aux acc t =
match t.t_node with
| Tquant(Tforall,q) ->
......@@ -775,14 +788,14 @@ let extract_rule t =
| Tbinop(Tiff,t1,t2) ->
begin
match t1.t_node with
| Tapp(ls,args) -> acc,ls,args,t2
| Tapp(ls,args) -> check_ls ls; acc,ls,args,t2
| _ -> raise
(NotARewriteRule "lhs of <-> should be a predicate symbol")
end
| Tapp(ls,[t1;t2]) when ls == ps_equ ->
begin
match t1.t_node with
| Tapp(ls,args) -> acc,ls,args,t2
| Tapp(ls,args) -> check_ls ls; acc,ls,args,t2
| _ -> raise
(NotARewriteRule "lhs of = should be a function symbol")
end
......@@ -793,7 +806,7 @@ let extract_rule t =
let add_rule t e =
let vars,ls,args,r = extract_rule t in
let vars,ls,args,r = extract_rule e.known_map t in
let rules =
try Mls.find ls e.rules
with Not_found -> []
......
......@@ -204,7 +204,9 @@ theory Rinteger
lemma l1 : forall x:int. x + 0 = x
meta "rewrite" prop l1
(* not allowed: + is a built-in symbol
meta "rewrite" prop l1
*)
goal g1 : forall y. 2+2 = y
......
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