Mercurial > urweb

comparison src/elab_util.sml @ 76:522f4bd3955e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Broaden unification context
author Adam Chlipala <adamc@hcoop.net>
date Sun, 29 Jun 2008 10:39:43 -0400
parents 6431b315a1e3
children b4f2a258e52c
comparison
equal deleted inserted replaced
75:88ffb3d61817 76:522f4bd3955e
56 fn k' => 56 fn k' =>
57 (KRecord k', loc)) 57 (KRecord k', loc))
58 58
59 | KError => S.return2 kAll 59 | KError => S.return2 kAll
60 60
61 | KUnif (_, ref (SOME k)) => mfk' k 61 | KUnif (_, _, ref (SOME k)) => mfk' k
62 | KUnif _ => S.return2 kAll 62 | KUnif _ => S.return2 kAll
63 in 63 in
64 mfk 64 mfk
65 end 65 end
66 66
149 S.map2 (mfk k2, 149 S.map2 (mfk k2,
150 fn k2' => 150 fn k2' =>
151 (CFold (k1', k2'), loc))) 151 (CFold (k1', k2'), loc)))
152 152
153 | CError => S.return2 cAll 153 | CError => S.return2 cAll
154 | CUnif (_, _, ref (SOME c)) => mfc' ctx c 154 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
155 | CUnif _ => S.return2 cAll 155 | CUnif _ => S.return2 cAll
156 in 156 in
157 mfc 157 mfc
158 end 158 end
159 159
415 S.Return () => raise Fail "Elab_util.Sgn.map" 415 S.Return () => raise Fail "Elab_util.Sgn.map"
416 | S.Continue (s, ()) => s 416 | S.Continue (s, ()) => s
417 417
418 end 418 end
419 419
420 structure Decl = struct
421
422 datatype binder =
423 RelC of string * Elab.kind
424 | NamedC of string * Elab.kind
425 | RelE of string * Elab.con
426 | NamedE of string * Elab.con
427 | Str of string * Elab.sgn
428 | Sgn of string * Elab.sgn
429
430 fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
431 let
432 val mfk = Kind.mapfold fk
433
434 fun bind' (ctx, b) =
435 let
436 val b' = case b of
437 Con.Rel x => RelC x
438 | Con.Named x => NamedC x
439 in
440 bind (ctx, b')
441 end
442 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
443
444 fun bind' (ctx, b) =
445 let
446 val b' = case b of
447 Exp.RelC x => RelC x
448 | Exp.NamedC x => NamedC x
449 | Exp.RelE x => RelE x
450 | Exp.NamedE x => NamedE x
451 in
452 bind (ctx, b')
453 end
454 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'}
455
456 fun bind' (ctx, b) =
457 let
458 val b' = case b of
459 Sgn.RelC x => RelC x
460 | Sgn.NamedC x => NamedC x
461 | Sgn.Sgn x => Sgn x
462 | Sgn.Str x => Str x
463 in
464 bind (ctx, b')
465 end
466 val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'}
467
468 fun mfst ctx str acc =
469 S.bindP (mfst' ctx str acc, fst ctx)
470
471 and mfst' ctx (strAll as (str, loc)) =
472 case str of
473 StrConst ds =>
474 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
475 (case #1 d of
476 DCon (x, _, k, _) =>
477 bind (ctx, NamedC (x, k))
478 | DVal (x, _, c, _) =>
479 bind (ctx, NamedE (x, c))
480 | DSgn (x, _, sgn) =>
481 bind (ctx, Sgn (x, sgn))
482 | DStr (x, _, sgn, _) =>
483 bind (ctx, Str (x, sgn))
484 | DFfiStr (x, _, sgn) =>
485 bind (ctx, Str (x, sgn)),
486 mfd ctx d)) ctx ds,
487 fn ds' => (StrConst ds', loc))
488 | StrVar _ => S.return2 strAll
489 | StrProj (str, x) =>
490 S.map2 (mfst ctx str,
491 fn str' =>
492 (StrProj (str', x), loc))
493 | StrFun (x, n, sgn1, sgn2, str) =>
494 S.bind2 (mfsg ctx sgn1,
495 fn sgn1' =>
496 S.bind2 (mfsg ctx sgn2,
497 fn sgn2' =>
498 S.map2 (mfst ctx str,
499 fn str' =>
500 (StrFun (x, n, sgn1', sgn2', str'), loc))))
501 | StrApp (str1, str2) =>
502 S.bind2 (mfst ctx str1,
503 fn str1' =>
504 S.map2 (mfst ctx str2,
505 fn str2' =>
506 (StrApp (str1', str2'), loc)))
507 | StrError => S.return2 strAll
508
509 and mfd ctx d acc =
510 S.bindP (mfd' ctx d acc, fd ctx)
511
512 and mfd' ctx (dAll as (d, loc)) =
513 case d of
514 DCon (x, n, k, c) =>
515 S.bind2 (mfk k,
516 fn k' =>
517 S.map2 (mfc ctx c,
518 fn c' =>
519 (DCon (x, n, k', c'), loc)))
520 | DVal (x, n, c, e) =>
521 S.bind2 (mfc ctx c,
522 fn c' =>
523 S.map2 (mfe ctx e,
524 fn e' =>
525 (DVal (x, n, c', e'), loc)))
526 | DSgn (x, n, sgn) =>
527 S.map2 (mfsg ctx sgn,
528 fn sgn' =>
529 (DSgn (x, n, sgn'), loc))
530 | DStr (x, n, sgn, str) =>
531 S.bind2 (mfsg ctx sgn,
532 fn sgn' =>
533 S.map2 (mfst ctx str,
534 fn str' =>
535 (DStr (x, n, sgn', str'), loc)))
536 | DFfiStr (x, n, sgn) =>
537 S.map2 (mfsg ctx sgn,
538 fn sgn' =>
539 (DFfiStr (x, n, sgn'), loc))
540 in
541 mfd
542 end
543
544 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
545 mapfoldB {kind = kind,
546 con = fn () => con,
547 exp = fn () => exp,
548 sgn_item = fn () => sgn_item,
549 sgn = fn () => sgn,
550 str = fn () => str,
551 decl = fn () => decl,
552 bind = fn ((), _) => ()} ()
553
554 fun exists {kind, con, exp, sgn_item, sgn, str, decl} k =
555 case mapfold {kind = fn k => fn () =>
556 if kind k then
557 S.Return ()
558 else
559 S.Continue (k, ()),
560 con = fn c => fn () =>
561 if con c then
562 S.Return ()
563 else
564 S.Continue (c, ()),
565 exp = fn e => fn () =>
566 if exp e then
567 S.Return ()
568 else
569 S.Continue (e, ()),
570 sgn_item = fn sgi => fn () =>
571 if sgn_item sgi then
572 S.Return ()
573 else
574 S.Continue (sgi, ()),
575 sgn = fn x => fn () =>
576 if sgn x then
577 S.Return ()
578 else
579 S.Continue (x, ()),
580 str = fn x => fn () =>
581 if str x then
582 S.Return ()
583 else
584 S.Continue (x, ()),
585 decl = fn x => fn () =>
586 if decl x then
587 S.Return ()
588 else
589 S.Continue (x, ())} k () of
590 S.Return _ => true
591 | S.Continue _ => false
592
593 fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
594 case mapfold {kind = fn x => fn () =>
595 case kind x of
596 NONE => S.Continue (x, ())
597 | SOME v => S.Return v,
598
599 con = fn x => fn () =>
600 case con x of
601 NONE => S.Continue (x, ())
602 | SOME v => S.Return v,
603
604 exp = fn x => fn () =>
605 case exp x of
606 NONE => S.Continue (x, ())
607 | SOME v => S.Return v,
608
609 sgn_item = fn x => fn () =>
610 case sgn_item x of
611 NONE => S.Continue (x, ())
612 | SOME v => S.Return v,
613
614 sgn = fn x => fn () =>
615 case sgn x of
616 NONE => S.Continue (x, ())
617 | SOME v => S.Return v,
618
619 str = fn x => fn () =>
620 case str x of
621 NONE => S.Continue (x, ())
622 | SOME v => S.Return v,
623
624 decl = fn x => fn () =>
625 case decl x of
626 NONE => S.Continue (x, ())
627 | SOME v => S.Return v
628
629 } k () of
630 S.Return x => SOME x
631 | S.Continue _ => NONE
632
420 end 633 end
634
635 end