summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-22 16:10:25 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-22 16:10:25 -0500
commitef4284bc3cf37e2f32ae2faddf07b4b8ed01ddac (patch)
tree7f9fc4189681a0186e8ecbfcc84a0eec50d03be9 /src/elab_env.sml
parentfdff38cbee53e566859c55bf9a9410396a3a00ab (diff)
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml130
1 files changed, 117 insertions, 13 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 53c934dd..083e7d55 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -45,8 +45,32 @@ exception UnboundNamed of int
exception SynUnif
+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 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 =>
@@ -56,13 +80,27 @@ val liftConInCon =
CRel (xn + 1)
(*| CUnif _ => raise SynUnif*)
| _ => c,
- bind = fn (bound, U.Con.Rel _) => bound + 1
+ bind = fn (bound, U.Con.RelC _) => bound + 1
| (bound, _) => bound}
val lift = liftConInCon 0
+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 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 =>
@@ -76,7 +114,7 @@ val liftConInExp =
| (bound, _) => bound}
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
@@ -93,7 +131,7 @@ val liftExpInExp =
val liftExp = liftExpInExp 0
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
@@ -203,6 +241,9 @@ fun printClasses cs = (print "Classes:\n";
print "\n")) cs)
type env = {
+ renameK : int SM.map,
+ relK : string list,
+
renameC : kind var' SM.map,
relC : (string * kind) list,
namedC : (string * kind * con option) IM.map,
@@ -234,6 +275,9 @@ fun newNamed () =
end
val empty = {
+ renameK = SM.empty,
+ relK = [],
+
renameC = SM.empty,
relC = [],
namedC = IM.empty,
@@ -261,12 +305,51 @@ fun liftClassKey ck =
| CkProj _ => ck
| CkApp (ck1, ck2) => CkApp (liftClassKey ck1, liftClassKey ck2)
+fun pushKRel (env : env) x =
+ let
+ val renameK = SM.map (fn n => n+1) (#renameK env)
+ in
+ {renameK = SM.insert (renameK, x, 0),
+ relK = x :: #relK env,
+
+ renameC = SM.map (fn Rel' (n, k) => Rel' (n, liftKindInKind 0 k)
+ | x => x) (#renameC env),
+ relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
+ namedC = #namedC env,
+
+ datatypes = #datatypes env,
+ constructors = #constructors env,
+
+ classes = #classes env,
+
+ renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c)
+ | Named' (n, c) => Named' (n, c)) (#renameE env),
+ relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
+ namedE = #namedE env,
+
+ renameSgn = #renameSgn env,
+ sgn = #sgn env,
+
+ renameStr = #renameStr env,
+ str = #str env
+ }
+ end
+
+fun lookupKRel (env : env) n =
+ (List.nth (#relK env, n))
+ handle Subscript => raise UnboundRel n
+
+fun lookupK (env : env) x = SM.find (#renameK env, x)
+
fun pushCRel (env : env) x k =
let
val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
| x => x) (#renameC env)
in
- {renameC = SM.insert (renameC, x, Rel' (0, k)),
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = SM.insert (renameC, x, Rel' (0, k)),
relC = (x, k) :: #relC env,
namedC = #namedC env,
@@ -298,7 +381,10 @@ fun lookupCRel (env : env) n =
handle Subscript => raise UnboundRel n
fun pushCNamedAs (env : env) x n k co =
- {renameC = SM.insert (#renameC env, x, Named' (n, k)),
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = SM.insert (#renameC env, x, Named' (n, k)),
relC = #relC env,
namedC = IM.insert (#namedC env, n, (x, k, co)),
@@ -340,7 +426,10 @@ fun pushDatatype (env : env) n xs xncs =
let
val dk = U.classifyDatatype xncs
in
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
@@ -380,7 +469,10 @@ fun datatypeArgs (xs, _) = xs
fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
fun pushClass (env : env) n =
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
@@ -468,7 +560,10 @@ fun pushERel (env : env) x t =
CM.insert (classes, f, class)
end
in
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
@@ -509,7 +604,10 @@ fun pushENamedAs (env : env) x n t =
CM.insert (classes, f, class)
end
in
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
@@ -552,7 +650,10 @@ fun lookupE (env : env) x =
| SOME (Named' x) => Named x
fun pushSgnNamedAs (env : env) x n sgis =
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
@@ -868,7 +969,10 @@ fun enrichClasses env classes (m1, ms) sgn =
| _ => classes
fun pushStrNamedAs (env : env) x n sgn =
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,