dos2unix

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