% $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.