Commit 1aefe837 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

trans compute: a few details

parent a78087aa
......@@ -98,9 +98,11 @@ let eval_equ _ls l _ty =
(*
let eval_true _ls _l _ty = Term t_true
let eval_false _ls _l _ty = Term t_false
*)
let t_app_value ls l ty =
Term (t_app ls (List.map term_of_value l) ty)
......@@ -144,10 +146,13 @@ let eval_int_uop op ls l ty =
let built_in_theories =
[ ["bool"],"Bool", [],
[
(*
["bool"],"Bool", [],
[ "True", None, eval_true ;
"False", None, eval_false ;
] ;
*)
["int"],"Int", [],
[ "infix +", None, eval_int_op BigInt.add;
"infix -", None, eval_int_op BigInt.sub;
......@@ -216,7 +221,7 @@ type engine =
}
(*
(* OBSOLETE COMMENT
A configuration is a pair (t,s) where t is a stack of terms and s is a
stack of function symbols.
......@@ -481,8 +486,14 @@ and reduce_eval st t sigma rem =
cont_stack = rem;
}
with Not_found ->
Format.eprintf "Tvar not found: %a@." Pretty.print_vs v;
assert false
(* this may happen, e.g when computing below a quantified formula *)
(*
Format.eprintf "Tvar not found: %a@." Pretty.print_vs v;
assert false
*)
{ value_stack = Term t :: st ;
cont_stack = rem;
}
end
| Tif(t1,t2,t3) ->
{ value_stack = st;
......
theory T
theory Test
goal g1: true
......@@ -11,19 +11,17 @@ theory T
goal g11: let x=1 in x=1
end
theory TestArith
use import int.Int
goal h1: 2+2=4
goal h2: 2+(-2)=0
type t = { f : int }
goal i1: let x = { f = 4 } in x.f < 5
goal i2: let x = { f = 4 } in
match x with { f = y } -> y + 1 > 3 end
goal h3: 10 = 0xA
function g int : int
......@@ -33,8 +31,30 @@ theory T
goal j1: g (2+2) = 7
use import int.Power
meta "rewrite" prop Power_0
(* not a rule: conditional
meta "rewrite" prop Power_s
*)
goal k1: power 4 3 = 64
end
theory TestRecord
use import int.Int
type t = { f : int }
goal i1: let x = { f = 4 } in x.f < 5
goal i2: let x = { f = 4 } in
match x with { f = y } -> y + 1 > 3 end
end
theory TestList
......@@ -185,6 +205,10 @@ theory Rinteger
meta "rewrite" prop l1
goal g1 : forall y. 2+2 = y
goal g2 : forall y. 0 + y + 0 + y - y = y
end
theory TestInteger
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../test_compute.why" expanded="true">
<theory name="T" expanded="true">
<theory name="Test" expanded="true">
<goal name="g1" sum="1ad4ea691c2d3b0a420f5b0819ebc531">
<transf name="compute_in_goal">
</transf>
......@@ -26,6 +26,8 @@
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
<theory name="TestArith" expanded="true">
<goal name="h1" sum="5d9ea52d9f6b9033794f44b5aa590306">
<transf name="compute_in_goal">
</transf>
......@@ -34,15 +36,23 @@
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="i1" sum="dfe815a019525fce8a2b755ff30f708a">
<goal name="h3" sum="0790685f50da7d77b303ccadd7687366">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="i2" sum="28f0e4a6c637d7af3829655f5173f1e7">
<goal name="j1" sum="27f290f0ac50c629aed289631283782c">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="k1" sum="8ddeb713a5eb541bac88d6b627655a5a" expanded="true">
</goal>
</theory>
<theory name="TestRecord">
<goal name="i1" sum="dfe815a019525fce8a2b755ff30f708a">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="j1" sum="89e081884a488d0109ef1938861ab614">
<goal name="i2" sum="28f0e4a6c637d7af3829655f5173f1e7">
<transf name="compute_in_goal">
</transf>
</goal>
......@@ -73,47 +83,47 @@
</theory>
<theory name="Rstandard" expanded="true">
</theory>
<theory name="TestStandard">
<goal name="g00" sum="0ceddda03e7e96cda00c67eebccb8ce2">
<transf name="compute_in_goal">
<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">
<transf name="compute_in_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">
<transf name="compute_in_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">
<transf name="compute_in_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">
<transf name="compute_in_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">
<transf name="compute_in_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">
<goal name="g06" sum="447bada60ec36071cd53b698cbf73823" expanded="true">
</goal>
<goal name="g07" sum="9f175ea63c4a17c0a01aadffe9cf5e9f">
<transf name="compute_in_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>
......@@ -126,8 +136,8 @@
</goal>
</transf>
</goal>
<goal name="g01" sum="0a7faedd8825702fce72f3e84ec82571" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g01" sum="0a7faedd8825702fce72f3e84ec82571">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g1" sum="825053ebfb5449346b8ed12490cc9354" expanded="true">
......@@ -136,18 +146,26 @@
</goal>
</transf>
</goal>
<goal name="g2" sum="76634810995226e5b7def51a0259205b" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g2" sum="76634810995226e5b7def51a0259205b">
<transf name="compute_in_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">
<goal name="g1" sum="ee2ca5eabcbb8846e87b36cbced8c06c" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g1.1" expl="1." sum="61e58a21f092e1273ef7e133fe055088">
</goal>
</transf>
</goal>
<goal name="g2" sum="12fd3d04b943352a3c6f36b5f06ec89a" expanded="true">
</goal>
</theory>
<theory name="TestInteger">
<goal name="g1" sum="dab58bcd2a433e50f94afd9cd1659810">
<transf name="compute_in_goal">
<goal name="g1.1" expl="1." sum="4c4937d701abd0d106d51fa154f0e03c">
</goal>
</transf>
......@@ -164,32 +182,32 @@
<theory name="MoreSets" expanded="true">
</theory>
<theory name="TestSets" expanded="true">
<goal name="g00" sum="f038e056e11482d4fcfb897f4952d3e4">
<transf name="compute_in_goal">
<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">
<transf name="compute_in_goal">
<goal name="g01" sum="7177ee4dcc6665dea602aced3271f562" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g01.1" expl="1." sum="d41e69e131353b6c9f0b213b7cea5c12">
</goal>
</transf>
</goal>
<goal name="g015" sum="bb4d9978c3fa326961606408c9cc9cd5">
<transf name="compute_in_goal">
<goal name="g015" sum="bb4d9978c3fa326961606408c9cc9cd5" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g015.1" expl="1." sum="d41e69e131353b6c9f0b213b7cea5c12">
</goal>
</transf>
</goal>
<goal name="g02" sum="bf942bd01c45cd6931b03788e6d9065e">
<transf name="compute_in_goal">
<goal name="g02" sum="bf942bd01c45cd6931b03788e6d9065e" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g02.1" expl="1." sum="d41e69e131353b6c9f0b213b7cea5c12">
</goal>
</transf>
</goal>
<goal name="g025" sum="396190e131bb8f99956a2f2a7d61e075">
<transf name="compute_in_goal">
<goal name="g025" sum="396190e131bb8f99956a2f2a7d61e075" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g025.1" expl="1." sum="d41e69e131353b6c9f0b213b7cea5c12">
</goal>
</transf>
......
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