Mercurial > urweb

comparison src/elab_env.sml @ 297:59dc042629b9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
pquery working with all four types of columns
author Adam Chlipala <adamc@hcoop.net>
date Sun, 07 Sep 2008 13:29:01 -0400
parents 42dfb0d61cf0
children 58f1260f293f
comparison
equal deleted inserted replaced
296:5dc11235129d 297:59dc042629b9
989 fun declBinds env (d, loc) = 989 fun declBinds env (d, loc) =
990 case d of 990 case d of
991 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 991 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
992 | DDatatype (x, n, xs, xncs) => 992 | DDatatype (x, n, xs, xncs) =>
993 let 993 let
994 val env = pushCNamedAs env x n (KType, loc) NONE 994 val k = (KType, loc)
995 val nxs = length xs
996 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
997 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
998 (KArrow (k, kb), loc)))
999 ((CNamed n, loc), k) xs
1000
1001 val env = pushCNamedAs env x n kb NONE
995 val env = pushDatatype env n xs xncs 1002 val env = pushDatatype env n xs xncs
996 in 1003 in
997 foldl (fn ((x', n', to), env) => 1004 foldl (fn ((x', n', to), env) =>
998 let 1005 let
999 val t = 1006 val t =
1000 case to of 1007 case to of
1001 NONE => (CNamed n, loc) 1008 NONE => tb
1002 | SOME t => (TFun (t, (CNamed n, loc)), loc) 1009 | SOME t => (TFun (t, tb), loc)
1003 val k = (KType, loc) 1010 val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
1004 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
1005 in 1011 in
1006 pushENamedAs env x' n' t 1012 pushENamedAs env x' n' t
1007 end) 1013 end)
1008 env xncs 1014 env xncs
1009 end 1015 end
1010 | DDatatypeImp (x, n, m, ms, x', xs, xncs) => 1016 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
1011 let 1017 let
1012 val t = (CModProj (m, ms, x'), loc) 1018 val t = (CModProj (m, ms, x'), loc)
1013 val env = pushCNamedAs env x n (KType, loc) (SOME t) 1019 val k = (KType, loc)
1020 val nxs = length xs
1021 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
1022 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
1023 (KArrow (k, kb), loc)))
1024 ((CNamed n, loc), k) xs
1025
1026 val t' = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
1027 val env = pushCNamedAs env x n kb (SOME t')
1014 val env = pushDatatype env n xs xncs 1028 val env = pushDatatype env n xs xncs
1015
1016 val t = (CNamed n, loc)
1017 in 1029 in
1018 foldl (fn ((x', n', to), env) => 1030 foldl (fn ((x', n', to), env) =>
1019 let 1031 let
1020 val t = 1032 val t =
1021 case to of 1033 case to of
1022 NONE => (CNamed n, loc) 1034 NONE => tb
1023 | SOME t => (TFun (t, (CNamed n, loc)), loc) 1035 | SOME t => (TFun (t, tb), loc)
1024 val k = (KType, loc) 1036 val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
1025 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
1026 in 1037 in
1027 pushENamedAs env x' n' t 1038 pushENamedAs env x' n' t
1028 end) 1039 end)
1029 env xncs 1040 env xncs
1030 end 1041 end