Mercurial > urweb

comparison src/elab_env.sml @ 216:38b299373676

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Looking up in a type class from a module
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 15:58:25 -0400
parents 0343557355fc
children 56db662ebcfd
comparison
equal deleted inserted replaced
215:2f574c07df2e 216:38b299373676
29 29
30 open Elab 30 open Elab
31 31
32 structure U = ElabUtil 32 structure U = ElabUtil
33 33
34 structure IS = IntBinarySet
35 structure IM = IntBinaryMap 34 structure IM = IntBinaryMap
36 structure SM = BinaryMapFn(struct 35 structure SM = BinaryMapFn(struct
37 type ord_key = string 36 type ord_key = string
38 val compare = String.compare 37 val compare = String.compare
39 end) 38 end)
94 93
95 datatype class_name = 94 datatype class_name =
96 ClNamed of int 95 ClNamed of int
97 | ClProj of int * string list * string 96 | ClProj of int * string list * string
98 97
98 fun cn2s cn =
99 case cn of
100 ClNamed n => "Named(" ^ Int.toString n ^ ")"
101 | ClProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
102
99 structure CK = struct 103 structure CK = struct
100 type ord_key = class_name 104 type ord_key = class_name
101 open Order 105 open Order
102 fun compare x = 106 fun compare x =
103 case x of 107 case x of
116 datatype class_key = 120 datatype class_key =
117 CkNamed of int 121 CkNamed of int
118 | CkRel of int 122 | CkRel of int
119 | CkProj of int * string list * string 123 | CkProj of int * string list * string
120 124
125 fun ck2s ck =
126 case ck of
127 CkNamed n => "Named(" ^ Int.toString n ^ ")"
128 | CkRel n => "Rel(" ^ Int.toString n ^ ")"
129 | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
130
131 fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")"
132
121 structure KK = struct 133 structure KK = struct
122 type ord_key = class_key 134 type ord_key = class_key
123 open Order 135 open Order
124 fun compare x = 136 fun compare x =
125 case x of 137 case x of
144 } 156 }
145 157
146 val empty_class = { 158 val empty_class = {
147 ground = KM.empty 159 ground = KM.empty
148 } 160 }
161
162 fun printClasses cs = CM.appi (fn (cn, {ground = km}) =>
163 (print (cn2s cn ^ ":");
164 KM.appi (fn (ck, _) => print (" " ^ ck2s ck)) km;
165 print "\n")) cs
149 166
150 type env = { 167 type env = {
151 renameC : kind var' SM.map, 168 renameC : kind var' SM.map,
152 relC : (string * kind) list, 169 relC : (string * kind) list,
153 namedC : (string * kind * con option) IM.map, 170 namedC : (string * kind * con option) IM.map,
512 NONE => raise UnboundNamed n 529 NONE => raise UnboundNamed n
513 | SOME x => x 530 | SOME x => x
514 531
515 fun lookupStr (env : env) x = SM.find (#renameStr env, x) 532 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
516 533
534
535 fun sgiSeek (sgi, (sgns, strs, cons)) =
536 case sgi of
537 SgiConAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
538 | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
539 | SgiDatatype (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
540 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x))
541 | SgiVal _ => (sgns, strs, cons)
542 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
543 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons)
544 | SgiConstraint _ => (sgns, strs, cons)
545 | SgiTable _ => (sgns, strs, cons)
546 | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x))
547 | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
517 548
518 fun sgnSeek f sgis = 549 fun sgnSeek f sgis =
519 let 550 let
520 fun seek (sgis, sgns, strs, cons) = 551 fun seek (sgis, sgns, strs, cons) =
521 case sgis of 552 case sgis of
531 | _ => cons 562 | _ => cons
532 in 563 in
533 SOME (v, (sgns, strs, cons)) 564 SOME (v, (sgns, strs, cons))
534 end 565 end
535 | NONE => 566 | NONE =>
536 case sgi of 567 let
537 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 568 val (sgns, strs, cons) = sgiSeek (sgi, (sgns, strs, cons))
538 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 569 in
539 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 570 seek (sgis, sgns, strs, cons)
540 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 571 end
541 | SgiVal _ => seek (sgis, sgns, strs, cons)
542 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
543 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
544 | SgiConstraint _ => seek (sgis, sgns, strs, cons)
545 | SgiTable _ => seek (sgis, sgns, strs, cons)
546 | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
547 | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
548 in 572 in
549 seek (sgis, IM.empty, IM.empty, IM.empty) 573 seek (sgis, IM.empty, IM.empty, IM.empty)
550 end 574 end
551 575
552 fun id x = x 576 fun id x = x
582 in 606 in
583 CModProj (m1, ms, nx) 607 CModProj (m1, ms, nx)
584 end) 608 end)
585 | _ => c 609 | _ => c
586 610
611 fun sgnS_con' (m1, ms', (sgns, strs, cons)) c =
612 case c of
613 CModProj (m1, ms, x) =>
614 (case IM.find (strs, m1) of
615 NONE => c
616 | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x))
617 | CNamed n =>
618 (case IM.find (cons, n) of
619 NONE => c
620 | SOME nx => CModProj (m1, ms', nx))
621 | _ => c
622
587 fun sgnS_sgn (str, (sgns, strs, cons)) sgn = 623 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
588 case sgn of 624 case sgn of
589 SgnProj (m1, ms, x) => 625 SgnProj (m1, ms, x) =>
590 (case IM.find (strs, m1) of 626 (case IM.find (strs, m1) of
591 NONE => sgn 627 NONE => sgn
662 698
663 fun enrichClasses env classes (m1, ms) sgn = 699 fun enrichClasses env classes (m1, ms) sgn =
664 case #1 (hnormSgn env sgn) of 700 case #1 (hnormSgn env sgn) of
665 SgnConst sgis => 701 SgnConst sgis =>
666 let 702 let
667 val (classes, _) = 703 val (classes, _, _) =
668 foldl (fn (sgi, (classes, newClasses)) => 704 foldl (fn (sgi, (classes, newClasses, fmap)) =>
669 let 705 let
670 fun found (x, n) = 706 fun found (x, n) =
671 (CM.insert (classes, 707 (CM.insert (classes,
672 ClProj (m1, ms, x), 708 ClProj (m1, ms, x),
673 empty_class), 709 empty_class),
674 IS.add (newClasses, n)) 710 IM.insert (newClasses, n, x),
711 sgiSeek (#1 sgi, fmap))
712
713 fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap))
675 in 714 in
676 case #1 sgi of 715 case #1 sgi of
677 SgiClassAbs xn => found xn 716 SgiClassAbs xn => found xn
678 | SgiClass (x, n, _) => found (x, n) 717 | SgiClass (x, n, _) => found (x, n)
679 | _ => (classes, newClasses) 718 | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) =>
719 (case IM.find (newClasses, f) of
720 NONE => default ()
721 | SOME fx =>
722 case class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a) of
723 NONE => default ()
724 | SOME ck =>
725 let
726 val cn = ClProj (m1, ms, fx)
727 val class = Option.getOpt (CM.find (classes, cn), empty_class)
728 val class = {
729 ground = KM.insert (#ground class, ck,
730 (EModProj (m1, ms, x), #2 sgn))
731 }
732
733 in
734 (CM.insert (classes, cn, class),
735 newClasses,
736 fmap)
737 end)
738 | _ => default ()
680 end) 739 end)
681 (classes, IS.empty) sgis 740 (classes, IM.empty, (IM.empty, IM.empty, IM.empty)) sgis
682 in 741 in
683 classes 742 classes
684 end 743 end
685 | _ => classes 744 | _ => classes
686 745
801 | SgiDatatypeImp (x, _, m1, ms, x', _, _) => 860 | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
802 if x = field then 861 if x = field then
803 SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn)) 862 SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn))
804 else 863 else
805 NONE 864 NONE
865 | SgiClassAbs (x, _) => if x = field then
866 SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), NONE)
867 else
868 NONE
869 | SgiClass (x, _, c) => if x = field then
870 SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), SOME c)
871 else
872 NONE
806 | _ => NONE) sgis of 873 | _ => NONE) sgis of
807 NONE => NONE 874 NONE => NONE
808 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co)) 875 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
809 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) 876 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
810 | _ => NONE 877 | _ => NONE