Mercurial > urweb
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)