Mercurial > urweb

comparison src/elab_env.sml @ 675:43430b7190f4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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,