# HG changeset patch # User Adam Chlipala # Date 1215699095 14400 # Node ID f0f59e918cacb9338bd887f50e543bf9fbfefd64 # Parent 5182f0c80d2e1147b228b96901866161727a2316 page declaration, up through monoize diff -r 5182f0c80d2e -r f0f59e918cac src/cloconv.sml --- a/src/cloconv.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/cloconv.sml Thu Jul 10 10:11:35 2008 -0400 @@ -158,7 +158,6 @@ 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 @@ in Ds.exp D (x, n, t, e) end + | L.DPage _ => raise Fail "Cloconv DPage" fun cloconv ds = let diff -r 5182f0c80d2e -r f0f59e918cac src/core.sml --- a/src/core.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/core.sml Thu Jul 10 10:11:35 2008 -0400 @@ -79,6 +79,7 @@ datatype decl' = DCon of string * int * kind * con | DVal of string * int * con * exp + | DPage of con * exp withtype decl = decl' located diff -r 5182f0c80d2e -r f0f59e918cac src/core_env.sml --- a/src/core_env.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/core_env.sml Thu Jul 10 10:11:35 2008 -0400 @@ -123,5 +123,6 @@ 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 -r 5182f0c80d2e -r f0f59e918cac src/core_print.sml --- a/src/core_print.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/core_print.sml Thu Jul 10 10:11:35 2008 -0400 @@ -272,6 +272,12 @@ 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 -r 5182f0c80d2e -r f0f59e918cac src/core_util.sml --- a/src/core_util.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/core_util.sml Thu Jul 10 10:11:35 2008 -0400 @@ -376,6 +376,12 @@ 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 @@ 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 -r 5182f0c80d2e -r f0f59e918cac src/corify.sml --- a/src/corify.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/corify.sml Thu Jul 10 10:11:35 2008 -0400 @@ -427,6 +427,7 @@ 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 @@ | 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 -r 5182f0c80d2e -r f0f59e918cac src/elab.sml --- a/src/elab.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/elab.sml Thu Jul 10 10:11:35 2008 -0400 @@ -115,6 +115,7 @@ | 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 -r 5182f0c80d2e -r f0f59e918cac src/elab_env.sml --- a/src/elab_env.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/elab_env.sml Thu Jul 10 10:11:35 2008 -0400 @@ -292,6 +292,7 @@ | 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 -r 5182f0c80d2e -r f0f59e918cac src/elab_print.sml --- a/src/elab_print.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/elab_print.sml Thu Jul 10 10:11:35 2008 -0400 @@ -450,6 +450,12 @@ 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 -r 5182f0c80d2e -r f0f59e918cac src/elab_util.sml --- a/src/elab_util.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/elab_util.sml Thu Jul 10 10:11:35 2008 -0400 @@ -510,7 +510,8 @@ 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 @@ 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 -r 5182f0c80d2e -r f0f59e918cac src/elaborate.sml --- a/src/elaborate.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/elaborate.sml Thu Jul 10 10:11:35 2008 -0400 @@ -1593,12 +1593,13 @@ 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 @@ ([], (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 -r 5182f0c80d2e -r f0f59e918cac src/expl.sml --- a/src/expl.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/expl.sml Thu Jul 10 10:11:35 2008 -0400 @@ -98,6 +98,7 @@ | 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 -r 5182f0c80d2e -r f0f59e918cac src/expl_env.sml --- a/src/expl_env.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/expl_env.sml Thu Jul 10 10:11:35 2008 -0400 @@ -243,6 +243,7 @@ | 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 -r 5182f0c80d2e -r f0f59e918cac src/expl_print.sml --- a/src/expl_print.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/expl_print.sml Thu Jul 10 10:11:35 2008 -0400 @@ -392,6 +392,12 @@ 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 -r 5182f0c80d2e -r f0f59e918cac src/explify.sml --- a/src/explify.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/explify.sml Thu Jul 10 10:11:35 2008 -0400 @@ -116,6 +116,7 @@ | 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 -r 5182f0c80d2e -r f0f59e918cac src/lacweb.grm --- a/src/lacweb.grm Thu Jul 10 09:24:43 2008 -0400 +++ b/src/lacweb.grm Thu Jul 10 10:11:35 2008 -0400 @@ -46,7 +46,7 @@ | 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 @@ [] => 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 -r 5182f0c80d2e -r f0f59e918cac src/lacweb.lex --- a/src/lacweb.lex Thu Jul 10 09:24:43 2008 -0400 +++ b/src/lacweb.lex Thu Jul 10 10:11:35 2008 -0400 @@ -261,6 +261,7 @@ "open" => (Tokens.OPEN (pos yypos, pos yypos + size yytext)); "constraint"=> (Tokens.CONSTRAINT (pos yypos, pos yypos + size yytext)); "constraints"=> (Tokens.CONSTRAINTS (pos yypos, pos yypos + size yytext)); + "page" => (Tokens.PAGE (pos yypos, pos yypos + size yytext)); "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext)); "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext)); diff -r 5182f0c80d2e -r f0f59e918cac src/mono.sml --- a/src/mono.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/mono.sml Thu Jul 10 10:11:35 2008 -0400 @@ -56,6 +56,7 @@ datatype decl' = DVal of string * int * typ * exp + | DPage of (string * typ) list * exp withtype decl = decl' located diff -r 5182f0c80d2e -r f0f59e918cac src/mono_env.sml --- a/src/mono_env.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/mono_env.sml Thu Jul 10 10:11:35 2008 -0400 @@ -84,5 +84,6 @@ fun declBinds env (d, _) = case d of DVal (x, n, t, e) => pushENamed env x n t (SOME e) + | DPage _ => env end diff -r 5182f0c80d2e -r f0f59e918cac src/mono_print.sml --- a/src/mono_print.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/mono_print.sml Thu Jul 10 10:11:35 2008 -0400 @@ -143,7 +143,20 @@ 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 -r 5182f0c80d2e -r f0f59e918cac src/mono_util.sml --- a/src/mono_util.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/mono_util.sml Thu Jul 10 10:11:35 2008 -0400 @@ -205,6 +205,15 @@ 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 @@ 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 -r 5182f0c80d2e -r f0f59e918cac src/monoize.sml --- a/src/monoize.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/monoize.sml Thu Jul 10 10:11:35 2008 -0400 @@ -164,6 +164,13 @@ 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 -r 5182f0c80d2e -r f0f59e918cac src/shake.sml --- a/src/shake.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/shake.sml Thu Jul 10 10:11:35 2008 -0400 @@ -42,61 +42,62 @@ } 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 -r 5182f0c80d2e -r f0f59e918cac src/source.sml --- a/src/source.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/source.sml Thu Jul 10 10:11:35 2008 -0400 @@ -113,6 +113,7 @@ | DOpen of string * string list | DConstraint of con * con | DOpenConstraints of string * string list + | DPage of exp and str' = StrConst of decl list diff -r 5182f0c80d2e -r f0f59e918cac src/source_print.sml --- a/src/source_print.sml Thu Jul 10 09:24:43 2008 -0400 +++ b/src/source_print.sml Thu Jul 10 10:11:35 2008 -0400 @@ -418,6 +418,10 @@ 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", diff -r 5182f0c80d2e -r f0f59e918cac tests/html_fn.lac --- a/tests/html_fn.lac Thu Jul 10 09:24:43 2008 -0400 +++ b/tests/html_fn.lac Thu Jul 10 10:11:35 2008 -0400 @@ -7,3 +7,5 @@ Hello World! + +page main