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
