diff options
Diffstat (limited to 'src/core_env.sml')
| -rw-r--r-- | src/core_env.sml | 95 |
1 files changed, 82 insertions, 13 deletions
diff --git a/src/core_env.sml b/src/core_env.sml index 07162606..2c100aa5 100644 --- a/src/core_env.sml +++ b/src/core_env.sml @@ -36,8 +36,46 @@ structure IM = IntBinaryMap (* AST utility functions *) +val liftKindInKind = + U.Kind.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + bind = fn (bound, _) => bound + 1} + +val liftKindInCon = + U.Con.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + con = fn _ => fn c => c, + bind = fn (bound, U.Con.RelK _) => bound + 1 + | (bound, _) => bound} + +val liftKindInExp = + U.Exp.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + con = fn _ => fn c => c, + exp = fn _ => fn e => e, + bind = fn (bound, U.Exp.RelK _) => bound + 1 + | (bound, _) => bound} + val liftConInCon = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn bound => fn c => case c of CRel xn => @@ -46,13 +84,13 @@ val liftConInCon = else CRel (xn + 1) | _ => c, - bind = fn (bound, U.Con.Rel _) => bound + 1 + bind = fn (bound, U.Con.RelC _) => bound + 1 | (bound, _) => bound} val lift = liftConInCon 0 val subConInCon = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn (xn, rep) => fn c => case c of CRel xn' => @@ -61,12 +99,12 @@ val subConInCon = | GREATER => CRel (xn' - 1) | LESS => c) | _ => c, - bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) + bind = fn ((xn, rep), U.Con.RelC _) => (xn+1, liftConInCon 0 rep) | (ctx, _) => ctx} val liftConInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn bound => fn c => case c of CRel xn => @@ -80,7 +118,7 @@ val liftConInExp = | (bound, _) => bound} val subConInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn (xn, rep) => fn c => case c of CRel xn' => @@ -94,7 +132,7 @@ val subConInExp = | (ctx, _) => ctx} val liftExpInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn bound => fn e => case e of @@ -108,7 +146,7 @@ val liftExpInExp = | (bound, _) => bound} val subExpInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn (xn, rep) => fn e => case e of @@ -128,6 +166,8 @@ exception UnboundRel of int exception UnboundNamed of int type env = { + relK : string list, + relC : (string * kind) list, namedC : (string * kind * con option) IM.map, @@ -139,6 +179,8 @@ type env = { } val empty = { + relK = [], + relC = [], namedC = IM.empty, @@ -149,8 +191,27 @@ val empty = { namedE = IM.empty } +fun pushKRel (env : env) x = + {relK = x :: #relK env, + + relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env), + namedC = #namedC env, + + relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env), + namedE = #namedE env, + + datatypes = #datatypes env, + constructors = #constructors env + } + +fun lookupKRel (env : env) n = + (List.nth (#relK env, n)) + handle Subscript => raise UnboundRel n + fun pushCRel (env : env) x k = - {relC = (x, k) :: #relC env, + {relK = #relK env, + + relC = (x, k) :: #relC env, namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), datatypes = #datatypes env, @@ -164,7 +225,9 @@ fun lookupCRel (env : env) n = handle Subscript => raise UnboundRel n fun pushCNamed (env : env) x n k co = - {relC = #relC env, + {relK = #relK env, + + relC = #relC env, namedC = IM.insert (#namedC env, n, (x, k, co)), datatypes = #datatypes env, @@ -179,7 +242,9 @@ fun lookupCNamed (env : env) n = | SOME x => x fun pushDatatype (env : env) x n xs xncs = - {relC = #relC env, + {relK = #relK env, + + relC = #relC env, namedC = #namedC env, datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)), @@ -201,7 +266,9 @@ fun lookupConstructor (env : env) n = | SOME x => x fun pushERel (env : env) x t = - {relC = #relC env, + {relK = #relK env, + + relC = #relC env, namedC = #namedC env, datatypes = #datatypes env, @@ -215,7 +282,9 @@ fun lookupERel (env : env) n = handle Subscript => raise UnboundRel n fun pushENamed (env : env) x n t eo s = - {relC = #relC env, + {relK = #relK env, + + relC = #relC env, namedC = #namedC env, datatypes = #datatypes env, |