summaryrefslogtreecommitdiff
path: root/assignment-2/serialize2start.icl
blob: d8b5cccd094b4b48dad9a96956fc1a071e0e7773 (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
module serialize2start

/*
  Definition for assignment 2 in AFP 2017
  Pieter Koopman pieter@cs.ru.nl
  September 2017
*/

import StdEnv, StdMaybe

/**
 * Review questions
 *
 * 1. A type is a set of values. In the case of UNIT, UNIT = {UNIT}. The set of
 * possible arguments to == on a type T is {(x,y) | x <- T, y <- T}, so in the
 * case of UNIT we have {(UNIT,UNIT)}. Hence, this alternative matches always.
 * The other suggestions are equivalent, as the pattern match is because of
 * this meaningless and therefore all alternatives in the question are
 * equivalent.
 *
 * 2. The name of the constructor is redundant information, since the same
 * information can also be derived (compile-time only, hence it has to be
 * stored) from the LEFT/RIGHT-path through the ADT tree. Hence, checking on
 * the constructor name is not needed.
 *
 * 3.
 * - []   = LEFT (CONS "_Nil" UNIT)
 * - Leaf = LEFT (CONS "Leaf" UNIT)
 * == has type a a -> Bool, so we cannot apply it to Leaf and [], which are not
 * of the same type. So no, this does not yield True (it does not yield
 * anything, as you won't be able to compile it).
 */

/**
 * The number of elements in an expression that will be placed on the outer
 * level w.r.t. parentheses when pretty-printing.
 *
 * For instance:
 *  - "37"             -> 1
 *  - "_Nil"           -> 1
 *  - "_Cons 1 _Nil"   -> 3
 *  - "(_Cons 1 _Nil)" -> 1
 */
class outerElems a
where
	outerElems :: a -> Int

	/**
	 * An expression needs parentheses when it has more than one element on the
	 * outer level.
	 */
	needsParens x :== outerElems x > 1

/**
 * In the default case, parentheses are placed around the whole expression, so
 * the number of elements on the outer level is 1.
 */
instance outerElems a    where outerElems _ = 1

//* UNITs are not printed.
instance outerElems UNIT where outerElems _ = 0

//* The arguments and the constructor
instance outerElems (CONS a) | outerElems a
where outerElems (CONS _ x) = 1 + outerElems x

//* Both elements appear on the outer level
instance outerElems (PAIR a b) | outerElems a & outerElems b
where outerElems (PAIR x y) = outerElems x + outerElems y

instance outerElems (EITHER a b) | outerElems a & outerElems b
where
	outerElems (LEFT x)  = outerElems x
	outerElems (RIGHT x) = outerElems x

/**
 * We extended the definition with a restriction on outerElems. This extra
 * restriction is OK, since there is an instance of outerElems for every type
 * (and hence, this restriction does not exclude any type).
 */
class serialize a | outerElems 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

// ---

writeP :: a [String] -> [String] | serialize a
writeP x s = if (needsParens x) ["(":write x [")":s]] (write x s)

readP :: [String] -> Maybe (a, [String]) | serialize a
readP ["(":r] = case read r of
	Just (x,[")":r]) -> Just (x,r)
	_                -> read ["(":r]
readP r = case read r of
	Just (x,r) -> if (needsParens x) Nothing (Just (x,r))
	_          -> Nothing

instance serialize UNIT
where
	write _ c = c
	read r = Just (UNIT,r)

instance serialize (EITHER a b) | serialize a & serialize b
where
	write (LEFT x)  c = write x c
	write (RIGHT x) c = write x c
	read r = case read r of
		Just (x,r) -> Just (LEFT x, r)
		Nothing    -> case read r of
			Just (x,r) -> Just (RIGHT x,r)
			Nothing    -> Nothing

instance serialize (PAIR a b) | serialize a & serialize b
where
	write (PAIR x y) c = writeP x [" ":writeP y c]
	read r = case readP r of
		Just (x,[" ":r]) -> case readP r of
			Nothing    -> Nothing
			Just (y,r) -> Just (PAIR x y, r)
		_ -> Nothing

instance serialize (CONS a) | serialize a
where
	write e=:(CONS s x) c
	| needsParens e = ["(":s:" ":write x [")":c]]
	| otherwise     = [s:c]
	read ["(":s:" ":r] = case read r of
		Just (x,[")":r]) -> Just (CONS s x,r)
		_                -> Nothing
	read [s:r] = case read r of
		Just (x,r) -> let e = CONS s x in if (needsParens e) Nothing (Just (e,r))
		Nothing    -> Nothing
	read _ = Nothing

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

fromList :: [a] -> ListG a
fromList []     = LEFT (CONS "_Nil" UNIT)
fromList [x:xs] = RIGHT (CONS "_Cons" (PAIR x xs))

toList :: (ListG a) -> [a]
toList (LEFT _)                     = []
toList (RIGHT (CONS _ (PAIR x xs))) = [x:xs]

instance serialize [a] | serialize a
where
	write l c = write (fromList l) c
	read l = case read l of
		Just (g,r) -> Just (toList g,r)
		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 x r) = RIGHT (CONS "Bin" (PAIR l (PAIR x r)))

toBin :: (BinG a) -> Bin a
toBin (LEFT _)                             = Leaf
toBin (RIGHT (CONS _ (PAIR l (PAIR x r)))) = Bin l x r

instance serialize (Bin a) | serialize a
where
	write a c = write (fromBin a) c
	read l = case read l of
		Just (g,r) -> Just (toBin g,r)
		Nothing    -> Nothing

instance == (Bin a) | == a where // better use the generic approach
	(==) Leaf Leaf = True
	(==) (Bin l a r) (Bin k b s) = l == k && a == b && r == s
	(==) _ _ = False

// ---

/**
 * Reflection:
 * The following is parsed as Just ([], []), which shows that the fact that
 * there is no check on the name of the constructor can be exploited.
 *
 * In the actual Clean implementation, there is the construct `CONS of d` where
 * d :: GenericConsDescriptor. This way, the name, arity, etc. of the
 * constructor are available as part of the CONS type (even though this type
 * does not explicitly contain the information). It is essentially a very
 * restricted form of dependent typing, which makes it possible to distinguish
 * the _Nil-CONS and the _Cons-CONS at compile-time.
 *
 * This requires the `CONS of d` construct, so I don't think this exploit is
 * fixable in the current setup. It would of course be possible to redefine
 * toList and toBin to result in a Maybe and check on the constructor there.
 */
Start :: Maybe ([Int], [String])
Start = read ["_Cons"]

Start = 
	[ test True
	, test False
	, test 0
	, test 123
	, test -36
	, test [42]
	, test [0..4]
	, test [[True],[]]
	, 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 :: a -> ([String],[String]) | serialize, == a
test a = 
	(if (isJust r)
		(if (fst jr == a)
			(if (isEmpty (tl (snd jr)))
				["Oke "]
				["Fail: not all input is consumed! ":snd jr])
			["Fail: Wrong result ":write (fst jr) []])
		["Fail: read result is Nothing "]
	, ["write produces ": s]
	)
	where
		s = write a ["\n"]
		r = read s
		jr = fromJust r