Commit 08ae6cbf authored by Reg Huijben's avatar Reg Huijben

week7reg

parent 83aaaaf0
module serialize7start
/*
Definition for assignment 7 in AFP 2019
Pieter Koopman pieter@cs.ru.nl
Use this in a project with Environment StdEnv
Use project option 'Basic Values Only' for nicer output
*/
import StdEnv, StdMaybe
class serialize a | isUnit 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
// ---
class isUnit a where
isUnit :: a -> Bool
instance isUnit UNIT where
isUnit a = True
instance isUnit a where
isUnit a = False
/* 2.1
instance serialize (EITHER a b) | serialize a & serialize b where
write (LEFT a) c = ["LEFT" : write a [] ++ c]
write (RIGHT b) c = ["RIGHT" : write b [] ++ c]
read ["LEFT":r] = case read r of
Nothing -> Nothing
Just (a,r) -> Just (LEFT a ,r)
read ["RIGHT":r] = case read r of
Nothing -> Nothing
Just (a,r) -> Just (RIGHT a ,r)
read _ = Nothing
instance serialize (CONS a) | serialize a where
write (CONS s a) c = ["CONS":s:(write a []) ++ c]
read ["CONS":s:r] = case read r of
Nothing -> Nothing
Just (a,r) -> Just(CONS s a, r)
read _ = Nothing
instance serialize (PAIR a b) | serialize a & serialize b where
write (PAIR a b) c = ["PAIR" : (write a []) ++ (write b []) ++ c]
read ["PAIR":r] = case read r of
Nothing -> Nothing
Just (a,r) -> case read r of
Nothing -> Nothing
Just (b,r) -> Just (PAIR a b, r)
read _ = Nothing
instance serialize UNIT where
write u c = ["UNIT":c]
read ["UNIT":r] = Just (UNIT,r)
read _ = Nothing
*/
//
//
//
//
// Generic serialization
//
instance serialize UNIT where
write u c = c
read r = Just (UNIT,r)
instance serialize (PAIR a b) | serialize a & serialize b where
write (PAIR a b) c = (write a (write b c))
read r = case read r of
Nothing -> Nothing
Just (a,r) -> case read r of
Nothing -> Nothing
Just (b,r) -> Just (PAIR a b, r)
instance serialize (EITHER a b) | serialize a & serialize b where
write (LEFT a) c = write a c
write (RIGHT b) c = write b c
read r = case read r of // try to parse the left side...
Just (a,r) -> Just (LEFT a ,r)
Nothing -> case read r of // if that fails, try to parse the right side
Just (a,r) -> Just (RIGHT a ,r)
Nothing -> Nothing
// Don't flip left and right though, that makes reading using the 'unit without parentheses' take very long
instance serialize (CONS a) | serialize a & isUnit a where
// Cheekily using the fact that a written unit is an empty list
//write (CONS s a) c = let written = write a [] in
// if (length (written) == 0)
// [s: written++c] // unit without parentheses
// ["(":s: (written ++ [")":c])] // else with parentheses
write (CONS s a) c = //let aa = isUnit a in
if (isUnit a)//(fst aa)
[s: (write a c)] // unit without parentheses
["(":s: (write a [")":c])] // else with parentheses
// (snd aa)
read ["(":s:r] = case read r of
Just (a,[")":r]) -> Just(CONS s a, r)
_ -> Nothing
read [s:r] = case read r of
Just (a,r) -> Just (CONS s a, r)
Nothing -> Nothing
read _ = Nothing
/* // for 2.2 CONS with some traces to see how often it fails/ succeeds
instance serialize (CONS a) | serialize a & isUnit a where
write (CONS s a) c = if (isUnit a) /* unit without () */ [s: (write a c)] /* else with () */ ["(":s: (write a [")":c])]
read ["(":s:r] = case trace "(" read r of
Just (a,[")":r]) -> trace ")" Just(CONS s a, r)
_ -> trace "-" Nothing
read [s:r] = case trace "{" read r of
Just (a,r) -> trace "}" if (isUnit a) (Just (CONS s a, r)) (trace "*" Nothing)
_ -> trace "~" Nothing
read _ = Nothing
*/
//
//
//
//
// Generic equality
//
instance == UNIT where
== _ _ = True
instance == (PAIR a b) | == a & == b where
== (PAIR a b) (PAIR a2 b2) = a == a2 && b == b2
instance == (EITHER a b) | == a & == b where
== (LEFT a) (LEFT b) = a == b
== (RIGHT a) (RIGHT b) = a == b
== _ _ = False
instance == (CONS a) | == a where
== (CONS _ a) (CONS _ b) = a == b
//
//
//
//
// Generic value count
//
class values a where
values :: a -> Int
instance values Int where
values _ = 1
instance values Bool where
values _ = 1
instance values UNIT where
values _ = 0
instance values (PAIR a b) | values a & values b where
values (PAIR a b) = values a + values b
instance values (EITHER a b) | values a & values b where
values (LEFT a) = values a
values (RIGHT b) = values b
instance values (CONS a) | values a where
values (CONS _ a) = values a
//
//
//
//
// Generic non-unit constructor count
//
class conses a where
conses :: a -> Int
instance conses Int where
conses _ = 0
instance conses Bool where
conses _ = 0
instance conses UNIT where
conses _ = 0
instance conses (PAIR a b) | conses a & conses b where
conses (PAIR a b) = conses a + conses b
instance conses (EITHER a b) | conses a & conses b where
conses (LEFT a) = conses a
conses (RIGHT b) = conses b
instance conses (CONS a) | conses a & isUnit a where
conses (CONS _ a) = conses a + if ( (isUnit a)) 0 1
//
//
//
//
// List definitions
//
:: ListG a :== EITHER (CONS UNIT) (CONS (PAIR a [a]))
fromList :: [a] -> ListG a
fromList [] = LEFT (CONS "Nil" UNIT)
fromList [a:l] = RIGHT (CONS "Cons" (PAIR a l))
toList :: (ListG a) -> [a]
toList (LEFT (CONS _ UNIT)) = []
toList (RIGHT (CONS _ (PAIR a l))) = [a:l]
instance serialize [a] | serialize a where
write l c = (write (fromList l) c)
read r = case read r of
Just (s,r) -> Just (toList s, r)
Nothing -> Nothing
instance values [a] | values a where
values l = values (fromList l)
// equality for lists is already defined
instance conses [a] | conses a where
conses l = conses (fromList l)
//
//
//
//
// Bin definitions
//
:: 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 a r) = RIGHT (CONS "Bin" (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)
instance serialize (Bin a) | serialize a where
write a c = write (fromBin a) c
read l = case read l of
Just (s,r) -> Just (toBin s,r)
Nothing -> Nothing
instance values (Bin a) | values a where
values a = values (fromBin a)
instance == (Bin a) | == a where
(==) t1 t2 = (fromBin t1) == (fromBin t2)
instance conses (Bin a) | conses a where
conses a = conses (fromBin a)
//
//
//
//
// Rose definitions
//
:: Rose a = Rose a [Rose a]
:: RoseG a :== CONS (PAIR (a) ([(Rose a)]))
fromRose :: (Rose a) -> (RoseG a)
fromRose (Rose e l) = CONS "Rose" (PAIR e l)
toRose :: (RoseG a) -> (Rose a)
toRose (CONS _ (PAIR e l)) = (Rose e l)
instance serialize (Rose a) | serialize a where
write l c = write (fromRose l) c
read r = case read r of
Nothing -> Nothing
Just (s,r) -> Just (toRose s, r)
instance values (Rose a) | values a where
values a = values (fromRose a)
instance == (Rose a) | == a where
(==) t1 t2 = (fromRose t1) == (fromRose t2)
instance conses (Rose a) | conses a where
conses a = conses (fromRose a)
//
//
//
//
// Tuple definitions
//
:: TupleG a b :== CONS (PAIR a b)
fromTup :: (a,b) -> (TupleG a b)
fromTup (a,b) = CONS "Tuple" (PAIR a b)
toTup :: (TupleG a b) -> (a,b)
toTup (CONS _ (PAIR a b)) = (a,b)
instance serialize (a,b) | serialize a & serialize b where
write l c = write (fromTup l) c
read r = case read r of
Nothing -> Nothing
Just (s,r) -> Just (toTup s, r)
// == already defined for tuple
//
//
//
//
// Triple definitions
//
:: Triple a b c = Triple a b c
:: TripleG a b c :== CONS (PAIR a (PAIR b c))
fromTrip :: (Triple a b c) -> (TripleG a b c)
fromTrip (Triple a b c) = CONS "Triple" (PAIR a (PAIR b c))
toTrip :: (TripleG a b c) -> (Triple a b c)
toTrip (CONS _ (PAIR a (PAIR b c))) = (Triple a b c)
instance serialize (Triple a b c) | serialize a & serialize b & serialize c where
write l c = write (fromTrip l) c
read r = case read r of
Nothing -> Nothing
Just (s,r) -> Just (toTrip s, r)
instance == (Triple a b c) | == a & == b & == c where
(==) t1 t2 = (fromTrip t1) == (fromTrip t2)
//
//
//
//
// Maybe definitions
//
:: MaybeG a :== (EITHER (CONS UNIT) (CONS a))
fromMaybe :: (Maybe a) -> (MaybeG a)
fromMaybe Nothing = LEFT (CONS "Nothing" UNIT)
fromMaybe (Just a) = RIGHT (CONS "Just" a)
toMaybe :: (MaybeG a) -> (Maybe a)
toMaybe (LEFT _) = Nothing
toMaybe (RIGHT (CONS _ a)) = Just a
instance serialize (Maybe a) | serialize a where // 'isUnit a' is neccessary since we get 'CONS "Just" a',
write l c = write (fromMaybe l) c // and serialize (CONS a) uses isUnit on that 'a'
read r = case read r of // Before we had the constraint here, but now it is moved to the serialize class
Nothing -> Nothing
Just (s,r) -> Just (toMaybe s, r)
//Start = values(Rose 1 [Rose 2 [], Rose 2 [], Rose 2 []])
//Start = conses [0..4] //(Rose 1 [Rose 2 [], Rose 2 [], Rose 2 []])
//Start = conses (Bin Leaf True (Bin Leaf True Leaf))
//Start = conses [1]//(Rose 1 [Rose 2 [], Rose 2 []])
//Start = zoepie (write (Rose 1 [Rose 2 [], Rose 2 [], Rose 2 []]) [])
//Start = conses (Rose 1 [Rose 2 [], Rose 2 [], Rose 2 []])// [0..4]
Start =
[test True
,test False
,test 0
,test 123
,test -36
,test (True,3) // Added (Bool,Int)
,test (Triple 1 True [1]) // Added (Int,Bool,[Int])
,test (Just True) // Added (Maybe Bool)
,test [Just True, Nothing] // Added [Maybe Bool]
,test [42]
,test [0..4]
,test [[True],[]]
,test (Bin Leaf True Leaf)
,test (Rose 1 [Rose 2 [], Rose 2 [], Rose 2 []]) // Added a Rrose Int
,test (Bin (Bin Leaf (Rose True [Rose False []]) Leaf) (Rose True []) Leaf) // And a Bin Rose Bool
,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)))]
]
zoepie :: [String] -> String
zoepie [a:r] = a +++ " " +++ zoepie r
zoepie [] = ""
test :: a -> ([String],[String]) | serialize, == a
test a =
(if (isJust r)
(if (fst jr == a)
(if (isEmpty (tl (snd jr)))
["Ok "]
["Fail: not all input is consumed! ":snd jr])
["Fail: Wrong result ":write (fst jr) []])
["Fail: read result is Nothing "]
, ["write produces ": [zoepie s]]
)
where
s = write a ["\n"]
r = read s
jr = fromJust r
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment