aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-12-16 13:35:40 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2010-12-16 13:35:40 -0500
commit6aaa09dfff50fdd22aeef563de63a50926bb553f (patch)
treeed45e1d909672cac6d74d612f2c9531bb71681fa
parentc7996285ff4b1b05a4cecdb2c1e944f7c17b18a7 (diff)
Fiddly tweaks
Diffstat
-rw-r--r--doc/manual.tex2
-rw-r--r--lib/ur/list.ur13
-rw-r--r--lib/ur/list.urs1
-rw-r--r--src/elab_util.sig23
-rw-r--r--src/elab_util.sml43
-rw-r--r--src/elaborate.sml42
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{<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}$$
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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 09:04:41 +0000