Mercurial > urweb
diff src/core_env.sml @ 192:9bbf4d383381
Parametrized datatypes through corify
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 08 Aug 2008 10:59:06 -0400 |
parents | d11754ffe252 |
children | 8a70e2919e86 |
line wrap: on
line diff
--- a/src/core_env.sml Fri Aug 08 10:28:32 2008 -0400 +++ b/src/core_env.sml Fri Aug 08 10:59:06 2008 -0400 @@ -61,8 +61,8 @@ 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 @@ 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 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 ""