From 6aaa09dfff50fdd22aeef563de63a50926bb553f Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 16 Dec 2010 13:35:40 -0500 Subject: Fiddly tweaks --- doc/manual.tex | 2 +- lib/ur/list.ur | 13 +++++++++++++ lib/ur/list.urs | 1 + src/elab_util.sig | 23 +++++++++++++++++++++-- src/elab_util.sml | 43 +++++++++++++++++++++++++++++++++---------- src/elaborate.sml | 42 +++++++++++++++++------------------------- 6 files changed, 86 insertions(+), 38 deletions(-) diff --git a/doc/manual.tex b/doc/manual.tex index 03219a4e..58fbc84d 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -1823,7 +1823,7 @@ $$\begin{array}{l} 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{} tag is $[\mt{Body}, \mt{Tr}]$, to indicate a kind of nesting inside \texttt{} and \texttt{}. 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}$$ diff --git a/lib/ur/list.ur b/lib/ur/list.ur index 354ef132..3153cc32 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -322,6 +322,19 @@ val nth [a] = 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)) = diff --git a/lib/ur/list.urs b/lib/ur/list.urs index c23bf840..9ad738f1 100644 --- a/lib/ur/list.urs +++ b/lib/ur/list.urs @@ -72,6 +72,7 @@ val mapQueryPartialM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type 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 *) diff --git a/src/elab_util.sig b/src/elab_util.sig index dc0f25e8..88bdc892 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -157,8 +157,8 @@ structure Decl : sig | 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 @@ structure Decl : sig 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 diff --git a/src/elab_util.sml b/src/elab_util.sml index d297ccbc..fd8163c2 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -771,8 +771,8 @@ datatype binder = | 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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 @@ fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d = 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 diff --git a/src/elaborate.sml b/src/elaborate.sml index 3134c3d4..550e3b8f 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -4262,31 +4262,17 @@ fun elabFile basis topStr topSgn env file = 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 @@ fun elabFile basis topStr topSgn env file = ("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 @@ fun elabFile basis topStr topSgn env file = (!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 @@ fun elabFile basis topStr topSgn env file = (!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) -- cgit v1.2.3