page declaration, up through monoize

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",