XMLNames

% $Id: XMLNames.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
%

References

XML Information Set
Working Draft of August 30, 1999
Editors: John Cowan, David Megginson

%
%updating w.r.t.
20 Dec 1999 draft
XMLNames: trait

    includes
        XMLElement,

        Seq(Char, List[Char]),
        Set(Name, FiniteSet[Name] for Set[E]),
        Set(URIwf, FiniteSet[URIwf] for Set[E]),
        Set(NamespaceDeclarationItem,
            FiniteSet[NamespaceDeclarationItem] for Set[E]),
        FiniteMap(Name, URIwf,
                  FiniteSet[NamespaceDeclarationItem] for Map[D, R]),
        PointwiseImage(NamespaceDeclarationItem for DE,
                       Name for RE,
                       FiniteSet[NamespaceDeclarationItem] for DC,
                       FiniteSet[Name] for RC,
                       prefixes for containerOp,
                       prefix for elemOp)

% 2.13. Namespace Declaration Information Items
        NamespaceDeclarationItem tuple of prefix: Name, id: URIwf %@@REVIEW: including frag

    introduces
        asString: List[Item] → List[Char]
        ucsChar: Int → Char
        asURIRef: List[Char] → URI_reference %@@specify this in URISyntax trait?

% 2.2. Element Information Items
        URI: ElementItem → FiniteSet[URIwf] %@@REVIEW: including fragment
%@@REVIEW: URI is the type of the object
% of the property, but properties
% should be named according to
% the relationship between subj & obj

        declaredNamespaces: ElementItem → FiniteSet[NamespaceDeclarationItem]
        inScopeNamespaces: ElementItem → FiniteSet[NamespaceDeclarationItem]
%@@REVIEW: I added these to show how to compute declaredNamespaces
% from attribute values
        namespaceDecls: absoluteURI, FiniteSet[AttributeItem] → FiniteSet[NamespaceDeclarationItem]
        prefix: Name → Name
        localPart: Name → Name
        xmlns: → Name
        empty: → Name %@@double-check use of Name sort

% 2.3. Attribute Information Items
        URI: AttributeItem → FiniteSet[URIwf] %@@REVIEW: including fragment
%@@REVIEW: URI is the type of the object
% of the property, but properties
% should be named according to
% the relationship between subj & obj

% 2.13. Namespace Declaration Information Items

        merge: FiniteSet[NamespaceDeclarationItem], FiniteSet[NamespaceDeclarationItem]
                → FiniteSet[NamespaceDeclarationItem] % auxiliary

    asserts
        forall
                i, i1, i2: Item,
                is: InformationSet,
                li, li1, li2: List[Item],
                n: Name,
                ns: NamespaceDeclarationItem,
                sns1, sns2: FiniteSet[NamespaceDeclarationItem],
                base: absoluteURI, nsid: URIwf, uref: URI_reference,
                elti: ElementItem,
                ai: AttributeItem, sai: FiniteSet[AttributeItem]

% auxiliary
        asString(empty) = empty;
        asString(i -| li) =
             (if tag(i) = char
             then ucsChar(code(i.char)) -| asString(li)
             else asString(li));

% 2.2. Element Information Items
        size(URI(elti)) <= 1;
        URI(elti) = (if defined(inScopeNamespaces(elti), prefix(name(elti)))
                     then {apply(inScopeNamespaces(elti), prefix(name(elti)))}
                     else {});

        size(URI(ai)) <= 1;
        ai ∈ attributes(elti)
        ⇒ URI(ai) = (if ¬(prefix(name(ai))=empty)
                           ∧ defined(inScopeNamespaces(elti), prefix(name(ai)))
                     then {apply(inScopeNamespaces(elti), prefix(name(ai)))}
                     else {});

        declaredNamespaces(elti) = namespaceDecls(baseURI(elti), attributes(elti));
        namespaceDecls(base, {}) = {};

        uref = asURIRef(asString(children(attribute(ai))))
        ⇒ namespaceDecls(base, insert(ai, sai)) =
                 (if name(ai) = xmlns
                 then insert([empty, combine(base, uref)],
                             namespaceDecls(base, sai))
                 else if prefix(name(ai)) = xmlns
                 then insert([localPart(name(ai)), combine(base, uref)],
                             namespaceDecls(base, sai))
                 else namespaceDecls(base, sai));

% namespaces in scope
% root element case:
        tag(i) = element
        ∧ i ∈ children(documentItem(is))
        ⇒ inScopeNamespaces(i.element) = declaredNamespaces(i.element);
% child case
        tag(i1) = element
        ∧ tag(i2) = element
        ∧ i2 ∈ children(i1)
        ⇒ inScopeNamespaces(i2.element) =merge(declaredNamespaces(i2.element),
                                                inScopeNamespaces(i1.element));

        update(sns1, n, nsid) = merge({[n, nsid]}, sns1);

        merge(sns1, empty) = sns1;
        merge(sns1, insert(ns, sns2)) = (if prefix(ns) ∈ prefixes(sns1)
                                         then merge(sns1, sns2)
                                         else insert(ns, merge(sns1, sns2)));

[Index]

HTML generated using lsl2html.