summaryrefslogtreecommitdiff
path: root/src/core_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 15:47:44 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 15:47:44 -0400
commite18863bcabc5d185b7fe1fc750bdf0bbdb5a4f78 (patch)
tree180c8271605929d6c902c4dda9b8b756ff0e1fda /src/core_env.sml
parentb0bf85209e8ddd4937393908d953f451556e73e9 (diff)
Some con reducing
Diffstat (limited to 'src/core_env.sml')
-rw-r--r--src/core_env.sml10
1 files changed, 5 insertions, 5 deletions
diff --git a/src/core_env.sml b/src/core_env.sml
index e123c9a9..904c71f5 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -62,7 +62,7 @@ type env = {
namedC : (string * kind * con option) IM.map,
relE : (string * con) list,
- namedE : (string * con) IM.map
+ namedE : (string * con * exp option) IM.map
}
val empty = {
@@ -78,7 +78,7 @@ fun pushCRel (env : env) x k =
namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
relE = map (fn (x, c) => (x, lift c)) (#relE env),
- namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)}
+ namedE = IM.map (fn (x, c, eo) => (x, lift c, eo)) (#namedE env)}
fun lookupCRel (env : env) n =
(List.nth (#relC env, n))
@@ -107,12 +107,12 @@ fun lookupERel (env : env) n =
(List.nth (#relE env, n))
handle Subscript => raise UnboundRel n
-fun pushENamed (env : env) x n t =
+fun pushENamed (env : env) x n t eo =
{relC = #relC env,
namedC = #namedC env,
relE = #relE env,
- namedE = IM.insert (#namedE env, n, (x, t))}
+ namedE = IM.insert (#namedE env, n, (x, t, eo))}
fun lookupENamed (env : env) n =
case IM.find (#namedE env, n) of
@@ -122,7 +122,7 @@ fun lookupENamed (env : env) n =
fun declBinds env (d, _) =
case d of
DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
- | DVal (x, n, t, _) => pushENamed env x n t
+ | DVal (x, n, t, e) => pushENamed env x n t (SOME e)
val ktype = (KType, ErrorMsg.dummySpan)