summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/cloconv.sml2
-rw-r--r--src/core.sml1
-rw-r--r--src/core_env.sml1
-rw-r--r--src/core_print.sml6
-rw-r--r--src/core_util.sml14
-rw-r--r--src/corify.sml4
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_env.sml1
-rw-r--r--src/elab_print.sml6
-rw-r--r--src/elab_util.sml9
-rw-r--r--src/elaborate.sml38
-rw-r--r--src/expl.sml1
-rw-r--r--src/expl_env.sml1
-rw-r--r--src/expl_print.sml6
-rw-r--r--src/explify.sml1
-rw-r--r--src/lacweb.grm3
-rw-r--r--src/lacweb.lex1
-rw-r--r--src/mono.sml1
-rw-r--r--src/mono_env.sml1
-rw-r--r--src/mono_print.sml15
-rw-r--r--src/mono_util.sml15
-rw-r--r--src/monoize.sml7
-rw-r--r--src/shake.sml101
-rw-r--r--src/source.sml1
-rw-r--r--src/source_print.sml4
25 files changed, 172 insertions, 69 deletions
diff --git a/src/cloconv.sml b/src/cloconv.sml
index d9863cb5..9c1825cc 100644
--- a/src/cloconv.sml
+++ b/src/cloconv.sml
@@ -158,7 +158,6 @@ fun ccExp env ((e, loc), D) =
val body = (L'.ELet ([("env", envT, (L'.EField ((L'.ERel 0, loc), "env"), loc)),
("arg", dom, (L'.EField ((L'.ERel 1, loc), "arg"), loc))],
body), loc)
-
val (D, fi) = Ds.func D (x, (L'.TRecord [("env", envT), ("arg", dom)], loc), ran, body)
in
@@ -198,6 +197,7 @@ fun ccDecl ((d, loc), D) =
in
Ds.exp D (x, n, t, e)
end
+ | L.DPage _ => raise Fail "Cloconv DPage"
fun cloconv ds =
let
diff --git a/src/core.sml b/src/core.sml
index badb08ea..62a5b700 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -79,6 +79,7 @@ withtype exp = exp' located
datatype decl' =
DCon of string * int * kind * con
| DVal of string * int * con * exp
+ | DPage of con * exp
withtype decl = decl' located
diff --git a/src/core_env.sml b/src/core_env.sml
index 1ea687dc..2b6de82c 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -123,5 +123,6 @@ fun declBinds env (d, _) =
case d of
DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
| DVal (x, n, t, e) => pushENamed env x n t (SOME e)
+ | DPage _ => env
end
diff --git a/src/core_print.sml b/src/core_print.sml
index 935cfbac..18d9a7f5 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -272,6 +272,12 @@ fun p_decl env ((d, _) : decl) =
space,
p_exp env e]
end
+ | DPage (c, e) => box [string "page",
+ p_con env c,
+ space,
+ string "=",
+ space,
+ p_exp env e]
fun p_file env file =
let
diff --git a/src/core_util.sml b/src/core_util.sml
index f0a37356..d65f0b87 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -376,6 +376,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
S.map2 (mfe ctx e,
fn e' =>
(DVal (x, n, t', e'), loc)))
+ | DPage (c, e) =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (DPage (c', e'), loc)))
in
mfd
end
@@ -412,11 +418,11 @@ fun mapfoldB (all as {bind, ...}) =
S.bind2 (mfd ctx d,
fn d' =>
let
- val b =
+ val ctx' =
case #1 d' of
- DCon (x, n, k, c) => NamedC (x, n, k, SOME c)
- | DVal (x, n, t, e) => NamedE (x, n, t, SOME e)
- val ctx' = bind (ctx, b)
+ DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
+ | DVal (x, n, t, e) => bind (ctx, NamedE (x, n, t, SOME e))
+ | DPage _ => ctx
in
S.map2 (mff ctx' ds',
fn ds' =>
diff --git a/src/corify.sml b/src/corify.sml
index baff8182..118255b7 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -427,6 +427,7 @@ fun corifyDecl ((d, loc : EM.span), st) =
end
| _ => raise Fail "Non-const signature for FFI structure")
+ | L.DPage (c, e) => ([(L'.DPage (corifyCon st c, corifyExp st e), loc)], st)
and corifyStr ((str, _), st) =
case str of
@@ -473,7 +474,8 @@ fun maxName ds = foldl (fn ((d, _), n) =>
| L.DVal (_, n', _ , _) => Int.max (n, n')
| 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.DFfiStr (_, n', _) => Int.max (n, n')
+ | L.DPage _ => n)
0 ds
and maxNameStr (str, _) =
diff --git a/src/elab.sml b/src/elab.sml
index 9eb8ad2f..9fca4e13 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -115,6 +115,7 @@ datatype decl' =
| DStr of string * int * sgn * str
| DFfiStr of string * int * sgn
| DConstraint of con * con
+ | DPage of con * exp
and str' =
StrConst of decl list
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 897f481d..be49d06f 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -292,6 +292,7 @@ fun declBinds env (d, _) =
| DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
| DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
| DConstraint _ => env
+ | DPage _ => env
fun sgiBinds env (sgi, _) =
case sgi of
diff --git a/src/elab_print.sml b/src/elab_print.sml
index d394c679..51ff6a95 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -450,6 +450,12 @@ fun p_decl env ((d, _) : decl) =
string "~",
space,
p_con env c2]
+ | DPage (c, e) => box [string "page",
+ p_con env c,
+ space,
+ string "=",
+ space,
+ p_exp env e]
and p_str env (str, _) =
case str of
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 9879a9f9..293e53ac 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -510,7 +510,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
bind (ctx, Str (x, sgn))
| DFfiStr (x, _, sgn) =>
bind (ctx, Str (x, sgn))
- | DConstraint _ => ctx,
+ | DConstraint _ => ctx
+ | DPage _ => ctx,
mfd ctx d)) ctx ds,
fn ds' => (StrConst ds', loc))
| StrVar _ => S.return2 strAll
@@ -571,6 +572,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
S.map2 (mfc ctx c2,
fn c2' =>
(DConstraint (c1', c2'), loc)))
+ | DPage (c, e) =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (DPage (c', e'), loc)))
in
mfd
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 2ad3f936..faa19ec4 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1593,12 +1593,13 @@ fun dopenConstraints (loc, env, denv) {str, strs} =
fun sgiOfDecl (d, loc) =
case d of
- L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc)
- | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc)
- | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc)
- | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc)
- | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc)
- | L'.DConstraint cs => (L'.SgiConstraint cs, loc)
+ L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc)
+ | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc)
+ | L'.DSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, sgn), loc)
+ | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
+ | L'.DFfiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, sgn), loc)
+ | L'.DConstraint cs => SOME (L'.SgiConstraint cs, loc)
+ | L'.DPage _ => NONE
fun sgiBindsD (env, denv) (sgi, _) =
case sgi of
@@ -1928,12 +1929,35 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
([], (env, denv, []))
end
+ | L.DPage e =>
+ let
+ val basis =
+ case E.lookupStr env "Basis" of
+ NONE => raise Fail "elabExp: Unbound Basis"
+ | SOME (n, _) => n
+
+ val (e', t, gs1) = elabExp (env, denv) e
+
+ val k = (L'.KRecord (L'.KType, loc), loc)
+ val vs = cunif (loc, k)
+
+ val c = (L'.TFun ((L'.TRecord vs, loc),
+ (L'.CApp ((L'.CModProj (basis, [], "xml"), loc),
+ (L'.CRecord ((L'.KUnit, loc),
+ [((L'.CName "Html", loc),
+ (L'.CUnit, loc))]), loc)), loc)), loc)
+
+ val gs2 = checkCon (env, denv) e' t c
+ in
+ ([(L'.DPage (vs, e'), loc)], (env, denv, gs1 @ gs2))
+ end
+
and elabStr (env, denv) (str, loc) =
case str of
L.StrConst ds =>
let
val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
- val sgis = map sgiOfDecl ds'
+ val sgis = List.mapPartial sgiOfDecl ds'
val (sgis, _, _, _, _) =
foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
diff --git a/src/expl.sml b/src/expl.sml
index b3bcf96b..bf40a511 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -98,6 +98,7 @@ datatype decl' =
| DSgn of string * int * sgn
| DStr of string * int * sgn * str
| DFfiStr of string * int * sgn
+ | DPage of con * exp
and str' =
StrConst of decl list
diff --git a/src/expl_env.sml b/src/expl_env.sml
index ad4ec00b..93d21c31 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -243,6 +243,7 @@ fun declBinds env (d, _) =
| DSgn (x, n, sgn) => pushSgnNamed env x n sgn
| DStr (x, n, sgn, _) => pushStrNamed env x n sgn
| DFfiStr (x, n, sgn) => pushStrNamed env x n sgn
+ | DPage _ => env
fun sgiBinds env (sgi, _) =
case sgi of
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 447845a2..c891528f 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -392,6 +392,12 @@ fun p_decl env ((d, _) : decl) =
string ":",
space,
p_sgn env sgn]
+ | DPage (c, e) => box [string "page",
+ p_con env c,
+ space,
+ string "=",
+ space,
+ p_exp env e]
and p_str env (str, _) =
case str of
diff --git a/src/explify.sml b/src/explify.sml
index c5e7fbd4..8c6cc9f5 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -116,6 +116,7 @@ fun explifyDecl (d, loc : EM.span) =
| L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc)
| L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc)
| L.DConstraint (c1, c2) => NONE
+ | L.DPage (c, e) => SOME (L'.DPage (explifyCon c, explifyExp e), loc)
and explifyStr (str, loc) =
case str of
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 4c721cc0..811876f2 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -46,7 +46,7 @@ val s = ErrorMsg.spanOf
| ARROW | LARROW | DARROW
| FN | PLUSPLUS | DOLLAR | TWIDDLE
| STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN
- | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS
+ | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | PAGE
| XML_BEGIN of string | XML_END
| NOTAGS of string
@@ -140,6 +140,7 @@ decl : CON SYMBOL EQ cexp (DCon (SYMBOL, NONE, cexp), s (CONleft,
[] => raise Fail "Impossible mpath parse [3]"
| m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright)))
| CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
+ | PAGE eexp (DPage eexp, s (PAGEleft, eexpright))
sgn : sgntm (sgntm)
| FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 3fc6577c..8a57dba9 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -261,6 +261,7 @@ notags = [^<{\n]+;
<INITIAL> "open" => (Tokens.OPEN (pos yypos, pos yypos + size yytext));
<INITIAL> "constraint"=> (Tokens.CONSTRAINT (pos yypos, pos yypos + size yytext));
<INITIAL> "constraints"=> (Tokens.CONSTRAINTS (pos yypos, pos yypos + size yytext));
+<INITIAL> "page" => (Tokens.PAGE (pos yypos, pos yypos + size yytext));
<INITIAL> "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext));
<INITIAL> "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext));
diff --git a/src/mono.sml b/src/mono.sml
index 39de583c..21d1cbe3 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -56,6 +56,7 @@ withtype exp = exp' located
datatype decl' =
DVal of string * int * typ * exp
+ | DPage of (string * typ) list * exp
withtype decl = decl' located
diff --git a/src/mono_env.sml b/src/mono_env.sml
index 66396264..cfe7b159 100644
--- a/src/mono_env.sml
+++ b/src/mono_env.sml
@@ -84,5 +84,6 @@ fun lookupENamed (env : env) n =
fun declBinds env (d, _) =
case d of
DVal (x, n, t, e) => pushENamed env x n t (SOME e)
+ | DPage _ => env
end
diff --git a/src/mono_print.sml b/src/mono_print.sml
index c0847019..b3c5f3a5 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -143,7 +143,20 @@ fun p_decl env ((d, _) : decl) =
space,
p_exp env e]
end
-
+ | DPage (xcs, e) => box [string "page",
+ string "[",
+ p_list (fn (x, t) =>
+ box [string x,
+ space,
+ string ":",
+ space,
+ p_typ env t]) xcs,
+ string "]",
+ space,
+ string "=",
+ space,
+ p_exp env e]
+
fun p_file env file =
let
val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
diff --git a/src/mono_util.sml b/src/mono_util.sml
index 54eb9be7..cde2d57a 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -205,6 +205,15 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
S.map2 (mfe ctx e,
fn e' =>
(DVal (x, n, t', e'), loc)))
+ | DPage (xts, e) =>
+ S.bind2 (ListUtil.mapfold (fn (x, t) =>
+ S.map2 (mft t,
+ fn t' =>
+ (x, t'))) xts,
+ fn xts' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (DPage (xts', e'), loc)))
in
mfd
end
@@ -239,10 +248,10 @@ fun mapfoldB (all as {bind, ...}) =
S.bind2 (mfd ctx d,
fn d' =>
let
- val b =
+ val ctx' =
case #1 d' of
- DVal (x, n, t, e) => NamedE (x, n, t, SOME e)
- val ctx' = bind (ctx, b)
+ DVal (x, n, t, e) => bind (ctx, NamedE (x, n, t, SOME e))
+ | DPage _ => ctx
in
S.map2 (mff ctx' ds',
fn ds' =>
diff --git a/src/monoize.sml b/src/monoize.sml
index e5d7c374..29e94b3f 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -164,6 +164,13 @@ fun monoDecl env (all as (d, loc)) =
L.DCon _ => NONE
| L.DVal (x, n, t, e) => SOME (Env.pushENamed env x n t (SOME e),
(L'.DVal (x, n, monoType env t, monoExp env e), loc))
+ | L.DPage ((c, _), e) =>
+ (case c of
+ L.CRecord (_, vs) => SOME (env,
+ (L'.DPage (map (fn (nm, t) => (monoName env nm,
+ monoType env t)) vs,
+ monoExp env e), loc))
+ | _ => poly ())
end
fun monoize env ds =
diff --git a/src/shake.sml b/src/shake.sml
index e51d7013..36657dfc 100644
--- a/src/shake.sml
+++ b/src/shake.sml
@@ -42,61 +42,62 @@ type free = {
}
fun shake file =
- case List.foldl (fn ((DVal ("main", n, t, e), _), _) => SOME (n, t, e)
- | (_, s) => s) NONE file of
- NONE => []
- | SOME (main, mainT, body) =>
- let
- val (cdef, edef) = foldl (fn ((DCon (_, n, _, c), _), (cdef, edef)) => (IM.insert (cdef, n, c), edef)
- | ((DVal (_, n, t, e), _), (cdef, edef)) => (cdef, IM.insert (edef, n, (t, e))))
- (IM.empty, IM.empty) file
+ let
+ val (page_cs, page_es) = List.foldl
+ (fn ((DPage (c, e), _), (cs, es)) => (c :: cs, e :: es)
+ | (_, acc) => acc) ([], []) file
- fun kind (_, s) = s
+ val (cdef, edef) = foldl (fn ((DCon (_, n, _, c), _), (cdef, edef)) => (IM.insert (cdef, n, c), edef)
+ | ((DVal (_, n, t, e), _), (cdef, edef)) => (cdef, IM.insert (edef, n, (t, e)))
+ | ((DPage _, _), acc) => acc)
+ (IM.empty, IM.empty) file
- fun con (c, s) =
- case c of
- CNamed n =>
- if IS.member (#con s, n) then
- s
- else
- let
- val s' = {con = IS.add (#con s, n),
- exp = #exp s}
- in
- case IM.find (cdef, n) of
- NONE => s'
- | SOME c => shakeCon s' c
- end
- | _ => s
+ fun kind (_, s) = s
- and shakeCon s = U.Con.fold {kind = kind, con = con} s
+ fun con (c, s) =
+ case c of
+ CNamed n =>
+ if IS.member (#con s, n) then
+ s
+ else
+ let
+ val s' = {con = IS.add (#con s, n),
+ exp = #exp s}
+ in
+ case IM.find (cdef, n) of
+ NONE => s'
+ | SOME c => shakeCon s' c
+ end
+ | _ => s
- fun exp (e, s) =
- case e of
- ENamed n =>
- if IS.member (#exp s, n) then
- s
- else
- let
- val s' = {exp = IS.add (#exp s, n),
- con = #con s}
- in
- case IM.find (edef, n) of
- NONE => s'
- | SOME (t, e) => shakeExp (shakeCon s' t) e
- end
- | _ => s
+ and shakeCon s = U.Con.fold {kind = kind, con = con} s
- and shakeExp s = U.Exp.fold {kind = kind, con = con, exp = exp} s
+ fun exp (e, s) =
+ case e of
+ ENamed n =>
+ if IS.member (#exp s, n) then
+ s
+ else
+ let
+ val s' = {exp = IS.add (#exp s, n),
+ con = #con s}
+ in
+ case IM.find (edef, n) of
+ NONE => s'
+ | SOME (t, e) => shakeExp (shakeCon s' t) e
+ end
+ | _ => s
- val s = {con = IS.empty,
- exp = IS.singleton main}
-
- val s = U.Con.fold {kind = kind, con = con} s mainT
- val s = U.Exp.fold {kind = kind, con = con, exp = exp} s body
- in
- List.filter (fn (DCon (_, n, _, _), _) => IS.member (#con s, n)
- | (DVal (_, n, _, _), _) => IS.member (#exp s, n)) file
- end
+ and shakeExp s = U.Exp.fold {kind = kind, con = con, exp = exp} s
+
+ val s = {con = IS.empty, exp = IS.empty}
+
+ val s = foldl (fn (c, s) => U.Con.fold {kind = kind, con = con} s c) s page_cs
+ val s = foldl (fn (e, s) => U.Exp.fold {kind = kind, con = con, exp = exp} s e) s page_es
+ in
+ List.filter (fn (DCon (_, n, _, _), _) => IS.member (#con s, n)
+ | (DVal (_, n, _, _), _) => IS.member (#exp s, n)
+ | (DPage _, _) => true) file
+ end
end
diff --git a/src/source.sml b/src/source.sml
index 4aea002e..e52f5630 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -113,6 +113,7 @@ datatype decl' =
| DOpen of string * string list
| DConstraint of con * con
| DOpenConstraints of string * string list
+ | DPage of exp
and str' =
StrConst of decl list
diff --git a/src/source_print.sml b/src/source_print.sml
index 8fc27106..827bb554 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -418,6 +418,10 @@ fun p_decl ((d, _) : decl) =
space,
p_list_sep (string ".") string (m :: ms)]
+ | DPage e => box [string "page",
+ space,
+ p_exp e]
+
and p_str (str, _) =
case str of
StrConst ds => box [string "struct",
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-22 10:30:56 +0000