1 files changed, 260 insertions, 260 deletions
diff --git a/assignment-2/serialize2start.icl b/assignment-2/serialize2start.icl
index 3717b9c..291b837 100644
--- a/assignment-2/serialize2start.icl
+++ b/assignment-2/serialize2start.icl
@@ -1,260 +1,260 @@
-module serialize2start
-
-/*
-  Definition for assignment 2 in AFP 2017
-  Pieter Koopman pieter@cs.ru.nl
-  September 2017
-
-  Laurens Kuiper (s4467299)
-  Camil Staps (s4498062)
-*/
-
-import StdEnv, StdMaybe
-
-/**
- * Review questions
- *
- * 1. A type is a set of values. In the case of UNIT, UNIT = {UNIT}. The set of
- * possible arguments to == on a type T is {(x,y) | x <- T, y <- T}, so in the
- * case of UNIT we have {(UNIT,UNIT)}. Hence, this alternative matches always.
- * The other suggestions are equivalent, as the pattern match is because of
- * this meaningless and therefore all alternatives in the question are
- * equivalent.
- *
- * 2. The name of the constructor is redundant information, since the same
- * information can also be derived (compile-time only, hence it has to be
- * stored) from the LEFT/RIGHT-path through the ADT tree. Hence, checking on
- * the constructor name is not needed.
- *
- * 3.
- * - []   = LEFT (CONS "_Nil" UNIT)
- * - Leaf = LEFT (CONS "Leaf" UNIT)
- * == has type a a -> Bool, so we cannot apply it to Leaf and [], which are not
- * of the same type. So no, this does not yield True (it does not yield
- * anything, as you won't be able to compile it).
- */
-
-/**
- * The number of elements in an expression that will be placed on the outer
- * level w.r.t. parentheses when pretty-printing.
- *
- * For instance:
- *  - "37"             -> 1
- *  - "_Nil"           -> 1
- *  - "_Cons 1 _Nil"   -> 3
- *  - "(_Cons 1 _Nil)" -> 1
- */
-class outerElems a
-where
-	outerElems :: a -> Int
-
-	/**
-	 * An expression needs parentheses when it has more than one element on the
-	 * outer level.
-	 */
-	needsParens x :== outerElems x > 1
-
-/**
- * In the default case, parentheses are placed around the whole expression, so
- * the number of elements on the outer level is 1.
- */
-instance outerElems a    where outerElems _ = 1
-
-//* UNITs are not printed.
-instance outerElems UNIT where outerElems _ = 0
-
-//* The arguments and the constructor
-instance outerElems (CONS a) | outerElems a
-where outerElems (CONS _ x) = 1 + outerElems x
-
-//* Both elements appear on the outer level
-instance outerElems (PAIR a b) | outerElems a & outerElems b
-where outerElems (PAIR x y) = outerElems x + outerElems y
-
-instance outerElems (EITHER a b) | outerElems a & outerElems b
-where
-	outerElems (LEFT x)  = outerElems x
-	outerElems (RIGHT x) = outerElems x
-
-/**
- * We extended the definition with a restriction on outerElems. This extra
- * restriction is OK, since there is an instance of outerElems for every type
- * (and hence, this restriction does not exclude any type).
- */
-class serialize a | outerElems a
-where
-	write :: a [String] -> [String]
-	read	:: [String] -> Maybe (a,[String])
-
-instance serialize Bool where
-	write b c = [toString b:c]
-	read ["True":r]	= Just (True,r)
-	read ["False":r] = Just (False,r)
-	read _ = Nothing
-
-instance serialize Int where
-	write i c = [toString i:c]
-	read [s:r]
-		# i = toInt s
-		| s == toString i
-			= Just (i,r)
-			= Nothing
-	read _ = Nothing
-
-// ---
-
-:: UNIT       = UNIT
-:: EITHER a b = LEFT a | RIGHT b
-:: PAIR   a b = PAIR a b
-:: CONS   a   = CONS String a
-
-// ---
-
-writeP :: a [String] -> [String] | serialize a
-writeP x s = if (needsParens x) ["(":write x [")":s]] (write x s)
-
-readP :: [String] -> Maybe (a, [String]) | serialize a
-readP ["(":r] = case read r of
-	Just (x,[")":r]) -> Just (x,r)
-	_                -> read ["(":r]
-readP r = case read r of
-	Just (x,r) -> if (needsParens x) Nothing (Just (x,r))
-	_          -> Nothing
-
-instance serialize UNIT
-where
-	write _ c = c
-	read r = Just (UNIT,r)
-
-instance serialize (EITHER a b) | serialize a & serialize b
-where
-	write (LEFT x)  c = write x c
-	write (RIGHT x) c = write x c
-	read r = case read r of
-		Just (x,r) -> Just (LEFT x, r)
-		Nothing    -> case read r of
-			Just (x,r) -> Just (RIGHT x,r)
-			Nothing    -> Nothing
-		// This goes wrong if the two type variables of EITHER are equal (and
-		// hence read for LEFT is the same as read for RIGHT: we will always
-		// return a LEFT. Therefore, given a type
-		//
-		//   :: T = C1 Int | C2 Int
-		//
-		// it is not possible to write and read C2 (C1 will be read, since LEFT
-		// has precedence). Like the example given as the answer to the
-		// reflection questin below, we don't think this to be fixable in the
-		// current setup.
-
-instance serialize (PAIR a b) | serialize a & serialize b
-where
-	write (PAIR x y) c = writeP x [" ":writeP y c]
-	read r = case readP r of
-		Just (x,[" ":r]) -> case readP r of
-			Nothing    -> Nothing
-			Just (y,r) -> Just (PAIR x y, r)
-		_ -> Nothing
-
-instance serialize (CONS a) | serialize a
-where
-	write e=:(CONS s x) c
-	| needsParens e = ["(":s:" ":write x [")":c]]
-	| otherwise     = [s:c]
-	read ["(":s:" ":r] = case read r of
-		Just (x,[")":r]) -> Just (CONS s x,r)
-		_                -> Nothing
-	read [s:r] = case read r of
-		Just (x,r) -> let e = CONS s x in if (needsParens e) Nothing (Just (e,r))
-		Nothing    -> Nothing
-	read _ = Nothing
-
-:: ListG a :== EITHER (CONS UNIT) (CONS (PAIR a [a]))
-
-fromList :: [a] -> ListG a
-fromList []     = LEFT (CONS "_Nil" UNIT)
-fromList [x:xs] = RIGHT (CONS "_Cons" (PAIR x xs))
-
-toList :: (ListG a) -> [a]
-toList (LEFT _)                     = []
-toList (RIGHT (CONS _ (PAIR x xs))) = [x:xs]
-
-instance serialize [a] | serialize a
-where
-	write l c = write (fromList l) c
-	read l = case read l of
-		Just (g,r) -> Just (toList g,r)
-		Nothing    -> Nothing
-
-:: Bin a = Leaf | Bin (Bin a) a (Bin a)
-:: BinG a :== EITHER (CONS UNIT) (CONS (PAIR (Bin a) (PAIR a (Bin a))))
-
-fromBin :: (Bin a) -> BinG a
-fromBin Leaf        = LEFT (CONS "Leaf" UNIT)
-fromBin (Bin l x r) = RIGHT (CONS "Bin" (PAIR l (PAIR x r)))
-
-toBin :: (BinG a) -> Bin a
-toBin (LEFT _)                             = Leaf
-toBin (RIGHT (CONS _ (PAIR l (PAIR x r)))) = Bin l x r
-
-instance serialize (Bin a) | serialize a
-where
-	write a c = write (fromBin a) c
-	read l = case read l of
-		Just (g,r) -> Just (toBin g,r)
-		Nothing    -> Nothing
-
-instance == (Bin a) | == a where // better use the generic approach
-	(==) Leaf Leaf = True
-	(==) (Bin l a r) (Bin k b s) = l == k && a == b && r == s
-	(==) _ _ = False
-
-// ---
-
-/**
- * Reflection:
- * The following is parsed as Just ([], []), which shows that the fact that
- * there is no check on the name of the constructor can be exploited.
- *
- * In the actual Clean implementation, there is the construct `CONS of d` where
- * d :: GenericConsDescriptor. This way, the name, arity, etc. of the
- * constructor are available as part of the CONS type (even though this type
- * does not explicitly contain the information). It is essentially a very
- * restricted form of dependent typing, which makes it possible to distinguish
- * the _Nil-CONS and the _Cons-CONS at compile-time.
- *
- * This requires the `CONS of d` construct, so I don't think this exploit is
- * fixable in the current setup. It would of course be possible to redefine
- * toList and toBin to result in a Maybe and check on the constructor there.
- */
-Start :: Maybe ([Int], [String])
-Start = read ["_Cons"]
-
-Start = 
-	[ test True
-	, test False
-	, test 0
-	, test 123
-	, test -36
-	, test [42]
-	, test [0..4]
-	, test [[True],[]]
-	, test (Bin Leaf True Leaf)
-	, test [Bin (Bin Leaf [1] Leaf) [2] (Bin Leaf [3] (Bin Leaf [4,5] Leaf))]
-	, test [Bin (Bin Leaf [1] Leaf) [2] (Bin Leaf [3] (Bin (Bin Leaf [4,5] Leaf) [6,7] (Bin Leaf [8,9] Leaf)))]
-	]
-
-test :: a -> ([String],[String]) | serialize, == a
-test a = 
-	(if (isJust r)
-		(if (fst jr == a)
-			(if (isEmpty (tl (snd jr)))
-				["Oke "]
-				["Fail: not all input is consumed! ":snd jr])
-			["Fail: Wrong result ":write (fst jr) []])
-		["Fail: read result is Nothing "]
-	, ["write produces ": s]
-	)
-	where
-		s = write a ["\n"]
-		r = read s
-		jr = fromJust r
+module serialize2start
+
+/*
+  Definition for assignment 2 in AFP 2017
+  Pieter Koopman pieter@cs.ru.nl
+  September 2017
+
+  Laurens Kuiper (s4467299)
+  Camil Staps (s4498062)
+*/
+
+import StdEnv, StdMaybe
+
+/**
+ * Review questions
+ *
+ * 1. A type is a set of values. In the case of UNIT, UNIT = {UNIT}. The set of
+ * possible arguments to == on a type T is {(x,y) | x <- T, y <- T}, so in the
+ * case of UNIT we have {(UNIT,UNIT)}. Hence, this alternative matches always.
+ * The other suggestions are equivalent, as the pattern match is because of
+ * this meaningless and therefore all alternatives in the question are
+ * equivalent.
+ *
+ * 2. The name of the constructor is redundant information, since the same
+ * information can also be derived (compile-time only, hence it has to be
+ * stored) from the LEFT/RIGHT-path through the ADT tree. Hence, checking on
+ * the constructor name is not needed.
+ *
+ * 3.
+ * - []   = LEFT (CONS "_Nil" UNIT)
+ * - Leaf = LEFT (CONS "Leaf" UNIT)
+ * == has type a a -> Bool, so we cannot apply it to Leaf and [], which are not
+ * of the same type. So no, this does not yield True (it does not yield
+ * anything, as you won't be able to compile it).
+ */
+
+/**
+ * The number of elements in an expression that will be placed on the outer
+ * level w.r.t. parentheses when pretty-printing.
+ *
+ * For instance:
+ *  - "37"             -> 1
+ *  - "_Nil"           -> 1
+ *  - "_Cons 1 _Nil"   -> 3
+ *  - "(_Cons 1 _Nil)" -> 1
+ */
+class outerElems a
+where
+	outerElems :: a -> Int
+
+	/**
+	 * An expression needs parentheses when it has more than one element on the
+	 * outer level.
+	 */
+	needsParens x :== outerElems x > 1
+
+/**
+ * In the default case, parentheses are placed around the whole expression, so
+ * the number of elements on the outer level is 1.
+ */
+instance outerElems a    where outerElems _ = 1
+
+//* UNITs are not printed.
+instance outerElems UNIT where outerElems _ = 0
+
+//* The arguments and the constructor
+instance outerElems (CONS a) | outerElems a
+where outerElems (CONS _ x) = 1 + outerElems x
+
+//* Both elements appear on the outer level
+instance outerElems (PAIR a b) | outerElems a & outerElems b
+where outerElems (PAIR x y) = outerElems x + outerElems y
+
+instance outerElems (EITHER a b) | outerElems a & outerElems b
+where
+	outerElems (LEFT x)  = outerElems x
+	outerElems (RIGHT x) = outerElems x
+
+/**
+ * We extended the definition with a restriction on outerElems. This extra
+ * restriction is OK, since there is an instance of outerElems for every type
+ * (and hence, this restriction does not exclude any type).
+ */
+class serialize a | outerElems a
+where
+	write :: a [String] -> [String]
+	read	:: [String] -> Maybe (a,[String])
+
+instance serialize Bool where
+	write b c = [toString b:c]
+	read ["True":r]	= Just (True,r)
+	read ["False":r] = Just (False,r)
+	read _ = Nothing
+
+instance serialize Int where
+	write i c = [toString i:c]
+	read [s:r]
+		# i = toInt s
+		| s == toString i
+			= Just (i,r)
+			= Nothing
+	read _ = Nothing
+
+// ---
+
+:: UNIT       = UNIT
+:: EITHER a b = LEFT a | RIGHT b
+:: PAIR   a b = PAIR a b
+:: CONS   a   = CONS String a
+
+// ---
+
+writeP :: a [String] -> [String] | serialize a
+writeP x s = if (needsParens x) ["(":write x [")":s]] (write x s)
+
+readP :: [String] -> Maybe (a, [String]) | serialize a
+readP ["(":r] = case read r of
+	Just (x,[")":r]) -> Just (x,r)
+	_                -> read ["(":r]
+readP r = case read r of
+	Just (x,r) -> if (needsParens x) Nothing (Just (x,r))
+	_          -> Nothing
+
+instance serialize UNIT
+where
+	write _ c = c
+	read r = Just (UNIT,r)
+
+instance serialize (EITHER a b) | serialize a & serialize b
+where
+	write (LEFT x)  c = write x c
+	write (RIGHT x) c = write x c
+	read r = case read r of
+		Just (x,r) -> Just (LEFT x, r)
+		Nothing    -> case read r of
+			Just (x,r) -> Just (RIGHT x,r)
+			Nothing    -> Nothing
+		// This goes wrong if the two type variables of EITHER are equal (and
+		// hence read for LEFT is the same as read for RIGHT: we will always
+		// return a LEFT. Therefore, given a type
+		//
+		//   :: T = C1 Int | C2 Int
+		//
+		// it is not possible to write and read C2 (C1 will be read, since LEFT
+		// has precedence). Like the example given as the answer to the
+		// reflection questin below, we don't think this to be fixable in the
+		// current setup.
+
+instance serialize (PAIR a b) | serialize a & serialize b
+where
+	write (PAIR x y) c = writeP x [" ":writeP y c]
+	read r = case readP r of
+		Just (x,[" ":r]) -> case readP r of
+			Nothing    -> Nothing
+			Just (y,r) -> Just (PAIR x y, r)
+		_ -> Nothing
+
+instance serialize (CONS a) | serialize a
+where
+	write e=:(CONS s x) c
+	| needsParens e = ["(":s:" ":write x [")":c]]
+	| otherwise     = [s:c]
+	read ["(":s:" ":r] = case read r of
+		Just (x,[")":r]) -> Just (CONS s x,r)
+		_                -> Nothing
+	read [s:r] = case read r of
+		Just (x,r) -> let e = CONS s x in if (needsParens e) Nothing (Just (e,r))
+		Nothing    -> Nothing
+	read _ = Nothing
+
+:: ListG a :== EITHER (CONS UNIT) (CONS (PAIR a [a]))
+
+fromList :: [a] -> ListG a
+fromList []     = LEFT (CONS "_Nil" UNIT)
+fromList [x:xs] = RIGHT (CONS "_Cons" (PAIR x xs))
+
+toList :: (ListG a) -> [a]
+toList (LEFT _)                     = []
+toList (RIGHT (CONS _ (PAIR x xs))) = [x:xs]
+
+instance serialize [a] | serialize a
+where
+	write l c = write (fromList l) c
+	read l = case read l of
+		Just (g,r) -> Just (toList g,r)
+		Nothing    -> Nothing
+
+:: Bin a = Leaf | Bin (Bin a) a (Bin a)
+:: BinG a :== EITHER (CONS UNIT) (CONS (PAIR (Bin a) (PAIR a (Bin a))))
+
+fromBin :: (Bin a) -> BinG a
+fromBin Leaf        = LEFT (CONS "Leaf" UNIT)
+fromBin (Bin l x r) = RIGHT (CONS "Bin" (PAIR l (PAIR x r)))
+
+toBin :: (BinG a) -> Bin a
+toBin (LEFT _)                             = Leaf
+toBin (RIGHT (CONS _ (PAIR l (PAIR x r)))) = Bin l x r
+
+instance serialize (Bin a) | serialize a
+where
+	write a c = write (fromBin a) c
+	read l = case read l of
+		Just (g,r) -> Just (toBin g,r)
+		Nothing    -> Nothing
+
+instance == (Bin a) | == a where // better use the generic approach
+	(==) Leaf Leaf = True
+	(==) (Bin l a r) (Bin k b s) = l == k && a == b && r == s
+	(==) _ _ = False
+
+// ---
+
+/**
+ * Reflection:
+ * The following is parsed as Just ([], []), which shows that the fact that
+ * there is no check on the name of the constructor can be exploited.
+ *
+ * In the actual Clean implementation, there is the construct `CONS of d` where
+ * d :: GenericConsDescriptor. This way, the name, arity, etc. of the
+ * constructor are available as part of the CONS type (even though this type
+ * does not explicitly contain the information). It is essentially a very
+ * restricted form of dependent typing, which makes it possible to distinguish
+ * the _Nil-CONS and the _Cons-CONS at compile-time.
+ *
+ * This requires the `CONS of d` construct, so I don't think this exploit is
+ * fixable in the current setup. It would of course be possible to redefine
+ * toList and toBin to result in a Maybe and check on the constructor there.
+ */
+Start :: Maybe ([Int], [String])
+Start = read ["_Cons"]
+
+Start = 
+	[ test True
+	, test False
+	, test 0
+	, test 123
+	, test -36
+	, test [42]
+	, test [0..4]
+	, test [[True],[]]
+	, test (Bin Leaf True Leaf)
+	, test [Bin (Bin Leaf [1] Leaf) [2] (Bin Leaf [3] (Bin Leaf [4,5] Leaf))]
+	, test [Bin (Bin Leaf [1] Leaf) [2] (Bin Leaf [3] (Bin (Bin Leaf [4,5] Leaf) [6,7] (Bin Leaf [8,9] Leaf)))]
+	]
+
+test :: a -> ([String],[String]) | serialize, == a
+test a = 
+	(if (isJust r)
+		(if (fst jr == a)
+			(if (isEmpty (tl (snd jr)))
+				["Oke "]
+				["Fail: not all input is consumed! ":snd jr])
+			["Fail: Wrong result ":write (fst jr) []])
+		["Fail: read result is Nothing "]
+	, ["write produces ": s]
+	)
+	where
+		s = write a ["\n"]
+		r = read s
+		jr = fromJust r