From b9661b6d185fcb92e9106cfd174484489e0c8d78 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Mon, 2 Oct 2017 20:15:34 +0200 Subject: dos2unix --- assignment-2/serialize2start.icl | 520 +++++++++++++++++++-------------------- 1 file changed, 260 insertions(+), 260 deletions(-) (limited to 'assignment-2/serialize2start.icl') 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 -- cgit v1.2.3