diff options
Diffstat (limited to 'assignment-2/serialize2start.icl')
-rw-r--r-- | assignment-2/serialize2start.icl | 520 |
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 |