diff src/core_env.sml @ 315:e21d0dddda09

Unpoly non-recursive function
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 09:36:47 -0400
parents 42dfb0d61cf0
children e976b187d73a
line wrap: on
line diff
--- a/src/core_env.sml	Tue Sep 09 12:36:13 2008 -0400
+++ b/src/core_env.sml	Thu Sep 11 09:36:47 2008 -0400
@@ -65,6 +65,34 @@
                         | (ctx, _) => ctx}
 
 
+val liftConInExp =
+    U.Exp.mapB {kind = fn k => k,
+                con = fn bound => fn c =>
+                                     case c of
+                                         CRel xn =>
+                                         if xn < bound then
+                                             c
+                                         else
+                                             CRel (xn + 1)
+                                       | _ => c,
+                exp = fn _ => fn e => e,
+                bind = fn (bound, U.Exp.RelC _) => bound + 1
+                        | (bound, _) => bound}
+
+val subConInExp =
+    U.Exp.mapB {kind = fn k => k,
+                con = fn (xn, rep) => fn c =>
+                                  case c of
+                                      CRel xn' =>
+                                      (case Int.compare (xn', xn) of
+                                           EQUAL => #1 rep
+                                         | GREATER => CRel (xn' - 1)
+                                         | LESS => c)
+                                    | _ => c,
+                exp = fn _ => fn e => e,
+                bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
+                        | (ctx, _) => ctx}
+
 (* Back to environments *)
 
 exception UnboundRel of int