Skip to content

Commit 1b99824

Browse files
ntc2ntc2
committedNov 15, 2011
Updated all tests to the new haskell compatible syntax.
There is some regression here, due to the use of more 'import's. The problem is orthogonal to the new syntax: since I had to edit all the files, I decided to use 'import's more effectively. However, this results in a many irrelevant definitions being in scope, and so in turn the generated theory is much larger in some cases. There are two obvious fixes: 1. go back to more granular files, with fewer or more granular 'import's 2. make the theory generation phase only generate the relevant axioms. (1) is easier in the short run, but sloppy. (2) is harder, but a good approximation is probably straightforward: transitively search for free variables, and generate axioms for all names found this way. In detail, here's how the 20 second timeout tests degraded: $ diff -U0 results/46.20s-equinox.txt results/47.20s-equinox.txt --- results/46.20s-equinox.txt 2011-11-08 15:20:04.000000000 +0000 +++ results/47.20s-equinox.txt 2011-11-15 18:52:11.000000000 +0000 @@ -14,2 +14,2 @@ -./yes/bintree-height-is-cf-to-cf.hs: passed -./yes/bintree-size-is-cf-to-cf.hs: passed +./yes/bintree-height-is-cf-to-cf.hs: TIMED OUT +./yes/bintree-size-is-cf-to-cf.hs: TIMED OUT @@ -17,0 +18 @@ +./yes/gt-inc.hs: TIMED OUT @@ -23 +24 @@ -./yes/prediate-on-constant-function.hs: passed +./yes/predicate-on-constant-function.hs: FAILED WITH EXIT CODE 1 @@ -30 +31 @@ -./no/add-and-mult-nonZero.hs: FAILED WITH EXIT CODE 1 +./no/add-and-mult-nonZero.hs: timed out @@ -33,0 +35 @@ +./no/mult-gt.hs: FAILED WITH EXIT CODE 1 The tests no/mult-gt.hs and yes/gt-inc.hs are new since results/46.
1 parent 7c73700 commit 1b99824

34 files changed

+368
-282
lines changed
 

‎Lib/Arithmetic.hs

+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
module Lib.Arithmetic(module Lib.Prelude, module Lib.Arithmetic) where
2+
3+
import Lib.Prelude ;;
4+
5+
one = Succ Zero;;
6+
two = Succ one;;
7+
8+
add x y = case x of
9+
; Zero -> y
10+
; Succ x_ -> Succ (add x_ y);;
11+
12+
mult a b = case a of
13+
; Zero -> Zero
14+
; Succ x -> add b (mult x b);;
15+
16+
notZero x = case x of
17+
; Zero -> False
18+
; Succ x_ -> True;;
19+
20+
isZero x = case x of
21+
; Zero -> True
22+
; Succ x_ -> False;;
23+
24+
eqNat x y = case x of
25+
; Zero -> isZero y
26+
; Succ x_ -> eqNatAux x_ y;;
27+
28+
eqNatAux x y = case y of
29+
; Zero -> False
30+
; Succ y_ -> eqNat x y_;;
31+
32+
gt x y = case x of
33+
; Zero -> False
34+
; Succ x_ -> gtAux x_ y;;
35+
36+
gtAux x y = case y of
37+
; Zero -> True
38+
; Succ y_ -> gt x y_;;
39+
40+
max a b = case (ge a b) of
41+
; True -> a
42+
; False -> b;;
43+
44+
ge x y = case x of
45+
; Zero -> isZero y
46+
; Succ x_ -> ge_ x_ y;;
47+
48+
ge_ x y = case y of
49+
; Zero -> True
50+
; Succ y_ -> ge x y_;;

‎Lib/BinaryTree.hs

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
module Lib.BinaryTree where
2+
3+
import Lib.Arithmetic ;;
4+
import Lib.Logic ;;
5+
6+
data Tree
7+
= Leaf
8+
| Node Tree Tree;;
9+
10+
isLeaf t = case t of
11+
; Leaf -> True
12+
; Node a b -> False;;
13+
14+
eqTree t1 t2 = case t1 of
15+
; Leaf -> isLeaf t2
16+
; Node a b -> eqTreeAux t2 a b;;
17+
18+
eqTreeAux t a b = case t of
19+
; Leaf -> False
20+
; Node c d -> and (eqTree a c) (eqTree b d);;
21+
22+
height t = case t of
23+
; Leaf -> Zero
24+
; Node l r -> Succ (max (height l) (height r));;
25+
26+
size t = case t of
27+
; Leaf -> Succ Zero
28+
; Node l r -> Succ (add (size l) (size r));;

‎Lib/List.hs

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
module Lib.List where
2+
3+
import Lib.Prelude ;;
4+
5+
length x = case x of
6+
; Nil -> Zero
7+
; Cons a b -> Succ (length b);;
8+
9+
null x = case x of
10+
; Nil -> False
11+
; Cons a b -> True;;
12+
13+
reverse x acc = case x of
14+
; Nil -> acc
15+
; Cons a b -> reverse b (Cons a acc);;

‎Lib/Logic.hs

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
-- Boolean logic.
2+
module Lib.Logic where
3+
4+
data Bool
5+
= False
6+
| True ;;
7+
8+
and a b = case a of
9+
; True -> b
10+
; False -> False;;
11+
12+
or a b = case a of
13+
; True -> True
14+
; False -> b;;
15+
16+
not a = case a of
17+
; True -> False
18+
; False -> True;;
19+
20+
implies a b = case a of
21+
; False -> True
22+
; True -> b;;

‎Lib/Prelude.hs

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
module Lib.Prelude(module Prelude,module Lib.Prelude) where
2+
3+
{- SKIP -}
4+
import Prelude(error,Show)
5+
6+
data Bool
7+
= False
8+
| True
9+
{- SKIP -}
10+
deriving Show
11+
;;
12+
13+
data Nat
14+
= Zero
15+
| Succ Nat
16+
{- SKIP -}
17+
deriving Show
18+
;;
19+
20+
data List
21+
= Nil
22+
| Cons Nat List
23+
{- SKIP -}
24+
deriving Show
25+
;;
26+
27+
{- SKIP -}
28+
unr = unr
29+
{- SKIP -}
30+
bad = error "BAD"

‎TODO.org

+27-2
Original file line numberDiff line numberDiff line change
@@ -55,9 +55,13 @@ is very wrong!
5555
fewer quantifiers seems good, but i need to experiment to see if
5656
there is an improvement in practice.
5757
- [ ] whether the 'forall a. a = ...' versions are used.
58-
** TODO move 'Bool' into a library
58+
** DONE move 'Bool' into a library
5959
the translation of 'Bool' is hardcoded in the translation, but we
6060
could have lib/bool.hs and then tests could 'import "../lib/bool.hs"'.
61+
** TODO restrict generated theory to relevant defs
62+
right now we insert more defs than neccessary when generating the
63+
theory, which slows things down significantly in some cases.
64+
something like a transitive free variable check should be sufficient.
6165
** TODO better test suite
6266
borrow IsaPlanner examples from Zeno directly, or from the IsaPlanner
6367
site. the urls are in the zeno tech report:
@@ -87,7 +91,7 @@ but if nested case were allowed we'd simply need to change the (e = pi
8791
: [[ f xs = ei ]]
8892

8993
when ei = case e' of [pi' -> ei'].
90-
** TODO use haskell syntax
94+
** DONE use haskell syntax
9195
zeno does this, and it seems like a good idea. we only require a few
9296
changes:
9397
1. use real imports
@@ -217,3 +221,24 @@ then, when axiomitizing a function def, we can have
217221
: -> T(f x1 ... xn) /\ <the usual axiomitization>
218222

219223
where f : T1 -> ... -> Tn -> T.
224+
** MAYBE add type checking for contracts
225+
they're in comments and not haskell, so GHQ ignores them. one easy
226+
way to type check them would be to generate a lambda and typecheck it
227+
with ghc. a translation like
228+
229+
: [[ x:c -> c' ]] ==> \x -> ([[ c ]], [[ c' ]])
230+
: [[ c -> c' ]] ==> [[ _:c -> c' ]]
231+
: [[ c1&&c2 ]] ==> ([[ c1 ]], [[ c2 ]])
232+
: [[ c1||c2 ]] ==> ([[ c1 ]], [[ c2 ]])
233+
: [[ CF ]] ==> ()
234+
: [[ {x : p } ]] ==> \x . p
235+
236+
might work. so, e.g., we'd have
237+
238+
: [[ CF -> {x: nonZero x} -> y:(CF&&{y: p y}) -> {r : q y r} ]]
239+
: ==>
240+
: \_ -> ((),
241+
: \_ -> (\x -> nonZero x,
242+
: \y -> (((),
243+
: \y -> p y),
244+
: \r -> q y r)))

‎lib/arithmetic.hs

-37
This file was deleted.

‎lib/logic.hs

-16
This file was deleted.

‎macros.el

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
;; wraps a 'f ::: c;;' style contract in a 'CONTRACT' pragma comment.
2+
(setq last-kbd-macro
3+
[?\C-m up ?\{ ?- ?# ? ?C ?O ?N ?T ?R ?A ?C ?T down end left left ?\C-m ?# ?- ?\} end down home])

‎no/add-and-mult-nonZero.hs

+8-17
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,11 @@
33
--
44
-- Note the '{y:True}' (i.e. 'Any') contract on 'mult's second
55
-- argument: this is wrong. cf. ../yes/add-and-mult-nonZero.hs.
6-
data Nat = Zero 0
7-
| Succ 1;;
8-
9-
add a b = case a of
10-
| Zero -> b
11-
| Succ x -> Succ (add x b);;
12-
13-
mult a b = case a of
14-
| Zero -> Zero
15-
| Succ x -> add b (mult x b);;
16-
17-
notZero x = case x of
18-
| Zero -> False
19-
| Succ a -> True;;
20-
21-
add ::: {x:notZero x} -> {y:notZero y} -> {z:notZero z};;
22-
mult ::: {x:notZero x} -> {y:True} -> {z:notZero z};;
6+
import Lib.Arithmetic ;;
7+
8+
{-# CONTRACT
9+
add ::: {x:notZero x} -> {y:notZero y} -> {z:notZero z}
10+
#-};;
11+
{-# CONTRACT
12+
mult ::: {x:notZero x} -> {y:True} -> {z:notZero z}
13+
#-};;

‎no/bad-is-cf.hs

+8-2
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
11
-- Wrongly assert that 'BAD' is CF.
2-
bad = BAD;;
3-
bad ::: CF;;
2+
3+
-- XXX: doesn't work to simply use 'bad' below? I don't think it's
4+
-- worth fixing.
5+
f = bad ;;
6+
7+
{-# CONTRACT
8+
f ::: CF
9+
#-};;

‎no/const-bad-is-cf-to-cf.hs

+7-2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,9 @@
1+
import Lib.Prelude ;;
2+
13
-- Wrongly assert that 'const BAD' is CF.
24
const x y = x;;
3-
cbad = const BAD;;
4-
cbad ::: CF -> CF;;
5+
cbad = const bad;;
6+
7+
{-# CONTRACT
8+
cbad ::: CF -> CF
9+
#-};;

‎no/crash-on-wrong-nat.hs

+11-16
Original file line numberDiff line numberDiff line change
@@ -2,25 +2,20 @@
22
-- to swapping 'Zero' and 'Succ'. This is wrong because 'Succ' may
33
-- contain a crashing subexpression that 'isZero' did not inspect.
44
-- cf. ../yes/crash-on-wrong-nat.hs.
5-
data Nat = Zero 0
6-
| Succ 1;;
5+
import Lib.Arithmetic ;;
76

87
crashOnSucc x = case x of
9-
| Zero -> Zero
10-
| Succ y -> BAD;;
8+
; Zero -> Zero
9+
; Succ y -> bad;;
1110

1211
crashOnZero x = case x of
13-
| Zero -> BAD
14-
| Succ y -> x;;
12+
; Zero -> bad
13+
; Succ y -> x;;
1514

16-
isZero x = case x of
17-
| Zero -> True
18-
| Succ a -> False;;
19-
20-
not x = case x of
21-
| True -> False
22-
| False -> True;;
23-
24-
crashOnSucc ::: {x: isZero x} -> CF;;
15+
{-# CONTRACT
16+
crashOnSucc ::: {x: isZero x} -> CF
17+
#-};;
2518
-- Wrong!
26-
crashOnZero ::: {x:not (isZero x)} -> CF;;
19+
{-# CONTRACT
20+
crashOnZero ::: {x:not (isZero x)} -> CF
21+
#-};;

‎no/mult-gt.hs

+5-3
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
1-
import "../lib/arithmetic.hs";;
2-
import "../lib/logic.hs";;
1+
import Lib.Arithmetic ;;
2+
import Lib.Logic ;;
33

44
-- Not true, e.g. 'positive 1' and 'CF 1' and '1 = 1 * 1' but not 'gt 1 1'.
5+
{-# CONTRACT
56
mult ::: x:CF -> y:CF -> {z: implies (and (positive x) (positive y))
6-
(and (gt z x) (gt z y))};;
7+
(and (gt z x) (gt z y))}
8+
#-};;

‎run-tests.sh

+2-2
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ TIMEOUT=${TIMEOUT:-10}
1212
trap 'exit 1' INT
1313

1414
# Run a test and report results
15-
run-test () {
15+
run-test () {
1616
test="$1"
1717
passMsg="$2"
1818
timeoutMsg="$3"
@@ -22,7 +22,7 @@ run-test () {
2222
# z3 processes with us as parent?
2323
killall --user `whoami` z3 &>/dev/null
2424

25-
"$egsDir"/timeout.sh $TIMEOUT "$CHECK" "$test" -q -p # --engine vampire32 # --engine z3
25+
"$egsDir"/timeout.sh $TIMEOUT "$CHECK" "$test" -q -p -i "$egsDir" # --engine vampire32 # --engine z3
2626
ret=$?
2727
printf "%-50s" "$test: "
2828
if [[ $ret -eq 0 ]]; then

‎yes/add-and-mult-nonZero.hs

+7-3
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,11 @@
44
-- Note the '{y:True}' (i.e. 'Any') contract on 'add's second
55
-- argument. We can't do the same for 'mult's second argument.
66
-- cf. ../no/add-and-mult-nonZero.hs.
7-
import "../lib/arithmetic.hs";;
7+
import Lib.Arithmetic ;;
88

9-
add ::: {x:notZero x} -> {y:True} -> {z:notZero z};;
10-
mult ::: {x:notZero x} -> {y:notZero y} -> {z:notZero z};;
9+
{-# CONTRACT
10+
add ::: {x:notZero x} -> {y:True} -> {z:notZero z}
11+
#-};;
12+
{-# CONTRACT
13+
mult ::: {x:notZero x} -> {y:notZero y} -> {z:notZero z}
14+
#-};;

0 commit comments

Comments
 (0)
Please sign in to comment.