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