summaryrefslogtreecommitdiff
path: root/assignment-3/serialize3Start.icl
blob: 73f7df442b78b5a5d760995bb8ba434a540a7451 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
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.
*/