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.sml95
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,