diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-08-08 10:59:06 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-08 10:59:06 -0400 |
| commit | e2a9136ed7123cb8e5cac4a20cbce5467643ecd6 (patch) | |
| tree | cf96ee150816d9120f27370837c836e5641bbdd9 /src/core_env.sml | |
| parent | baf22271ef6e646c97ddfa1e4193a8857816c67d (diff) | |
Parametrized datatypes through corify
Diffstat (limited to 'src/core_env.sml')
| -rw-r--r-- | src/core_env.sml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/core_env.sml b/src/core_env.sml index 1cc10ada..5b7cfa2e 100644 --- a/src/core_env.sml +++ b/src/core_env.sml @@ -61,8 +61,8 @@ type env = { relC : (string * kind) list, namedC : (string * kind * con option) IM.map, - datatypes : (string * (string * int * con option) list) IM.map, - constructors : (string * con option * int) IM.map, + datatypes : (string * string list * (string * int * con option) list) IM.map, + constructors : (string * string list * con option * int) IM.map, relE : (string * con) list, namedE : (string * con * exp option * string) IM.map @@ -108,13 +108,13 @@ fun lookupCNamed (env : env) n = NONE => raise UnboundNamed n | SOME x => x -fun pushDatatype (env : env) x n xncs = +fun pushDatatype (env : env) x n xs xncs = {relC = #relC env, namedC = #namedC env, - datatypes = IM.insert (#datatypes env, n, (x, xncs)), + datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)), constructors = foldl (fn ((x, n', to), constructors) => - IM.insert (constructors, n', (x, to, n))) + IM.insert (constructors, n', (x, xs, to, n))) (#constructors env) xncs, relE = #relE env, @@ -162,9 +162,9 @@ fun lookupENamed (env : env) n = fun declBinds env (d, loc) = case d of DCon (x, n, k, c) => pushCNamed env x n k (SOME c) - | DDatatype (x, n, xncs) => + | DDatatype (x, n, xs, xncs) => let - val env = pushDatatype env x n xncs + val env = pushDatatype env x n xs xncs val env = pushCNamed env x n (KType, loc) NONE in foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE "" |