Mercurial > urweb
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} = |