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)