diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-07-29 14:28:44 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-07-29 14:28:44 -0400 |
commit | 6855e4766fa8d07e2f3e3cd468de6c58fed0c903 (patch) | |
tree | 4098c6f3f8d9bacfe652f2b210ede504a9a5d4e9 /src/cjr_env.sml | |
parent | 166bccac16d35d8a4b75a4c04c7479b389a81c4f (diff) |
Start of unurlify for datatypes
Diffstat (limited to 'src/cjr_env.sml')
-rw-r--r-- | src/cjr_env.sml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/cjr_env.sml b/src/cjr_env.sml index 0d34b98f..88d7972f 100644 --- a/src/cjr_env.sml +++ b/src/cjr_env.sml @@ -38,7 +38,7 @@ exception UnboundF of int exception UnboundStruct of int type env = { - namedT : (string * typ option) IM.map, + datatypes : (string * (string * int * typ option) list) IM.map, numRelE : int, relE : (string * typ) list, @@ -48,7 +48,7 @@ type env = { } val empty = { - namedT = IM.empty, + datatypes = IM.empty, numRelE = 0, relE = [], @@ -57,8 +57,8 @@ val empty = { structs = IM.empty } -fun pushTNamed (env : env) x n co = - {namedT = IM.insert (#namedT env, n, (x, co)), +fun pushDatatype (env : env) x n xncs = + {datatypes = IM.insert (#datatypes env, n, (x, xncs)), numRelE = #numRelE env, relE = #relE env, @@ -66,13 +66,13 @@ fun pushTNamed (env : env) x n co = structs = #structs env} -fun lookupTNamed (env : env) n = - case IM.find (#namedT env, n) of +fun lookupDatatype (env : env) n = + case IM.find (#datatypes env, n) of NONE => raise UnboundNamed n | SOME x => x fun pushERel (env : env) x t = - {namedT = #namedT env, + {datatypes = #datatypes env, numRelE = #numRelE env + 1, relE = (x, t) :: #relE env, @@ -89,7 +89,7 @@ fun countERels (env : env) = #numRelE env fun listERels (env : env) = #relE env fun pushENamed (env : env) x n t = - {namedT = #namedT env, + {datatypes = #datatypes env, numRelE = #numRelE env, relE = #relE env, @@ -103,7 +103,7 @@ fun lookupENamed (env : env) n = | SOME x => x fun pushStruct (env : env) n xts = - {namedT = #namedT env, + {datatypes = #datatypes env, numRelE = #numRelE env, relE = #relE env, @@ -120,10 +120,10 @@ fun declBinds env (d, loc) = case d of DDatatype (x, n, xncs) => let - val env = pushTNamed env x n NONE + val env = pushDatatype env x n xncs 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)) + foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype n, loc) + | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype n, loc)), loc)) env xncs end | DStruct (n, xts) => pushStruct env n xts |