% $Id: Refinement9907.lsl,v 1.2 1999/11/05 22:27:41 connolly Exp $
%
Details of the Proposal on Refinement and Tolerance
(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 __ á __ ñ __),
��������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
��������__ Î __ : 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
��������"
�������������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)) Π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 Πs.E;
��������antisymmetric(s.v) % v is a partial order @@over s.T
��������٠transitive(s.v)
��������٠reflexive(s.v);
��������refinement(s) = s.v *; % transitive closure
��������basic(s, t) º (t Î s.T
������������������������Ù Ø($ t1 (t \< s.v \> t1)));
��������implicit(t) º t = \bot;
��������basicValid(s, inst) º
������������name(rootElt(inst.doc)) = s.e0
������������٠" n (n Πflatten({document(inst.doc)}) ٠tag(n) = element
������������������Þ implicit(type(inst.l, n)) Ù basicValid(s, inst, n));
��������basicValid(s, inst, n) º
������������tag(n) = element ٠n Πflatten({document(inst.doc)})
������������٠elementNames(children(n)) ΠL(s.f[s.h[name(n.element)]]) %namespaces URIs?
������������٠" a (defined(attribution(inst.l, n), a)
���������������������Þ attribution(inst.l, n)[a]
������������������������Π(s.g[s.h[name(n.element)]])[a])
������������٠" n1 (n1 Πchildren(n) ٠tag(n1) = element
����������������������Þ basicValid(s, inst, n));
��������v_alternative(s, e, e1) º
������������e Πs.E ٠e1 Πs.E
������������٠(s.h[e1]) \< s.v * \> (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
[Index]
[source]
HTML generated using lsl2html.