Mercurial > urweb
comparison src/elab_env.sml @ 675:43430b7190f4
Type class inclusions
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 26 Mar 2009 15:13:36 -0400 |
parents | fab5998b840e |
children | 81573f62d6c3 |
comparison
equal
deleted
inserted
replaced
674:fab5998b840e | 675:43430b7190f4 |
---|---|
231 fn () => compare' (k1, k2)) | 231 fn () => compare' (k1, k2)) |
232 end | 232 end |
233 | 233 |
234 structure KM = BinaryMapFn(KK) | 234 structure KM = BinaryMapFn(KK) |
235 | 235 |
236 type class = ((class_name * class_key) list * exp) KM.map | 236 type class = {ground : ((class_name * class_key) list * exp) KM.map, |
237 val empty_class = KM.empty | 237 inclusions : exp CM.map} |
238 val empty_class = {ground = KM.empty, | |
239 inclusions = CM.empty} | |
238 | 240 |
239 fun printClasses cs = (print "Classes:\n"; | 241 fun printClasses cs = (print "Classes:\n"; |
240 CM.appi (fn (cn, km) => | 242 CM.appi (fn (cn, {ground = km, ...} : class) => |
241 (print (cn2s cn ^ ":"); | 243 (print (cn2s cn ^ ":"); |
242 KM.appi (fn (ck, _) => print (" " ^ ckn2s ck)) km; | 244 KM.appi (fn (ck, _) => print (" " ^ ckn2s ck)) km; |
243 print "\n")) cs) | 245 print "\n")) cs) |
244 | 246 |
245 type env = { | 247 type env = { |
359 | 361 |
360 datatypes = #datatypes env, | 362 datatypes = #datatypes env, |
361 constructors = #constructors env, | 363 constructors = #constructors env, |
362 | 364 |
363 classes = CM.map (fn class => | 365 classes = CM.map (fn class => |
364 KM.foldli (fn (ck, e, km) => | 366 {ground = KM.foldli (fn (ck, e, km) => |
365 KM.insert (km, liftClassKey ck, e)) | 367 KM.insert (km, liftClassKey ck, e)) |
366 KM.empty class) | 368 KM.empty (#ground class), |
369 inclusions = #inclusions class}) | |
367 (#classes env), | 370 (#classes env), |
368 | 371 |
369 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c) | 372 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c) |
370 | Named' (n, c) => Named' (n, c)) (#renameE env), | 373 | Named' (n, c) => Named' (n, c)) (#renameE env), |
371 relE = map (fn (x, c) => (x, lift c)) (#relE env), | 374 relE = map (fn (x, c) => (x, lift c)) (#relE env), |
480 namedC = #namedC env, | 483 namedC = #namedC env, |
481 | 484 |
482 datatypes = #datatypes env, | 485 datatypes = #datatypes env, |
483 constructors = #constructors env, | 486 constructors = #constructors env, |
484 | 487 |
485 classes = CM.insert (#classes env, ClNamed n, KM.empty), | 488 classes = CM.insert (#classes env, ClNamed n, empty_class), |
486 | 489 |
487 renameE = #renameE env, | 490 renameE = #renameE env, |
488 relE = #relE env, | 491 relE = #relE env, |
489 namedE = #namedE env, | 492 namedE = #namedE env, |
490 | 493 |
563 case CM.find (#classes env, f) of | 566 case CM.find (#classes env, f) of |
564 NONE => NONE | 567 NONE => NONE |
565 | SOME class => | 568 | SOME class => |
566 let | 569 let |
567 val loc = #2 c | 570 val loc = #2 c |
568 | 571 |
572 fun tryIncs () = | |
573 let | |
574 fun tryIncs fs = | |
575 case fs of | |
576 [] => NONE | |
577 | (f', e') :: fs => | |
578 case doPair (f', x) of | |
579 NONE => tryIncs fs | |
580 | SOME e => | |
581 let | |
582 val e' = (ECApp (e', class_key_out loc x), loc) | |
583 val e' = (EApp (e', e), loc) | |
584 in | |
585 SOME e' | |
586 end | |
587 in | |
588 tryIncs (CM.listItemsi (#inclusions class)) | |
589 end | |
590 | |
569 fun tryRules (k, args) = | 591 fun tryRules (k, args) = |
570 let | 592 let |
571 val len = length args | 593 val len = length args |
594 | |
595 fun tryNext () = | |
596 case k of | |
597 CkApp (k1, k2) => tryRules (k1, k2 :: args) | |
598 | _ => tryIncs () | |
572 in | 599 in |
573 case KM.find (class, (k, length args)) of | 600 case KM.find (#ground class, (k, length args)) of |
574 SOME (cs, e) => | 601 SOME (cs, e) => |
575 let | 602 let |
576 val es = map (fn (cn, ck) => | 603 val es = map (fn (cn, ck) => |
577 let | 604 let |
578 val ck = ListUtil.foldli (fn (i, arg, ck) => | 605 val ck = ListUtil.foldli (fn (i, arg, ck) => |
583 in | 610 in |
584 doPair (cn, ck) | 611 doPair (cn, ck) |
585 end) cs | 612 end) cs |
586 in | 613 in |
587 if List.exists (not o Option.isSome) es then | 614 if List.exists (not o Option.isSome) es then |
588 NONE | 615 tryNext () |
589 else | 616 else |
590 let | 617 let |
591 val e = foldl (fn (arg, e) => (ECApp (e, class_key_out loc arg), loc)) | 618 val e = foldl (fn (arg, e) => (ECApp (e, class_key_out loc arg), loc)) |
592 e args | 619 e args |
593 val e = foldr (fn (pf, e) => (EApp (e, pf), loc)) | 620 val e = foldr (fn (pf, e) => (EApp (e, pf), loc)) |
594 e (List.mapPartial (fn x => x) es) | 621 e (List.mapPartial (fn x => x) es) |
595 in | 622 in |
596 SOME e | 623 SOME e |
597 end | 624 end |
598 end | 625 end |
599 | NONE => | 626 | NONE => tryNext () |
600 case k of | |
601 CkApp (k1, k2) => tryRules (k1, k2 :: args) | |
602 | _ => NONE | |
603 end | 627 end |
604 in | 628 in |
605 tryRules (x, []) | 629 tryRules (x, []) |
606 end | 630 end |
607 in | 631 in |
613 fun pushERel (env : env) x t = | 637 fun pushERel (env : env) x t = |
614 let | 638 let |
615 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) | 639 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) |
616 | x => x) (#renameE env) | 640 | x => x) (#renameE env) |
617 | 641 |
618 val classes = CM.map (KM.map (fn (ps, e) => (ps, liftExp e))) (#classes env) | 642 val classes = CM.map (fn class => |
643 {ground = KM.map (fn (ps, e) => (ps, liftExp e)) (#ground class), | |
644 inclusions = #inclusions class}) (#classes env) | |
619 val classes = case class_pair_in t of | 645 val classes = case class_pair_in t of |
620 NONE => classes | 646 NONE => classes |
621 | SOME (f, x) => | 647 | SOME (f, x) => |
622 case CM.find (classes, f) of | 648 case CM.find (classes, f) of |
623 NONE => classes | 649 NONE => classes |
624 | SOME class => | 650 | SOME class => |
625 let | 651 let |
626 val class = KM.insert (class, (x, 0), ([], (ERel 0, #2 t))) | 652 val class = {ground = KM.insert (#ground class, (x, 0), ([], (ERel 0, #2 t))), |
653 inclusions = #inclusions class} | |
627 in | 654 in |
628 CM.insert (classes, f, class) | 655 CM.insert (classes, f, class) |
629 end | 656 end |
630 in | 657 in |
631 {renameK = #renameK env, | 658 {renameK = #renameK env, |
652 end | 679 end |
653 | 680 |
654 fun lookupERel (env : env) n = | 681 fun lookupERel (env : env) n = |
655 (List.nth (#relE env, n)) | 682 (List.nth (#relE env, n)) |
656 handle Subscript => raise UnboundRel n | 683 handle Subscript => raise UnboundRel n |
684 | |
685 datatype rule = | |
686 Normal of int * (class_name * class_key) list * class_key | |
687 | Inclusion of class_name | |
657 | 688 |
658 fun rule_in c = | 689 fun rule_in c = |
659 let | 690 let |
660 fun quantifiers (c, nvars) = | 691 fun quantifiers (c, nvars) = |
661 case #1 c of | 692 case #1 c of |
673 NONE => NONE | 704 NONE => NONE |
674 | SOME (cn, ck) => | 705 | SOME (cn, ck) => |
675 let | 706 let |
676 fun dearg (ck, i) = | 707 fun dearg (ck, i) = |
677 if i >= nvars then | 708 if i >= nvars then |
678 SOME (nvars, hyps, (cn, ck)) | 709 SOME (cn, Normal (nvars, hyps, ck)) |
679 else case ck of | 710 else case ck of |
680 CkApp (ck, CkRel i') => | 711 CkApp (ck, CkRel i') => |
681 if i' = i then | 712 if i' = i then |
682 dearg (ck, i + 1) | 713 dearg (ck, i + 1) |
683 else | 714 else |
688 end | 719 end |
689 in | 720 in |
690 clauses (c, []) | 721 clauses (c, []) |
691 end | 722 end |
692 in | 723 in |
693 quantifiers (c, 0) | 724 case #1 c of |
725 TCFun (_, _, _, (TFun ((CApp (f1, (CRel 0, _)), _), | |
726 (CApp (f2, (CRel 0, _)), _)), _)) => | |
727 (case (class_name_in f1, class_name_in f2) of | |
728 (SOME f1, SOME f2) => SOME (f2, Inclusion f1) | |
729 | _ => NONE) | |
730 | _ => quantifiers (c, 0) | |
694 end | 731 end |
695 | 732 |
696 fun pushENamedAs (env : env) x n t = | 733 fun pushENamedAs (env : env) x n t = |
697 let | 734 let |
698 val classes = #classes env | 735 val classes = #classes env |
699 val classes = case rule_in t of | 736 val classes = case rule_in t of |
700 NONE => classes | 737 NONE => classes |
701 | SOME (nvars, hyps, (f, x)) => | 738 | SOME (f, rule) => |
702 case CM.find (classes, f) of | 739 case CM.find (classes, f) of |
703 NONE => classes | 740 NONE => classes |
704 | SOME class => | 741 | SOME class => |
705 let | 742 let |
706 val class = KM.insert (class, (x, nvars), (hyps, (ENamed n, #2 t))) | 743 val e = (ENamed n, #2 t) |
744 | |
745 val class = | |
746 case rule of | |
747 Normal (nvars, hyps, x) => | |
748 {ground = KM.insert (#ground class, (x, nvars), (hyps, e)), | |
749 inclusions = #inclusions class} | |
750 | Inclusion f' => | |
751 {ground = #ground class, | |
752 inclusions = CM.insert (#inclusions class, f', e)} | |
707 in | 753 in |
708 CM.insert (classes, f, class) | 754 CM.insert (classes, f, class) |
709 end | 755 end |
710 in | 756 in |
711 {renameK = #renameK env, | 757 {renameK = #renameK env, |
1021 | SgiClassAbs (x, n, _) => found (x, n) | 1067 | SgiClassAbs (x, n, _) => found (x, n) |
1022 | SgiClass (x, n, _, _) => found (x, n) | 1068 | SgiClass (x, n, _, _) => found (x, n) |
1023 | SgiVal (x, n, c) => | 1069 | SgiVal (x, n, c) => |
1024 (case rule_in c of | 1070 (case rule_in c of |
1025 NONE => default () | 1071 NONE => default () |
1026 | SOME (nvars, hyps, (cn, a)) => | 1072 | SOME (cn, rule) => |
1027 let | 1073 let |
1074 val globalizeN = sgnS_class_name (m1, ms, fmap) | |
1028 val globalize = sgnS_class_key (m1, ms, fmap) | 1075 val globalize = sgnS_class_key (m1, ms, fmap) |
1029 val ck = globalize a | |
1030 val hyps = map (fn (n, k) => (sgnS_class_name (m1, ms, fmap) n, | |
1031 globalize k)) hyps | |
1032 | 1076 |
1033 fun unravel c = | 1077 fun unravel c = |
1034 case c of | 1078 case c of |
1035 ClNamed n => | 1079 ClNamed n => |
1036 ((case lookupCNamed env n of | 1080 ((case lookupCNamed env n of |
1053 val classes = | 1097 val classes = |
1054 case CM.find (classes, cn) of | 1098 case CM.find (classes, cn) of |
1055 NONE => classes | 1099 NONE => classes |
1056 | SOME class => | 1100 | SOME class => |
1057 let | 1101 let |
1058 val class = KM.insert (class, (ck, nvars), | 1102 val e = (EModProj (m1, ms, x), |
1059 (hyps, | 1103 #2 sgn) |
1060 (EModProj (m1, ms, x), | 1104 |
1061 #2 sgn))) | 1105 val class = |
1106 case rule of | |
1107 Normal (nvars, hyps, a) => | |
1108 {ground = | |
1109 KM.insert (#ground class, (globalize a, nvars), | |
1110 (map (fn (n, k) => | |
1111 (globalizeN n, | |
1112 globalize k)) hyps, e)), | |
1113 inclusions = #inclusions class} | |
1114 | Inclusion f' => | |
1115 {ground = #ground class, | |
1116 inclusions = CM.insert (#inclusions class, | |
1117 globalizeN f', e)} | |
1062 in | 1118 in |
1063 CM.insert (classes, cn, class) | 1119 CM.insert (classes, cn, class) |
1064 end | 1120 end |
1065 in | 1121 in |
1066 (classes, | 1122 (classes, |
1075 val classes = | 1131 val classes = |
1076 case CM.find (classes, cn) of | 1132 case CM.find (classes, cn) of |
1077 NONE => classes | 1133 NONE => classes |
1078 | SOME class => | 1134 | SOME class => |
1079 let | 1135 let |
1080 val class = KM.insert (class, (ck, nvars), | 1136 val e = (EModProj (m1, ms, x), #2 sgn) |
1081 (hyps, | 1137 |
1082 (EModProj (m1, ms, x), #2 sgn))) | 1138 val class = |
1139 case rule of | |
1140 Normal (nvars, hyps, a) => | |
1141 {ground = | |
1142 KM.insert (#ground class, (globalize a, nvars), | |
1143 (map (fn (n, k) => | |
1144 (globalizeN n, | |
1145 globalize k)) hyps, e)), | |
1146 inclusions = #inclusions class} | |
1147 | Inclusion f' => | |
1148 {ground = #ground class, | |
1149 inclusions = CM.insert (#inclusions class, | |
1150 globalizeN f', e)} | |
1083 in | 1151 in |
1084 CM.insert (classes, cn, class) | 1152 CM.insert (classes, cn, class) |
1085 end | 1153 end |
1086 in | 1154 in |
1087 (classes, | 1155 (classes, |