Mercurial > urweb

comparison src/elab_env.sml @ 341:389399d65331

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Crud update form
author Adam Chlipala <adamc@hcoop.net>
date Sun, 14 Sep 2008 19:03:55 -0400
parents e976b187d73a
children 8084fa9216de
comparison
equal deleted inserted replaced
340:5ccb1c6412e4 341:389399d65331
793 case sgi of 793 case sgi of
794 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE 794 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
795 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 795 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
796 | SgiDatatype (x, n, xs, xncs) => 796 | SgiDatatype (x, n, xs, xncs) =>
797 let 797 let
798 val env = pushCNamedAs env x n (KType, loc) NONE 798 val k = (KType, loc)
799 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
800
801 val env = pushCNamedAs env x n k' NONE
799 in 802 in
800 foldl (fn ((x', n', to), env) => 803 foldl (fn ((x', n', to), env) =>
801 let 804 let
802 val t = 805 val t =
803 case to of 806 case to of
811 end) 814 end)
812 env xncs 815 env xncs
813 end 816 end
814 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => 817 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
815 let 818 let
816 val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) 819 val k = (KType, loc)
820 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
821
822 val env = pushCNamedAs env x n k' (SOME (CModProj (m1, ms, x'), loc))
817 in 823 in
818 foldl (fn ((x', n', to), env) => 824 foldl (fn ((x', n', to), env) =>
819 let 825 let
820 val t = 826 val t =
821 case to of 827 case to of
878 fun projectCon env {sgn, str, field} = 884 fun projectCon env {sgn, str, field} =
879 case #1 (hnormSgn env sgn) of 885 case #1 (hnormSgn env sgn) of
880 SgnConst sgis => 886 SgnConst sgis =>
881 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE 887 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
882 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE 888 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
883 | SgiDatatype (x, _, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE 889 | SgiDatatype (x, _, xs, _) =>
884 | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
885 if x = field then 890 if x = field then
886 SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn)) 891 let
892 val k = (KType, #2 sgn)
893 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
894 in
895 SOME (k', NONE)
896 end
897 else
898 NONE
899 | SgiDatatypeImp (x, _, m1, ms, x', xs, _) =>
900 if x = field then
901 let
902 val k = (KType, #2 sgn)
903 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
904 in
905 SOME (k', SOME (CModProj (m1, ms, x'), #2 sgn))
906 end
887 else 907 else
888 NONE 908 NONE
889 | SgiClassAbs (x, _) => if x = field then 909 | SgiClassAbs (x, _) => if x = field then
890 SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), NONE) 910 SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), NONE)
891 else 911 else
1030 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) => 1050 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
1031 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc), 1051 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
1032 (KArrow (k, kb), loc))) 1052 (KArrow (k, kb), loc)))
1033 ((CNamed n, loc), k) xs 1053 ((CNamed n, loc), k) xs
1034 1054
1035 val t' = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs 1055 val env = pushCNamedAs env x n kb (SOME t)
1036 val env = pushCNamedAs env x n kb (SOME t')
1037 val env = pushDatatype env n xs xncs 1056 val env = pushDatatype env n xs xncs
1038 in 1057 in
1039 foldl (fn ((x', n', to), env) => 1058 foldl (fn ((x', n', to), env) =>
1040 let 1059 let
1041 val t = 1060 val t =