Commit 12c64ce4 authored by MARCHE Claude's avatar MARCHE Claude

trans compute: more tests

parent dbc31d46
......@@ -63,6 +63,16 @@ let eval_int_op op ls l ty =
end
| _ -> t_app ls l ty
let eval_int_rel op ls l ty =
match l with
| [{t_node = Tconst c1};{t_node = Tconst c2}] ->
begin
try to_bool (op (big_int_of_const c1) (big_int_of_const c2))
with NotNum | Division_by_zero ->
t_app ls l ty
end
| _ -> t_app ls l ty
let eval_int_uop op ls l ty =
match l with
| [{t_node = Tconst c1}] ->
......@@ -84,14 +94,11 @@ let built_in_theories =
"infix -", None, eval_int_op BigInt.sub;
"infix *", None, eval_int_op BigInt.mul;
"prefix -", Some ls_minus, eval_int_uop BigInt.minus;
(*
"infix <", None, eval_int_rel BigInt.lt;
"infix <=", None, eval_int_rel BigInt.le;
"infix >", None, eval_int_rel BigInt.gt;
"infix >=", None, eval_int_rel BigInt.ge;
*)
] ;
(*
["int"],"MinMax", [],
[ "min", None, eval_int_op BigInt.min;
"max", None, eval_int_op BigInt.max;
......@@ -104,6 +111,7 @@ let built_in_theories =
[ "div", None, eval_int_op BigInt.euclidean_div;
"mod", None, eval_int_op BigInt.euclidean_mod;
] ;
(*
["map"],"Map", ["map", builtin_map_type],
[ "const", Some ls_map_const, eval_map_const;
"get", Some ls_map_get, eval_map_get;
......
......@@ -25,10 +25,216 @@ theory T
function g int : int
axiom g4 : g 4 = 7
axiom g4: g 4 = 7
meta "rewrite" prop g4
goal j1 : g (2+2) = 7
goal j1: g (2+2) = 7
end
theory TestList
use import int.Int
use import list.List
constant l1 : list int = Cons 12 (Cons 34 (Cons 56 Nil))
goal g1: match l1 with Nil -> 0 | Cons x y -> x end = 12
use import list.Length
goal g2: length l1 = 3
use import list.HdTlNoOpt
meta "rewrite" prop hd_cons
meta "rewrite" prop tl_cons
goal g3: hd l1 = 12
(* typing bug
use import list.Append
constant l2 : list int =
Cons 12 (Cons 34 (Cons 56 Nil)) ++ Cons 78 (Cons 90 Nil)
goal h1: l2 = l1
goal h2: length l2 = 5
*)
end
theory Rstandard
type t
constant u : t
constant a : t
function f t t : t
function g t : t
axiom a1 : g a = a
meta "rewrite" prop a1
constant b : t
axiom a2 : f b b = g b
meta "rewrite" prop a2
function h t : t
axiom a3 : forall x:t. f (h x) a = g x
meta "rewrite" prop a3
function i t t : t
axiom a4 : forall x y:t. i x y = f x y
meta "rewrite" prop a4
function j t t : t
axiom a5 : forall x:t. j x x = x
meta "rewrite" prop a5
end
theory TestStandard
use import Rstandard
goal g00 : u = g a
goal g01 : f (g (g a)) u = f a (g a)
goal g02 : u = f b b
goal g03 : f (f b b) (g b) = f u (f b b)
goal g04 : f (h u) a = f (h a) a
goal g05 : i a b = u
goal g06 : j a b = u
goal g07 : j a a = u
end
theory Rgroup
type t
function ( * ) t t : t
function e : t
function i t : t
axiom assoc : forall x y z:t. (x * y) * z = x * (y * z)
meta "rewrite" prop assoc
axiom id_left : forall x:t. e * x = x
meta "rewrite" prop id_left
axiom inv_left : forall x:t. i x * x = e
meta "rewrite" prop inv_left
constant a:t
constant b:t
constant c:t
goal g0: (a * b) * c = e
goal g01: (a * e) * c = a * c
goal g1: (b * i a) * a = b
goal g2: ((b * i a) * a) * a = b * a
end
theory Rinteger
use export int.Int
lemma l1 : forall x:int. x + 0 = x
meta "rewrite" prop l1
end
theory TestInteger
use import Rinteger
predicate f1 (y:int) = y > 0 /\ true
goal g1 : true /\ false
predicate f2 (y:int) = y + 0 >= 1
function f3 (y:int) : int = y + 0
goal g2 : 1 + 0 = 1
goal g3 : 1 + 0 >= 1
end
theory MoreSets
use export set.Set
meta "rewrite" prop mem_empty
meta "rewrite" prop add_def1
meta "rewrite" prop union_def1
end
theory TestSets
use import MoreSets
type t = A | B | C | D
goal g00 : mem A empty
goal g01 : mem A (add B empty)
goal g015 : mem A (singleton B)
goal g02 : mem A (union (add B empty) (add C empty))
goal g025 : mem A (union (singleton B) (singleton C))
end
......@@ -32,22 +32,146 @@
</goal>
<goal name="i1" sum="dfe815a019525fce8a2b755ff30f708a" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="i1.1" expl="1." sum="9b65938796ec0367c432c6b1d65fe493">
</goal>
</transf>
</goal>
<goal name="i2" sum="28f0e4a6c637d7af3829655f5173f1e7" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="i2.1" expl="1." sum="479799d9b39348879ba94f8a07c969f6">
</goal>
</transf>
</goal>
<goal name="j1" sum="89e081884a488d0109ef1938861ab614" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="j1.1" expl="1." sum="e8153b085c774d327b6f8e32b778795d">
</transf>
</goal>
</theory>
<theory name="TestList" expanded="true">
<goal name="g1" sum="f55bdd48b7c84d63db3d500485f0d1f5" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="g2" sum="ea853a23a637408ca6f2a1d4f21d0bf7" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="g3" sum="f1e9a9ae39f7d5c63ce17202d5b6a04f" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
</theory>
<theory name="Rstandard" expanded="true">
</theory>
<theory name="TestStandard" expanded="true">
<goal name="g00" sum="0ceddda03e7e96cda00c67eebccb8ce2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g00.1" expl="1." sum="72e859206601f617bc9e8d202f1736c7">
</goal>
</transf>
</goal>
<goal name="g01" sum="033e36efdc75e7ebee7089bb79aae621" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g01.1" expl="1." sum="d6d954e45cea3cfb507006372f300730">
</goal>
</transf>
</goal>
<goal name="g02" sum="e9fe9f1ccbd8b3e9306f10125f9884fe" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g02.1" expl="1." sum="bf81b44246d2030307c2cbbc6036407a">
</goal>
</transf>
</goal>
<goal name="g03" sum="0d4620924ddd3999e33c97573f5b78e0" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g03.1" expl="1." sum="4f95c487067aa0d0dee0ac82ede93e99">
</goal>
</transf>
</goal>
<goal name="g04" sum="e37cdc4814159dbd3887a5880f33246c" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g04.1" expl="1." sum="15d82520ff40518ce3e75cf46bb5c135">
</goal>
</transf>
</goal>
<goal name="g05" sum="4e7c955211deed29770e221db4c89bca" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g05.1" expl="1." sum="6f9cf28d8e4785900d38fff421f2260d">
</goal>
</transf>
</goal>
<goal name="g06" sum="447bada60ec36071cd53b698cbf73823" expanded="true">
</goal>
<goal name="g07" sum="9f175ea63c4a17c0a01aadffe9cf5e9f" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g07.1" expl="1." sum="ffa418ac5ab3f343a3554872c65c8bd9">
</goal>
</transf>
</goal>
</theory>
<theory name="Rgroup" expanded="true">
<goal name="g0" sum="1e4b57ee823bf83fde917bdd0b03d14a" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g0.1" expl="1." sum="143d0d6addcac455f08acfb659827668">
</goal>
</transf>
</goal>
<goal name="g01" sum="0a7faedd8825702fce72f3e84ec82571" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g01.1" expl="1." sum="a66352ac30125db23e59fdc4823816b6">
</goal>
</transf>
</goal>
<goal name="g1" sum="825053ebfb5449346b8ed12490cc9354" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g1.1" expl="1." sum="992aa1eb1a8bf3883d4100848222a45e">
</goal>
</transf>
</goal>
<goal name="g2" sum="76634810995226e5b7def51a0259205b" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g2.1" expl="1." sum="061d6069cfc72329b2dacb4392f050c9">
</goal>
</transf>
</goal>
</theory>
<theory name="Rinteger" expanded="true">
<goal name="l1" sum="9d62555b2a847e0ba9a9e9199cbf2c38" expanded="true">
</goal>
</theory>
<theory name="TestInteger" expanded="true">
<goal name="g1" sum="dab58bcd2a433e50f94afd9cd1659810" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g1.1" expl="1." sum="4c4937d701abd0d106d51fa154f0e03c">
</goal>
</transf>
</goal>
<goal name="g2" sum="58217b4a5d78d925ea3cf1a798093f35" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="g3" sum="3dcaf92c24507ef6b9d45c146cfeffa1" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
</theory>
<theory name="MoreSets" expanded="true">
</theory>
<theory name="TestSets" expanded="true">
<goal name="g00" sum="f038e056e11482d4fcfb897f4952d3e4" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g00.1" expl="1." sum="d41e69e131353b6c9f0b213b7cea5c12">
</goal>
</transf>
</goal>
<goal name="g01" sum="7177ee4dcc6665dea602aced3271f562" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g01.1" expl="1." sum="70eeef8e11e94a8fc0fcf899903c1a7c">
</goal>
</transf>
</goal>
<goal name="g015" sum="bb4d9978c3fa326961606408c9cc9cd5" expanded="true">
</goal>
<goal name="g02" sum="bf942bd01c45cd6931b03788e6d9065e" expanded="true">
</goal>
<goal name="g025" sum="396190e131bb8f99956a2f2a7d61e075" expanded="true">
</goal>
</theory>
</file>
</why3session>
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