Mercurial > urweb

comparison src/core_util.sml @ 193:8a70e2919e86

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Specialization of single-parameter datatypes
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 17:55:51 -0400
parents 9bbf4d383381
children 890a61991263
comparison
equal deleted inserted replaced
192:9bbf4d383381 193:8a70e2919e86
37 37
38 structure S = Search 38 structure S = Search
39 39
40 structure Kind = struct 40 structure Kind = struct
41 41
42 open Order
43
44 fun compare ((k1, _), (k2, _)) =
45 case (k1, k2) of
46 (KType, KType) => EQUAL
47 | (KType, _) => LESS
48 | (_, KType) => GREATER
49
50 | (KArrow (d1, r1), KArrow (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2))
51 | (KArrow _, _) => LESS
52 | (_, KArrow _) => GREATER
53
54 | (KName, KName) => EQUAL
55 | (KName, _) => LESS
56 | (_, KName) => GREATER
57
58 | (KRecord k1, KRecord k2) => compare (k1, k2)
59 | (KRecord _, _) => LESS
60 | (_, KRecord _) => GREATER
61
62 | (KUnit, KUnit) => EQUAL
63
42 fun mapfold f = 64 fun mapfold f =
43 let 65 let
44 fun mfk k acc = 66 fun mfk k acc =
45 S.bindP (mfk' k acc, f) 67 S.bindP (mfk' k acc, f)
46 68
82 | S.Continue _ => false 104 | S.Continue _ => false
83 105
84 end 106 end
85 107
86 structure Con = struct 108 structure Con = struct
109
110 open Order
111
112 fun compare ((c1, _), (c2, _)) =
113 case (c1, c2) of
114 (TFun (d1, r1), TFun (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2))
115 | (TFun _, _) => LESS
116 | (_, TFun _) => GREATER
117
118 | (TCFun (x1, k1, r1), TCFun (x2, k2, r2)) =>
119 join (String.compare (x1, x2),
120 fn () => join (Kind.compare (k1, k2),
121 fn () => compare (r1, r2)))
122 | (TCFun _, _) => LESS
123 | (_, TCFun _) => GREATER
124
125 | (TRecord c1, TRecord c2) => compare (c1, c2)
126 | (TRecord _, _) => LESS
127 | (_, TRecord _) => GREATER
128
129 | (CRel n1, CRel n2) => Int.compare (n1, n2)
130 | (CRel _, _) => LESS
131 | (_, CRel _) => GREATER
132
133 | (CNamed n1, CNamed n2) => Int.compare (n1, n2)
134 | (CNamed _, _) => LESS
135 | (_, CNamed _) => GREATER
136
137 | (CFfi (m1, s1), CFfi (m2, s2)) => join (String.compare (m1, m2),
138 fn () => String.compare (s1, s2))
139 | (CFfi _, _) => LESS
140 | (_, CFfi _) => GREATER
141
142 | (CApp (f1, x1), CApp (f2, x2)) => join (compare (f1, f2),
143 fn () => compare (x1, x2))
144 | (CApp _, _) => LESS
145 | (_, CApp _) => GREATER
146
147 | (CAbs (x1, k1, b1), CAbs (x2, k2, b2)) =>
148 join (String.compare (x1, x2),
149 fn () => join (Kind.compare (k1, k2),
150 fn () => compare (b1, b2)))
151 | (CAbs _, _) => LESS
152 | (_, CAbs _) => GREATER
153
154 | (CName s1, CName s2) => String.compare (s1, s2)
155 | (CName _, _) => LESS
156 | (_, CName _) => GREATER
157
158 | (CRecord (k1, xvs1), CRecord (k2, xvs2)) =>
159 join (Kind.compare (k1, k2),
160 fn () => joinL (fn ((x1, v1), (x2, v2)) =>
161 join (compare (x1, x2),
162 fn () => compare (v1, v2))) (xvs1, xvs2))
163 | (CRecord _, _) => LESS
164 | (_, CRecord _) => GREATER
165
166 | (CConcat (f1, s1), CConcat (f2, s2)) =>
167 join (compare (f1, f2),
168 fn () => compare (s1, s2))
169 | (CConcat _, _) => LESS
170 | (_, CConcat _) => GREATER
171
172 | (CFold (d1, r1), CFold (d2, r2)) =>
173 join (Kind.compare (d1, r2),
174 fn () => Kind.compare (r1, r2))
175 | (CFold _, _) => LESS
176 | (_, CFold _) => GREATER
177
178 | (CUnit, CUnit) => EQUAL
87 179
88 datatype binder = 180 datatype binder =
89 Rel of string * kind 181 Rel of string * kind
90 | Named of string * int * kind * con option 182 | Named of string * int * kind * con option
91 183
198 S.Return () 290 S.Return ()
199 else 291 else
200 S.Continue (c, ())} k () of 292 S.Continue (c, ())} k () of
201 S.Return _ => true 293 S.Return _ => true
202 | S.Continue _ => false 294 | S.Continue _ => false
295
296 fun foldMap {kind, con} s c =
297 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
298 con = fn c => fn s => S.Continue (con (c, s))} c s of
299 S.Continue v => v
300 | S.Return _ => raise Fail "CoreUtil.Con.foldMap: Impossible"
203 301
204 end 302 end
205 303
206 structure Exp = struct 304 structure Exp = struct
207 305
315 413
316 | ECase (e, pes, {disc, result}) => 414 | ECase (e, pes, {disc, result}) =>
317 S.bind2 (mfe ctx e, 415 S.bind2 (mfe ctx e,
318 fn e' => 416 fn e' =>
319 S.bind2 (ListUtil.mapfold (fn (p, e) => 417 S.bind2 (ListUtil.mapfold (fn (p, e) =>
320 S.map2 (mfe ctx e, 418 let
321 fn e' => (p, e'))) pes, 419 fun pb ((p, _), ctx) =
420 case p of
421 PWild => ctx
422 | PVar (x, t) => bind (ctx, RelE (x, t))
423 | PPrim _ => ctx
424 | PCon (_, _, _, NONE) => ctx
425 | PCon (_, _, _, SOME p) => pb (p, ctx)
426 | PRecord xps => foldl (fn ((_, p, _), ctx) =>
427 pb (p, ctx)) ctx xps
428 in
429 S.bind2 (mfp ctx p,
430 fn p' =>
431 S.map2 (mfe (pb (p', ctx)) e,
432 fn e' => (p', e')))
433 end) pes,
322 fn pes' => 434 fn pes' =>
323 S.bind2 (mfc ctx disc, 435 S.bind2 (mfc ctx disc,
324 fn disc' => 436 fn disc' =>
325 S.map2 (mfc ctx result, 437 S.map2 (mfc ctx result,
326 fn result' => 438 fn result' =>
333 445
334 | EClosure (n, es) => 446 | EClosure (n, es) =>
335 S.map2 (ListUtil.mapfold (mfe ctx) es, 447 S.map2 (ListUtil.mapfold (mfe ctx) es,
336 fn es' => 448 fn es' =>
337 (EClosure (n, es'), loc)) 449 (EClosure (n, es'), loc))
450
451 and mfp ctx (pAll as (p, loc)) =
452 case p of
453 PWild => S.return2 pAll
454 | PVar (x, t) =>
455 S.map2 (mfc ctx t,
456 fn t' =>
457 (PVar (x, t'), loc))
458 | PPrim _ => S.return2 pAll
459 | PCon (dk, pc, args, po) =>
460 S.bind2 (mfpc ctx pc,
461 fn pc' =>
462 S.bind2 (ListUtil.mapfold (mfc ctx) args,
463 fn args' =>
464 S.map2 ((case po of
465 NONE => S.return2 NONE
466 | SOME p => S.map2 (mfp ctx p, SOME)),
467 fn po' =>
468 (PCon (dk, pc', args', po'), loc))))
469 | PRecord xps =>
470 S.map2 (ListUtil.mapfold (fn (x, p, c) =>
471 S.bind2 (mfp ctx p,
472 fn p' =>
473 S.map2 (mfc ctx c,
474 fn c' =>
475 (x, p', c')))) xps,
476 fn xps' =>
477 (PRecord xps', loc))
478
479 and mfpc ctx pc =
480 case pc of
481 PConVar _ => S.return2 pc
482 | PConFfi {mod = m, datatyp, params, con, arg, kind} =>
483 S.map2 ((case arg of
484 NONE => S.return2 NONE
485 | SOME c => S.map2 (mfc ctx c, SOME)),
486 fn arg' =>
487 PConFfi {mod = m, datatyp = datatyp, params = params,
488 con = con, arg = arg', kind = kind})
338 in 489 in
339 mfe 490 mfe
340 end 491 end
341 492
342 fun mapfold {kind = fk, con = fc, exp = fe} = 493 fun mapfold {kind = fk, con = fc, exp = fe} =