Mercurial > urweb
comparison src/elab_env.sml @ 674:fab5998b840e
Type class reductions, but no inclusions yet
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 26 Mar 2009 14:37:31 -0400 |
parents | 588b9d16b00a |
children | 43430b7190f4 |
comparison
equal
deleted
inserted
replaced
673:a8effb6159c2 | 674:fab5998b840e |
---|---|
1 (* Copyright (c) 2008, Adam Chlipala | 1 (* Copyright (c) 2008-2009, Adam Chlipala |
2 * All rights reserved. | 2 * All rights reserved. |
3 * | 3 * |
4 * Redistribution and use in source and binary forms, with or without | 4 * Redistribution and use in source and binary forms, with or without |
5 * modification, are permitted provided that the following conditions are met: | 5 * modification, are permitted provided that the following conditions are met: |
6 * | 6 * |
195 CkNamed n => "Named(" ^ Int.toString n ^ ")" | 195 CkNamed n => "Named(" ^ Int.toString n ^ ")" |
196 | CkRel n => "Rel(" ^ Int.toString n ^ ")" | 196 | CkRel n => "Rel(" ^ Int.toString n ^ ")" |
197 | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" | 197 | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" |
198 | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")" | 198 | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")" |
199 | 199 |
200 type class_key_n = class_key * int | |
201 | |
202 fun ckn2s (ck, n) = ck2s ck ^ "[" ^ Int.toString n ^ "]" | |
203 | |
200 fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")" | 204 fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")" |
201 | 205 |
202 structure KK = struct | 206 structure KK = struct |
203 type ord_key = class_key | 207 type ord_key = class_key_n |
204 open Order | 208 open Order |
205 fun compare x = | 209 fun compare' x = |
206 case x of | 210 case x of |
207 (CkNamed n1, CkNamed n2) => Int.compare (n1, n2) | 211 (CkNamed n1, CkNamed n2) => Int.compare (n1, n2) |
208 | (CkNamed _, _) => LESS | 212 | (CkNamed _, _) => LESS |
209 | (_, CkNamed _) => GREATER | 213 | (_, CkNamed _) => GREATER |
210 | 214 |
218 fn () => String.compare (x1, x2))) | 222 fn () => String.compare (x1, x2))) |
219 | (CkProj _, _) => LESS | 223 | (CkProj _, _) => LESS |
220 | (_, CkProj _) => GREATER | 224 | (_, CkProj _) => GREATER |
221 | 225 |
222 | (CkApp (f1, x1), CkApp (f2, x2)) => | 226 | (CkApp (f1, x1), CkApp (f2, x2)) => |
223 join (compare (f1, f2), | 227 join (compare' (f1, f2), |
224 fn () => compare (x1, x2)) | 228 fn () => compare' (x1, x2)) |
229 fun compare ((k1, n1), (k2, n2)) = | |
230 join (Int.compare (n1, n2), | |
231 fn () => compare' (k1, k2)) | |
225 end | 232 end |
226 | 233 |
227 structure KM = BinaryMapFn(KK) | 234 structure KM = BinaryMapFn(KK) |
228 | 235 |
229 type class = { | 236 type class = ((class_name * class_key) list * exp) KM.map |
230 ground : exp KM.map | 237 val empty_class = KM.empty |
231 } | |
232 | |
233 val empty_class = { | |
234 ground = KM.empty | |
235 } | |
236 | 238 |
237 fun printClasses cs = (print "Classes:\n"; | 239 fun printClasses cs = (print "Classes:\n"; |
238 CM.appi (fn (cn, {ground = km}) => | 240 CM.appi (fn (cn, km) => |
239 (print (cn2s cn ^ ":"); | 241 (print (cn2s cn ^ ":"); |
240 KM.appi (fn (ck, _) => print (" " ^ ck2s ck)) km; | 242 KM.appi (fn (ck, _) => print (" " ^ ckn2s ck)) km; |
241 print "\n")) cs) | 243 print "\n")) cs) |
242 | 244 |
243 type env = { | 245 type env = { |
244 renameK : int SM.map, | 246 renameK : int SM.map, |
245 relK : string list, | 247 relK : string list, |
296 | 298 |
297 renameStr = SM.empty, | 299 renameStr = SM.empty, |
298 str = IM.empty | 300 str = IM.empty |
299 } | 301 } |
300 | 302 |
301 fun liftClassKey ck = | 303 fun liftClassKey' ck = |
302 case ck of | 304 case ck of |
303 CkNamed _ => ck | 305 CkNamed _ => ck |
304 | CkRel n => CkRel (n + 1) | 306 | CkRel n => CkRel (n + 1) |
305 | CkProj _ => ck | 307 | CkProj _ => ck |
306 | CkApp (ck1, ck2) => CkApp (liftClassKey ck1, liftClassKey ck2) | 308 | CkApp (ck1, ck2) => CkApp (liftClassKey' ck1, liftClassKey' ck2) |
309 | |
310 fun liftClassKey (ck, n) = (liftClassKey' ck, n) | |
307 | 311 |
308 fun pushKRel (env : env) x = | 312 fun pushKRel (env : env) x = |
309 let | 313 let |
310 val renameK = SM.map (fn n => n+1) (#renameK env) | 314 val renameK = SM.map (fn n => n+1) (#renameK env) |
311 in | 315 in |
354 namedC = #namedC env, | 358 namedC = #namedC env, |
355 | 359 |
356 datatypes = #datatypes env, | 360 datatypes = #datatypes env, |
357 constructors = #constructors env, | 361 constructors = #constructors env, |
358 | 362 |
359 classes = CM.map (fn class => { | 363 classes = CM.map (fn class => |
360 ground = KM.foldli (fn (ck, e, km) => | 364 KM.foldli (fn (ck, e, km) => |
361 KM.insert (km, liftClassKey ck, e)) | 365 KM.insert (km, liftClassKey ck, e)) |
362 KM.empty (#ground class) | 366 KM.empty class) |
363 }) | |
364 (#classes env), | 367 (#classes env), |
365 | 368 |
366 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c) | 369 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c) |
367 | Named' (n, c) => Named' (n, c)) (#renameE env), | 370 | Named' (n, c) => Named' (n, c)) (#renameE env), |
368 relE = map (fn (x, c) => (x, lift c)) (#relE env), | 371 relE = map (fn (x, c) => (x, lift c)) (#relE env), |
477 namedC = #namedC env, | 480 namedC = #namedC env, |
478 | 481 |
479 datatypes = #datatypes env, | 482 datatypes = #datatypes env, |
480 constructors = #constructors env, | 483 constructors = #constructors env, |
481 | 484 |
482 classes = CM.insert (#classes env, ClNamed n, {ground = KM.empty}), | 485 classes = CM.insert (#classes env, ClNamed n, KM.empty), |
483 | 486 |
484 renameE = #renameE env, | 487 renameE = #renameE env, |
485 relE = #relE env, | 488 relE = #relE env, |
486 namedE = #namedE env, | 489 namedE = #namedE env, |
487 | 490 |
516 (case (class_key_in c1, class_key_in c2) of | 519 (case (class_key_in c1, class_key_in c2) of |
517 (SOME k1, SOME k2) => SOME (CkApp (k1, k2)) | 520 (SOME k1, SOME k2) => SOME (CkApp (k1, k2)) |
518 | _ => NONE) | 521 | _ => NONE) |
519 | _ => NONE | 522 | _ => NONE |
520 | 523 |
524 fun class_key_out loc = | |
525 let | |
526 fun cko k = | |
527 case k of | |
528 CkRel n => (CRel n, loc) | |
529 | CkNamed n => (CNamed n, loc) | |
530 | CkProj x => (CModProj x, loc) | |
531 | CkApp (k1, k2) => (CApp (cko k1, cko k2), loc) | |
532 in | |
533 cko | |
534 end | |
535 | |
521 fun class_pair_in (c, _) = | 536 fun class_pair_in (c, _) = |
522 case c of | 537 case c of |
523 CApp (f, x) => | 538 CApp (f, x) => |
524 (case (class_name_in f, class_key_in x) of | 539 (case (class_name_in f, class_key_in x) of |
525 (SOME f, SOME x) => SOME (f, x) | 540 (SOME f, SOME x) => SOME (f, x) |
526 | _ => NONE) | 541 | _ => NONE) |
527 | CUnif (_, _, _, ref (SOME c)) => class_pair_in c | 542 | CUnif (_, _, _, ref (SOME c)) => class_pair_in c |
528 | _ => NONE | 543 | _ => NONE |
529 | 544 |
545 fun sub_class_key (n, c) = | |
546 let | |
547 fun csk k = | |
548 case k of | |
549 CkRel n' => if n' = n then | |
550 c | |
551 else | |
552 k | |
553 | CkNamed _ => k | |
554 | CkProj _ => k | |
555 | CkApp (k1, k2) => CkApp (csk k1, csk k2) | |
556 in | |
557 csk | |
558 end | |
559 | |
530 fun resolveClass (env : env) c = | 560 fun resolveClass (env : env) c = |
531 case class_pair_in c of | 561 let |
532 SOME (f, x) => | 562 fun doPair (f, x) = |
533 (case CM.find (#classes env, f) of | 563 case CM.find (#classes env, f) of |
534 NONE => NONE | 564 NONE => NONE |
535 | SOME class => | 565 | SOME class => |
536 case KM.find (#ground class, x) of | 566 let |
537 NONE => NONE | 567 val loc = #2 c |
538 | SOME e => SOME e) | 568 |
539 | _ => NONE | 569 fun tryRules (k, args) = |
570 let | |
571 val len = length args | |
572 in | |
573 case KM.find (class, (k, length args)) of | |
574 SOME (cs, e) => | |
575 let | |
576 val es = map (fn (cn, ck) => | |
577 let | |
578 val ck = ListUtil.foldli (fn (i, arg, ck) => | |
579 sub_class_key (len - i - 1, | |
580 arg) | |
581 ck) | |
582 ck args | |
583 in | |
584 doPair (cn, ck) | |
585 end) cs | |
586 in | |
587 if List.exists (not o Option.isSome) es then | |
588 NONE | |
589 else | |
590 let | |
591 val e = foldl (fn (arg, e) => (ECApp (e, class_key_out loc arg), loc)) | |
592 e args | |
593 val e = foldr (fn (pf, e) => (EApp (e, pf), loc)) | |
594 e (List.mapPartial (fn x => x) es) | |
595 in | |
596 SOME e | |
597 end | |
598 end | |
599 | NONE => | |
600 case k of | |
601 CkApp (k1, k2) => tryRules (k1, k2 :: args) | |
602 | _ => NONE | |
603 end | |
604 in | |
605 tryRules (x, []) | |
606 end | |
607 in | |
608 case class_pair_in c of | |
609 SOME p => doPair p | |
610 | _ => NONE | |
611 end | |
540 | 612 |
541 fun pushERel (env : env) x t = | 613 fun pushERel (env : env) x t = |
542 let | 614 let |
543 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) | 615 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) |
544 | x => x) (#renameE env) | 616 | x => x) (#renameE env) |
545 | 617 |
546 val classes = CM.map (fn class => { | 618 val classes = CM.map (KM.map (fn (ps, e) => (ps, liftExp e))) (#classes env) |
547 ground = KM.map liftExp (#ground class) | |
548 }) (#classes env) | |
549 val classes = case class_pair_in t of | 619 val classes = case class_pair_in t of |
550 NONE => classes | 620 NONE => classes |
551 | SOME (f, x) => | 621 | SOME (f, x) => |
552 case CM.find (classes, f) of | 622 case CM.find (classes, f) of |
553 NONE => classes | 623 NONE => classes |
554 | SOME class => | 624 | SOME class => |
555 let | 625 let |
556 val class = { | 626 val class = KM.insert (class, (x, 0), ([], (ERel 0, #2 t))) |
557 ground = KM.insert (#ground class, x, (ERel 0, #2 t)) | |
558 } | |
559 in | 627 in |
560 CM.insert (classes, f, class) | 628 CM.insert (classes, f, class) |
561 end | 629 end |
562 in | 630 in |
563 {renameK = #renameK env, | 631 {renameK = #renameK env, |
585 | 653 |
586 fun lookupERel (env : env) n = | 654 fun lookupERel (env : env) n = |
587 (List.nth (#relE env, n)) | 655 (List.nth (#relE env, n)) |
588 handle Subscript => raise UnboundRel n | 656 handle Subscript => raise UnboundRel n |
589 | 657 |
658 fun rule_in c = | |
659 let | |
660 fun quantifiers (c, nvars) = | |
661 case #1 c of | |
662 TCFun (_, _, _, c) => quantifiers (c, nvars + 1) | |
663 | _ => | |
664 let | |
665 fun clauses (c, hyps) = | |
666 case #1 c of | |
667 TFun (hyp, c) => | |
668 (case class_pair_in hyp of | |
669 NONE => NONE | |
670 | SOME p => clauses (c, p :: hyps)) | |
671 | _ => | |
672 case class_pair_in c of | |
673 NONE => NONE | |
674 | SOME (cn, ck) => | |
675 let | |
676 fun dearg (ck, i) = | |
677 if i >= nvars then | |
678 SOME (nvars, hyps, (cn, ck)) | |
679 else case ck of | |
680 CkApp (ck, CkRel i') => | |
681 if i' = i then | |
682 dearg (ck, i + 1) | |
683 else | |
684 NONE | |
685 | _ => NONE | |
686 in | |
687 dearg (ck, 0) | |
688 end | |
689 in | |
690 clauses (c, []) | |
691 end | |
692 in | |
693 quantifiers (c, 0) | |
694 end | |
695 | |
590 fun pushENamedAs (env : env) x n t = | 696 fun pushENamedAs (env : env) x n t = |
591 let | 697 let |
592 val classes = #classes env | 698 val classes = #classes env |
593 val classes = case class_pair_in t of | 699 val classes = case rule_in t of |
594 NONE => classes | 700 NONE => classes |
595 | SOME (f, x) => | 701 | SOME (nvars, hyps, (f, x)) => |
596 case CM.find (classes, f) of | 702 case CM.find (classes, f) of |
597 NONE => classes | 703 NONE => classes |
598 | SOME class => | 704 | SOME class => |
599 let | 705 let |
600 val class = { | 706 val class = KM.insert (class, (x, nvars), (hyps, (ENamed n, #2 t))) |
601 ground = KM.insert (#ground class, x, (ENamed n, #2 t)) | |
602 } | |
603 in | 707 in |
604 CM.insert (classes, f, class) | 708 CM.insert (classes, f, class) |
605 end | 709 end |
606 in | 710 in |
607 {renameK = #renameK env, | 711 {renameK = #renameK env, |
781 NONE => c | 885 NONE => c |
782 | SOME nx => CModProj (m1, ms', nx)) | 886 | SOME nx => CModProj (m1, ms', nx)) |
783 | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1), | 887 | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1), |
784 (sgnS_con' arg (#1 c2), #2 c2)) | 888 (sgnS_con' arg (#1 c2), #2 c2)) |
785 | _ => c | 889 | _ => c |
890 | |
891 fun sgnS_class_name (arg as (m1, ms', (sgns, strs, cons))) nm = | |
892 case nm of | |
893 ClProj (m1, ms, x) => | |
894 (case IM.find (strs, m1) of | |
895 NONE => nm | |
896 | SOME m1x => ClProj (m1, ms' @ m1x :: ms, x)) | |
897 | ClNamed n => | |
898 (case IM.find (cons, n) of | |
899 NONE => nm | |
900 | SOME nx => ClProj (m1, ms', nx)) | |
901 | |
902 fun sgnS_class_key (arg as (m1, ms', (sgns, strs, cons))) k = | |
903 case k of | |
904 CkProj (m1, ms, x) => | |
905 (case IM.find (strs, m1) of | |
906 NONE => k | |
907 | SOME m1x => CkProj (m1, ms' @ m1x :: ms, x)) | |
908 | CkNamed n => | |
909 (case IM.find (cons, n) of | |
910 NONE => k | |
911 | SOME nx => CkProj (m1, ms', nx)) | |
912 | CkApp (k1, k2) => CkApp (sgnS_class_key arg k1, | |
913 sgnS_class_key arg k2) | |
914 | _ => k | |
786 | 915 |
787 fun sgnS_sgn (str, (sgns, strs, cons)) sgn = | 916 fun sgnS_sgn (str, (sgns, strs, cons)) sgn = |
788 case sgn of | 917 case sgn of |
789 SgnProj (m1, ms, x) => | 918 SgnProj (m1, ms, x) => |
790 (case IM.find (strs, m1) of | 919 (case IM.find (strs, m1) of |
889 fmap, | 1018 fmap, |
890 pushSgnNamedAs env x n sgn) | 1019 pushSgnNamedAs env x n sgn) |
891 | 1020 |
892 | SgiClassAbs (x, n, _) => found (x, n) | 1021 | SgiClassAbs (x, n, _) => found (x, n) |
893 | SgiClass (x, n, _, _) => found (x, n) | 1022 | SgiClass (x, n, _, _) => found (x, n) |
894 | SgiVal (x, n, (CApp (f, a), _)) => | 1023 | SgiVal (x, n, c) => |
895 let | 1024 (case rule_in c of |
896 fun unravel c = | 1025 NONE => default () |
897 case #1 c of | 1026 | SOME (nvars, hyps, (cn, a)) => |
898 CUnif (_, _, _, ref (SOME c)) => unravel c | 1027 let |
899 | CNamed n => | 1028 val globalize = sgnS_class_key (m1, ms, fmap) |
900 ((case lookupCNamed env n of | 1029 val ck = globalize a |
901 (_, _, SOME c) => unravel c | 1030 val hyps = map (fn (n, k) => (sgnS_class_name (m1, ms, fmap) n, |
902 | _ => c) | 1031 globalize k)) hyps |
903 handle UnboundNamed _ => c) | 1032 |
904 | _ => c | 1033 fun unravel c = |
905 | 1034 case c of |
906 val nc = | 1035 ClNamed n => |
907 case f of | 1036 ((case lookupCNamed env n of |
908 (CNamed f, _) => IM.find (newClasses, f) | 1037 (_, _, SOME c') => |
909 | _ => NONE | 1038 (case class_name_in c' of |
910 in | 1039 NONE => c |
911 case nc of | 1040 | SOME k => unravel k) |
912 NONE => | 1041 | _ => c) |
913 (case (class_name_in (unravel f), | 1042 handle UnboundNamed _ => c) |
914 class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a)) of | 1043 | _ => c |
915 (SOME cn, SOME ck) => | 1044 |
1045 val nc = | |
1046 case cn of | |
1047 ClNamed f => IM.find (newClasses, f) | |
1048 | _ => NONE | |
1049 in | |
1050 case nc of | |
1051 NONE => | |
916 let | 1052 let |
917 val classes = | 1053 val classes = |
918 case CM.find (classes, cn) of | 1054 case CM.find (classes, cn) of |
919 NONE => classes | 1055 NONE => classes |
920 | SOME class => | 1056 | SOME class => |
921 let | 1057 let |
922 val class = { | 1058 val class = KM.insert (class, (ck, nvars), |
923 ground = KM.insert (#ground class, ck, | 1059 (hyps, |
924 (EModProj (m1, ms, x), #2 sgn)) | 1060 (EModProj (m1, ms, x), |
925 } | 1061 #2 sgn))) |
926 in | 1062 in |
927 CM.insert (classes, cn, class) | 1063 CM.insert (classes, cn, class) |
928 end | 1064 end |
929 in | 1065 in |
930 (classes, | 1066 (classes, |
931 newClasses, | 1067 newClasses, |
932 fmap, | 1068 fmap, |
933 env) | 1069 env) |
934 end | 1070 end |
935 | _ => default ()) | 1071 | SOME fx => |
936 | SOME fx => | 1072 let |
937 case class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a) of | 1073 val cn = ClProj (m1, ms, fx) |
938 NONE => default () | 1074 |
939 | SOME ck => | 1075 val classes = |
940 let | 1076 case CM.find (classes, cn) of |
941 val cn = ClProj (m1, ms, fx) | 1077 NONE => classes |
942 | 1078 | SOME class => |
943 val classes = | 1079 let |
944 case CM.find (classes, cn) of | 1080 val class = KM.insert (class, (ck, nvars), |
945 NONE => classes | 1081 (hyps, |
946 | SOME class => | 1082 (EModProj (m1, ms, x), #2 sgn))) |
947 let | 1083 in |
948 val class = { | 1084 CM.insert (classes, cn, class) |
949 ground = KM.insert (#ground class, ck, | 1085 end |
950 (EModProj (m1, ms, x), #2 sgn)) | 1086 in |
951 } | 1087 (classes, |
952 in | 1088 newClasses, |
953 CM.insert (classes, cn, class) | 1089 fmap, |
954 end | 1090 env) |
955 in | 1091 end |
956 (classes, | 1092 end) |
957 newClasses, | |
958 fmap, | |
959 env) | |
960 end | |
961 end | |
962 | SgiVal _ => default () | |
963 | _ => default () | 1093 | _ => default () |
964 end) | 1094 end) |
965 (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis | 1095 (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis |
966 in | 1096 in |
967 classes | 1097 classes |