From b9661b6d185fcb92e9106cfd174484489e0c8d78 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Mon, 2 Oct 2017 20:15:34 +0200 Subject: dos2unix --- assignment-3/genericMap.icl | 74 +++--- assignment-3/serialize3Start.icl | 526 +++++++++++++++++++-------------------- 2 files changed, 300 insertions(+), 300 deletions(-) (limited to 'assignment-3') diff --git a/assignment-3/genericMap.icl b/assignment-3/genericMap.icl index 6ea1bf4..f2d99e2 100644 --- a/assignment-3/genericMap.icl +++ b/assignment-3/genericMap.icl @@ -1,37 +1,37 @@ -module genericMap - -import StdEnv -import StdGeneric -import GenEq - -generic gMap a b :: a -> b -gMap{|Int|} x = x -gMap{|Real|} x = x -gMap{|UNIT|} x = x -gMap{|PAIR|} f g (PAIR x y) = PAIR (f x) (g y) -gMap{|EITHER|} f g (LEFT x) = LEFT (f x) -gMap{|EITHER|} f g (RIGHT x) = RIGHT (g x) -gMap{|CONS|} f (CONS x) = CONS (f x) -gMap{|OBJECT|} f (OBJECT x) = OBJECT (f x) - -:: Bin a = Leaf | Bin (Bin a) a (Bin a) - -derive gMap [], (,), Bin - -t = Bin (Bin Leaf 1 Leaf) 2 (Bin (Bin Leaf 3 Leaf) 4 Leaf) -l = [1..7] - -// Part 1 -Start = gMap{|*->*|} fac t - // (Bin (Bin Leaf 1 Leaf) 2 (Bin (Bin Leaf 3 Leaf) 5 Leaf)) -Start = gMap{|*->*|} (\i -> (i, fac i)) l - // [(1,1),(2,2),(3,3),(4,5),(5,8),(6,13),(7,21)] -Start = gMap{|*->*->*|} (gMap{|*->*|} fac) (gMap{|*->*|} fac) (l,t) - // ([1,2,3,5,8,13,21],(Bin (Bin Leaf 1 Leaf) 2 (Bin (Bin Leaf 3 Leaf) 5 Leaf))) - -// Part 2 -Start = gEq{|*|} [1,2] [1,2] // True -Start = gEq{|*|} [1,2] [2,3] // False -Start = gEq{|*->*|} (\a b -> not (a < b || b < a)) [1,2] [2,3] // False - -fac n = let fs = [1:1:[(fs!!(i-1)) + (fs!!(i-2)) \\ i <- [2..]]] in fs !! n +module genericMap + +import StdEnv +import StdGeneric +import GenEq + +generic gMap a b :: a -> b +gMap{|Int|} x = x +gMap{|Real|} x = x +gMap{|UNIT|} x = x +gMap{|PAIR|} f g (PAIR x y) = PAIR (f x) (g y) +gMap{|EITHER|} f g (LEFT x) = LEFT (f x) +gMap{|EITHER|} f g (RIGHT x) = RIGHT (g x) +gMap{|CONS|} f (CONS x) = CONS (f x) +gMap{|OBJECT|} f (OBJECT x) = OBJECT (f x) + +:: Bin a = Leaf | Bin (Bin a) a (Bin a) + +derive gMap [], (,), Bin + +t = Bin (Bin Leaf 1 Leaf) 2 (Bin (Bin Leaf 3 Leaf) 4 Leaf) +l = [1..7] + +// Part 1 +Start = gMap{|*->*|} fac t + // (Bin (Bin Leaf 1 Leaf) 2 (Bin (Bin Leaf 3 Leaf) 5 Leaf)) +Start = gMap{|*->*|} (\i -> (i, fac i)) l + // [(1,1),(2,2),(3,3),(4,5),(5,8),(6,13),(7,21)] +Start = gMap{|*->*->*|} (gMap{|*->*|} fac) (gMap{|*->*|} fac) (l,t) + // ([1,2,3,5,8,13,21],(Bin (Bin Leaf 1 Leaf) 2 (Bin (Bin Leaf 3 Leaf) 5 Leaf))) + +// Part 2 +Start = gEq{|*|} [1,2] [1,2] // True +Start = gEq{|*|} [1,2] [2,3] // False +Start = gEq{|*->*|} (\a b -> not (a < b || b < a)) [1,2] [2,3] // False + +fac n = let fs = [1:1:[(fs!!(i-1)) + (fs!!(i-2)) \\ i <- [2..]]] in fs !! n diff --git a/assignment-3/serialize3Start.icl b/assignment-3/serialize3Start.icl index 962716a..73f7df4 100644 --- a/assignment-3/serialize3Start.icl +++ b/assignment-3/serialize3Start.icl @@ -1,263 +1,263 @@ -module serialize3Start - -/* - Definitions for assignment 3 in AFP 2017 - Kind indexed gennerics - Pieter Koopman, pieter@cs.ru.nl - September 2017 - - use environment: StdMaybe from Libraries/StdLib -*/ - -import StdEnv, StdMaybe - -:: Write a :== a [String] -> [String] -:: Read a :== [String] -> Maybe (a,[String]) - -// use this as serialize0 for kind * -class serialize a -where - write :: a [String] -> [String] - read :: [String] -> Maybe (a,[String]) - -class serialize1 t -where - write1 :: (Write a) (t a) [String] -> [String] - read1 :: (Read a) [String] -> Maybe (t a, [String]) - -class serialize2 t -where - write2 :: (Write a) (Write b) (t a b) [String] -> [String] - read2 :: (Read a) (Read b) [String] -> Maybe (t a b, [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 - -instance serialize UNIT -where - write UNIT s = s - read l = Just (UNIT, l) - -instance serialize2 EITHER -where - write2 f _ (LEFT x) s = f x s - write2 _ g (RIGHT x) s = g x s - read2 f g s = case f s of - Just (x,s) -> Just (LEFT x,s) - Nothing -> case g s of - Just (x,s) -> Just (RIGHT x,s) - Nothing -> Nothing - -instance serialize2 PAIR -where - write2 f g (PAIR x y) s = f x [" ":g y s] - read2 f g s = case f s of - Just (x,[" ":s]) -> case g s of - Just (y,s) -> Just (PAIR x y,s) - Nothing -> Nothing - _ -> Nothing - -instance serialize1 CONS -where - write1 f (CONS c x) s = cleanup ["(":c:" ":f x [")":s]] - where - // Remove redundant parentheses - cleanup :: [String] -> [String] - cleanup ["(":c:" ":")":s] = [c:s] - cleanup s = s - read1 _ _ = abort "Use read1Cons instead\n" - -/** - * Special read1 variant which checks for a constructor name. - * @param The constructor name to match - * @param The read function for the constructor argument - * @param The stream - * @result The parsed constructor and the rest of the stream, if successful - */ -read1Cons :: String (Read a) [String] -> Maybe (CONS a, [String]) -read1Cons n f ["(":c:" ":s] -| c == n = case f s of - Just (x,[")":s]) -> Just (CONS c x,s) - _ -> Nothing -| otherwise = Nothing -// Special case for constructors without parentheses. After reading the -// argument, we continue with the original stream, because cleanup only removes -// parentheses for constructors where the write of the argument did not write -// anything. It is probably equivalent to continuing with the new stream (as -// the read should not read anything), but this seems safer. -read1Cons n f [c:s] -| c == n = case f s of - Just (x,_) -> Just (CONS c x,s) - Nothing -> Nothing -| otherwise = Nothing -read1Cons _ _ _ = Nothing - -// --- - -:: ListG a :== EITHER (CONS UNIT) (CONS (PAIR a [a])) - -fromList :: [a] -> ListG a -fromList [] = LEFT (CONS NilString UNIT) -fromList [a:x] = RIGHT (CONS ConsString (PAIR a x)) - -toList :: (ListG a) -> [a] -toList (LEFT (CONS NilString UNIT)) = [] -toList (RIGHT (CONS ConsString (PAIR a x))) = [a:x] - -NilString :== "Nil" -ConsString :== "Cons" - -instance serialize [a] | serialize a -where - write xs s = write2 (write1 write) (write1 (write2 write write)) (fromList xs) s - read s = case read2 (read1Cons NilString read) (read1Cons ConsString (read2 read read)) s of - Just (xs,s) -> Just (toList xs,s) - 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 LeafString UNIT) -fromBin (Bin l a r) = RIGHT (CONS BinString (PAIR l (PAIR a r))) - -toBin :: (BinG a) -> Bin a -toBin (LEFT (CONS _ UNIT)) = Leaf -toBin (RIGHT (CONS _ (PAIR l (PAIR a r)))) = Bin l a r - -LeafString :== "Leaf" -BinString :== "Bin" - -instance == (Bin a) | == a where - (==) Leaf Leaf = True - (==) (Bin l a r) (Bin k b s) = l == k && a == b && r == s - (==) _ _ = False - -instance serialize (Bin a) | serialize a where - write b s = write2 (write1 write) (write1 (write2 write (write2 write write))) (fromBin b) s - read l = case read2 (read1Cons LeafString read) (read1Cons BinString (read2 read (read2 read read))) l of - Just (b,s) -> Just (toBin b,s) - Nothing -> Nothing - -// --- - -:: Coin = Head | Tail -:: CoinG :== EITHER (CONS UNIT) (CONS UNIT) - -fromCoin :: Coin -> CoinG -fromCoin Head = LEFT (CONS "Head" UNIT) -fromCoin Tail = RIGHT (CONS "Tail" UNIT) - -toCoin :: CoinG -> Coin -toCoin (LEFT (CONS _ UNIT)) = Head -toCoin (RIGHT (CONS _ UNIT)) = Tail - -instance == Coin where - (==) Head Head = True - (==) Tail Tail = True - (==) _ _ = False - -instance serialize Coin where - write c s = write2 (write1 write) (write1 write) (fromCoin c) s - read l = case read2 (read1Cons "Head" read) (read1Cons "Tail" read) l of - Just (c,l) -> Just (toCoin c,l) - Nothing -> Nothing - -/* - Define a special purpose version for this type that writes and reads - the value (7,True) as ["(","7",",","True",")"] -*/ -instance serialize (a,b) | serialize a & serialize b where - write t c = write2 write write t c - read l = read2 read read l - -instance serialize2 (,) -where - write2 f g (x,y) s = ["(":f x [",":g y [")":s]]] - read2 f g ["(":s] = case f s of - Just (x,[",":s]) -> case g s of - Just (y,[")":s]) -> Just ((x,y), s) - _ -> Nothing - _ -> Nothing - read2 _ _ _ = Nothing - -// --- -// output looks nice if compiled with "Basic Values Only" for console in project options -Start = - [test True - ,test False - ,test 0 - ,test 123 - ,test -36 - ,test [42] - ,test [0..4] - ,test [[True],[]] - ,test [[[1]],[[2],[3,4]],[[]]] - ,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 Head - ,test Tail - ,test (7,True) - ,test (Head,(7,[Tail])) - ,["End of the tests.\n"] - ] - -test :: a -> [String] | serialize, == a -test a = - (if (isJust r) - (if (fst jr == a) - (if (isEmpty (tl (snd jr))) - ["Oke"] - ["Not all input is consumed! ":snd jr]) - ["Wrong result: ":write (fst jr) []]) - ["read result is Nothing"] - ) ++ [", write produces: ": s] - where - s = write a ["\n"] - r = read s - jr = fromJust r - -/* -Oke, write produces: True -Oke, write produces: False -Oke, write produces: 0 -Oke, write produces: 123 -Oke, write produces: -36 -Oke, write produces: (Cons 42 Nil) -Oke, write produces: (Cons 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))) -Oke, write produces: (Cons (Cons True Nil) (Cons Nil Nil)) -Oke, write produces: (Cons (Cons (Cons 1 Nil) Nil) (Cons (Cons (Cons 2 Nil) (Cons (Cons 3 (Cons 4 Nil)) Nil)) (Cons (Cons Nil Nil) Nil))) -Oke, write produces: (Bin Leaf True Leaf) -Oke, write produces: (Cons (Bin (Bin Leaf (Cons 1 Nil) Leaf) (Cons 2 Nil) (Bin Leaf (Cons 3 Nil) (Bin Leaf (Cons 4 (Cons 5 Nil)) Leaf))) Nil) -Oke, write produces: (Cons (Bin (Bin Leaf (Cons 1 Nil) Leaf) (Cons 2 Nil) (Bin Leaf (Cons 3 Nil) (Bin (Bin Leaf (Cons 4 (Cons 5 Nil)) Leaf) (Cons 6 (Cons 7 Nil)) (Bin Leaf (Cons 8 (Cons 9 Nil)) Leaf)))) Nil) -Oke, write produces: Head -Oke, write produces: Tail -Oke, write produces: (7,True) -Oke, write produces: (Head,(7,(Cons Tail Nil))) -End of the tests. -*/ +module serialize3Start + +/* + Definitions for assignment 3 in AFP 2017 + Kind indexed gennerics + Pieter Koopman, pieter@cs.ru.nl + September 2017 + + use environment: StdMaybe from Libraries/StdLib +*/ + +import StdEnv, StdMaybe + +:: Write a :== a [String] -> [String] +:: Read a :== [String] -> Maybe (a,[String]) + +// use this as serialize0 for kind * +class serialize a +where + write :: a [String] -> [String] + read :: [String] -> Maybe (a,[String]) + +class serialize1 t +where + write1 :: (Write a) (t a) [String] -> [String] + read1 :: (Read a) [String] -> Maybe (t a, [String]) + +class serialize2 t +where + write2 :: (Write a) (Write b) (t a b) [String] -> [String] + read2 :: (Read a) (Read b) [String] -> Maybe (t a b, [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 + +instance serialize UNIT +where + write UNIT s = s + read l = Just (UNIT, l) + +instance serialize2 EITHER +where + write2 f _ (LEFT x) s = f x s + write2 _ g (RIGHT x) s = g x s + read2 f g s = case f s of + Just (x,s) -> Just (LEFT x,s) + Nothing -> case g s of + Just (x,s) -> Just (RIGHT x,s) + Nothing -> Nothing + +instance serialize2 PAIR +where + write2 f g (PAIR x y) s = f x [" ":g y s] + read2 f g s = case f s of + Just (x,[" ":s]) -> case g s of + Just (y,s) -> Just (PAIR x y,s) + Nothing -> Nothing + _ -> Nothing + +instance serialize1 CONS +where + write1 f (CONS c x) s = cleanup ["(":c:" ":f x [")":s]] + where + // Remove redundant parentheses + cleanup :: [String] -> [String] + cleanup ["(":c:" ":")":s] = [c:s] + cleanup s = s + read1 _ _ = abort "Use read1Cons instead\n" + +/** + * Special read1 variant which checks for a constructor name. + * @param The constructor name to match + * @param The read function for the constructor argument + * @param The stream + * @result The parsed constructor and the rest of the stream, if successful + */ +read1Cons :: String (Read a) [String] -> Maybe (CONS a, [String]) +read1Cons n f ["(":c:" ":s] +| c == n = case f s of + Just (x,[")":s]) -> Just (CONS c x,s) + _ -> Nothing +| otherwise = Nothing +// Special case for constructors without parentheses. After reading the +// argument, we continue with the original stream, because cleanup only removes +// parentheses for constructors where the write of the argument did not write +// anything. It is probably equivalent to continuing with the new stream (as +// the read should not read anything), but this seems safer. +read1Cons n f [c:s] +| c == n = case f s of + Just (x,_) -> Just (CONS c x,s) + Nothing -> Nothing +| otherwise = Nothing +read1Cons _ _ _ = Nothing + +// --- + +:: ListG a :== EITHER (CONS UNIT) (CONS (PAIR a [a])) + +fromList :: [a] -> ListG a +fromList [] = LEFT (CONS NilString UNIT) +fromList [a:x] = RIGHT (CONS ConsString (PAIR a x)) + +toList :: (ListG a) -> [a] +toList (LEFT (CONS NilString UNIT)) = [] +toList (RIGHT (CONS ConsString (PAIR a x))) = [a:x] + +NilString :== "Nil" +ConsString :== "Cons" + +instance serialize [a] | serialize a +where + write xs s = write2 (write1 write) (write1 (write2 write write)) (fromList xs) s + read s = case read2 (read1Cons NilString read) (read1Cons ConsString (read2 read read)) s of + Just (xs,s) -> Just (toList xs,s) + 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 LeafString UNIT) +fromBin (Bin l a r) = RIGHT (CONS BinString (PAIR l (PAIR a r))) + +toBin :: (BinG a) -> Bin a +toBin (LEFT (CONS _ UNIT)) = Leaf +toBin (RIGHT (CONS _ (PAIR l (PAIR a r)))) = Bin l a r + +LeafString :== "Leaf" +BinString :== "Bin" + +instance == (Bin a) | == a where + (==) Leaf Leaf = True + (==) (Bin l a r) (Bin k b s) = l == k && a == b && r == s + (==) _ _ = False + +instance serialize (Bin a) | serialize a where + write b s = write2 (write1 write) (write1 (write2 write (write2 write write))) (fromBin b) s + read l = case read2 (read1Cons LeafString read) (read1Cons BinString (read2 read (read2 read read))) l of + Just (b,s) -> Just (toBin b,s) + Nothing -> Nothing + +// --- + +:: Coin = Head | Tail +:: CoinG :== EITHER (CONS UNIT) (CONS UNIT) + +fromCoin :: Coin -> CoinG +fromCoin Head = LEFT (CONS "Head" UNIT) +fromCoin Tail = RIGHT (CONS "Tail" UNIT) + +toCoin :: CoinG -> Coin +toCoin (LEFT (CONS _ UNIT)) = Head +toCoin (RIGHT (CONS _ UNIT)) = Tail + +instance == Coin where + (==) Head Head = True + (==) Tail Tail = True + (==) _ _ = False + +instance serialize Coin where + write c s = write2 (write1 write) (write1 write) (fromCoin c) s + read l = case read2 (read1Cons "Head" read) (read1Cons "Tail" read) l of + Just (c,l) -> Just (toCoin c,l) + Nothing -> Nothing + +/* + Define a special purpose version for this type that writes and reads + the value (7,True) as ["(","7",",","True",")"] +*/ +instance serialize (a,b) | serialize a & serialize b where + write t c = write2 write write t c + read l = read2 read read l + +instance serialize2 (,) +where + write2 f g (x,y) s = ["(":f x [",":g y [")":s]]] + read2 f g ["(":s] = case f s of + Just (x,[",":s]) -> case g s of + Just (y,[")":s]) -> Just ((x,y), s) + _ -> Nothing + _ -> Nothing + read2 _ _ _ = Nothing + +// --- +// output looks nice if compiled with "Basic Values Only" for console in project options +Start = + [test True + ,test False + ,test 0 + ,test 123 + ,test -36 + ,test [42] + ,test [0..4] + ,test [[True],[]] + ,test [[[1]],[[2],[3,4]],[[]]] + ,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 Head + ,test Tail + ,test (7,True) + ,test (Head,(7,[Tail])) + ,["End of the tests.\n"] + ] + +test :: a -> [String] | serialize, == a +test a = + (if (isJust r) + (if (fst jr == a) + (if (isEmpty (tl (snd jr))) + ["Oke"] + ["Not all input is consumed! ":snd jr]) + ["Wrong result: ":write (fst jr) []]) + ["read result is Nothing"] + ) ++ [", write produces: ": s] + where + s = write a ["\n"] + r = read s + jr = fromJust r + +/* +Oke, write produces: True +Oke, write produces: False +Oke, write produces: 0 +Oke, write produces: 123 +Oke, write produces: -36 +Oke, write produces: (Cons 42 Nil) +Oke, write produces: (Cons 0 (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))) +Oke, write produces: (Cons (Cons True Nil) (Cons Nil Nil)) +Oke, write produces: (Cons (Cons (Cons 1 Nil) Nil) (Cons (Cons (Cons 2 Nil) (Cons (Cons 3 (Cons 4 Nil)) Nil)) (Cons (Cons Nil Nil) Nil))) +Oke, write produces: (Bin Leaf True Leaf) +Oke, write produces: (Cons (Bin (Bin Leaf (Cons 1 Nil) Leaf) (Cons 2 Nil) (Bin Leaf (Cons 3 Nil) (Bin Leaf (Cons 4 (Cons 5 Nil)) Leaf))) Nil) +Oke, write produces: (Cons (Bin (Bin Leaf (Cons 1 Nil) Leaf) (Cons 2 Nil) (Bin Leaf (Cons 3 Nil) (Bin (Bin Leaf (Cons 4 (Cons 5 Nil)) Leaf) (Cons 6 (Cons 7 Nil)) (Bin Leaf (Cons 8 (Cons 9 Nil)) Leaf)))) Nil) +Oke, write produces: Head +Oke, write produces: Tail +Oke, write produces: (7,True) +Oke, write produces: (Head,(7,(Cons Tail Nil))) +End of the tests. +*/ -- cgit v1.2.3