changeset 246:3aa010e97db9

Explify tables
author Adam Chlipala <adamc@hcoop.net>
date Sun, 31 Aug 2008 08:46:22 -0400
parents 1e24a3e6d614
children 5c50b17f5e4a
files src/corify.sml src/expl.sml src/expl_env.sml src/expl_print.sml src/expl_util.sml src/explify.sml
diffstat 6 files changed, 41 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/corify.sml	Sun Aug 31 08:35:00 2008 -0400
+++ b/src/corify.sml	Sun Aug 31 08:46:22 2008 -0400
@@ -806,6 +806,8 @@
              end
            | _ => raise Fail "Non-const signature for 'export'")
 
+      | L.DTable _ => raise Fail "Corify DTable"
+
 and corifyStr ((str, _), st) =
     case str of
         L.StrConst ds =>
@@ -855,7 +857,8 @@
                              | L.DSgn (_, n', _) => Int.max (n, n')
                              | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))
                              | L.DFfiStr (_, n', _) => Int.max (n, n')
-                             | L.DExport _ => n)
+                             | L.DExport _ => n
+                             | L.DTable (_, _, n', _) => Int.max (n, n'))
                  0 ds
 
 and maxNameStr (str, _) =
--- a/src/expl.sml	Sun Aug 31 08:35:00 2008 -0400
+++ b/src/expl.sml	Sun Aug 31 08:46:22 2008 -0400
@@ -107,6 +107,7 @@
        | SgiVal of string * int * con
        | SgiSgn of string * int * sgn
        | SgiStr of string * int * sgn
+       | SgiTable of int * string * int * con
 
 and sgn' =
     SgnConst of sgn_item list
@@ -128,6 +129,7 @@
        | DStr of string * int * sgn * str
        | DFfiStr of string * int * sgn
        | DExport of int * sgn * str
+       | DTable of int * string * int * con
 
      and str' =
          StrConst of decl list
--- a/src/expl_env.sml	Sun Aug 31 08:35:00 2008 -0400
+++ b/src/expl_env.sml	Sun Aug 31 08:46:22 2008 -0400
@@ -282,6 +282,12 @@
       | DStr (x, n, sgn, _) => pushStrNamed env x n sgn
       | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn
       | DExport _ => env
+      | DTable (tn, x, n, c) =>
+        let
+            val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
+        in
+            pushENamed env x n t
+        end
 
 fun sgiBinds env (sgi, loc) =
     case sgi of
@@ -328,4 +334,11 @@
       | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
       | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
 
+      | SgiTable (tn, x, n, c) =>
+        let
+            val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
+        in
+            pushENamed env x n t
+        end
+
 end
--- a/src/expl_print.sml	Sun Aug 31 08:35:00 2008 -0400
+++ b/src/expl_print.sml	Sun Aug 31 08:46:22 2008 -0400
@@ -417,6 +417,13 @@
                                    string "=",
                                    space,
                                    p_sgn env sgn]
+      | SgiTable (_, x, n, c) => box [string "table",
+                                      space,
+                                      p_named x n,
+                                      space,
+                                      string ":",
+                                      space,
+                                      p_con env c]
 
 and p_sgn env (sgn, loc) =
     case sgn of
@@ -558,6 +565,13 @@
                                       string ":",
                                       space,
                                       p_sgn env sgn]
+      | DTable (_, x, n, c) => box [string "table",
+                                    space,
+                                    p_named x n,
+                                    space,
+                                    string ":",
+                                    space,
+                                    p_con env c]
 
 and p_str env (str, _) =
     case str of
--- a/src/expl_util.sml	Sun Aug 31 08:35:00 2008 -0400
+++ b/src/expl_util.sml	Sun Aug 31 08:46:22 2008 -0400
@@ -412,6 +412,10 @@
                 S.map2 (sg ctx s,
                      fn s' =>
                         (SgiSgn (x, n, s'), loc))
+              | SgiTable (tn, x, n, c) =>
+                S.map2 (con ctx c,
+                        fn c' =>
+                           (SgiTable (tn, x, n, c'), loc))
 
         and sg ctx s acc =
             S.bindP (sg' ctx s acc, sgn ctx)
@@ -433,7 +437,8 @@
                                                  | SgiStr (x, _, sgn) =>
                                                    bind (ctx, Str (x, sgn))
                                                  | SgiSgn (x, _, sgn) =>
-                                                   bind (ctx, Sgn (x, sgn)),
+                                                   bind (ctx, Sgn (x, sgn))
+                                                 | SgiTable _ => ctx,
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
--- a/src/explify.sml	Sun Aug 31 08:35:00 2008 -0400
+++ b/src/explify.sml	Sun Aug 31 08:46:22 2008 -0400
@@ -129,7 +129,7 @@
       | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
       | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
       | L.SgiConstraint _ => NONE
-      | L.SgiTable _ => raise Fail "Explify SgiTable"
+      | L.SgiTable (nt, x, n, c) => SOME (L'.SgiTable (nt, x, n, explifyCon c), loc)
       | L.SgiClassAbs (x, n) => SOME (L'.SgiConAbs (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)), loc)
       | L.SgiClass (x, n, c) => SOME (L'.SgiCon (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc),
                                                  explifyCon c), loc)
@@ -161,7 +161,7 @@
       | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc)
       | 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.DTable (nt, x, n, c) => SOME (L'.DTable (nt, x, n, explifyCon c), loc)
       | L.DClass (x, n, c) => SOME (L'.DCon (x, n,
                                              (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), explifyCon c), loc)