Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Make tests use nicer notation

  • Loading branch information...
commit 214b3290c15f038e180e262fc7895d16803577f3 1 parent 8bca705
@yav authored
Showing with 8 additions and 21 deletions.
  1. +4 −12 tests/3.hs
  2. +4 −9 tests/4.hs
View
16 tests/3.hs
@@ -1,23 +1,14 @@
import Data.Integer.Presburger
mytest5 =
- Not $ Forall $ \a ->
- Forall $ \b ->
- Forall $ \c ->
- Forall $ \d ->
- Forall $ \e ->
+ Not $ forall $ \a b c d e ->
Not $ a :=: 2 .* b
:/\: b :=: c + 2
:/\: d :=: 2 * c
:/\: c :=: e + 1
:/\: e :=: 1
-mytest6 =
- Exists $ \a ->
- Exists $ \b ->
- Exists $ \c ->
- Exists $ \d ->
- Exists $ \e ->
+mytest6 = exists $ \a b c d e ->
a :=: 2 .* b
:/\: b :=: c + 2
:/\: d :=: 2 * c
@@ -25,4 +16,5 @@ mytest6 =
:/\: e :=: 1
-main = print $ check mytest5
+main = do print $ check mytest5
+ print $ check mytest6
View
13 tests/4.hs
@@ -5,28 +5,23 @@ import Debug.Trace
l = 16 * 8 * 8
given :: Formula
-given = Forall $ \a ->
- Forall $ \b ->
- l .* b - 8 .* a :>=: 65
+given = forall $ \a b -> l .* b - 8 .* a :>=: 65
divided :: Term -> Integer -> (Term -> Term -> Formula) -> Formula
-divided t k body =
- Exists $ \q ->
- Exists $ \r ->
+divided t k body = exists $ \q r ->
0 :<=: r
:/\: r :<: fromInteger k
:/\: k .* q + r :=: t
:/\: body q r
-inferred = Forall $ \a ->
- Forall $ \b ->
+inferred = forall $ \a b ->
divided (8 .* a + 64) l $ \q r ->
l .* q - 8 .* a + fromInteger l - 65 :>=: 0 :/\:
b :=: 1 + q
-test1 = inferred :<=>: given
+main = print $ check (inferred :<=>: given)
Please sign in to comment.
Something went wrong with that request. Please try again.