% $Id: XMLWadler.lsl,v 1.5 2000/01/17 21:33:41 connolly Exp $
%
A formal semantics of patterns in XSLT 16 July 1999 by Philip Wadler
XMLWadler: trait
    includes
        Relation(Node, R[Node],
         __ \< __ \> __ for __ á __ ñ __, %@@ LP doesn't grok lslinit.ini
        bot for \bot, top for \top),
        Set(Node, FiniteSet[Node] for Set[E]),
        RelSet(String, Set[String]),
        TotalOrder(Node),
        MinMax(Node)

    introduces
% section 2: Sets and relations
% where Wadler writes y \in rel[x], larch folks write
% x \langle rel \rangle y
% @@hmm... LP doesn't seem to understand \langle as
% a bracket symbol, so I'll use \<.
        __ [ __ ] : R[Node], Node ® FiniteSet[Node]
        
        first, last: FiniteSet[Node] ® FiniteSet[Node] % Set1 below

% section 3: A data model for XML
        isRoot, isElement, isAttribute, isText, isComment, isPI: Node ® Bool
% why not make those disjoint types? hm...
        parent: ® R[Node]
        children: ® R[Node]
        attributes: ® R[Node]
        root: Node ® Node

        subnodes: ® R[Node]

        name: Node ® String
        value: Node ® String        

        id: String ® FiniteSet[Node] % Set1... see below
        split: String ® Set[String]


    asserts " x, y, x1, x2: Node,
                    r:R[Node],
                    n, s, s1: String,
                    ns: FiniteSet[Node]

% section 2: Sets and relations
% where Wadler writes y \in rel[x], larch folks write
% x \langle rel \rangle y
        y Î r[x] = (x \< r \> y);

        first({}) = {};
        last({}) = {};
        first({x}) = {x};
        last({x}) = {x};
        first(ns) = {y} Þ first(insert(x, ns)) = {min(x,y)};
        last(ns) = {y} Þ last(insert(x, ns)) = {max(x,y)};

% section 3: A data model for XML
        functional(parent);
        isRoot(x) Þ parent[x] = {};

        children[x] ¹ {} Þ isRoot(x) Ú isElement(x);
        attributes[x] ¹ {} Þ isElement(x);
        y Î children[x] Þ
         isElement(y) Ú isText(y) Ú isComment(y) Ú isPI(y);
        y Î attributes[x] Þ isAttribute(y);
        y = root(x) Þ isRoot(y); % i.e. isRoot(root(x))

        subnodes[x] = children[x] \U attributes[x];

% @@ name/value table

        x Î id(n) Ù y Î id(n) Þ x=y; % Set1

        y Î subnodes[x] = (parent[y] = {x}); % p. 5

        x Î (subnodes*)[root(x)] ; % p. 5
% @@hmm... I thought I could use
% Node generated by root, children, attributes
% but children and attributes aren't Node->Node operators.
% Hm... a more natural larch definition might go bottom-up:
% makeElement : List[Node], List[Node] -> Node
% Node generated by makeElement, root

% @@ I added this specification of root
        isRoot(x) Þ root(x) = x;
         x \< subnodes \> y Þ root(x) = root(y);

    implies
        " x: Node
             root(root(x)) = root(x)
%@@? converts first, last, __[__]:Node->FiniteSet[Node], root

[Index]

[source]

HTML generated using lsl2html.