Mercurial > urweb

changeset 213:0343557355fc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Explifying type classes
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 14:45:23 -0400
parents ba4d7c33a45f
children 766b5475477f
files src/corify.sml src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/expl.sml src/expl_print.sml src/expl_util.sml src/explify.sml
diffstat 10 files changed, 63 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/corify.sml	Sat Aug 16 14:36:17 2008 -0400
+++ b/src/corify.sml	Sat Aug 16 14:45:23 2008 -0400
@@ -380,6 +380,7 @@
        | 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 @@
        | 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
--- a/src/elab.sml	Sat Aug 16 14:36:17 2008 -0400
+++ b/src/elab.sml	Sat Aug 16 14:45:23 2008 -0400
@@ -150,6 +150,7 @@
        | 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
--- a/src/elab_env.sml	Sat Aug 16 14:36:17 2008 -0400
+++ b/src/elab_env.sml	Sat Aug 16 14:45:23 2008 -0400
@@ -958,5 +958,12 @@
         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
--- a/src/elab_print.sml	Sat Aug 16 14:36:17 2008 -0400
+++ b/src/elab_print.sml	Sat Aug 16 14:45:23 2008 -0400
@@ -630,6 +630,13 @@
                                     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
--- a/src/elab_util.sml	Sat Aug 16 14:36:17 2008 -0400
+++ b/src/elab_util.sml	Sat Aug 16 14:45:23 2008 -0400
@@ -634,7 +634,9 @@
                                                  | 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 @@
                         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' =>
--- a/src/elaborate.sml	Sat Aug 16 14:36:17 2008 -0400
+++ b/src/elaborate.sml	Sat Aug 16 14:45:23 2008 -0400
@@ -2235,6 +2235,7 @@
       | 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 @@
             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) =
--- a/src/expl.sml	Sat Aug 16 14:36:17 2008 -0400
+++ b/src/expl.sml	Sat Aug 16 14:45:23 2008 -0400
@@ -34,6 +34,7 @@
        | KArrow of kind * kind
        | KName
        | KUnit
+       | KTuple of kind list
        | KRecord of kind
 
 withtype kind = kind' located
@@ -57,6 +58,9 @@
 
        | CUnit
 
+       | CTuple of con list
+       | CProj of con * int
+
 withtype con = con' located
 
 datatype datatype_kind = datatype Elab.datatype_kind
--- a/src/expl_print.sml	Sat Aug 16 14:36:17 2008 -0400
+++ b/src/expl_print.sml	Sat Aug 16 14:45:23 2008 -0400
@@ -49,6 +49,9 @@
       | 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 @@
                                               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
 
--- a/src/expl_util.sml	Sat Aug 16 14:36:17 2008 -0400
+++ b/src/expl_util.sml	Sat Aug 16 14:45:23 2008 -0400
@@ -57,6 +57,11 @@
                            (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 @@
                                        (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
--- a/src/explify.sml	Sat Aug 16 14:36:17 2008 -0400
+++ b/src/explify.sml	Sat Aug 16 14:45:23 2008 -0400
@@ -39,7 +39,7 @@
       | 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 @@
 
       | 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 @@
       | 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