% $Id: Refinement9907.lsl,v 1.3 2000/01/17 21:33:40 connolly Exp $
%
%html <cite><a href="Details of the Proposal on Refinement and Tolerance">Details of the Proposal on Refinement and Tolerance</a></cite>
%html (member-confidential, sorry)

Refinement9907: trait
    includes
        XMLInfoSet, % use this for 4.2 instances
	RegExp(Name for Symbol, List[Name] for String, RegEx[Name] for Exp),
	Relation(Name, Rel[Name],
 	         __ \< __ \> __ for __ \langle __ \rangle __,
		bot for \bot, top for \top),
	Set(Name, FiniteSet[Name]),
	FiniteMap(Attribution, Name, Value, __[__] for apply)

        Schema tuple of
            E: FiniteSet[Name], % namespace URI?
	    T: FiniteSet[Name],
	    A: FiniteSet[Name],
	    V: ValueSet, % not necessarily finite
	    e0: Name,
	    f: TypeDeclFunc,
	    g: AttrDeclFunc,
	    h: NameToName,
	    v: Rel[Name]

        Instance tuple of doc: DocumentItem, l: LabelingFunc

    introduces
        rootElt: DocumentItem -> ElementItem
	elementNames: List[Item] -> List[Name]

        __ [ __ ] : TypeDeclFunc, Name -> RegEx[Name]
        __ [ __ ] : AttrDeclFunc, Name -> AttrTypeFunc
	__ [ __ ] : AttrTypeFunc, Name -> ValueSet
        __ [ __ ] : NameToName, Name -> Name
	__ \in __ : Value, ValueSet -> Bool

	refinement: Schema -> Rel[Name]
	basic: Schema, Name -> Bool
	\bot: -> Name %@@need separate sort for this?
	implicit: Name -> Bool

	tag: LabelingFunc, Item -> Name
	attribution: LabelingFunc, Item -> Attribution
	type: LabelingFunc, Item -> Name


        basicValid: Schema, Instance -> Bool
        basicValid: Schema, Instance, Item -> Bool

        v_alternative: Schema, Name, Name -> Bool
	sv_closure: Schema, Name -> RegEx[Name]
	sv_closure: Schema, Name, FiniteSet[Name] -> RegEx[Name]
	sv_closure: Schema, RegEx[Name] -> RegEx[Name]

    asserts
        \forall
 	    s: Schema,
	    t, t1, a, e, e1: Name, elts: FiniteSet[Name],
	    doc: DocumentItem, inst: Instance,
	    n, n1: Item, % "node"
	    n2k: List[Item],
	    r, r1, r2: RegEx[Name]

	element(rootElt(doc)) \in children(document(doc));
 	% and it's the only one.

        elementNames(empty) = empty;
	elementNames({n} || n2k) ==
	    if tag(n) = element then {name(n.element)} || elementNames(n2k)
	    else elementNames(n2k);

	s.e0 \in s.E;

	antisymmetric(s.v) % v is a partial order @@over s.T
	/\ transitive(s.v)
	/\ reflexive(s.v);

	refinement(s) = s.v \superstar; % transitive closure

        basic(s, t) == (t \in s.T
	                /\ ~(\E t1 (t \< s.v \> t1)));

        implicit(t) == t = \bot;

        basicValid(s, inst) ==
            name(rootElt(inst.doc)) = s.e0
	    /\ \A n (n \in flatten({document(inst.doc)}) /\ tag(n) = element
	          => implicit(type(inst.l, n)) /\ basicValid(s, inst, n));

        basicValid(s, inst, n) ==
	    tag(n) = element /\ n \in flatten({document(inst.doc)})
	    /\ elementNames(children(n)) \in L(s.f[s.h[name(n.element)]]) %namespaces URIs?
	    /\ \A a (defined(attribution(inst.l, n), a)
	             => attribution(inst.l, n)[a]
                        \in (s.g[s.h[name(n.element)]])[a])
            /\ \A n1 (n1 \in children(n) /\ tag(n1) = element
	              => basicValid(s, inst, n));

        v_alternative(s, e, e1) ==
	    e \in s.E /\ e1 \in s.E
            /\ (s.h[e1]) \< s.v \superstar \> (s.h[e]);

	sv_closure(s, e, {}) == [e];
	sv_closure(s, e, insert(e1, elts)) ==
 	    if v_alternative(s, e, e1) then sv_closure(s, e, elts) \U [e1]
	    else sv_closure(s, e, elts);
	sv_closure(s, e) = sv_closure(s, e, s.E);

        sv_closure(s, [e]) = sv_closure(s, e);
        sv_closure(s, empty:RegEx[Name]) = empty;
	sv_closure(s, r \*) = sv_closure(s, r)\*;
	sv_closure(s, r1 \U r2) = sv_closure(s, r1) \U sv_closure(s, r2);
	sv_closure(s, r1 || r2) = sv_closure(s, r1) || sv_closure(s, r2);

        %@@ continue with S-refinement valid