demo/hello compiles with kind polymorphism

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,