# HG changeset patch # User Adam Chlipala # Date 1220367101 14400 # Node ID 42dfb0d61cf06714ccfd542a72f12367fa2d9d44 # Parent b9b02613c0c2170a491e188f8b6e84f4fa77de85 'database' declaration threaded through compiler diff -r b9b02613c0c2 -r 42dfb0d61cf0 src/cjr.sml --- a/src/cjr.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/cjr.sml Tue Sep 02 10:51:41 2008 -0400 @@ -87,6 +87,7 @@ | 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/cjr_env.sml --- a/src/cjr_env.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/cjr_env.sml Tue Sep 02 10:51:41 2008 -0400 @@ -162,6 +162,7 @@ in pushENamed env fx n t end) env vis + | DDatabase _ => env end diff -r b9b02613c0c2 -r 42dfb0d61cf0 src/cjr_print.sml --- a/src/cjr_print.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/cjr_print.sml Tue Sep 02 10:51:41 2008 -0400 @@ -709,6 +709,9 @@ 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/cjrize.sml --- a/src/cjrize.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/cjrize.sml Tue Sep 02 10:51:41 2008 -0400 @@ -423,6 +423,8 @@ (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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/compiler.sml --- a/src/compiler.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/compiler.sml Tue Sep 02 10:51:41 2008 -0400 @@ -230,6 +230,7 @@ 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 @@ 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/core.sml --- a/src/core.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/core.sml Tue Sep 02 10:51:41 2008 -0400 @@ -115,6 +115,7 @@ | 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/core_env.sml --- a/src/core_env.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/core_env.sml Tue Sep 02 10:51:41 2008 -0400 @@ -193,6 +193,7 @@ in pushENamed env x n t NONE s end + | DDatabase _ => env fun patBinds env (p, loc) = case p of diff -r b9b02613c0c2 -r 42dfb0d61cf0 src/core_print.sml --- a/src/core_print.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/core_print.sml Tue Sep 02 10:51:41 2008 -0400 @@ -446,6 +446,9 @@ string ":", space, p_con env c] + | DDatabase s => box [string "database", + space, + string s] fun p_file env file = let diff -r b9b02613c0c2 -r 42dfb0d61cf0 src/core_util.sml --- a/src/core_util.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/core_util.sml Tue Sep 02 10:51:41 2008 -0400 @@ -631,6 +631,7 @@ 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 @@ in bind (ctx, NamedE (x, n, t, NONE, s)) end + | DDatabase _ => ctx in S.map2 (mff ctx' ds', fn ds' => @@ -767,7 +769,8 @@ | 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/corify.sml --- a/src/corify.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/corify.sml Tue Sep 02 10:51:41 2008 -0400 @@ -863,6 +863,8 @@ ([(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 @@ | 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/elab.sml --- a/src/elab.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/elab.sml Tue Sep 02 10:51:41 2008 -0400 @@ -152,6 +152,7 @@ | 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/elab_env.sml --- a/src/elab_env.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/elab_env.sml Tue Sep 02 10:51:41 2008 -0400 @@ -1048,6 +1048,7 @@ in pushClass env n end + | DDatabase _ => env fun patBinds env (p, loc) = case p of diff -r b9b02613c0c2 -r 42dfb0d61cf0 src/elab_print.sml --- a/src/elab_print.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/elab_print.sml Tue Sep 02 10:51:41 2008 -0400 @@ -632,13 +632,16 @@ 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/elab_util.sml --- a/src/elab_util.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/elab_util.sml Tue Sep 02 10:51:41 2008 -0400 @@ -638,7 +638,8 @@ 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 @@ 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/elaborate.sml --- a/src/elaborate.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/elaborate.sml Tue Sep 02 10:51:41 2008 -0400 @@ -2361,6 +2361,7 @@ | 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 @@ 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/expl.sml --- a/src/expl.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/expl.sml Tue Sep 02 10:51:41 2008 -0400 @@ -130,6 +130,7 @@ | 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/expl_print.sml --- a/src/expl_print.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/expl_print.sml Tue Sep 02 10:51:41 2008 -0400 @@ -572,6 +572,9 @@ string ":", space, p_con env c] + | DDatabase s => box [string "database", + space, + string s] and p_str env (str, _) = case str of diff -r b9b02613c0c2 -r 42dfb0d61cf0 src/explify.sml --- a/src/explify.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/explify.sml Tue Sep 02 10:51:41 2008 -0400 @@ -164,6 +164,7 @@ | 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/mono.sml --- a/src/mono.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/mono.sml Tue Sep 02 10:51:41 2008 -0400 @@ -90,6 +90,7 @@ | 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/mono_env.sml --- a/src/mono_env.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/mono_env.sml Tue Sep 02 10:51:41 2008 -0400 @@ -107,6 +107,7 @@ | 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/mono_print.sml --- a/src/mono_print.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/mono_print.sml Tue Sep 02 10:51:41 2008 -0400 @@ -312,6 +312,10 @@ string "(", p_typ env t, string ")"]) ts] + + | DDatabase s => box [string "database", + space, + string s] fun p_file env file = let diff -r b9b02613c0c2 -r 42dfb0d61cf0 src/mono_shake.sml --- a/src/mono_shake.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/mono_shake.sml Tue Sep 02 10:51:41 2008 -0400 @@ -53,7 +53,8 @@ (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 @@ 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/mono_util.sml --- a/src/mono_util.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/mono_util.sml Tue Sep 02 10:51:41 2008 -0400 @@ -342,6 +342,7 @@ 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 @@ | 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/monoize.sml --- a/src/monoize.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/monoize.sml Tue Sep 02 10:51:41 2008 -0400 @@ -1423,6 +1423,7 @@ 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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/shake.sml --- a/src/shake.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/shake.sml Tue Sep 02 10:51:41 2008 -0400 @@ -59,7 +59,8 @@ (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 @@ | (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 -r b9b02613c0c2 -r 42dfb0d61cf0 src/source.sml --- a/src/source.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/source.sml Tue Sep 02 10:51:41 2008 -0400 @@ -142,6 +142,7 @@ | DExport of str | DTable of string * con | DClass of string * con + | DDatabase of string and str' = StrConst of decl list diff -r b9b02613c0c2 -r 42dfb0d61cf0 src/source_print.sml --- a/src/source_print.sml Tue Sep 02 10:31:16 2008 -0400 +++ b/src/source_print.sml Tue Sep 02 10:51:41 2008 -0400 @@ -550,6 +550,10 @@ space, p_con c] + | DDatabase s => box [string "database", + space, + string s] + and p_str (str, _) = case str of StrConst ds => box [string "struct",