diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-09-07 13:29:01 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-09-07 13:29:01 -0400 |
| commit | 9f8b222f6667f4e7dec2105ea4f5c2abdfd29dc9 (patch) | |
| tree | 90104da9ab622189caffe5a38bddcb8bfe797233 /src/elab_env.sml | |
| parent | 4a627a550cb54c18cb16cc0ad852e6a0bbc59c31 (diff) | |
pquery working with all four types of columns
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 35 |
1 files changed, 23 insertions, 12 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 89a2b4ff..1b9de129 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -991,17 +991,23 @@ fun declBinds env (d, loc) = DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) | DDatatype (x, n, xs, xncs) => let - val env = pushCNamedAs env x n (KType, loc) NONE + val k = (KType, loc) + val nxs = length xs + val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) => + ((CApp (tb, (CRel (nxs - i - 1), loc)), loc), + (KArrow (k, kb), loc))) + ((CNamed n, loc), k) xs + + val env = pushCNamedAs env x n kb NONE val env = pushDatatype env n xs xncs in foldl (fn ((x', n', to), env) => let val t = case to of - NONE => (CNamed n, loc) - | SOME t => (TFun (t, (CNamed n, loc)), loc) - val k = (KType, loc) - val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs + NONE => tb + | SOME t => (TFun (t, tb), loc) + val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs in pushENamedAs env x' n' t end) @@ -1010,19 +1016,24 @@ fun declBinds env (d, loc) = | DDatatypeImp (x, n, m, ms, x', xs, xncs) => let val t = (CModProj (m, ms, x'), loc) - val env = pushCNamedAs env x n (KType, loc) (SOME t) + val k = (KType, loc) + val nxs = length xs + val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) => + ((CApp (tb, (CRel (nxs - i - 1), loc)), loc), + (KArrow (k, kb), loc))) + ((CNamed n, loc), k) xs + + val t' = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs + val env = pushCNamedAs env x n kb (SOME t') val env = pushDatatype env n xs xncs - - val t = (CNamed n, loc) in foldl (fn ((x', n', to), env) => let val t = case to of - NONE => (CNamed n, loc) - | SOME t => (TFun (t, (CNamed n, loc)), loc) - val k = (KType, loc) - val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs + NONE => tb + | SOME t => (TFun (t, tb), loc) + val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs in pushENamedAs env x' n' t end) |