summaryrefslogtreecommitdiff
path: root/src/cjr_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-29 13:50:53 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-29 13:50:53 -0400
commit166bccac16d35d8a4b75a4c04c7479b389a81c4f (patch)
tree0674876271c5e871d53bb786e88dd1d2049bdb02 /src/cjr_env.sml
parentac7c66e703f70f57c59697fd90504539c475244d (diff)
Datatypes through cjrize, modulo decoding
Diffstat (limited to 'src/cjr_env.sml')
-rw-r--r--src/cjr_env.sml13
1 files changed, 11 insertions, 2 deletions
diff --git a/src/cjr_env.sml b/src/cjr_env.sml
index a44359db..0d34b98f 100644
--- a/src/cjr_env.sml
+++ b/src/cjr_env.sml
@@ -118,7 +118,16 @@ fun lookupStruct (env : env) n =
fun declBinds env (d, loc) =
case d of
- DVal (x, n, t, _) => pushENamed env x n t
+ DDatatype (x, n, xncs) =>
+ let
+ val env = pushTNamed env x n NONE
+ in
+ foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TNamed n, loc)
+ | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TNamed n, loc)), loc))
+ env xncs
+ end
+ | DStruct (n, xts) => pushStruct env n xts
+ | DVal (x, n, t, _) => pushENamed env x n t
| DFun (fx, n, args, ran, _) =>
let
val t = foldl (fn ((_, arg), t) => (TFun (arg, t), loc)) ran args
@@ -132,6 +141,6 @@ fun declBinds env (d, loc) =
in
pushENamed env fx n t
end) env vis
- | DStruct (n, xts) => pushStruct env n xts
+
end