% $Id: XPathWadler.lsl,v 1.8 2000/01/17 21:33:41 connolly Exp $
%
A formal semantics of patterns in XSLT
16 July 1999
by Philip Wadler
XPathWadler: trait
includes
XMLWadler % sections 2, 3 of the paper
introduces
% 5 A semantics for Patterns
__ | __: Pattern, Pattern ® Pattern
% default larch config doesn't have / as an op char, so we use !
! __ : Pattern ® Pattern
!! __ : Pattern ® Pattern
__ ! __ : Pattern, Pattern ® Pattern
__ !! __ : Pattern, Pattern ® Pattern
__ [__] : Pattern, Qualifier ® Pattern
[__] : String ® Pattern % Wadler's notation doesn't need []
% @@isName: where does the Name set comefrom?
% is it a subset of String?
star : ® Pattern % *
@ __ : String ® Pattern % isName@@
atStar : ® Pattern
text : ® Pattern
comment : ® Pattern
pi: String ® Pattern % isName
pi: ® Pattern
id: Pattern ® Pattern
id: String ® Pattern
ancestor: Pattern ® Pattern
ancestor_or_self: Pattern ® Pattern
dot : ® Pattern
dotdot : ® Pattern
and: Qualifier, Qualifier ® Qualifier
or: Qualifier, Qualifier ® Qualifier
notq: Qualifier ® Qualifier
first_of_type: ® Qualifier
last_of_type: ® Qualifier
first_of_any: ® Qualifier
last_of_any: ® Qualifier
__ \equal __ : Pattern, String ® Qualifier
[ __ ] : Pattern ® Qualifier % wadler's notation doesn't need []
M: Pattern, Node ® Bool
% Wadler's formulation is M : Pattern -> Node -> Boolean
% but larch is 1st order, so I (un?)curried it.
S: Pattern ® R[Node]
Q: Qualifier, Node ® Bool
% again, curried
siblingElements: Node ® FiniteSet[Node]
ancAux: Pattern, Node ® FiniteSet[Node]
ancSelfAux: Pattern, Node ® FiniteSet[Node]
firstAux: Node ® FiniteSet[Node]
asserts
Pattern generated by
| , !__, __ ! __ , !! __, __!!__,
__ [__], [__],
star, @, atStar,
text, comment, pi:String®Pattern, pi:®Pattern,
id:Pattern®Pattern, id:String®Pattern,
ancestor, ancestor_or_self, dot, dotdot
Qualifier generated by
and, or, notq,
first_of_type, last_of_type, first_of_any, last_of_any,
\equal, [__]
" p, p1, p2: Pattern, x, y, x1, x2, x3: Node,
q, q1, q2: Qualifier,
n, s, s1: String,
ns: FiniteSet[Node]
% Figure 1: Semantics of patterns ...
M(p, x) = $ x1 (x1 Î (subnodes*)[root(x)]
Ù x Î S(p)[x1]);
S(p1 | p2)[x] = S(p1)[x] \U S(p2)[x];
S(!p)[x] = S(p)[root(x)];
% where wadler writes S ::= { x | P(x) }
% we write x \in S = P(x)
% @@c.f. comp.specification.larch discussion
x2 Î S(!!p)[x] = $ x1 (x1 Î (subnodes*)[root(x)]
Ù x2 Î S(p)[x1]);
x2 Î S(p1!p2)[x] = $ x1 (x1 Î S(p1)[x] Ù x2 Î S(p2)[x1]);
x3 Î S(p1!!p2)[x] = $ x1 $ x2 (x1 Î S(p1)[x]
Ù x2 Î (subnodes*)[x1]
Ù x3 Î S(p2)[x2]);
x1 Î S(p[q])[x] = x1 Î S(p)[x] Ù Q(q, x1);
x1 Î S([n])[x] = x1 Î subnodes[x] Ù isElement(x1)
Ù name(x1) = n;
x1 Î S(star)[x] = x1 Î subnodes[x] Ù isElement(x1);
x1 Î S(@ n)[x] = x1 Î subnodes[x] Ù isAttribute(x1)
Ù name(x1) = n;
x1 Î S(atStar)[x] = x1 Î subnodes[x] Ù isAttribute(x1);
x1 Î S(text)[x] = x1 Î subnodes[x] Ù isText(x1);
x1 Î S(comment)[x] = x1 Î subnodes[x] Ù isComment(x1);
x1 Î S(pi(n))[x] = x1 Î subnodes[x] Ù isPI(x1) Ù name(x1) = n;
x1 Î S(pi)[x] = x1 Î subnodes[x] Ù isPI(x1);
x2 Î S(id(p))[x] = $ x1 (x1 Î S(p)[x]
Ù $ s (s Î split(value(x1))
Ù x2 Î id(s)));
x1 Î S(id(s))[x] = $ s1 (s1 Î split(s) Ù x1 Î id(s1));
S(ancestor(p))[x] = last(ancAux(p, x));
x1 Î ancAux(p, x) = x1 Î (parent\superplus)[x] Ù M(p, x1);
S(ancestor_or_self(p))[x] = last(ancSelfAux(p, x));
x1 Î ancSelfAux(p, x) = x1 Î (parent*)[x] Ù M(p, x1);
S(dot)[x] = {x};
S(dotdot)[x] = parent[x];
Q(and(q1, q2), x) = Q(q1, x) Ù Q(q2, x);
Q(or(q1, q2), x) = Q(q1, x) Ú Q(q2, x);
Q(notq(q), x) = Ø Q(q, x);
Q(first_of_type, x) = x Î first(firstAux(x));
x1 Î firstAux(x) = x1 Î siblingElements(x) Ù name(x1) = name(x);
% Wadler paper missing x1 \in before siblingElements???
Q(last_of_type, x) = x Î last(firstAux(x));
Q(first_of_any, x) = x Î first(siblingElements(x));
Q(last_of_any, x) = x Î last(siblingElements(x));
Q(p \equal s, x) = $ x1 (x1 Î S(p)[x] Ù value(x1) = s);
Q([p], x) = (S(p)[x] ¹ {});
x2 Î siblingElements(x) = $ x1 (x1 Î parent[x]
Ù x2 Î subnodes[x]
Ù isElement(x2));
implies
converts
siblingElements,
ancAux, ancSelfAux, firstAux,
M, S, Q
[Index]
[source]
HTML generated using lsl2html.