summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-01 15:58:55 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-01 15:58:55 -0400
commit6578fad1ed0871839d4b99a40cd626d4f39bf162 (patch)
treef4112230acc95c284530da52a823ff9b88516349 /src/elab_env.sml
parent3c78af90b54d01c97ab75fd7290281dfb96921ee (diff)
First Unnest tests working
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml29
1 files changed, 29 insertions, 0 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index f4f5d2cb..2732de13 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -61,6 +61,20 @@ val liftConInCon =
val lift = liftConInCon 0
+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 liftExpInExp =
U.Exp.mapB {kind = fn k => k,
con = fn _ => fn c => c,
@@ -78,6 +92,21 @@ val liftExpInExp =
val liftExp = liftExpInExp 0
+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 *)
datatype 'a var' =