aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/cjr.sml1
-rw-r--r--src/cjr_env.sml1
-rw-r--r--src/cjr_print.sml3
-rw-r--r--src/cjrize.sml2
-rw-r--r--src/compiler.sml7
-rw-r--r--src/core.sml1
-rw-r--r--src/core_env.sml1
-rw-r--r--src/core_print.sml3
-rw-r--r--src/core_util.sml5
-rw-r--r--src/corify.sml5
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_env.sml1
-rw-r--r--src/elab_print.sml17
-rw-r--r--src/elab_util.sml5
-rw-r--r--src/elaborate.sml3
-rw-r--r--src/expl.sml1
-rw-r--r--src/expl_print.sml3
-rw-r--r--src/explify.sml1
-rw-r--r--src/mono.sml1
-rw-r--r--src/mono_env.sml1
-rw-r--r--src/mono_print.sml4
-rw-r--r--src/mono_shake.sml6
-rw-r--r--src/mono_util.sml2
-rw-r--r--src/monoize.sml1
-rw-r--r--src/shake.sml6
-rw-r--r--src/source.sml1
-rw-r--r--src/source_print.sml4
27 files changed, 72 insertions, 15 deletions
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",
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 13:50:08 +0000