Explifying type classes

10 files changed, 63 insertions, 5 deletions

diff --git a/src/corify.sml b/src/corify.sml
index eb46eec8..1badcb9a 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -380,6 +380,7 @@ structure St : sig
        | L.KName => (L'.KName, loc)
        | L.KRecord k => (L'.KRecord (corifyKind k), loc)
        | L.KUnit => (L'.KUnit, loc)
+       | L.KTuple _ => raise Fail "Corify KTuple"
 
  fun corifyCon st (c, loc) =
      case c of
@@ -413,6 +414,9 @@ structure St : sig
        | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
        | L.CUnit => (L'.CUnit, loc)
 
+       | L.CTuple _ => raise Fail "Corify CTuple"
+       | L.CProj _ => raise Fail "Corify CProj"
+
  fun corifyPatCon st pc =
      case pc of
          L.PConVar n => St.lookupConstructorById st n
diff --git a/src/elab.sml b/src/elab.sml
index ec8a811d..10f9bba6 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -150,6 +150,7 @@ datatype decl' =
        | DConstraint of con * con
        | DExport of int * sgn * str
        | DTable of int * string * int * con
+       | DClass of string * int * con
 
      and str' =
          StrConst of decl list
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 47868e3c..b9ab587e 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -958,5 +958,12 @@ fun declBinds env (d, loc) =
         in
             pushENamedAs env x n t
         end
+      | DClass (x, n, c) =>
+        let
+            val k = (KArrow ((KType, loc), (KType, loc)), loc)
+            val env = pushCNamedAs env x n k (SOME c)
+        in
+            pushClass env n
+        end
 
 end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 73b91b67..12abf6b0 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -630,6 +630,13 @@ fun p_decl env (dAll as (d, _) : decl) =
                                     string ":",
                                     space,
                                     p_con env c]
+      | DClass ( x, n, c) => box [string "class",
+                                  space,
+                                  p_named x n,
+                                  space,
+                                  string "=",
+                                  space,
+                                  p_con env c]
 
 and p_str env (str, _) =
     case str of
diff --git a/src/elab_util.sml b/src/elab_util.sml
index c3ed2d19..1c2ce4bd 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -634,7 +634,9 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                                                  | DExport _ => ctx
                                                  | DTable (tn, x, n, c) =>
                                                    bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc),
-                                                                                c), loc))),
+                                                                                c), loc)))
+                                                 | DClass (x, _, _) =>
+                                                   bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))),
                                                mfd ctx d)) ctx ds,
                      fn ds' => (StrConst ds', loc))
               | StrVar _ => S.return2 strAll
@@ -727,6 +729,11 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
                         fn c' =>
                            (DTable (tn, x, n, c'), loc))
 
+             | DClass (x, n, c) =>
+                S.map2 (mfc ctx c,
+                        fn c' =>
+                           (DClass (x, n, c'), loc))
+
         and mfvi ctx (x, n, c, e) =
             S.bind2 (mfc ctx c,
                   fn c' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index e4369dd4..49498570 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2235,6 +2235,7 @@ fun sgiOfDecl (d, loc) =
       | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
       | L'.DExport _ => []
       | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)]
+      | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)]
 
 fun sgiBindsD (env, denv) (sgi, _) =
     case sgi of
@@ -2941,7 +2942,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
             val env = E.pushClass env n
         in
             checkKind env c' ck k;
-            ([(L'.DCon (x, n, k, c'), loc)], (env, denv, []))
+            ([(L'.DClass (x, n, c'), loc)], (env, denv, []))
         end
 
 and elabStr (env, denv) (str, loc) =
diff --git a/src/expl.sml b/src/expl.sml
index 4ba835ea..0edff46b 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -34,6 +34,7 @@ datatype kind' =
        | KArrow of kind * kind
        | KName
        | KUnit
+       | KTuple of kind list
        | KRecord of kind
 
 withtype kind = kind' located
@@ -57,6 +58,9 @@ datatype con' =
 
        | CUnit
 
+       | CTuple of con list
+       | CProj of con * int
+
 withtype con = con' located
 
 datatype datatype_kind = datatype Elab.datatype_kind
diff --git a/src/expl_print.sml b/src/expl_print.sml
index d3638d18..f854c03d 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -49,6 +49,9 @@ fun p_kind' par (k, _) =
       | KName => string "Name"
       | KRecord k => box [string "{", p_kind k, string "}"]
       | KUnit => string "Unit"
+      | KTuple ks => box [string "(",
+                          p_list_sep (box [space, string "*", space]) p_kind ks,
+                          string ")"]
 
 and p_kind k = p_kind' false k
 
@@ -147,6 +150,13 @@ fun p_con' par env (c, _) =
                                               p_con env c2])
       | CFold _ => string "fold"
       | CUnit => string "()"
+
+      | CTuple cs => box [string "(",
+                          p_list (p_con env) cs,
+                          string ")"]
+      | CProj (c, n) => box [p_con env c,
+                             string ".",
+                             string (Int.toString n)]
         
 and p_con env = p_con' false env
 
diff --git a/src/expl_util.sml b/src/expl_util.sml
index ef82af44..a90e6bed 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -57,6 +57,11 @@ fun mapfold f =
                            (KRecord k', loc))
 
               | KUnit => S.return2 kAll
+
+              | KTuple ks =>
+                S.map2 (ListUtil.mapfold mfk ks,
+                        fn ks' =>
+                           (KTuple ks', loc))
     in
         mfk
     end
@@ -148,6 +153,16 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                                        (CFold (k1', k2'), loc)))
 
               | CUnit => S.return2 cAll
+
+              | CTuple cs =>
+                S.map2 (ListUtil.mapfold (mfc ctx) cs,
+                        fn cs' =>
+                           (CTuple cs', loc))
+
+              | CProj (c, n) =>
+                S.map2 (mfc ctx c,
+                        fn c' =>
+                           (CProj (c', n), loc))
     in
         mfc
     end
diff --git a/src/explify.sml b/src/explify.sml
index 50a1851b..f5d19a17 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -39,7 +39,7 @@ fun explifyKind (k, loc) =
       | L.KRecord k => (L'.KRecord (explifyKind k), loc)
 
       | L.KUnit => (L'.KUnit, loc)
-      | L.KTuple _ => raise Fail "Explify KTuple"
+      | L.KTuple ks => (L'.KTuple (map explifyKind ks), loc)
 
       | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc)
       | L.KUnif (_, _, ref (SOME k)) => explifyKind k
@@ -68,8 +68,8 @@ fun explifyCon (c, loc) =
 
       | L.CUnit => (L'.CUnit, loc)
 
-      | L.CTuple _ => raise Fail "Explify CTuple"
-      | L.CProj _ => raise Fail "Explify CProj"
+      | L.CTuple cs => (L'.CTuple (map explifyCon cs), loc)
+      | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc)
 
       | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
       | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c
@@ -160,6 +160,8 @@ fun explifyDecl (d, loc : EM.span) =
       | L.DConstraint (c1, c2) => NONE
       | L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc)
       | L.DTable _ => raise Fail "Explify DTable"
+      | L.DClass (x, n, c) => SOME (L'.DCon (x, n,
+                                             (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), explifyCon c), loc)
 
 and explifyStr (str, loc) =
     case str of