summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/elab_ops.sml40
1 files changed, 28 insertions, 12 deletions
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 5102d0ab..0648d704 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -32,22 +32,38 @@ open Elab
structure E = ElabEnv
structure U = ElabUtil
-val liftConInCon = E.liftConInCon
+fun liftConInCon by =
+ U.Con.mapB {kind = fn k => k,
+ con = fn bound => fn c =>
+ case c of
+ CRel xn =>
+ if xn < bound then
+ c
+ else
+ CRel (xn + by)
+ (*| CUnif _ => raise SynUnif*)
+ | _ => c,
+ bind = fn (bound, U.Con.Rel _) => bound + 1
+ | (bound, _) => bound}
-val subConInCon =
+fun subConInCon' rep =
U.Con.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)
- (*| CUnif _ => raise SynUnif*)
- | _ => c,
- bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
+ con = fn (by, xn) => fn c =>
+ case c of
+ CRel xn' =>
+ (case Int.compare (xn', xn) of
+ EQUAL => #1 (liftConInCon by 0 rep)
+ | GREATER => CRel (xn' - 1)
+ | LESS => c)
+ (*| CUnif _ => raise SynUnif*)
+ | _ => c,
+ bind = fn ((by, xn), U.Con.Rel _) => (by+1, xn+1)
| (ctx, _) => ctx}
+val liftConInCon = liftConInCon 1
+
+fun subConInCon (xn, rep) = subConInCon' rep (0, xn)
+
fun subStrInSgn (m1, m2) =
U.Sgn.map {kind = fn k => k,
con = fn c as CModProj (m1', ms, x) =>