Mercurial > urweb

comparison src/elab_util.sml @ 623:588b9d16b00a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 8998114760c1
children 12b73f3c108e
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
41 41
42 structure S = Search 42 structure S = Search
43 43
44 structure Kind = struct 44 structure Kind = struct
45 45
46 fun mapfold f = 46 fun mapfoldB {kind, bind} =
47 let 47 let
48 fun mfk k acc = 48 fun mfk ctx k acc =
49 S.bindP (mfk' k acc, f) 49 S.bindP (mfk' ctx k acc, kind ctx)
50 50
51 and mfk' (kAll as (k, loc)) = 51 and mfk' ctx (kAll as (k, loc)) =
52 case k of 52 case k of
53 KType => S.return2 kAll 53 KType => S.return2 kAll
54 54
55 | KArrow (k1, k2) => 55 | KArrow (k1, k2) =>
56 S.bind2 (mfk k1, 56 S.bind2 (mfk ctx k1,
57 fn k1' => 57 fn k1' =>
58 S.map2 (mfk k2, 58 S.map2 (mfk ctx k2,
59 fn k2' => 59 fn k2' =>
60 (KArrow (k1', k2'), loc))) 60 (KArrow (k1', k2'), loc)))
61 61
62 | KName => S.return2 kAll 62 | KName => S.return2 kAll
63 63
64 | KRecord k => 64 | KRecord k =>
65 S.map2 (mfk k, 65 S.map2 (mfk ctx k,
66 fn k' => 66 fn k' =>
67 (KRecord k', loc)) 67 (KRecord k', loc))
68 68
69 | KUnit => S.return2 kAll 69 | KUnit => S.return2 kAll
70 70
71 | KTuple ks => 71 | KTuple ks =>
72 S.map2 (ListUtil.mapfold mfk ks, 72 S.map2 (ListUtil.mapfold (mfk ctx) ks,
73 fn ks' => 73 fn ks' =>
74 (KTuple ks', loc)) 74 (KTuple ks', loc))
75 75
76 | KError => S.return2 kAll 76 | KError => S.return2 kAll
77 77
78 | KUnif (_, _, ref (SOME k)) => mfk' k 78 | KUnif (_, _, ref (SOME k)) => mfk' ctx k
79 | KUnif _ => S.return2 kAll 79 | KUnif _ => S.return2 kAll
80
81 | KRel _ => S.return2 kAll
82 | KFun (x, k) =>
83 S.map2 (mfk (bind (ctx, x)) k,
84 fn k' =>
85 (KFun (x, k'), loc))
80 in 86 in
81 mfk 87 mfk
82 end 88 end
89
90 fun mapfold fk =
91 mapfoldB {kind = fn () => fk,
92 bind = fn ((), _) => ()} ()
93
94 fun mapB {kind, bind} ctx k =
95 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
96 bind = bind} ctx k () of
97 S.Continue (k, ()) => k
98 | S.Return _ => raise Fail "ElabUtil.Kind.mapB: Impossible"
83 99
84 fun exists f k = 100 fun exists f k =
85 case mapfold (fn k => fn () => 101 case mapfold (fn k => fn () =>
86 if f k then 102 if f k then
87 S.Return () 103 S.Return ()
93 end 109 end
94 110
95 structure Con = struct 111 structure Con = struct
96 112
97 datatype binder = 113 datatype binder =
98 Rel of string * Elab.kind 114 RelK of string
99 | Named of string * int * Elab.kind 115 | RelC of string * Elab.kind
116 | NamedC of string * int * Elab.kind
100 117
101 fun mapfoldB {kind = fk, con = fc, bind} = 118 fun mapfoldB {kind = fk, con = fc, bind} =
102 let 119 let
103 val mfk = Kind.mapfold fk 120 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, s) => bind (ctx, RelK s)}
104 121
105 fun mfc ctx c acc = 122 fun mfc ctx c acc =
106 S.bindP (mfc' ctx c acc, fc ctx) 123 S.bindP (mfc' ctx c acc, fc ctx)
107 124
108 and mfc' ctx (cAll as (c, loc)) = 125 and mfc' ctx (cAll as (c, loc)) =
112 fn c1' => 129 fn c1' =>
113 S.map2 (mfc ctx c2, 130 S.map2 (mfc ctx c2,
114 fn c2' => 131 fn c2' =>
115 (TFun (c1', c2'), loc))) 132 (TFun (c1', c2'), loc)))
116 | TCFun (e, x, k, c) => 133 | TCFun (e, x, k, c) =>
117 S.bind2 (mfk k, 134 S.bind2 (mfk ctx k,
118 fn k' => 135 fn k' =>
119 S.map2 (mfc (bind (ctx, Rel (x, k))) c, 136 S.map2 (mfc (bind (ctx, RelC (x, k))) c,
120 fn c' => 137 fn c' =>
121 (TCFun (e, x, k', c'), loc))) 138 (TCFun (e, x, k', c'), loc)))
122 | CDisjoint (ai, c1, c2, c3) => 139 | CDisjoint (ai, c1, c2, c3) =>
123 S.bind2 (mfc ctx c1, 140 S.bind2 (mfc ctx c1,
124 fn c1' => 141 fn c1' =>
140 fn c1' => 157 fn c1' =>
141 S.map2 (mfc ctx c2, 158 S.map2 (mfc ctx c2,
142 fn c2' => 159 fn c2' =>
143 (CApp (c1', c2'), loc))) 160 (CApp (c1', c2'), loc)))
144 | CAbs (x, k, c) => 161 | CAbs (x, k, c) =>
145 S.bind2 (mfk k, 162 S.bind2 (mfk ctx k,
146 fn k' => 163 fn k' =>
147 S.map2 (mfc (bind (ctx, Rel (x, k))) c, 164 S.map2 (mfc (bind (ctx, RelC (x, k))) c,
148 fn c' => 165 fn c' =>
149 (CAbs (x, k', c'), loc))) 166 (CAbs (x, k', c'), loc)))
150 167
151 | CName _ => S.return2 cAll 168 | CName _ => S.return2 cAll
152 169
153 | CRecord (k, xcs) => 170 | CRecord (k, xcs) =>
154 S.bind2 (mfk k, 171 S.bind2 (mfk ctx k,
155 fn k' => 172 fn k' =>
156 S.map2 (ListUtil.mapfold (fn (x, c) => 173 S.map2 (ListUtil.mapfold (fn (x, c) =>
157 S.bind2 (mfc ctx x, 174 S.bind2 (mfc ctx x,
158 fn x' => 175 fn x' =>
159 S.map2 (mfc ctx c, 176 S.map2 (mfc ctx c,
167 fn c1' => 184 fn c1' =>
168 S.map2 (mfc ctx c2, 185 S.map2 (mfc ctx c2,
169 fn c2' => 186 fn c2' =>
170 (CConcat (c1', c2'), loc))) 187 (CConcat (c1', c2'), loc)))
171 | CMap (k1, k2) => 188 | CMap (k1, k2) =>
172 S.bind2 (mfk k1, 189 S.bind2 (mfk ctx k1,
173 fn k1' => 190 fn k1' =>
174 S.map2 (mfk k2, 191 S.map2 (mfk ctx k2,
175 fn k2' => 192 fn k2' =>
176 (CMap (k1', k2'), loc))) 193 (CMap (k1', k2'), loc)))
177 194
178 | CUnit => S.return2 cAll 195 | CUnit => S.return2 cAll
179 196
188 (CProj (c', n), loc)) 205 (CProj (c', n), loc))
189 206
190 | CError => S.return2 cAll 207 | CError => S.return2 cAll
191 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c 208 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
192 | CUnif _ => S.return2 cAll 209 | CUnif _ => S.return2 cAll
210
211 | CKAbs (x, c) =>
212 S.map2 (mfc (bind (ctx, RelK x)) c,
213 fn c' =>
214 (CKAbs (x, c'), loc))
215 | CKApp (c, k) =>
216 S.bind2 (mfc ctx c,
217 fn c' =>
218 S.map2 (mfk ctx k,
219 fn k' =>
220 (CKApp (c', k'), loc)))
221 | TKFun (x, c) =>
222 S.map2 (mfc (bind (ctx, RelK x)) c,
223 fn c' =>
224 (TKFun (x, c'), loc))
193 in 225 in
194 mfc 226 mfc
195 end 227 end
196 228
197 fun mapfold {kind = fk, con = fc} = 229 fun mapfold {kind = fk, con = fc} =
198 mapfoldB {kind = fk, 230 mapfoldB {kind = fn () => fk,
199 con = fn () => fc, 231 con = fn () => fc,
200 bind = fn ((), _) => ()} () 232 bind = fn ((), _) => ()} ()
201 233
202 fun mapB {kind, con, bind} ctx c = 234 fun mapB {kind, con, bind} ctx c =
203 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), 235 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
204 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), 236 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
205 bind = bind} ctx c () of 237 bind = bind} ctx c () of
206 S.Continue (c, ()) => c 238 S.Continue (c, ()) => c
207 | S.Return _ => raise Fail "ElabUtil.Con.mapB: Impossible" 239 | S.Return _ => raise Fail "ElabUtil.Con.mapB: Impossible"
208 240
225 S.Continue (c, ())} k () of 257 S.Continue (c, ())} k () of
226 S.Return _ => true 258 S.Return _ => true
227 | S.Continue _ => false 259 | S.Continue _ => false
228 260
229 fun foldB {kind, con, bind} ctx st c = 261 fun foldB {kind, con, bind} ctx st c =
230 case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)), 262 case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
231 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)), 263 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
232 bind = bind} ctx c st of 264 bind = bind} ctx c st of
233 S.Continue (_, st) => st 265 S.Continue (_, st) => st
234 | S.Return _ => raise Fail "ElabUtil.Con.foldB: Impossible" 266 | S.Return _ => raise Fail "ElabUtil.Con.foldB: Impossible"
235 267
236 end 268 end
237 269
238 structure Exp = struct 270 structure Exp = struct
239 271
240 datatype binder = 272 datatype binder =
241 RelC of string * Elab.kind 273 RelK of string
274 | RelC of string * Elab.kind
242 | NamedC of string * int * Elab.kind 275 | NamedC of string * int * Elab.kind
243 | RelE of string * Elab.con 276 | RelE of string * Elab.con
244 | NamedE of string * Elab.con 277 | NamedE of string * Elab.con
245 278
246 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = 279 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
247 let 280 let
248 val mfk = Kind.mapfold fk 281 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
249 282
250 fun bind' (ctx, b) = 283 fun bind' (ctx, b) =
251 let 284 let
252 val b' = case b of 285 val b' = case b of
253 Con.Rel x => RelC x 286 Con.RelK x => RelK x
254 | Con.Named x => NamedC x 287 | Con.RelC x => RelC x
288 | Con.NamedC x => NamedC x
255 in 289 in
256 bind (ctx, b') 290 bind (ctx, b')
257 end 291 end
258 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} 292 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
259 293
286 fn e' => 320 fn e' =>
287 S.map2 (mfc ctx c, 321 S.map2 (mfc ctx c,
288 fn c' => 322 fn c' =>
289 (ECApp (e', c'), loc))) 323 (ECApp (e', c'), loc)))
290 | ECAbs (expl, x, k, e) => 324 | ECAbs (expl, x, k, e) =>
291 S.bind2 (mfk k, 325 S.bind2 (mfk ctx k,
292 fn k' => 326 fn k' =>
293 S.map2 (mfe (bind (ctx, RelC (x, k))) e, 327 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
294 fn e' => 328 fn e' =>
295 (ECAbs (expl, x, k', e'), loc))) 329 (ECAbs (expl, x, k', e'), loc)))
296 330
345 fn c' => 379 fn c' =>
346 S.map2 (mfc ctx rest, 380 S.map2 (mfc ctx rest,
347 fn rest' => 381 fn rest' =>
348 (ECutMulti (e', c', {rest = rest'}), loc)))) 382 (ECutMulti (e', c', {rest = rest'}), loc))))
349 383
350 | EFold k =>
351 S.map2 (mfk k,
352 fn k' =>
353 (EFold k', loc))
354
355 | ECase (e, pes, {disc, result}) => 384 | ECase (e, pes, {disc, result}) =>
356 S.bind2 (mfe ctx e, 385 S.bind2 (mfe ctx e,
357 fn e' => 386 fn e' =>
358 S.bind2 (ListUtil.mapfold (fn (p, e) => 387 S.bind2 (ListUtil.mapfold (fn (p, e) =>
359 let 388 let
404 S.map2 (mfe ctx e, 433 S.map2 (mfe ctx e,
405 fn e' => 434 fn e' =>
406 (ELet (des', e'), loc))) 435 (ELet (des', e'), loc)))
407 end 436 end
408 437
438 | EKAbs (x, e) =>
439 S.map2 (mfe (bind (ctx, RelK x)) e,
440 fn e' =>
441 (EKAbs (x, e'), loc))
442 | EKApp (e, k) =>
443 S.bind2 (mfe ctx e,
444 fn e' =>
445 S.map2 (mfk ctx k,
446 fn k' =>
447 (EKApp (e', k'), loc)))
448
409 and mfed ctx (dAll as (d, loc)) = 449 and mfed ctx (dAll as (d, loc)) =
410 case d of 450 case d of
411 EDVal vi => 451 EDVal vi =>
412 S.map2 (mfvi ctx vi, 452 S.map2 (mfvi ctx vi,
413 fn vi' => 453 fn vi' =>
430 in 470 in
431 mfe 471 mfe
432 end 472 end
433 473
434 fun mapfold {kind = fk, con = fc, exp = fe} = 474 fun mapfold {kind = fk, con = fc, exp = fe} =
435 mapfoldB {kind = fk, 475 mapfoldB {kind = fn () => fk,
436 con = fn () => fc, 476 con = fn () => fc,
437 exp = fn () => fe, 477 exp = fn () => fe,
438 bind = fn ((), _) => ()} () 478 bind = fn ((), _) => ()} ()
439 479
440 fun exists {kind, con, exp} k = 480 fun exists {kind, con, exp} k =
455 S.Continue (e, ())} k () of 495 S.Continue (e, ())} k () of
456 S.Return _ => true 496 S.Return _ => true
457 | S.Continue _ => false 497 | S.Continue _ => false
458 498
459 fun mapB {kind, con, exp, bind} ctx e = 499 fun mapB {kind, con, exp, bind} ctx e =
460 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), 500 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
461 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), 501 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
462 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), 502 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
463 bind = bind} ctx e () of 503 bind = bind} ctx e () of
464 S.Continue (e, ()) => e 504 S.Continue (e, ()) => e
465 | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible" 505 | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
466 506
467 fun foldB {kind, con, exp, bind} ctx st e = 507 fun foldB {kind, con, exp, bind} ctx st e =
468 case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)), 508 case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
469 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)), 509 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
470 exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)), 510 exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)),
471 bind = bind} ctx e st of 511 bind = bind} ctx e st of
472 S.Continue (_, st) => st 512 S.Continue (_, st) => st
473 | S.Return _ => raise Fail "ElabUtil.Exp.foldB: Impossible" 513 | S.Return _ => raise Fail "ElabUtil.Exp.foldB: Impossible"
475 end 515 end
476 516
477 structure Sgn = struct 517 structure Sgn = struct
478 518
479 datatype binder = 519 datatype binder =
480 RelC of string * Elab.kind 520 RelK of string
521 | RelC of string * Elab.kind
481 | NamedC of string * int * Elab.kind 522 | NamedC of string * int * Elab.kind
482 | Str of string * Elab.sgn 523 | Str of string * Elab.sgn
483 | Sgn of string * Elab.sgn 524 | Sgn of string * Elab.sgn
484 525
485 fun mapfoldB {kind, con, sgn_item, sgn, bind} = 526 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
486 let 527 let
487 fun bind' (ctx, b) = 528 fun bind' (ctx, b) =
488 let 529 let
489 val b' = case b of 530 val b' = case b of
490 Con.Rel x => RelC x 531 Con.RelK x => RelK x
491 | Con.Named x => NamedC x 532 | Con.RelC x => RelC x
533 | Con.NamedC x => NamedC x
492 in 534 in
493 bind (ctx, b') 535 bind (ctx, b')
494 end 536 end
495 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'} 537 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
496 538
497 val kind = Kind.mapfold kind 539 val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)}
498 540
499 fun sgi ctx si acc = 541 fun sgi ctx si acc =
500 S.bindP (sgi' ctx si acc, sgn_item ctx) 542 S.bindP (sgi' ctx si acc, sgn_item ctx)
501 543
502 and sgi' ctx (siAll as (si, loc)) = 544 and sgi' ctx (siAll as (si, loc)) =
503 case si of 545 case si of
504 SgiConAbs (x, n, k) => 546 SgiConAbs (x, n, k) =>
505 S.map2 (kind k, 547 S.map2 (kind ctx k,
506 fn k' => 548 fn k' =>
507 (SgiConAbs (x, n, k'), loc)) 549 (SgiConAbs (x, n, k'), loc))
508 | SgiCon (x, n, k, c) => 550 | SgiCon (x, n, k, c) =>
509 S.bind2 (kind k, 551 S.bind2 (kind ctx k,
510 fn k' => 552 fn k' =>
511 S.map2 (con ctx c, 553 S.map2 (con ctx c,
512 fn c' => 554 fn c' =>
513 (SgiCon (x, n, k', c'), loc))) 555 (SgiCon (x, n, k', c'), loc)))
514 | SgiDatatype (x, n, xs, xncs) => 556 | SgiDatatype (x, n, xs, xncs) =>
546 fn c1' => 588 fn c1' =>
547 S.map2 (con ctx c2, 589 S.map2 (con ctx c2,
548 fn c2' => 590 fn c2' =>
549 (SgiConstraint (c1', c2'), loc))) 591 (SgiConstraint (c1', c2'), loc)))
550 | SgiClassAbs (x, n, k) => 592 | SgiClassAbs (x, n, k) =>
551 S.map2 (kind k, 593 S.map2 (kind ctx k,
552 fn k' => 594 fn k' =>
553 (SgiClassAbs (x, n, k'), loc)) 595 (SgiClassAbs (x, n, k'), loc))
554 | SgiClass (x, n, k, c) => 596 | SgiClass (x, n, k, c) =>
555 S.bind2 (kind k, 597 S.bind2 (kind ctx k,
556 fn k' => 598 fn k' =>
557 S.map2 (con ctx c, 599 S.map2 (con ctx c,
558 fn c' => 600 fn c' =>
559 (SgiClass (x, n, k', c'), loc))) 601 (SgiClass (x, n, k', c'), loc)))
560 602
606 in 648 in
607 sg 649 sg
608 end 650 end
609 651
610 fun mapfold {kind, con, sgn_item, sgn} = 652 fun mapfold {kind, con, sgn_item, sgn} =
611 mapfoldB {kind = kind, 653 mapfoldB {kind = fn () => kind,
612 con = fn () => con, 654 con = fn () => con,
613 sgn_item = fn () => sgn_item, 655 sgn_item = fn () => sgn_item,
614 sgn = fn () => sgn, 656 sgn = fn () => sgn,
615 bind = fn ((), _) => ()} () 657 bind = fn ((), _) => ()} ()
616 658
625 end 667 end
626 668
627 structure Decl = struct 669 structure Decl = struct
628 670
629 datatype binder = 671 datatype binder =
630 RelC of string * Elab.kind 672 RelK of string
673 | RelC of string * Elab.kind
631 | NamedC of string * int * Elab.kind 674 | NamedC of string * int * Elab.kind
632 | RelE of string * Elab.con 675 | RelE of string * Elab.con
633 | NamedE of string * Elab.con 676 | NamedE of string * Elab.con
634 | Str of string * Elab.sgn 677 | Str of string * Elab.sgn
635 | Sgn of string * Elab.sgn 678 | Sgn of string * Elab.sgn
636 679
637 fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} = 680 fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
638 let 681 let
639 val mfk = Kind.mapfold fk 682 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
640 683
641 fun bind' (ctx, b) = 684 fun bind' (ctx, b) =
642 let 685 let
643 val b' = case b of 686 val b' = case b of
644 Con.Rel x => RelC x 687 Con.RelK x => RelK x
645 | Con.Named x => NamedC x 688 | Con.RelC x => RelC x
689 | Con.NamedC x => NamedC x
646 in 690 in
647 bind (ctx, b') 691 bind (ctx, b')
648 end 692 end
649 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} 693 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
650 694
651 fun bind' (ctx, b) = 695 fun bind' (ctx, b) =
652 let 696 let
653 val b' = case b of 697 val b' = case b of
654 Exp.RelC x => RelC x 698 Exp.RelK x => RelK x
699 | Exp.RelC x => RelC x
655 | Exp.NamedC x => NamedC x 700 | Exp.NamedC x => NamedC x
656 | Exp.RelE x => RelE x 701 | Exp.RelE x => RelE x
657 | Exp.NamedE x => NamedE x 702 | Exp.NamedE x => NamedE x
658 in 703 in
659 bind (ctx, b') 704 bind (ctx, b')
661 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'} 706 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'}
662 707
663 fun bind' (ctx, b) = 708 fun bind' (ctx, b) =
664 let 709 let
665 val b' = case b of 710 val b' = case b of
666 Sgn.RelC x => RelC x 711 Sgn.RelK x => RelK x
712 | Sgn.RelC x => RelC x
667 | Sgn.NamedC x => NamedC x 713 | Sgn.NamedC x => NamedC x
668 | Sgn.Sgn x => Sgn x 714 | Sgn.Sgn x => Sgn x
669 | Sgn.Str x => Str x 715 | Sgn.Str x => Str x
670 in 716 in
671 bind (ctx, b') 717 bind (ctx, b')
758 S.bindP (mfd' ctx d acc, fd ctx) 804 S.bindP (mfd' ctx d acc, fd ctx)
759 805
760 and mfd' ctx (dAll as (d, loc)) = 806 and mfd' ctx (dAll as (d, loc)) =
761 case d of 807 case d of
762 DCon (x, n, k, c) => 808 DCon (x, n, k, c) =>
763 S.bind2 (mfk k, 809 S.bind2 (mfk ctx k,
764 fn k' => 810 fn k' =>
765 S.map2 (mfc ctx c, 811 S.map2 (mfc ctx c,
766 fn c' => 812 fn c' =>
767 (DCon (x, n, k', c'), loc))) 813 (DCon (x, n, k', c'), loc)))
768 | DDatatype (x, n, xs, xncs) => 814 | DDatatype (x, n, xs, xncs) =>
823 fn c' => 869 fn c' =>
824 (DTable (tn, x, n, c'), loc)) 870 (DTable (tn, x, n, c'), loc))
825 | DSequence _ => S.return2 dAll 871 | DSequence _ => S.return2 dAll
826 872
827 | DClass (x, n, k, c) => 873 | DClass (x, n, k, c) =>
828 S.bind2 (mfk k, 874 S.bind2 (mfk ctx k,
829 fn k' => 875 fn k' =>
830 S.map2 (mfc ctx c, 876 S.map2 (mfc ctx c,
831 fn c' => 877 fn c' =>
832 (DClass (x, n, k', c'), loc))) 878 (DClass (x, n, k', c'), loc)))
833 879
847 in 893 in
848 mfd 894 mfd
849 end 895 end
850 896
851 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} = 897 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
852 mapfoldB {kind = kind, 898 mapfoldB {kind = fn () => kind,
853 con = fn () => con, 899 con = fn () => con,
854 exp = fn () => exp, 900 exp = fn () => exp,
855 sgn_item = fn () => sgn_item, 901 sgn_item = fn () => sgn_item,
856 sgn = fn () => sgn, 902 sgn = fn () => sgn,
857 str = fn () => str, 903 str = fn () => str,
936 } k () of 982 } k () of
937 S.Return x => SOME x 983 S.Return x => SOME x
938 | S.Continue _ => NONE 984 | S.Continue _ => NONE
939 985
940 fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d = 986 fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d =
941 case mapfoldB {kind = fn x => fn st => S.Continue (kind (x, st)), 987 case mapfoldB {kind = fn ctx => fn x => fn st => S.Continue (kind (ctx, x, st)),
942 con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)), 988 con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)),
943 exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)), 989 exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)),
944 sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)), 990 sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)),
945 sgn = fn ctx => fn x => fn st => S.Continue (sgn (ctx, x, st)), 991 sgn = fn ctx => fn x => fn st => S.Continue (sgn (ctx, x, st)),
946 str = fn ctx => fn x => fn st => S.Continue (str (ctx, x, st)), 992 str = fn ctx => fn x => fn st => S.Continue (str (ctx, x, st)),