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