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])

// ---

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

// ---

:: 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 a s = s
 read    s = 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 = s
	read    l = 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 = s
	read    l = 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 (a,b) c = c
	read _ = 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