module serialize3Start

/*
  Definitions for assignment 3 in AFP 2018
  Kind indexed gennerics
  Pieter Koopman, pieter@cs.ru.nl
  September 2018
  
  Use StdEnv or iTask environment.
  Use Basic Values Only as conclose option for a nicer output.
*/

import StdEnv, StdMaybe

// use this as serialize for kind *
class serialize a where
	write :: a [String] -> [String]
	read  :: [String] -> Maybe (a, [String])

class serialize1 t where
	write1 :: (a [String] -> [String]) (t a) [String] -> [String]
	read1  :: ([String] -> Maybe (a, [String])) [String] -> Maybe (t a, [String])

class serialize2 t where
	write2 :: (a [String] -> [String]) (b [String] -> [String]) (t a b) [String] -> [String]
	read2  :: ([String] -> Maybe (a, [String])) ([String] -> Maybe (b, [String])) [String] -> Maybe (t a b, [String])

// ---

instance serialize Bool where
	write b c = [toString b:c]
	read ["True":c] = Just (True, c)
	read ["False":c] = Just (False, c)
	read _ = Nothing

instance serialize Int where
	write i c = [toString i:c]
	read [i:c] = Just (toInt i, c)
	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 = c
	read c = Just (UNIT, c)

instance serialize2 EITHER
where
	write2 wl _  (LEFT a) c = wl a c
	write2 _  wr (RIGHT a) c = wr a c
	read2 rl rr c = case rl c of
		Just (a, c) = Just (LEFT a, c)
		Nothing = case rr c of
			Just (a, c) = Just (RIGHT a, c)
			Nothing = Nothing

instance serialize2 PAIR
where
	write2 wl wr (PAIR l r) c = wl l (wr r c)
	read2 rl rr c = case rl c of
		Just (a, c) = case rr c of
			Just (b, c) = Just (PAIR a b, c)
			Nothing = Nothing
		Nothing = Nothing

instance serialize1 CONS
where
	write1 wa (CONS n a) c = ["(",n:wa a [")":c]]
	read1 ra ["(",n:c] = case ra c of
		Just (a, [")":c]) = Just (CONS n a, c)
		_ = Nothing
	read1 _ _ = Nothing

// ---

:: ListG a :== EITHER (CONS UNIT) (CONS (PAIR a [a]))

fromList :: [a] -> ListG a
fromList []    = LEFT  (CONS "Nil" UNIT)
fromList [a:x] = RIGHT (CONS "Cons" (PAIR a x))

toList :: (ListG a) -> [a]
toList (LEFT  (CONS "Nil" UNIT)) = []
toList (RIGHT (CONS "Cons" (PAIR a x))) = [a:x]

instance serialize1 []
where
	write1 wa a c = write2 (write1 write) (write1 (write2 wa (write1 wa))) (fromList a) c
	read1 ra c = case read2 (read1 read) (read1 (read2 ra (read1 ra))) c of
		Just (a, c) = Just (toList a, c)
		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 a r) = RIGHT (CONS "Bin" (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

instance == (Bin a) | == a where
  (==) Leaf Leaf = True
  (==) (Bin l a r) (Bin k b s) = l == k && a == b && r == s
  (==) _ _ = False

instance serialize1 Bin
where
	write1 wa a c = write2 (write1 write) (write1 (write2 (write1 wa) (write2 wa (write1 wa)))) (fromBin a) c
	read1 ra c = case read2 (read1 read) (read1 (read2 (read1 ra) (read2 ra (read1 ra)))) c of
		Just (a, c) = Just (toBin a, c)
		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 s c = write2 (write1 write) (write1 write) (fromCoin s) c
	read c = case read2 (read1 read) (read1 read) c of
		Just (a, c) = Just (toCoin a, c)
		Nothing = Nothing

/*
	Define a special purpose version for this type that writes and reads
	the value (7,True) as ["(","7",",","True",")"]
*/
instance serialize2 (,)
where
	write2 wa wb (a, b) c = ["(":wa a [",":wb b [")":c]]]
	read2 ra rb ["(":c] = case ra c of
		Just (a, [",":c]) = case rb c of
			Just (b, [")":c]) = Just ((a, b), c)
			_ = Nothing
		_ = Nothing
	read2 _ _ _ = Nothing

instance serialize [a] | serialize a
where
	write a c = write1 write a c
	read c = read1 read c

instance serialize (Bin a) | serialize a
where
	write a c = write1 write a c
	read c = read1 read c

instance serialize (a, b) | serialize a & serialize b
where
	write a c = write2 write write a c
	read c = read2 read read c

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