module serialize2start

/*
  Definition for assignment 2 in AFP 2017
  Pieter Koopman pieter@cs.ru.nl
  September 2017
*/

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).
 */

class serialize 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

// ---

instance serialize UNIT
where
	write UNIT c = ["UNIT":c]
	read ["UNIT":r] = Just (UNIT, r)
	read _          = Nothing

instance serialize (EITHER a b) | serialize a & serialize b
where
	write (LEFT x)  c = ["LEFT": write x c]
	write (RIGHT x) c = ["RIGHT":write x c]
	read ["LEFT":r] = case read r of
		Just (x,r) -> Just (LEFT x, r)
		Nothing    -> Nothing
	read ["RIGHT":r] = case read r of
		Just (x,r) -> Just (RIGHT x, r)
		Nothing    -> Nothing
	read _ = Nothing

instance serialize (PAIR a b) | serialize a & serialize b
where
	write (PAIR x y) c = write x (write y c)
	read r = case read r of
		Nothing    -> Nothing
		Just (x,r) -> case read r of
			Nothing    -> Nothing
			Just (y,r) -> Just (PAIR x y, r)

instance serialize (CONS a) | serialize a
where
	write (CONS _ x) c = write x c
	read r = case read r of
		Just (x,r) -> Just (CONS "" x,r)
		Nothing    -> 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

// ---

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