% $Id: XPathWadler.lsl,v 1.8 2000/01/17 21:33:41 connolly Exp $
%
%html <cite><a href="http://cm.bell-labs.com/cm/cs/who/wadler/topics/xml.html#xsl-semantics">A formal semantics of patterns in XSLT</a></cite>
%html 16 July 1999
%html by <a href="http://cm.bell-labs.com/cm/cs/who/wadler/">Philip Wadler</a>

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, [__]

        \forall 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)       = \E x1 (x1 \in (subnodes\superstar)[root(x)]
		                /\ x \in 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 \in S(!!p)[x]     = \E x1 (x1 \in (subnodes\superstar)[root(x)]
					/\ x2 \in S(p)[x1]);

	x2 \in S(p1!p2)[x]   = \E x1 (x1 \in S(p1)[x] /\ x2 \in S(p2)[x1]);

	x3 \in S(p1!!p2)[x]  = \E x1 \E x2 (x1 \in S(p1)[x]
	                                     /\ x2 \in (subnodes\superstar)[x1]
	                                     /\ x3 \in S(p2)[x2]);

	x1 \in S(p[q])[x]    = x1 \in S(p)[x] /\ Q(q, x1);

	x1 \in S([n])[x]     = x1 \in subnodes[x] /\ isElement(x1)
				/\ name(x1) = n;

	x1 \in S(star)[x]    = x1 \in subnodes[x] /\ isElement(x1);

	x1 \in S(@ n)[x]     = x1 \in subnodes[x] /\ isAttribute(x1)
				/\ name(x1) = n;

	x1 \in S(atStar)[x]  = x1 \in subnodes[x] /\ isAttribute(x1);

	x1 \in S(text)[x]    = x1 \in subnodes[x] /\ isText(x1);

	x1 \in S(comment)[x] = x1 \in subnodes[x] /\ isComment(x1);

	x1 \in S(pi(n))[x]   = x1 \in subnodes[x] /\ isPI(x1) /\ name(x1) = n;

	x1 \in S(pi)[x]      = x1 \in subnodes[x] /\ isPI(x1);

	x2 \in S(id(p))[x]   = \E x1 (x1 \in S(p)[x]
				      /\ \E s (s \in split(value(x1))
				               /\ x2 \in id(s)));

	x1 \in S(id(s))[x]   = \E s1 (s1 \in split(s) /\ x1 \in id(s1));

	S(ancestor(p))[x]    = last(ancAux(p, x));
	x1 \in ancAux(p, x)  = x1 \in (parent\superplus)[x] /\ M(p, x1);

	S(ancestor_or_self(p))[x]  = last(ancSelfAux(p, x));
	x1 \in ancSelfAux(p, x)  = x1 \in (parent\superstar)[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 \in first(firstAux(x));
	x1 \in firstAux(x)  = x1 \in siblingElements(x) /\ name(x1) = name(x);
	   % Wadler paper missing x1 \in before siblingElements???

	Q(last_of_type, x)  = x \in last(firstAux(x));

	Q(first_of_any, x)  = x \in first(siblingElements(x));

	Q(last_of_any, x)   = x \in last(siblingElements(x));

	Q(p \equal s, x)    = \E x1 (x1 \in S(p)[x] /\ value(x1) = s);

	Q([p], x)           = (S(p)[x] \neq {});

	x2 \in siblingElements(x) = \E x1 (x1 \in parent[x]
					   /\ x2 \in subnodes[x]
					   /\ isElement(x2));
    implies
        converts
	    siblingElements,
	    ancAux, ancSelfAux, firstAux,
	    M, S, Q