From b4398c433195b75d5e03d0774b1128fae14e9f41 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 2 Sep 2008 10:51:41 -0400 Subject: 'database' declaration threaded through compiler --- src/cjr.sml | 1 + src/cjr_env.sml | 1 + src/cjr_print.sml | 3 +++ src/cjrize.sml | 2 ++ src/compiler.sml | 7 ++++++- src/core.sml | 1 + src/core_env.sml | 1 + src/core_print.sml | 3 +++ src/core_util.sml | 5 ++++- src/corify.sml | 5 ++++- src/elab.sml | 1 + src/elab_env.sml | 1 + src/elab_print.sml | 17 ++++++++++------- src/elab_util.sml | 5 ++++- src/elaborate.sml | 3 +++ src/expl.sml | 1 + src/expl_print.sml | 3 +++ src/explify.sml | 1 + src/mono.sml | 1 + src/mono_env.sml | 1 + src/mono_print.sml | 4 ++++ src/mono_shake.sml | 6 ++++-- src/mono_util.sml | 2 ++ src/monoize.sml | 1 + src/shake.sml | 6 ++++-- src/source.sml | 1 + src/source_print.sml | 4 ++++ 27 files changed, 72 insertions(+), 15 deletions(-) (limited to 'src') diff --git a/src/cjr.sml b/src/cjr.sml index e9b89bfc..727874a9 100644 --- a/src/cjr.sml +++ b/src/cjr.sml @@ -87,6 +87,7 @@ datatype decl' = | DVal of string * int * typ * exp | DFun of string * int * (string * typ) list * typ * exp | DFunRec of (string * int * (string * typ) list * typ * exp) list + | DDatabase of string withtype decl = decl' located diff --git a/src/cjr_env.sml b/src/cjr_env.sml index 331af45f..609bb699 100644 --- a/src/cjr_env.sml +++ b/src/cjr_env.sml @@ -162,6 +162,7 @@ fun declBinds env (d, loc) = in pushENamed env fx n t end) env vis + | DDatabase _ => env end diff --git a/src/cjr_print.sml b/src/cjr_print.sml index 4a65cd34..cefcad44 100644 --- a/src/cjr_print.sml +++ b/src/cjr_print.sml @@ -709,6 +709,9 @@ fun p_decl env (dAll as (d, _) : decl) = p_list_sep newline (p_fun env) vis, newline] end + | DDatabase s => box [string "database", + space, + string s] datatype 'a search = Found of 'a diff --git a/src/cjrize.sml b/src/cjrize.sml index 29182e2c..c4c77021 100644 --- a/src/cjrize.sml +++ b/src/cjrize.sml @@ -423,6 +423,8 @@ fun cifyDecl ((d, loc), sm) = (NONE, SOME (ek, "/" ^ s, n, ts), sm) end + | L.DDatabase s => (SOME (L'.DDatabase s, loc), NONE, sm) + fun cjrize ds = let val (dsF, ds, ps, sm) = foldl (fn (d, (dsF, ds, ps, sm)) => diff --git a/src/compiler.sml b/src/compiler.sml index 1f9da052..07bfecc2 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -230,6 +230,7 @@ val parseUrp = { val fname = String.implode (List.filter (fn x => not (Char.isSpace x)) (String.explode line)) val fname = OS.Path.concat (dir, fname) + handle OS.Path.Path => fname in fname :: acc end @@ -301,8 +302,12 @@ val parse = { in let val final = nameOf (List.last fnames) + + val ds = ds @ [(Source.DExport (Source.StrVar final, ErrorMsg.dummySpan), ErrorMsg.dummySpan)] in - ds @ [(Source.DExport (Source.StrVar final, ErrorMsg.dummySpan), ErrorMsg.dummySpan)] + case database of + NONE => ds + | SOME s => (Source.DDatabase s, ErrorMsg.dummySpan) :: ds end handle Empty => ds end, print = SourcePrint.p_file diff --git a/src/core.sml b/src/core.sml index a5af04cc..0eef7e96 100644 --- a/src/core.sml +++ b/src/core.sml @@ -115,6 +115,7 @@ datatype decl' = | DValRec of (string * int * con * exp * string) list | DExport of export_kind * int | DTable of string * int * con * string + | DDatabase of string withtype decl = decl' located diff --git a/src/core_env.sml b/src/core_env.sml index d0ae8a86..e2a3c40f 100644 --- a/src/core_env.sml +++ b/src/core_env.sml @@ -193,6 +193,7 @@ fun declBinds env (d, loc) = in pushENamed env x n t NONE s end + | DDatabase _ => env fun patBinds env (p, loc) = case p of diff --git a/src/core_print.sml b/src/core_print.sml index a5d3df95..0d5a61c1 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -446,6 +446,9 @@ fun p_decl env (dAll as (d, _) : decl) = string ":", space, p_con env c] + | DDatabase s => box [string "database", + space, + string s] fun p_file env file = let diff --git a/src/core_util.sml b/src/core_util.sml index 0b1b4a0b..dfd6fa77 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -631,6 +631,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} = S.map2 (mfc ctx c, fn c' => (DTable (x, n, c', s), loc)) + | DDatabase _ => S.return2 dAll and mfvi ctx (x, n, t, e, s) = S.bind2 (mfc ctx t, @@ -719,6 +720,7 @@ fun mapfoldB (all as {bind, ...}) = in bind (ctx, NamedE (x, n, t, NONE, s)) end + | DDatabase _ => ctx in S.map2 (mff ctx' ds', fn ds' => @@ -767,7 +769,8 @@ val maxName = foldl (fn ((d, _) : decl, count) => | DVal (_, n, _, _, _) => Int.max (n, count) | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis | DExport _ => count - | DTable (_, n, _, _) => Int.max (n, count)) 0 + | DTable (_, n, _, _) => Int.max (n, count) + | DDatabase _ => count) 0 end diff --git a/src/corify.sml b/src/corify.sml index 50d47068..91c82375 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -863,6 +863,8 @@ fun corifyDecl ((d, loc : EM.span), st) = ([(L'.DTable (x, n, corifyCon st c, s), loc)], st) end + | L.DDatabase s => ([(L'.DDatabase s, loc)], st) + and corifyStr ((str, _), st) = case str of L.StrConst ds => @@ -913,7 +915,8 @@ fun maxName ds = foldl (fn ((d, _), n) => | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str)) | L.DFfiStr (_, n', _) => Int.max (n, n') | L.DExport _ => n - | L.DTable (_, _, n', _) => Int.max (n, n')) + | L.DTable (_, _, n', _) => Int.max (n, n') + | L.DDatabase _ => n) 0 ds and maxNameStr (str, _) = diff --git a/src/elab.sml b/src/elab.sml index 30b53064..8e77d773 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -152,6 +152,7 @@ datatype decl' = | DExport of int * sgn * str | DTable of int * string * int * con | DClass of string * int * con + | DDatabase of string and str' = StrConst of decl list diff --git a/src/elab_env.sml b/src/elab_env.sml index a1a68974..89a2b4ff 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -1048,6 +1048,7 @@ fun declBinds env (d, loc) = in pushClass env n end + | DDatabase _ => env fun patBinds env (p, loc) = case p of diff --git a/src/elab_print.sml b/src/elab_print.sml index a0589b7d..f56f57dc 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -632,13 +632,16 @@ 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] + | DClass (x, n, c) => box [string "class", + space, + p_named x n, + space, + string "=", + space, + p_con env c] + | DDatabase s => box [string "database", + space, + string s] and p_str env (str, _) = case str of diff --git a/src/elab_util.sml b/src/elab_util.sml index 327848a3..d0f37a92 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -638,7 +638,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc), c), loc))) | DClass (x, _, _) => - bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))), + bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))) + | DDatabase _ => ctx, mfd ctx d)) ctx ds, fn ds' => (StrConst ds', loc)) | StrVar _ => S.return2 strAll @@ -736,6 +737,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f fn c' => (DClass (x, n, c'), loc)) + | DDatabase _ => S.return2 dAll + 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 27b3e3fe..d4b71b80 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2361,6 +2361,7 @@ fun sgiOfDecl (d, 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)] + | L'.DDatabase _ => [] fun sgiBindsD (env, denv) (sgi, _) = case sgi of @@ -3109,6 +3110,8 @@ fun elabDecl ((d, loc), (env, denv, gs : constraint list)) = checkKind env c' ck k; ([(L'.DClass (x, n, c'), loc)], (env, denv, [])) end + + | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, [])) in r end diff --git a/src/expl.sml b/src/expl.sml index bbc18097..3bb7beff 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -130,6 +130,7 @@ datatype decl' = | DFfiStr of string * int * sgn | DExport of int * sgn * str | DTable of int * string * int * con + | DDatabase of string and str' = StrConst of decl list diff --git a/src/expl_print.sml b/src/expl_print.sml index 7b34c9c3..05e6da02 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -572,6 +572,9 @@ fun p_decl env (dAll as (d, _) : decl) = string ":", space, p_con env c] + | DDatabase s => box [string "database", + space, + string s] and p_str env (str, _) = case str of diff --git a/src/explify.sml b/src/explify.sml index 689c18ca..142ddfcb 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -164,6 +164,7 @@ fun explifyDecl (d, loc : EM.span) = | 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) + | L.DDatabase s => SOME (L'.DDatabase s, loc) and explifyStr (str, loc) = case str of diff --git a/src/mono.sml b/src/mono.sml index ae1b95dc..3b6cc87e 100644 --- a/src/mono.sml +++ b/src/mono.sml @@ -90,6 +90,7 @@ datatype decl' = | DVal of string * int * typ * exp * string | DValRec of (string * int * typ * exp * string) list | DExport of Core.export_kind * string * int * typ list + | DDatabase of string withtype decl = decl' located diff --git a/src/mono_env.sml b/src/mono_env.sml index 6baf8b07..7352400a 100644 --- a/src/mono_env.sml +++ b/src/mono_env.sml @@ -107,6 +107,7 @@ fun declBinds env (d, loc) = | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis | DExport _ => env + | DDatabase _ => env fun patBinds env (p, loc) = case p of diff --git a/src/mono_print.sml b/src/mono_print.sml index 39db4c1c..450c5bee 100644 --- a/src/mono_print.sml +++ b/src/mono_print.sml @@ -312,6 +312,10 @@ fun p_decl env (dAll as (d, _) : decl) = string "(", p_typ env t, string ")"]) ts] + + | DDatabase s => box [string "database", + space, + string s] fun p_file env file = let diff --git a/src/mono_shake.sml b/src/mono_shake.sml index e694c0dd..8276b4d6 100644 --- a/src/mono_shake.sml +++ b/src/mono_shake.sml @@ -53,7 +53,8 @@ fun shake file = (cdef, IM.insert (edef, n, (t, e))) | ((DValRec vis, _), (cdef, edef)) => (cdef, foldl (fn ((_, n, t, e, _), edef) => IM.insert (edef, n, (t, e))) edef vis) - | ((DExport _, _), acc) => acc) + | ((DExport _, _), acc) => acc + | ((DDatabase _, _), acc) => acc) (IM.empty, IM.empty) file fun typ (c, s) = @@ -106,7 +107,8 @@ fun shake file = List.filter (fn (DDatatype (_, n, _), _) => IS.member (#con s, n) | (DVal (_, n, _, _, _), _) => IS.member (#exp s, n) | (DValRec vis, _) => List.exists (fn (_, n, _, _, _) => IS.member (#exp s, n)) vis - | (DExport _, _) => true) file + | (DExport _, _) => true + | (DDatabase _, _) => true) file end end diff --git a/src/mono_util.sml b/src/mono_util.sml index 5ccaf16c..9dddb477 100644 --- a/src/mono_util.sml +++ b/src/mono_util.sml @@ -342,6 +342,7 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} = S.map2 (ListUtil.mapfold mft ts, fn ts' => (DExport (ek, s, n, ts'), loc)) + | DDatabase _ => S.return2 dAll and mfvi ctx (x, n, t, e, s) = S.bind2 (mft t, @@ -404,6 +405,7 @@ fun mapfoldB (all as {bind, ...}) = | DValRec vis => foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s))) ctx vis | DExport _ => ctx + | DDatabase _ => ctx in S.map2 (mff ctx' ds', fn ds' => diff --git a/src/monoize.sml b/src/monoize.sml index 6624c971..f3b34a54 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -1423,6 +1423,7 @@ fun monoDecl (env, fm) (all as (d, loc)) = fm, (L'.DVal (x, n, t', e, s), loc)) end + | L.DDatabase s => SOME (env, fm, (L'.DDatabase s, loc)) end fun monoize env ds = diff --git a/src/shake.sml b/src/shake.sml index 6d8280fe..6395bfdc 100644 --- a/src/shake.sml +++ b/src/shake.sml @@ -59,7 +59,8 @@ fun shake file = (cdef, foldl (fn ((_, n, t, e, _), edef) => IM.insert (edef, n, (t, e))) edef vis) | ((DExport _, _), acc) => acc | ((DTable (_, n, c, _), _), (cdef, edef)) => - (cdef, IM.insert (edef, n, (c, dummye)))) + (cdef, IM.insert (edef, n, (c, dummye))) + | ((DDatabase _, _), acc) => acc) (IM.empty, IM.empty) file fun kind (_, s) = s @@ -114,7 +115,8 @@ fun shake file = | (DVal (_, n, _, _, _), _) => IS.member (#exp s, n) | (DValRec vis, _) => List.exists (fn (_, n, _, _, _) => IS.member (#exp s, n)) vis | (DExport _, _) => true - | (DTable _, _) => true) file + | (DTable _, _) => true + | (DDatabase _, _) => true) file end end diff --git a/src/source.sml b/src/source.sml index f8a12a93..70738c1a 100644 --- a/src/source.sml +++ b/src/source.sml @@ -142,6 +142,7 @@ datatype decl' = | DExport of str | DTable of string * con | DClass of string * con + | DDatabase of string and str' = StrConst of decl list diff --git a/src/source_print.sml b/src/source_print.sml index f98227ec..c37505d0 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -550,6 +550,10 @@ fun p_decl ((d, _) : decl) = space, p_con c] + | DDatabase s => box [string "database", + space, + string s] + and p_str (str, _) = case str of StrConst ds => box [string "struct", -- cgit v1.2.3