Mercurial > urweb
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)