### diff src/elab_env.sml @ 623:588b9d16b00a

Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala Sun, 22 Feb 2009 16:10:25 -0500 44958d74c43f fab5998b840e
line wrap: on
line diff
```--- a/src/elab_env.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/elab_env.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -45,8 +45,32 @@

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 @@
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 @@
| (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 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 @@
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 @@
end

val empty = {
+    renameK = SM.empty,
+    relK = [],
+
renameC = SM.empty,
relC = [],
namedC = IM.empty,
@@ -261,12 +305,51 @@
| 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 @@
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 @@
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 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 @@
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 @@
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 @@
| 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 @@
| _ => 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,
```