diff src/core_env.sml @ 20:1ab48e37d0ef

Some con reducing
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 15:47:44 -0400
parents bc7b76ca57e0
children d3cc191cb25f
line wrap: on
line diff
--- a/src/core_env.sml	Sun Jun 08 14:42:12 2008 -0400
+++ b/src/core_env.sml	Sun Jun 08 15:47:44 2008 -0400
@@ -62,7 +62,7 @@
      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 @@
      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 @@
     (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 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)