3 files changed, 24 insertions, 32 deletions

diff --git a/assignment-12/cashModel.icl b/assignment-12/cashModel.icl
index 5c11b31..c1200be 100644
--- a/assignment-12/cashModel.icl
+++ b/assignment-12/cashModel.icl
@@ -75,26 +75,26 @@ Start =
 	, ["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 :: Euro -> Property
 	prop_plus_zero_is_identity e = e + zero =.= e
 
-	prop_plus_is_commutative :: Euro Euro -> Equals Euro
+	prop_plus_is_commutative :: Euro Euro -> Property
 	prop_plus_is_commutative a b = a + b =.= b + a
 
-	prop_minus_zero_is_identity :: Euro -> Equals Euro
+	prop_minus_zero_is_identity :: Euro -> Property
 	prop_minus_zero_is_identity e = e - zero =.= e
 
-	prop_plus_minus_is_identity :: Euro Euro -> Equals Euro
+	prop_plus_minus_is_identity :: Euro Euro -> Property
 	prop_plus_minus_is_identity a b = a =.= a - b + b
 
-	prop_double_neg_is_identity :: Euro -> Equals Euro
+	prop_double_neg_is_identity :: Euro -> Property
 	prop_double_neg_is_identity e = ~(~e) =.= e
 
-	prop_neg_is_not_identity :: Euro -> Implies
+	prop_neg_is_not_identity :: Euro -> Property
 	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 :: Euro Euro -> Property
 	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 :: Euro Euro -> Property
 	prop_neg_distributes_over_plus a b = ~(a + b) =.= ~a + ~b
diff --git a/assignment-12/gastje.dcl b/assignment-12/gastje.dcl
index a08d35b..a52618c 100644
--- a/assignment-12/gastje.dcl
+++ b/assignment-12/gastje.dcl
@@ -21,14 +21,9 @@ 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
+:: Property
+	= E.p t: (For) infix 0 (t -> p) [t] & prop p & string{|*|} t
+	| E.p:   (==>) infix 0 Bool p       & prop p
+	| E.t:   (=.=) infix 4 t t          & ==, string{|*|} t
 
-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
+instance prop Property
diff --git a/assignment-12/gastje.icl b/assignment-12/gastje.icl
index 09fe76e..06148cf 100644
--- a/assignment-12/gastje.icl
+++ b/assignment-12/gastje.icl
@@ -87,24 +87,21 @@ where
 	rev []    accu = accu
 	rev [x:r] accu = rev r [x:accu]
 
-:: For t = E.p: (For) infix 0 (t -> p) [t] & prop p
-
-instance prop (For t) | string{|*|} t
+/**
+ * TODO: mixing deep and shallow embedding. This is not how this is supposed to
+ * be done. These can be plain functions or classes.
+ */
+:: Property
+	= E.p t: (For) infix 0 (t -> p) [t] & prop p & string{|*|} t
+	| E.p:   (==>) infix 0 Bool p       & prop p
+	| E.t:   (=.=) infix 4 t t          & ==, string{|*|} t
+
+instance prop Property
 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]}]
+	holds (x =.= y) p = [{bool=x==y, info=[string{|*|} y," <> ",string{|*|} x,"; ":p.info]}]
 
 Start =
 	[ ["pUpper:       ":test (pUpper For ['a'..'z'])]