Commit fad54f38 authored by MARCHE Claude's avatar MARCHE Claude

allow rewrite rules with a builtin symbol or a defined symbol, or a constructor

as root of the left-hand side
parent 1eb08942
......@@ -61,7 +61,7 @@ exception Undetermined
let to_bool b = if b then t_true else t_false
let t_app_value ls l ty =
let _t_app_value ls l ty =
Term (t_app ls (List.map term_of_value l) ty)
let is_zero v =
......@@ -83,41 +83,61 @@ let eval_int_op op simpl ls l ty =
with NotNum | Division_by_zero ->
simpl ls t1 t2 ty
end
| _ -> t_app_value ls l ty
| _ -> assert false (* t_app_value ls l ty *)
(* unused anymore, for the moment
let simpl_none ls t1 t2 ty =
t_app_value ls [t1;t2] ty
*)
let simpl_add ls t1 t2 ty =
let simpl_add _ls t1 t2 _ty =
if is_zero t1 then t2 else
if is_zero t2 then t1 else
raise Undetermined
(*
t_app_value ls [t1;t2] ty
*)
let simpl_sub ls t1 t2 ty =
let simpl_sub _ls t1 t2 _ty =
if is_zero t2 then t1 else
raise Undetermined
(*
t_app_value ls [t1;t2] ty
*)
let simpl_mul ls t1 t2 ty =
let simpl_mul _ls t1 t2 _ty =
if is_zero t1 then t1 else
if is_zero t2 then t2 else
if is_one t1 then t2 else
if is_one t2 then t1 else
raise Undetermined
(*
t_app_value ls [t1;t2] ty
*)
let simpl_divmod ls t1 t2 ty =
let simpl_divmod _ls t1 t2 _ty =
if is_zero t1 then t1 else
if is_one t2 then t1 else
raise Undetermined
(*
t_app_value ls [t1;t2] ty
*)
let simpl_minmax ls v1 v2 ty =
let simpl_minmax _ls v1 v2 _ty =
match v1,v2 with
| Term t1, Term t2 ->
if t_equal t1 t2 then v1 else t_app_value ls [v1;v2] ty
| _ -> t_app_value ls [v1;v2] ty
let eval_int_rel op ls l ty =
if t_equal t1 t2 then v1 else
raise Undetermined
(*
t_app_value ls [v1;v2] ty
*)
| _ ->
raise Undetermined
(*
t_app_value ls [v1;v2] ty
*)
let eval_int_rel op _ls l _ty =
match l with
| [t1 ; t2] ->
begin
......@@ -126,20 +146,23 @@ let eval_int_rel op ls l ty =
let n2 = big_int_of_value t2 in
Term (to_bool (op n1 n2))
with NotNum | Division_by_zero ->
t_app_value ls l ty
raise Undetermined
(* t_app_value ls l ty *)
end
| _ -> t_app_value ls l ty
| _ -> assert false
(* t_app_value ls l ty *)
let eval_int_uop op ls l ty =
let eval_int_uop op _ls l _ty =
match l with
| [t1] ->
begin
try
let n1 = big_int_of_value t1 in Int (op n1)
with NotNum | Division_by_zero ->
t_app_value ls l ty
raise Undetermined
(* t_app_value ls l ty *)
end
| _ -> t_app_value ls l ty
| _ -> assert false
let built_in_theories =
......@@ -561,13 +584,18 @@ and reduce_app engine st ls ~orig ty rem_cont =
else
if ls_equal ls fs_func_app then
match st with
| t2 :: t1 :: rem_st -> reduce_func_app ~orig ty rem_st t1 t2 rem_cont
| t2 :: t1 :: rem_st ->
begin
try
reduce_func_app ~orig ty rem_st t1 t2 rem_cont
with Undetermined ->
reduce_app_no_equ engine st ls ~orig ty rem_cont
end
| _ -> assert false
else
reduce_app_no_equ engine st ls ~orig ty rem_cont
and reduce_func_app ~orig ty rem_st t1 t2 rem_cont =
try
and reduce_func_app ~orig _ty rem_st t1 t2 rem_cont =
(* attempt to decompile t1 under the form
(epsilon fc. forall x. fc @ x = body)
that is equivalent to \x.body *)
......@@ -659,11 +687,6 @@ and reduce_func_app ~orig ty rem_st t1 t2 rem_cont =
| _ -> raise Undetermined
end
| _ -> raise Undetermined
with Undetermined ->
{ value_stack =
(v_label_copy orig (t_app_value fs_func_app [t1;t2] ty)) :: rem_st;
cont_stack = rem_cont;
}
and reduce_app_no_equ engine st ls ~orig ty rem_cont =
let arity = List.length ls.ls_args in
......@@ -674,7 +697,7 @@ and reduce_app_no_equ engine st ls ~orig ty rem_cont =
{ value_stack = (v_label_copy orig v) :: rem_st;
cont_stack = rem_cont;
}
with Not_found ->
with Not_found | Undetermined ->
let args = List.map term_of_value args in
try
let d = Ident.Mid.find ls.ls_name engine.known_map in
......@@ -942,7 +965,8 @@ let create p env km =
exception NotARewriteRule of string
let extract_rule km 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")
......@@ -956,6 +980,7 @@ let extract_rule km t =
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) ->
......@@ -964,14 +989,14 @@ let extract_rule km t =
| Tbinop(Tiff,t1,t2) ->
begin
match t1.t_node with
| Tapp(ls,args) -> check_ls ls; 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) -> check_ls ls; acc,ls,args,t2
| Tapp(ls,args) -> (* check_ls ls; *) acc,ls,args,t2
| _ -> raise
(NotARewriteRule "lhs of = should be a function symbol")
end
......
......@@ -15,6 +15,14 @@ constant compose : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c) =
goal g2: compose f f 42 = a
constant h : int -> int
axiom a1 : h 42 = 56
meta "rewrite" prop a1
goal g3: h 42 = 4
end
theory A
......@@ -109,6 +117,15 @@ theory TestArith
goal n3: min n n = 42
goal n4: min 3 4 = n
function f int : int
axiom a42 : f 42 + 43 = 56
meta rewrite prop a42
goal o1 : f (6*7) + (42 + 1) = n
end
theory TestRecord
......@@ -158,6 +175,14 @@ theory TestList
goal h3: forall x y:int. Cons x Nil = Cons y Nil
constant l3 : list int
axiom dangerous: Cons 12 Nil = l3
meta rewrite prop dangerous
goal i1: l3 = Nil ++ Nil
end
......
......@@ -3,176 +3,184 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../test_compute.why" expanded="true">
<theory name="Lambda" sum="688e289f6102a82e4b04b5dd390993b9" expanded="true">
<goal name="g1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<theory name="Lambda" sum="ac7b1c25f8dd32d440e0b14d115c7c15">
<goal name="g1">
<transf name="compute_in_goal">
<goal name="g1.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="g2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g2">
<transf name="compute_in_goal">
<goal name="g2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="g3">
</goal>
</theory>
<theory name="A" sum="0e4355327797e8f3d23d6df80a329362" expanded="true">
<goal name="G1" expanded="true">
<theory name="A" sum="0e4355327797e8f3d23d6df80a329362">
<goal name="G1">
</goal>
<goal name="G2" expanded="true">
<goal name="G2">
</goal>
<goal name="G3" expanded="true">
<goal name="G3">
</goal>
<goal name="g" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g">
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
<theory name="Test" sum="cd473d7e70fa0fdfbc7f9f5523952c9e" expanded="true">
<goal name="g1" expanded="true">
<theory name="Test" sum="cd473d7e70fa0fdfbc7f9f5523952c9e">
<goal name="g1">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g2">
<transf name="compute_in_goal">
<goal name="g2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="g3" expanded="true">
<goal name="g3">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g10" expanded="true">
<goal name="g10">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g11" expanded="true">
<goal name="g11">
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
<theory name="TestArith" sum="c65bbe94a2f17b37cf20ea306cff2375" expanded="true">
<goal name="h1" expanded="true">
<theory name="TestArith" sum="cf84efb4f92d0a90148d60fc86520337">
<goal name="h1">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="h2" expanded="true">
<goal name="h2">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="h3" expanded="true">
<goal name="h3">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="j1" expanded="true">
<goal name="j1">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="k1" expanded="true">
<goal name="k1">
</goal>
<goal name="l1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l1">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="l2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l2">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="l3" expanded="true">
<goal name="l3">
</goal>
<goal name="l4" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l4">
<transf name="compute_in_goal">
<goal name="l4.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="l5" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l5">
<transf name="compute_in_goal">
<goal name="l5.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="l6" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l6">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="l7" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l7">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="l8" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l8">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="l9" expanded="true">
<goal name="l9">
</goal>
<goal name="m1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="m1">
<transf name="compute_in_goal">
<goal name="m1.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="m2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="m2">
<transf name="compute_in_goal">
<goal name="m2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="m3" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="m3">
<transf name="compute_in_goal">
<goal name="m3.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="m4" expanded="true">
<goal name="m4">
</goal>
<goal name="n1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n1">
<transf name="compute_in_goal">
<goal name="n1.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="n2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n2">
<transf name="compute_in_goal">
<goal name="n2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="n3" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n3">
<transf name="compute_in_goal">
<goal name="n3.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="n4" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n4">
<transf name="compute_in_goal">
<goal name="n4.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="o1">
<transf name="compute_in_goal">
<goal name="o1.1" expl="1.">
</goal>
</transf>
</goal>
</theory>
<theory name="TestRecord" sum="01e5c2659bedbfaf6934498a0580aaef" expanded="true">
<goal name="i1" expanded="true">
<theory name="TestRecord" sum="01e5c2659bedbfaf6934498a0580aaef">
<goal name="i1">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="i2" expanded="true">
<goal name="i2">
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
<theory name="TestList" sum="323cd4beae7c0fb27accdd9b68ccc864" expanded="true">
<goal name="g1" expanded="true">
<theory name="TestList" sum="ec36d89b8213f71e7ce492154030a520" expanded="true">
<goal name="g1">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g2" expanded="true">
<goal name="g2">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g3" expanded="true">
<goal name="g3">
<transf name="compute_in_goal">
</transf>
</goal>
......@@ -182,7 +190,7 @@
</goal>
</transf>
</goal>
<goal name="h2" expanded="true">
<goal name="h2">
<transf name="compute_in_goal">
</transf>
</goal>
......@@ -192,6 +200,12 @@
</goal>
</transf>
</goal>
<goal name="i1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="i1.1" expl="1.">
</goal>
</transf>
</goal>
</theory>
<theory name="Rstandard" sum="d15a33b5087e18703e665562df77da7b" expanded="true">
</theory>
......@@ -248,7 +262,7 @@
</goal>
</transf>
</goal>
<goal name="g01" expanded="true">
<goal name="g01">
<transf name="compute_in_goal">
</transf>
</goal>
......@@ -258,7 +272,7 @@
</goal>
</transf>
</goal>
<goal name="g2" expanded="true">
<goal name="g2">
<transf name="compute_in_goal">
</transf>
</goal>
......@@ -338,11 +352,11 @@
</goal>
</transf>
</goal>
<goal name="g2" expanded="true">
<goal name="g2">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g3" expanded="true">
<goal name="g3">
<transf name="compute_in_goal">
</transf>
</goal>
......
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