summaryrefslogtreecommitdiff
path: root/assignment-12/gastje.icl
diff options
context:
space:
mode:
Diffstat (limited to 'assignment-12/gastje.icl')
-rw-r--r--assignment-12/gastje.icl49
1 files changed, 42 insertions, 7 deletions
diff --git a/assignment-12/gastje.icl b/assignment-12/gastje.icl
index 6ad6d68..09fe76e 100644
--- a/assignment-12/gastje.icl
+++ b/assignment-12/gastje.icl
@@ -1,4 +1,4 @@
-module gastje
+implementation module gastje
/*
Pieter Koopman, Radboud University, 2016, 2017
@@ -15,9 +15,9 @@ test p = check 1000 (holds p prop0)
check :: Int [Prop] -> [String]
check n [] = ["Proof\n"]
check 0 l = ["Passed\n"]
-check n [p:x] | p.bool
- = check (n-1) x
- = ["Fail for: ":reverse ["\n":p.info]]
+check n [p:x]
+| p.bool = check (n-1) x
+| otherwise = ["Fail for: ":reverse ["\n":p.info]]
class prop a where holds :: a Prop -> [Prop]
@@ -35,7 +35,7 @@ class testArg a | gen{|*|}, string{|*|}, gEq{|*|} a
}
prop0 = {bool = True, info = []}
-generic gen a :: [ a ]
+generic gen a :: [a]
gen{|Int|} = [0,1,-1,maxint,minint,maxint-1,minint+1:[j\\i<-[2..], j<-[i,~i]]]
gen{|Bool|} = [True,False]
gen{|Char|} = [' '..'~'] ++ ['\t\n\b']
@@ -63,7 +63,9 @@ string{|CONS of gcd|} f (CONS x)
| otherwise = gcd.gcd_name
string{|OBJECT|} f (OBJECT x) = f x
string{|RECORD of grd|} f (RECORD x) = "{" + grd.grd_name + "|" + f x + "}"
-string{|FIELD of gfd|} f (FIELD x) = gfd.gfd_name + " = " + f x + " "
+string{|FIELD of gfd|} f (FIELD x) = gfd.gfd_name + "=" + f x + if last "" ","
+where
+ last = gfd.gfd_index == length gfd.gfd_cons.grd_fields - 1
maxint :: Int
maxint =: IF_INT_64_OR_32 (2^63-1) (2^31-1) //2147483647
@@ -85,4 +87,37 @@ where
rev [] accu = accu
rev [x:r] accu = rev r [x:accu]
-Start = ()
+:: For t = E.p: (For) infix 0 (t -> p) [t] & prop p
+
+instance prop (For t) | string{|*|} t
+where
+ holds (f For xs) p = diagonal [holds (f x) {p & info=[string{|*|} x:p.info]} \\ x <- xs]
+
+:: Implies = E.p: (==>) infix 0 Bool p & prop p
+
+instance prop Implies
+where
+ holds (True ==> t) p = holds t p
+ holds (False ==> _) p = []
+
+:: Equals a = (=.=) infix 4 a a
+
+instance prop (Equals a) | ==, string{|*|} a
+where
+ holds (x =.= y) p = [{bool=x==y, info=[string{|*|} x," <> ",string{|*|} y,"; ":p.info]}]
+
+Start =
+ [ ["pUpper: ":test (pUpper For ['a'..'z'])]
+ , ["pUpper lower: ":test (\c -> isLower c ==> pUpper c)]
+ , ["pFac: ":test (\i -> abs i < 10 ==> prod [1..i] =.= fac i)]
+ ]
+where
+ pUpper :: Char -> Bool
+ pUpper c = c <> toUpper c
+
+ // This fails for 0; should be <=. If we fix that, the test does not
+ // terminate, as there are no 1000 integers with abs i < 10.
+ fac :: Int -> Int
+ fac n
+ | n < 0 = 1
+ | otherwise = n * fac (n-1)