changeset 1345:9e0fa4f6ac93

Fiddly tweaks
author Adam Chlipala <adam@chlipala.net>
date Thu, 16 Dec 2010 13:35:40 -0500
parents 660a2715e2bd
children faad7d01b200
files doc/manual.tex lib/ur/list.ur lib/ur/list.urs src/elab_util.sig src/elab_util.sml src/elaborate.sml
diffstat 6 files changed, 86 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/doc/manual.tex	Thu Dec 16 10:23:37 2010 -0500
+++ b/doc/manual.tex	Thu Dec 16 13:35:40 2010 -0500
@@ -1823,7 +1823,7 @@
 
 Ur/Web's library contains an encoding of XML syntax and semantic constraints.  We make no effort to follow the standards governing XML schemas.  Rather, XML fragments are viewed more as values of ML datatypes, and we only track which tags are allowed inside which other tags.  The Ur/Web standard library encodes a very loose version of XHTML, where it is very easy to produce documents which are invalid XHTML, but which still display properly in all major browsers.  The main purposes of the invariants that are enforced are first, to provide some documentation about the places where it would make sense to insert XML fragments; and second, to rule out code injection attacks and other abstraction violations related to HTML syntax.
 
-The basic XML type family has arguments respectively indicating the \emph{context} of a fragment, the fields that the fragment expects to be bound on entry (and their types), and the fields that the fragment will bind (and their types).  Contexts are a record-based ``poor man's subtyping'' encoding, with each possible set of valid tags corresponding to a different context record.  The arguments dealing with field binding are only relevant to HTML forms.
+The basic XML type family has arguments respectively indicating the \emph{context} of a fragment, the fields that the fragment expects to be bound on entry (and their types), and the fields that the fragment will bind (and their types).  Contexts are a record-based ``poor man's subtyping'' encoding, with each possible set of valid tags corresponding to a different context record.  For instance, the context for the \texttt{<td>} tag is $[\mt{Body}, \mt{Tr}]$, to indicate a kind of nesting inside \texttt{<body>} and \texttt{<tr>}.  Contexts are maintained in a somewhat ad-hoc way; the only definitive reference for their meanings is the types of the tag values in \texttt{basis.urs}.  The arguments dealing with field binding are only relevant to HTML forms.
 $$\begin{array}{l}
   \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
 \end{array}$$
--- a/lib/ur/list.ur	Thu Dec 16 10:23:37 2010 -0500
+++ b/lib/ur/list.ur	Thu Dec 16 13:35:40 2010 -0500
@@ -322,6 +322,19 @@
         nth
     end
 
+fun replaceNth [a] (ls : list a) (n : int) (v : a) : list a =
+    let
+        fun repNth (ls : list a) (n : int) (acc : list a) =
+            case ls of
+                [] => rev acc
+              | x :: ls' => if n <= 0 then
+                                revAppend acc (v :: ls')
+                            else
+                                repNth ls' (n-1) (x :: acc)
+    in
+        repNth ls n []
+    end
+
 fun assoc [a] [b] (_ : eq a) (x : a) =
     let
         fun assoc' (ls : list (a * b)) =
--- a/lib/ur/list.urs	Thu Dec 16 10:23:37 2010 -0500
+++ b/lib/ur/list.urs	Thu Dec 16 13:35:40 2010 -0500
@@ -72,6 +72,7 @@
 val sort : a ::: Type -> (a -> a -> bool) (* > predicate *) -> t a -> t a
 
 val nth : a ::: Type -> list a -> int -> option a
+val replaceNth : a ::: Type -> list a -> int -> a -> list a
 
 (** Association lists *)
 
--- a/src/elab_util.sig	Thu Dec 16 10:23:37 2010 -0500
+++ b/src/elab_util.sig	Thu Dec 16 13:35:40 2010 -0500
@@ -157,8 +157,8 @@
            | NamedC of string * int * Elab.kind * Elab.con option
            | RelE of string * Elab.con
            | NamedE of string * Elab.con
-           | Str of string * Elab.sgn
-           | Sgn of string * Elab.sgn
+           | Str of string * int * Elab.sgn
+           | Sgn of string * int * Elab.sgn
 
     val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
                     con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
@@ -203,6 +203,25 @@
                     decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state,
                     bind : 'context * binder -> 'context}
                    -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state
+
+    val map : {kind : Elab.kind' -> Elab.kind',
+               con : Elab.con' -> Elab.con',
+               exp : Elab.exp' -> Elab.exp',
+               sgn_item : Elab.sgn_item' -> Elab.sgn_item',
+               sgn : Elab.sgn' -> Elab.sgn',
+               str : Elab.str' -> Elab.str',
+               decl : Elab.decl' -> Elab.decl'}
+              -> Elab.decl -> Elab.decl
+
+    val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
+                con : 'context -> Elab.con' -> Elab.con',
+                exp : 'context -> Elab.exp' -> Elab.exp',
+                sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item',
+                sgn : 'context -> Elab.sgn' -> Elab.sgn',
+                str : 'context -> Elab.str' -> Elab.str',
+                decl : 'context -> Elab.decl' -> Elab.decl',
+                bind : 'context * binder -> 'context}
+               -> 'context -> Elab.decl -> Elab.decl
 end
 
 structure File : sig
--- a/src/elab_util.sml	Thu Dec 16 10:23:37 2010 -0500
+++ b/src/elab_util.sml	Thu Dec 16 13:35:40 2010 -0500
@@ -771,8 +771,8 @@
        | NamedC of string * int * Elab.kind * Elab.con option
        | RelE of string * Elab.con
        | NamedE of string * Elab.con
-       | Str of string * Elab.sgn
-       | Sgn of string * Elab.sgn
+       | Str of string * int * Elab.sgn
+       | Sgn of string * int * Elab.sgn
 
 fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
     let
@@ -808,8 +808,8 @@
                              Sgn.RelK x => RelK x
                            | Sgn.RelC x => RelC x
                            | Sgn.NamedC x => NamedC x
-                           | Sgn.Sgn (x, _, y) => Sgn (x, y)
-                           | Sgn.Str (x, _, y) => Str (x, y)
+                           | Sgn.Sgn x => Sgn x
+                           | Sgn.Str x => Str x
             in
                 bind (ctx, b')
             end
@@ -861,12 +861,12 @@
                                                    bind (ctx, NamedE (x, c))
                                                  | DValRec vis =>
                                                    foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
-                                                 | DSgn (x, _, sgn) =>
-                                                   bind (ctx, Sgn (x, sgn))
-                                                 | DStr (x, _, sgn, _) =>
-                                                   bind (ctx, Str (x, sgn))
-                                                 | DFfiStr (x, _, sgn) =>
-                                                   bind (ctx, Str (x, sgn))
+                                                 | DSgn (x, n, sgn) =>
+                                                   bind (ctx, Sgn (x, n, sgn))
+                                                 | DStr (x, n, sgn, _) =>
+                                                   bind (ctx, Str (x, n, sgn))
+                                                 | DFfiStr (x, n, sgn) =>
+                                                   bind (ctx, Str (x, n, sgn))
                                                  | DConstraint _ => ctx
                                                  | DExport _ => ctx
                                                  | DTable (tn, x, n, c, _, pc, _, cc) =>
@@ -1144,6 +1144,29 @@
         S.Continue x => x
       | S.Return _ => raise Fail "ElabUtil.Decl.foldMapB: Impossible"
 
+fun map {kind, con, exp, sgn_item, sgn, str, decl} s =
+    case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
+                  con = fn c => fn () => S.Continue (con c, ()),
+                  exp = fn e => fn () => S.Continue (exp e, ()),
+                  sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
+                  sgn = fn s => fn () => S.Continue (sgn s, ()),
+                  str = fn si => fn () => S.Continue (str si, ()),
+                  decl = fn s => fn () => S.Continue (decl s, ())} s () of
+        S.Return () => raise Fail "Elab_util.Decl.map"
+      | S.Continue (s, ()) => s
+
+fun mapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx s =
+    case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
+                   con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
+                   exp = fn ctx => fn c => fn () => S.Continue (exp ctx c, ()),
+                   sgn_item = fn ctx => fn sgi => fn () => S.Continue (sgn_item ctx sgi, ()),
+                   sgn = fn ctx => fn s => fn () => S.Continue (sgn ctx s, ()),
+                   str = fn ctx => fn sgi => fn () => S.Continue (str ctx sgi, ()),
+                   decl = fn ctx => fn s => fn () => S.Continue (decl ctx s, ()),
+                   bind = bind} ctx s () of
+        S.Continue (s, ()) => s
+      | S.Return _ => raise Fail "ElabUtil.Decl.mapB: Impossible"
+
 end
 
 structure File = struct
--- a/src/elaborate.sml	Thu Dec 16 10:23:37 2010 -0500
+++ b/src/elaborate.sml	Thu Dec 16 13:35:40 2010 -0500
@@ -4262,31 +4262,17 @@
 
         val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
 
-        val checks = ref ([] : (unit -> unit) list)
-
         fun elabDecl' (d, (env, gs)) =
             let
                 val () = resetKunif ()
                 val () = resetCunif ()
-                val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs))
+                val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs))
             in
-                checks :=
-                (fn () =>
-                    (if List.exists kunifsInDecl ds then
-                         declError env (KunifsRemain ds)
-                     else
-                         ();
-                     
-                     case ListUtil.search cunifsInDecl ds of
-                         NONE => ()
-                       | SOME loc =>
-                         declError env (CunifsRemain ds)))
-                :: !checks;
-
-                (ds, (env, gs))
+                                    (**)
+                (ds, (env', gs))
             end
 
-        val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
+        val (file, (env'', gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
 
         fun oneSummaryRound () =
             if ErrorMsg.anyErrors () then
@@ -4390,10 +4376,10 @@
                                                     ("Hnormed 1", p_con env c1'),
                                                     ("Hnormed 2", p_con env c2')];
 
-                                        app (fn (loc, env, k, s1, s2) =>
+                                        (*app (fn (loc, env, k, s1, s2) =>
                                                 eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)),
                                                             ("s2", p_summary env (normalizeRecordSummary env s2))])
-                                            (!delayedUnifs);
+                                            (!delayedUnifs);*)
 
                                         if (isUnif c1' andalso maybeAttr c2')
                                            orelse (isUnif c2' andalso maybeAttr c1') then
@@ -4422,10 +4408,16 @@
                  (!delayedUnifs);
              delayedUnifs := []);
 
-        if ErrorMsg.anyErrors () then
-            ()
-        else
-            app (fn f => f ()) (!checks);
+        ignore (List.exists (fn d => if kunifsInDecl d then
+                                         (declError env'' (KunifsRemain [d]);
+                                          true)
+                                     else
+                                         false) file);
+        
+        ignore (List.exists (fn d => case cunifsInDecl d of
+                                         NONE => false
+                                       | SOME _ => (declError env'' (CunifsRemain [d]);
+                                                    true)) file);
 
         if ErrorMsg.anyErrors () then
             ()
@@ -4437,7 +4429,7 @@
                 (!delayedExhaustives);
 
         (*preface ("file", p_file env' file);*)
-
+        
         (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
         :: ds
         @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)