Mercurial > urweb

comparison src/elab_env.sml @ 419:cb5897276abf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix bug with bringing functor argument instances into scope; Ref demo, minus prose
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Oct 2008 17:35:10 -0400
parents 8084fa9216de
children b77863cd0be2
comparison
equal deleted inserted replaced
418:ad7e854a518c 419:cb5897276abf
157 157
158 val empty_class = { 158 val empty_class = {
159 ground = KM.empty 159 ground = KM.empty
160 } 160 }
161 161
162 fun printClasses cs = CM.appi (fn (cn, {ground = km}) => 162 fun printClasses cs = (print "Classes:\n";
163 (print (cn2s cn ^ ":"); 163 CM.appi (fn (cn, {ground = km}) =>
164 KM.appi (fn (ck, _) => print (" " ^ ck2s ck)) km; 164 (print (cn2s cn ^ ":");
165 print "\n")) cs 165 KM.appi (fn (ck, _) => print (" " ^ ck2s ck)) km;
166 print "\n")) cs)
166 167
167 type env = { 168 type env = {
168 renameC : kind var' SM.map, 169 renameC : kind var' SM.map,
169 relC : (string * kind) list, 170 relC : (string * kind) list,
170 namedC : (string * kind * con option) IM.map, 171 namedC : (string * kind * con option) IM.map,
741 fmap, 742 fmap,
742 pushSgnNamedAs env x n sgn) 743 pushSgnNamedAs env x n sgn)
743 744
744 | SgiClassAbs xn => found xn 745 | SgiClassAbs xn => found xn
745 | SgiClass (x, n, _) => found (x, n) 746 | SgiClass (x, n, _) => found (x, n)
746 | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) => 747 | SgiVal (x, n, (CApp (f, a), _)) =>
747 (case IM.find (newClasses, f) of 748 let
748 NONE => default () 749 fun unravel c =
749 | SOME fx => 750 case #1 c of
750 case class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a) of 751 CUnif (_, _, _, ref (SOME c)) => unravel c
751 NONE => default () 752 | CNamed n =>
752 | SOME ck => 753 ((case lookupCNamed env n of
753 let 754 (_, _, SOME c) => unravel c
754 val cn = ClProj (m1, ms, fx) 755 | _ => c)
755 756 handle UnboundNamed _ => c)
756 val classes = 757 | _ => c
757 case CM.find (classes, cn) of 758
758 NONE => classes 759 val nc =
759 | SOME class => 760 case f of
760 let 761 (CNamed f, _) => IM.find (newClasses, f)
761 val class = { 762 | _ => NONE
762 ground = KM.insert (#ground class, ck, 763 in
763 (EModProj (m1, ms, x), #2 sgn)) 764 case nc of
764 } 765 NONE =>
765 in 766 (case (class_name_in (unravel f),
766 CM.insert (classes, cn, class) 767 class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a)) of
767 end 768 (SOME cn, SOME ck) =>
768 in 769 let
769 (classes, 770 val classes =
770 newClasses, 771 case CM.find (classes, cn) of
771 fmap, 772 NONE => classes
772 env) 773 | SOME class =>
773 end) 774 let
775 val class = {
776 ground = KM.insert (#ground class, ck,
777 (EModProj (m1, ms, x), #2 sgn))
778 }
779 in
780 CM.insert (classes, cn, class)
781 end
782 in
783 (classes,
784 newClasses,
785 fmap,
786 env)
787 end
788 | _ => default ())
789 | SOME fx =>
790 case class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a) of
791 NONE => default ()
792 | SOME ck =>
793 let
794 val cn = ClProj (m1, ms, fx)
795
796 val classes =
797 case CM.find (classes, cn) of
798 NONE => classes
799 | SOME class =>
800 let
801 val class = {
802 ground = KM.insert (#ground class, ck,
803 (EModProj (m1, ms, x), #2 sgn))
804 }
805 in
806 CM.insert (classes, cn, class)
807 end
808 in
809 (classes,
810 newClasses,
811 fmap,
812 env)
813 end
814 end
774 | SgiVal _ => default () 815 | SgiVal _ => default ()
775 | _ => default () 816 | _ => default ()
776 end) 817 end)
777 (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis 818 (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis
778 in 819 in