summaryrefslogtreecommitdiff
path: root/src/core_env.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/core_env.sml')
-rw-r--r--src/core_env.sml29
1 files changed, 29 insertions, 0 deletions
diff --git a/src/core_env.sml b/src/core_env.sml
index b399f62f..0faf5aab 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -93,6 +93,35 @@ val subConInExp =
bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
| (ctx, _) => ctx}
+val liftExpInExp =
+ U.Exp.mapB {kind = fn k => k,
+ con = fn _ => fn c => c,
+ 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}
+
+val subExpInExp =
+ U.Exp.mapB {kind = fn k => k,
+ con = fn _ => fn c => c,
+ exp = fn (xn, rep) => fn e =>
+ case e of
+ ERel xn' =>
+ (case Int.compare (xn', xn) of
+ EQUAL => #1 rep
+ | GREATER=> ERel (xn' - 1)
+ | LESS => e)
+ | _ => e,
+ bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
+ | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
+ | (ctx, _) => ctx}
+
(* Back to environments *)
exception UnboundRel of int