Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top

1 files changed, 66 insertions, 29 deletions

diff --git a/src/elab_print.sml b/src/elab_print.sml
index 098c9259..a0e1a54a 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -38,25 +38,36 @@ structure E = ElabEnv
 
 val debug = ref false
 
-fun p_kind' par (k, _) =
+fun p_kind' par env (k, _) =
     case k of
         KType => string "Type"
-      | KArrow (k1, k2) => parenIf par (box [p_kind' true k1,
+      | KArrow (k1, k2) => parenIf par (box [p_kind' true env k1,
                                              space,
                                              string "->",
                                              space,
-                                             p_kind k2])
+                                             p_kind env k2])
       | KName => string "Name"
-      | KRecord k => box [string "{", p_kind k, string "}"]
+      | KRecord k => box [string "{", p_kind env k, string "}"]
       | KUnit => string "Unit"
       | KTuple ks => box [string "(",
-                          p_list_sep (box [space, string "*", space]) p_kind ks,
+                          p_list_sep (box [space, string "*", space]) (p_kind env) ks,
                           string ")"]
 
       | KError => string "<ERROR>"
-      | KUnif (_, _, ref (SOME k)) => p_kind' par k
+      | KUnif (_, _, ref (SOME k)) => p_kind' par env k
       | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
 
+      | KRel n => ((if !debug then
+                         string (E.lookupKRel env n ^ "_" ^ Int.toString n)
+                     else
+                         string (E.lookupKRel env n))
+                    handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
+      | KFun (x, k) => box [string x,
+                            space,
+                            string "-->",
+                            space,
+                            p_kind (E.pushKRel env x) k]
+
 and p_kind k = p_kind' false k
 
 fun p_explicitness e =
@@ -66,7 +77,7 @@ fun p_explicitness e =
 
 fun p_con' par env (c, _) =
     case c of
-        TFun (t1, t2) => parenIf par (box [p_con' true env t1,
+        TFun (t1, t2) => parenIf true (box [p_con' true env t1,
                                            space,
                                            string "->",
                                            space,
@@ -75,20 +86,22 @@ fun p_con' par env (c, _) =
                                                 space,
                                                 p_explicitness e,
                                                 space,
-                                                p_kind k,
+                                                p_kind env k,
                                                 space,
                                                 string "->",
                                                 space,
                                                 p_con (E.pushCRel env x k) c])
-      | CDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1,
-                                                       space,
-                                                       string "~",
-                                                       space,
-                                                       p_con env c2,
-                                                       space,
-                                                       string "=>",
-                                                       space,
-                                                       p_con env c3])
+      | CDisjoint (ai, c1, c2, c3) => parenIf par (box [p_con env c1,
+                                                        space,
+                                                        string (case ai of
+                                                                    Instantiate => "~"
+                                                                  | LeaveAlone => "~~"),
+                                                        space,
+                                                        p_con env c2,
+                                                        space,
+                                                        string "=>",
+                                                        space,
+                                                        p_con env c3])
       | TRecord (CRecord (_, xcs), _) => box [string "{",
                                               p_list (fn (x, c) =>
                                                          box [p_name env x,
@@ -134,7 +147,7 @@ fun p_con' par env (c, _) =
                                              space,
                                              string "::",
                                              space,
-                                             p_kind k,
+                                             p_kind env k,
                                              space,
                                              string "=>",
                                              space,
@@ -152,7 +165,7 @@ fun p_con' par env (c, _) =
                                               space,
                                               p_con env c]) xcs,
                               string "]::",
-                              p_kind k])
+                              p_kind env k])
         else
             parenIf par (box [string "[",
                               p_list (fn (x, c) =>
@@ -181,8 +194,24 @@ fun p_con' par env (c, _) =
       | CError => string "<ERROR>"
       | CUnif (_, _, _, ref (SOME c)) => p_con' par env c
       | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
-                                   p_kind k,
+                                   p_kind env k,
                                    string ">"]
+
+      | CKAbs (x, c) => box [string x,
+                             space,
+                             string "==>",
+                             space,
+                             p_con (E.pushKRel env x) c]
+      | CKApp (c, k) => box [p_con env c,
+                             string "[[",
+                             p_kind env k,
+                             string "]]"]
+      | TKFun (x, c) => box [string x,
+                             space,
+                             string "-->",
+                             space,
+                             p_con (E.pushKRel env x) c]
+
         
 and p_con env = p_con' false env
 
@@ -286,7 +315,7 @@ fun p_exp' par env (e, _) =
                                                   space,
                                                   p_explicitness exp,
                                                   space,
-                                                  p_kind k,
+                                                  p_kind env k,
                                                   space,
                                                   string "=>",
                                                   space,
@@ -377,8 +406,6 @@ fun p_exp' par env (e, _) =
                               space,
                               p_con' true env c])
 
-      | EFold _ => string "fold"
-
       | ECase (e, pes, _) => parenIf par (box [string "case",
                                                space,
                                                p_exp env e,
@@ -415,6 +442,16 @@ fun p_exp' par env (e, _) =
                  string "end"]
         end
 
+      | EKAbs (x, e) => box [string x,
+                             space,
+                             string "==>",
+                             space,
+                             p_exp (E.pushKRel env x) e]
+      | EKApp (e, k) => box [p_exp env e,
+                             string "[[",
+                             p_kind env k,
+                             string "]]"]
+
 and p_exp env = p_exp' false env
 
 and p_edecl env (dAll as (d, _)) =
@@ -478,14 +515,14 @@ fun p_sgn_item env (sgi, _) =
                                     space,
                                     string "::",
                                     space,
-                                    p_kind k]
+                                    p_kind env k]
       | SgiCon (x, n, k, c) => box [string "con",
                                     space,
                                     p_named x n,
                                     space,
                                     string "::",
                                     space,
-                                    p_kind k,
+                                    p_kind env k,
                                     space,
                                     string "=",
                                     space,
@@ -540,14 +577,14 @@ fun p_sgn_item env (sgi, _) =
                                       space,
                                       string "::",
                                       space,
-                                      p_kind k]
+                                      p_kind env k]
       | SgiClass (x, n, k, c) => box [string "class",
                                       space,
                                       p_named x n,
                                       space,
                                       string "::",
                                       space,
-                                      p_kind k,
+                                      p_kind env k,
                                       space,
                                       string "=",
                                       space,
@@ -627,7 +664,7 @@ fun p_decl env (dAll as (d, _) : decl) =
                                   space,
                                   string "::",
                                   space,
-                                  p_kind k,
+                                  p_kind env k,
                                   space,
                                   string "=",
                                   space,
@@ -719,7 +756,7 @@ fun p_decl env (dAll as (d, _) : decl) =
                                     space,
                                     string "::",
                                     space,
-                                    p_kind k,
+                                    p_kind env k,
                                     space,
                                     string "=",
                                     space,