diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/elab_ops.sml | 40 |
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) => |