afp/a3/serialize3Start.icl

   1 module serialize3Start
   2
   3 /*
   4   Definitions for assignment 3 in AFP 2018
   5   Kind indexed gennerics
   6   Pieter Koopman, pieter@cs.ru.nl
   7   September 2018
   8
   9   Use StdEnv or iTask environment.
  10   Use Basic Values Only as conclose option for a nicer output.
  11 */
  12
  13 import StdEnv, StdMaybe
  14
  15 // use this as serialize for kind *
  16 class serialize a where
  17         write :: a [String] -> [String]
  18         read  :: [String] -> Maybe (a, [String])
  19
  20 class serialize1 t where
  21         write1 :: (a [String] -> [String]) (t a) [String] -> [String]
  22         read1  :: ([String] -> Maybe (a, [String])) [String] -> Maybe (t a, [String])
  23
  24 class serialize2 t where
  25         write2 :: (a [String] -> [String]) (b [String] -> [String]) (t a b) [String] -> [String]
  26         read2  :: ([String] -> Maybe (a, [String])) ([String] -> Maybe (b, [String])) [String] -> Maybe (t a b, [String])
  27
  28 // ---
  29
  30 instance serialize Bool where
  31         write b c = [toString b:c]
  32         read ["True":c] = Just (True, c)
  33         read ["False":c] = Just (False, c)
  34         read _ = Nothing
  35
  36 instance serialize Int where
  37         write i c = [toString i:c]
  38         read [i:c] = Just (toInt i, c)
  39         read _ = Nothing
  40
  41 // ---
  42
  43 :: UNIT     = UNIT
  44 :: EITHER a b = LEFT a | RIGHT b
  45 :: PAIR   a b = PAIR a b
  46 :: CONS   a   = CONS String a
  47
  48 instance serialize UNIT
  49 where
  50         write UNIT c = c
  51         read c = Just (UNIT, c)
  52
  53 instance serialize2 EITHER
  54 where
  55         write2 wl _  (LEFT a) c = wl a c
  56         write2 _  wr (RIGHT a) c = wr a c
  57         read2 rl rr c = case rl c of
  58                 Just (a, c) = Just (LEFT a, c)
  59                 Nothing = case rr c of
  60                         Just (a, c) = Just (RIGHT a, c)
  61                         Nothing = Nothing
  62
  63 instance serialize2 PAIR
  64 where
  65         write2 wl wr (PAIR l r) c = wl l (wr r c)
  66         read2 rl rr c = case rl c of
  67                 Just (a, c) = case rr c of
  68                         Just (b, c) = Just (PAIR a b, c)
  69                         Nothing = Nothing
  70                 Nothing = Nothing
  71
  72 instance serialize1 CONS
  73 where
  74         write1 wa (CONS n a) c = ["(",n:wa a [")":c]]
  75         read1 ra ["(",n:c] = case ra c of
  76                 Just (a, [")":c]) = Just (CONS n a, c)
  77                 _ = Nothing
  78         read1 _ _ = Nothing
  79
  80 // ---
  81
  82 :: ListG a :== EITHER (CONS UNIT) (CONS (PAIR a [a]))
  83
  84 fromList :: [a] -> ListG a
  85 fromList []    = LEFT  (CONS "Nil" UNIT)
  86 fromList [a:x] = RIGHT (CONS "Cons" (PAIR a x))
  87
  88 toList :: (ListG a) -> [a]
  89 toList (LEFT  (CONS "Nil" UNIT)) = []
  90 toList (RIGHT (CONS "Cons" (PAIR a x))) = [a:x]
  91
  92 instance serialize1 []
  93 where
  94         write1 wa a c = write2 (write1 write) (write1 (write2 wa (write1 wa))) (fromList a) c
  95         read1 ra c = case read2 (read1 read) (read1 (read2 ra (read1 ra))) c of
  96                 Just (a, c) = Just (toList a, c)
  97                 Nothing = Nothing
  98
  99 // ---
 100
 101 :: Bin a = Leaf | Bin (Bin a) a (Bin a)
 102
 103 :: BinG a :== EITHER (CONS UNIT) (CONS (PAIR (Bin a) (PAIR a (Bin a))))
 104
 105 fromBin :: (Bin a) -> BinG a
 106 fromBin Leaf = LEFT (CONS "Leaf" UNIT)
 107 fromBin (Bin l a r) = RIGHT (CONS "Bin" (PAIR l (PAIR a r)))
 108
 109 toBin :: (BinG a) -> Bin a
 110 toBin (LEFT (CONS _ UNIT)) = Leaf
 111 toBin (RIGHT (CONS _ (PAIR l (PAIR a r)))) = Bin l a r
 112
 113 instance == (Bin a) | == a where
 114   (==) Leaf Leaf = True
 115   (==) (Bin l a r) (Bin k b s) = l == k && a == b && r == s
 116   (==) _ _ = False
 117
 118 instance serialize1 Bin
 119 where
 120         write1 wa a c = write2 (write1 write) (write1 (write2 (write1 wa) (write2 wa (write1 wa)))) (fromBin a) c
 121         read1 ra c = case read2 (read1 read) (read1 (read2 (read1 ra) (read2 ra (read1 ra)))) c of
 122                 Just (a, c) = Just (toBin a, c)
 123                 Nothing = Nothing
 124
 125 // ---
 126
 127 :: Coin = Head | Tail
 128 :: CoinG :== EITHER (CONS UNIT) (CONS UNIT)
 129
 130 fromCoin :: Coin -> CoinG
 131 fromCoin Head = LEFT (CONS "Head" UNIT)
 132 fromCoin Tail = RIGHT (CONS "Tail" UNIT)
 133
 134 toCoin :: CoinG -> Coin
 135 toCoin (LEFT (CONS _ UNIT)) = Head
 136 toCoin (RIGHT (CONS _ UNIT)) = Tail
 137
 138 instance == Coin where
 139   (==) Head Head = True
 140   (==) Tail Tail = True
 141   (==) _    _    = False
 142
 143 instance serialize Coin where
 144         write s c = write2 (write1 write) (write1 write) (fromCoin s) c
 145         read c = case read2 (read1 read) (read1 read) c of
 146                 Just (a, c) = Just (toCoin a, c)
 147                 Nothing = Nothing
 148
 149 /*
 150         Define a special purpose version for this type that writes and reads
 151         the value (7,True) as ["(","7",",","True",")"]
 152 */
 153 instance serialize2 (,)
 154 where
 155         write2 wa wb (a, b) c = ["(":wa a [",":wb b [")":c]]]
 156         read2 ra rb ["(":c] = case ra c of
 157                 Just (a, [",":c]) = case rb c of
 158                         Just (b, [")":c]) = Just ((a, b), c)
 159                         _ = Nothing
 160                 _ = Nothing
 161         read2 _ _ _ = Nothing
 162
 163 instance serialize [a] | serialize a
 164 where
 165         write a c = write1 write a c
 166         read c = read1 read c
 167
 168 instance serialize (Bin a) | serialize a
 169 where
 170         write a c = write1 write a c
 171         read c = read1 read c
 172
 173 instance serialize (a, b) | serialize a & serialize b
 174 where
 175         write a c = write2 write write a c
 176         read c = read2 read read c
 177
 178 // ---
 179 // output looks nice if compiled with "Basic Values Only" for console in project options
 180 Start =
 181   [test True
 182   ,test False
 183   ,test 0
 184   ,test 123
 185   ,test -36
 186   ,test [42]
 187   ,test [0..4]
 188   ,test [[True],[]]
 189   ,test [[[1]],[[2],[3,4]],[[]]]
 190   ,test (Bin Leaf True Leaf)
 191   ,test [Bin (Bin Leaf [1] Leaf) [2] (Bin Leaf [3] (Bin Leaf [4,5] Leaf))]
 192   ,test [Bin (Bin Leaf [1] Leaf) [2] (Bin Leaf [3] (Bin (Bin Leaf [4,5] Leaf) [6,7] (Bin Leaf [8,9] Leaf)))]
 193   ,test Head
 194   ,test Tail
 195   ,test (7,True)
 196   ,test (Head,(7,[Tail]))
 197   ,["End of the tests.\n"]
 198   ]
 199
 200 test :: a -> [String] | serialize, == a
 201 test a =
 202   (if (isJust r)
 203     (if (fst jr == a)
 204       (if (isEmpty (tl (snd jr)))
 205         ["Oke"]
 206         ["Not all input is consumed! ":snd jr])
 207       ["Wrong result: ":write (fst jr) []])
 208     ["read result is Nothing"]
 209   ) ++ [", write produces: ": s]
 210   where
 211     s = write a ["\n"]
 212     r = read s
 213     jr = fromJust r