Mercurial > urweb

comparison src/elab_env.sml @ 218:a3413288cce1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Signature ascription for type classes
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 16:57:21 -0400
parents 56db662ebcfd
children 19e5791923d0
comparison
equal deleted inserted replaced
217:56db662ebcfd 218:a3413288cce1
698 698
699 fun enrichClasses env classes (m1, ms) sgn = 699 fun enrichClasses env classes (m1, ms) sgn =
700 case #1 (hnormSgn env sgn) of 700 case #1 (hnormSgn env sgn) of
701 SgnConst sgis => 701 SgnConst sgis =>
702 let 702 let
703 val (classes, _, _) = 703 val (classes, _, _, _) =
704 foldl (fn (sgi, (classes, newClasses, fmap)) => 704 foldl (fn (sgi, (classes, newClasses, fmap, env)) =>
705 let 705 let
706 fun found (x, n) = 706 fun found (x, n) =
707 (CM.insert (classes, 707 (CM.insert (classes,
708 ClProj (m1, ms, x), 708 ClProj (m1, ms, x),
709 empty_class), 709 empty_class),
710 IM.insert (newClasses, n, x), 710 IM.insert (newClasses, n, x),
711 sgiSeek (#1 sgi, fmap)) 711 sgiSeek (#1 sgi, fmap),
712 712 env)
713 fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap)) 713
714 fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env)
714 in 715 in
715 case #1 sgi of 716 case #1 sgi of
716 SgiStr (x, _, sgn) => 717 SgiStr (x, _, sgn) =>
717 (enrichClasses env classes (m1, ms @ [x]) sgn, 718 (enrichClasses env classes (m1, ms @ [x]) sgn,
718 newClasses, 719 newClasses,
719 sgiSeek (#1 sgi, fmap)) 720 sgiSeek (#1 sgi, fmap),
721 env)
722 | SgiSgn (x, n, sgn) =>
723 (classes,
724 newClasses,
725 fmap,
726 pushSgnNamedAs env x n sgn)
727
720 | SgiClassAbs xn => found xn 728 | SgiClassAbs xn => found xn
721 | SgiClass (x, n, _) => found (x, n) 729 | SgiClass (x, n, _) => found (x, n)
722 | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) => 730 | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) =>
723 (case IM.find (newClasses, f) of 731 (case IM.find (newClasses, f) of
724 NONE => default () 732 NONE => default ()
735 } 743 }
736 744
737 in 745 in
738 (CM.insert (classes, cn, class), 746 (CM.insert (classes, cn, class),
739 newClasses, 747 newClasses,
740 fmap) 748 fmap,
749 env)
741 end) 750 end)
742 | SgiVal _ => default () 751 | SgiVal _ => default ()
743 | _ => default () 752 | _ => default ()
744 end) 753 end)
745 (classes, IM.empty, (IM.empty, IM.empty, IM.empty)) sgis 754 (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis
746 in 755 in
747 classes 756 classes
748 end 757 end
749 | _ => classes 758 | _ => classes
750 759