comparison src/core_util.sml @ 214:766b5475477f

Corifying con-tuples
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 15:03:05 -0400
parents ab86aa858e6c
children 5c50b17f5e4a
comparison
equal deleted inserted replaced
213:0343557355fc 214:766b5475477f
52 | (KRecord k1, KRecord k2) => compare (k1, k2) 52 | (KRecord k1, KRecord k2) => compare (k1, k2)
53 | (KRecord _, _) => LESS 53 | (KRecord _, _) => LESS
54 | (_, KRecord _) => GREATER 54 | (_, KRecord _) => GREATER
55 55
56 | (KUnit, KUnit) => EQUAL 56 | (KUnit, KUnit) => EQUAL
57 | (KUnit, _) => LESS
58 | (_, KUnit) => GREATER
59
60 | (KTuple ks1, KTuple ks2) => joinL compare (ks1, ks2)
57 61
58 fun mapfold f = 62 fun mapfold f =
59 let 63 let
60 fun mfk k acc = 64 fun mfk k acc =
61 S.bindP (mfk' k acc, f) 65 S.bindP (mfk' k acc, f)
77 S.map2 (mfk k, 81 S.map2 (mfk k,
78 fn k' => 82 fn k' =>
79 (KRecord k', loc)) 83 (KRecord k', loc))
80 84
81 | KUnit => S.return2 kAll 85 | KUnit => S.return2 kAll
86
87 | KTuple ks =>
88 S.map2 (ListUtil.mapfold mfk ks,
89 fn ks' =>
90 (KTuple ks', loc))
82 in 91 in
83 mfk 92 mfk
84 end 93 end
85 94
86 fun map f k = 95 fun map f k =
168 fn () => Kind.compare (r1, r2)) 177 fn () => Kind.compare (r1, r2))
169 | (CFold _, _) => LESS 178 | (CFold _, _) => LESS
170 | (_, CFold _) => GREATER 179 | (_, CFold _) => GREATER
171 180
172 | (CUnit, CUnit) => EQUAL 181 | (CUnit, CUnit) => EQUAL
182 | (CUnit, _) => LESS
183 | (_, CUnit) => GREATER
184
185 | (CTuple cs1, CTuple cs2) => joinL compare (cs1, cs2)
186 | (CTuple _, _) => LESS
187 | (_, CTuple _) => GREATER
188
189 | (CProj (c1, n1), CProj (c2, n2)) => join (Int.compare (n1, n2),
190 fn () => compare (c1, c2))
173 191
174 datatype binder = 192 datatype binder =
175 Rel of string * kind 193 Rel of string * kind
176 | Named of string * int * kind * con option 194 | Named of string * int * kind * con option
177 195
243 S.map2 (mfk k2, 261 S.map2 (mfk k2,
244 fn k2' => 262 fn k2' =>
245 (CFold (k1', k2'), loc))) 263 (CFold (k1', k2'), loc)))
246 264
247 | CUnit => S.return2 cAll 265 | CUnit => S.return2 cAll
266
267 | CTuple cs =>
268 S.map2 (ListUtil.mapfold (mfc ctx) cs,
269 fn cs' =>
270 (CTuple cs', loc))
271
272 | CProj (c, n) =>
273 S.map2 (mfc ctx c,
274 fn c' =>
275 (CProj (c', n), loc))
248 in 276 in
249 mfc 277 mfc
250 end 278 end
251 279
252 fun mapfold {kind = fk, con = fc} = 280 fun mapfold {kind = fk, con = fc} =