% $Id: XMLQueryDataModel.lsl,v 1.1 2001/01/31 07:39:53 connolly Exp $

% a transcription of
% XML Query Data Model
%
%        W3C Working Draft 11 May 2000
%             http://www.w3.org/TR/2000/WD-query-datamodel-20000511 
%
% or rather:
%
% http://www.w3.org/XML/Group/2001/01/query-datamodel20010109.html

XMLQueryDataModel: trait
  includes
    List(Node, Instance for List[E]),
    List(Node),
    ElementTest(taggedAs, Node, List[Node], Node_tag) % for filter

    % sec 2.1.1 Schema Types
    T union of simple: S, complex: C

    % sec 3 Nodes
    Node union of doc: DocNode, elem: ElemNode,
		value: ValueNode, attr: AttrNode,
		ns: NSNode, pi: PINode, comment: CommentNode,
		item: InfoItemNode,
		ref: RefNode

  introduces


    isDocNode      : Node -> Bool
    isElemNode     : Node -> Bool
    isValueNode    : Node -> Bool
    isAttrNode     : Node -> Bool
    isNSNode       : Node -> Bool
    isPINode       : Node -> Bool
    isCommentNode  : Node -> Bool
    isInfoItemNode : Node -> Bool
    isRefNode      : Node -> Bool

    taggedAs: Node, Node_tag -> Bool % filter support

    % sec 3.2 Document

    docNode : uriReference, List[Node] -> DocNode

    uri :  DocNode -> uriReference
    children : DocNode -> List[Node] % list further constrained below
    root : DocNode -> ElemNode

    % sec 3.3 Elements
    elemNode : Ref[QNameValue], Set[Ref[NSNode]], Set[Ref[AttrNode]], 
                        List[Node], Ref[Def_T] 
                     -> ElemNode % @@constrain children to: elem, value, pi, comment, info


    % @@more sections

    % sec 3.8 Reference Node
    ref:         Node -> Ref[Node]
    deref:       Ref[Node] -> Node
    %@@parent
    node_equal:  Node, Node -> Bool
    NaR:         -> Ref[Node]


  asserts
    forall n: Node, i: Instance, nt: Node_tag

    % sec 3 Nodes
    isDocNode(n) = (tag(n) = doc);
    isElemNode(n) = (tag(n) = elem);
    %@@... and so on for all 9

    % sec 3.1 Data Model Instance
    n \in i => (tag(n) = doc
	        \/ tag(n) = elem
	        \/ tag(n) = value
	        \/ tag(n) = pi
	        \/ tag(n) = comment
	        \/ tag(n) = ref);

    % (filter support)
    taggedAs(n, nt) = (tag(n) = nt);

    % sec 3.2 Document
    forall n: Node, d:DocNode
    n \in children(d) => (tag(n) = elem
	                  /\ tag(n) = pi
	                  /\ tag(n) = comment);

    % "The root accessor returns the unique ElemNode in a DocNode's children list"
    len(filter(children(d), elem)) = 1; 
    (n \in children(d) /\ tag(n) = elem) => root(d) = n.elem;

    % sec 3.8 Reference Node
    node_equal(deref(ref(n)), n);

    % skipped: ref is surjective.

    % REVIEW: blech! "Def_T = ElemNode denotes the data model
    %                representation of schema type T."
    %  should be based on components, not surface syntax.
    % hm... let's check the wg-internal draft...