% $Id: XMLSchema.lsl,v 1.14 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>

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

        TypeDefinition union of
 	    simple: SimpleTypeDefinition,
	    complex: ComplexTypeDefinition

	BaseDatatype union of
	    abInitio: AbInitio,
            simple: SimpleTypeDefinition

        AbInitio union of
            string: StringAIT,
            boolean: BooleanAIT,
            real: RealAIT,
            binary: BinaryAIT,
            uri: URIAIT,
            language: LanguageAIT,
            nmtoken: NMTokenAIT,
            timeinstant: TimeInstantAIT,
            timeduration: TimeDurationAIT,
            recurringinstant: RecurringInstantAIT

        SimpleTypeDefinition tuple of
	    basetype: BaseDatatype
	    % @@others...

	ComplexTypeDefinition tuple of
	    basetype: TypeDefinition,
            contentModel: ContentModel,
	    attrDecls: FiniteSet[AttrDecl]
	    %@@others...

	ComplexRTypeDefinition tuple of %@@subtype of above??
            contentType: ContentType,
	    attrDecls: FiniteSet[AttrDecl]
	    %@@others...

        ContentType union of
	    unconstrained: Null,
            emptyCM: Null,
            simpleType: SimpleTypeDefinition,
            richModel: ContentModel

    introduces
        schema_valid: ElementItem, TypeDefinition, FiniteSet[Component] -> Bool
        schema_valid_string: List[Char], AbInitio -> Bool
        schema_valid_content: List[Item], ComplexRTypeDefinition, FiniteSet[Component] -> Bool
	effective_stype: SimpleTypeDefinition, FiniteSet[Component]-> AbInitio
	effective_ctype: ComplexTypeDefinition, FiniteSet[Component]-> ComplexRTypeDefinition
        find_component: Def_or_Decl_tag, List[Char], TargetNS,  FiniteSet[Component] -> Component
	all_white: List[Char] -> Bool

    asserts
        \forall
 	    eii: ElementItem,
	    tyDef: TypeDefinition,
	    effectiveSchema: FiniteSet[Component]

	    schema_valid(eii, tyDef, effectiveSchema) =
	        (tag(tyDef) = simple
		/\ attributes(eii) = {}
		/\ filter(children(element(eii)), element) = empty
		/\ schema_valid_string(asString(children(element(eii))),
		                       effective_stype(tyDef.simple,
				                       effectiveSchema)))
		\/
		(tag(tyDef) = complex
		/\ schema_valid_attrs(attributes(eii),
		                      effective_ctype(tyDef.complex,
				                    effectiveSchema).attrDecls,
				      effectiveSchema)
                /\ schema_valid_content(children(element(eii)),
		                        effective_ctype(tyDef.complex,
					                effectiveSchema),
					effectiveSchema)
					)

        \forall
            string: List[Char],
            ait: AbInitio

            schema_valid_string(string,ait) =
              (tag(ait) = string
               /\
	       string_is_string(string,ait.string))
            % @@ \/ (tag(ait) = boolean /\ ...) ...

	\forall
	    content: List[Item],
	    crt: ComplexRTypeDefinition,
	    effectiveSchema: FiniteSet[Component]

            schema_valid_content(content,crt,effectiveSchema) =
		(((tag(crt.contentType) = emptyCM)
		  /\ (filter(content,element) = empty)
		  /\ all_white(asString(content)))
		 \/
		 % @@ lots more clauses needed
		true)

         \forall
	     ccs: FiniteSet[Component],
	     comp: Component,
	     localname: List[Char],
	     tns: TargetNS,
	     dd: Def_or_Decl,
	     ddt: Def_or_Decl_tag
	     

	     (find_component(ddt,localname,tns,ccs) = comp) <=>
             (comp \in ccs) /\ (comp.localname=localname) /\ (comp.tns=tns)
	     /\ (comp.dex=dd) /\ (tag(dd)=ddt)

    implies
      % test the simplest case
	\forall
	    eii: ElementItem,
	    td: TypeDefinition,
	    ss: FiniteSet[Component],
	    content: List[Item],
	    i: Item,
	    ci: CharacterItem,
	    std: SimpleTypeDefinition,
	    bt: BaseDatatype,
	    ait: AbInitio,
	    sait: StringAIT

	    children(element(eii))=content /\
	    content={i} /\
	    tag(i)=char /\
	    tag(td)=simple /\
	    td.simple=std /\
	    std.basetype=bt /\
	    tag(bt)=abInitio /\
	    bt.abInitio=ait /\
	    tag(ait)=string /\
	    ait.string=sait /\
	    tag(sait.pattern)=null /\
	    tag(sait.maxLength)=null /\
	    tag(sait.length)=value /\
	    sait.length.value=1 => schema_valid(eii,td,ss)
            % phew!