diff src/mono_env.sml @ 800:e92cfac1608f

Proper lifting of MonoEnv stored expressions; avoidance of onchange clobbering
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 May 2009 13:18:31 -0400
parents 8688e01ae469
children d8f58d488cfb
line wrap: on
line diff
--- a/src/mono_env.sml	Thu May 14 11:04:56 2009 -0400
+++ b/src/mono_env.sml	Thu May 14 13:18:31 2009 -0400
@@ -70,11 +70,25 @@
         NONE => raise UnboundNamed n
       | SOME x => x
 
+structure U = MonoUtil
+
+val liftExpInExp =
+    U.Exp.mapB {typ = fn t => t,
+                exp = fn bound => fn e =>
+                                     case e of
+                                         ERel xn =>
+                                         if xn < bound then
+                                             e
+                                         else
+                                             ERel (xn + 1)
+                                       | _ => e,
+                bind = fn (bound, U.Exp.RelE _) => bound + 1
+                        | (bound, _) => bound}
+
 fun pushERel (env : env) x t eo =
     {datatypes = #datatypes env,
      constructors = #constructors env,
-
-     relE = (x, t, eo) :: #relE env,
+     relE = (x, t, eo) :: map (fn (x, t, eo) => (x, t, Option.map (liftExpInExp 0) eo)) (#relE env),
      namedE = #namedE env}
 
 fun lookupERel (env : env) n =