Assignment 12 up to 4

3 files changed, 128 insertions, 7 deletions

diff --git a/assignment-12/cashModel.icl b/assignment-12/cashModel.icl
index ed0174a..5c11b31 100644
--- a/assignment-12/cashModel.icl
+++ b/assignment-12/cashModel.icl
@@ -8,6 +8,9 @@ implementation module cashModel
 */
 
 import StdEnv, GenEq
+import gastje
+from Data.Func import mapSt
+import Data.Tuple
 
 class euro a :: a -> Euro
 instance euro Product
@@ -46,3 +49,52 @@ model list (Rem p)
 | isMember p list = (removeMember p list,[~ (euro p)])
 | otherwise       = (list,[])
 model list Pay = ([],[euro list])
+
+derive gen Euro
+derive string Euro
+derive bimap []
+
+/**
+ * plus_zero_is_identity:          Fail for: {Euro|euro=0, cent=1} ; {Euro|euro=0, cent=1} <> {Euro|euro=0, cent=0}
+ * plus_is_commutative:            Passed
+ * minus_zero_is_identity:         Fail for: {Euro|euro=0, cent=1} ; {Euro|euro=0, cent=1} <> {Euro|euro=0, cent=0}
+ * prop_double_neg_is_identity:    Passed
+ * prop_neg_is_not_identity:       Fail for: {Euro|euro=0, cent=1}
+ * prop_minus_is_plus_after_neg:   Fail for: {Euro|euro=1, cent=0} {Euro|euro=-9223372036854775808, cent=1} ; {Euro|euro=0, cent=99} <> {Euro|euro=1, cent=1}
+ * prop_neg_distributes_over_plus: Fail for: {Euro|euro=1, cent=0} {Euro|euro=-9223372036854775808, cent=1} ; {Euro|euro=-1, cent=1} <> {Euro|euro=0, cent=99}
+ * prop_plus_minus_is_identity:    Fail for: {Euro|euro=0, cent=1} {Euro|euro=0, cent=0} ; {Euro|euro=0, cent=0} <> {Euro|euro=0, cent=1}
+ */
+Start =
+	[ ["plus_zero_is_identity:          ": test prop_plus_zero_is_identity]
+	, ["plus_is_commutative:            ": test prop_plus_is_commutative]
+	, ["minus_zero_is_identity:         ": test prop_minus_zero_is_identity]
+	, ["prop_double_neg_is_identity:    ": test prop_double_neg_is_identity]
+	, ["prop_neg_is_not_identity:       ": test prop_neg_is_not_identity]
+	, ["prop_minus_is_plus_after_neg:   ": test prop_minus_is_plus_after_neg]
+	, ["prop_neg_distributes_over_plus: ": test prop_neg_distributes_over_plus]
+	, ["prop_plus_minus_is_identity:    ": test prop_plus_minus_is_identity]
+	]
+where
+	prop_plus_zero_is_identity :: Euro -> Equals Euro
+	prop_plus_zero_is_identity e = e + zero =.= e
+
+	prop_plus_is_commutative :: Euro Euro -> Equals Euro
+	prop_plus_is_commutative a b = a + b =.= b + a
+
+	prop_minus_zero_is_identity :: Euro -> Equals Euro
+	prop_minus_zero_is_identity e = e - zero =.= e
+
+	prop_plus_minus_is_identity :: Euro Euro -> Equals Euro
+	prop_plus_minus_is_identity a b = a =.= a - b + b
+
+	prop_double_neg_is_identity :: Euro -> Equals Euro
+	prop_double_neg_is_identity e = ~(~e) =.= e
+
+	prop_neg_is_not_identity :: Euro -> Implies
+	prop_neg_is_not_identity e = e <> zero ==> e <> ~e
+
+	prop_minus_is_plus_after_neg :: Euro Euro -> Equals Euro
+	prop_minus_is_plus_after_neg a b = a - b =.= a + ~b
+
+	prop_neg_distributes_over_plus :: Euro Euro -> Equals Euro
+	prop_neg_distributes_over_plus a b = ~(a + b) =.= ~a + ~b
diff --git a/assignment-12/gastje.dcl b/assignment-12/gastje.dcl
new file mode 100644
index 0000000..a08d35b
--- /dev/null
+++ b/assignment-12/gastje.dcl
@@ -0,0 +1,34 @@
+definition module gastje
+
+import StdGeneric
+from StdOverloaded import class ==
+from GenEq import generic gEq
+
+test :: p -> [String] | prop p
+
+class prop a where holds :: a Prop -> [Prop]
+
+instance prop Bool
+
+instance prop (a->b) | prop b & testArg a 
+
+class testArg a | gen{|*|}, string{|*|}, gEq{|*|} a
+
+:: Prop
+
+generic gen a :: [a]
+derive gen Int, Bool, Char, UNIT, PAIR, EITHER, CONS, OBJECT, RECORD, FIELD
+generic string a :: a -> String
+derive string Int, Bool, Char, UNIT, PAIR, EITHER, CONS of gcd, OBJECT, RECORD of grd, FIELD of gfd
+
+:: For t = E.p: (For) infix 0 (t -> p) [t] & prop p
+
+instance prop (For t) | string{|*|} t
+
+:: Implies = E.p: (==>) infix 0 Bool p & prop p
+
+instance prop Implies
+
+:: Equals a = (=.=) infix 4 a a
+
+instance prop (Equals a) | ==, string{|*|} a
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)