% $Id: XMLSchemaAttrs.lsl,v 1.3 2000/01/17 21:33:41 connolly Exp $
%
%html <h2>References</h2>
%html <ol><li><cite><a href="http://www.w3.org/XML/Group/xmlschema-current/new-design/structures.html#conformance-schemaValidity">XML Schema Part 1: Structures</a></cite><br />
%html internal draft: Id: structures.xml,v 1.13.1.15 1999/10/26 16:23:30 ht Exp
%html </ol></li>

% should use FiniteMap/PointwiseImage, c.f. XMLNames

XMLSchemaAttrs: trait
    includes
        XMLInfoSet,
	XMLSchemaBasics,
	Set(Component, FiniteSet[AttrDecl] for Set[E])

        AttrDecl tuple of
	    name: Name,
	    type: SimpleTypeDefinition,
	    min: ZeroOrOne,
	    max: ZeroOrOne,
	    vc: ValueConstraint

        ZeroOrOne enumeration of 0, 1

        ValueConstraint union of
	    null: Null,
    	    default: List[Char],
	    fixed: List[Char]

        AttributeItemOrNull union of
	    null: Null,
	    value: AttributeItem

    introduces
	schema_valid_attrs: FiniteSet[AttributeItem], FiniteSet[AttrDecl], FiniteSet[Component] -> Bool
	lookup_attr: List[Char], TargetNS, FiniteSet[AttributeItem] -> AttributeItemOrNull

    asserts
        \forall
	    ads: FiniteSet[AttrDecl],
            comp: Component

            (comp \in ads) => (tag(comp.dex) = attrDecl)
            
        \forall
            ad: AttrDecl

	    ad.min=1 => ad.max=1;
	    ad.max=0 => ad.min=0

        \forall
	    name: List[Char],
	    ais: FiniteSet[AttributeItem],
	    aion: AttributeItemOrNull,
	    tns: TargetNS,
	    ai: AttributeItem,
	    uris: FiniteSet[URIwf],
	    uri: URIwf

           %@@ HELP DAN -- the lookup here is hopelessly bogus -- how
            % do I get to the AttributeItem's actual namespace, if any?
            (lookup_attr(name,tns,ais) = aion) =
             (\E ai (tag(aion)=value /\ aion.value=ai /\ (ai \in ais)
	              /\ (asString(localPart(name(ai)))=name)
		      /\ ((prefix(name(ai))=empty /\ tag(tns)=null)
                          \/ ((URI(ai)=uris) /\ (size(uris)=1)
			      /\ (uri \in uris))))
		    \/ (tag(aion)=null))

        \forall
            attrs: FiniteSet[AttributeItem],
            ads: FiniteSet[AttrDecl],
	    ccs: FiniteSet[Component],
	    req: FiniteSet[AttrDecl],
	    opt: FiniteSet[AttrDecl],
	    absent: FiniteSet[AttrDecl],
	    ad: Component
	    
            schema_valid_attrs(attrs,ads,ccs) =

            % required, optional and absent partition the declarations
	    ((req \subset ads) /\
	     (opt \subset ads) /\
	     (absent \subset ads) /\
	     (((req \U opt) \U absent) = ads) /\
	     ((ad \in absent) <=> (tag(ad.dex)=attrDecl /\
	                          ad.dex.attrDecl.max = 0)) /\
             ((ad \in req) <=> (tag(ad.dex)=attrDecl /\
	                       ad.dex.attrDecl.min = 1)))