VERSIONE IMPLEMENTATA
MATHEMATICAL QUERY LANGUAGE (MathQL)
-<query> := <list> (* clausola iniziale *)
+<query> := <set> (* clausola iniziale *)
-<list> := ( <list> ) (* parentesizazione *)
- | <rvar> (* lista singoletto var
- (lista valori) *)
- | <lvar> (* lista singoletto var
- (lista valori) *)
- | REFERENCE <reference> (* oggetto referenziato da URI
- esplicita *)
- | PATTERN <pattern> (* espansione del pattern *)
- | SELECT <rvar> IN <list> WHERE <bool> (* selezione *)
- | LET <lvar> BE <list> IN <list> (* assegnazione a var in
+<set> := ( <set> ) (* parentesizzazione *)
+ | <rvar> (* var per insieme singoletto
+ di una risorsa *)
+ | <svar> (* var per insieme di risorse
+ (insieme di valori) *)
+ | REF <string-set> (* oggetto/i referenziato/i da
+ URI esplicita/e *)
+ | PATTERN <string-set> (* oggetto/i referenziato/i da
+ URI ottenute da espansione
+ del pattern *)
+ | SELECT <rvar> IN <set> WHERE <bool> (* selezione *)
+ | LET <svar> BE <set> IN <set> (* assegnazione a set-var in
contesto *)
- | USE <list> POSITION <svar> (* unione lista backward *)
- | USEDBY <list> POSITION <svar> (* unione lista forward *)
- | <list> UNION <list> (* unione *)
- | <list> INTERSECT <list> (* intersezione *)
- | <list> SORTEDBY <function> <order> (* unione lista ordinata secondo
- valore funzione e ordine *)
-<order>:= DESC (* ordinamento decrescente *)
- | ASC (* ordinamento crescente *)
+ | RELATION <quoted-constant-string> <set> ATTR <vvar-list>
+ (* unione insieme risorse in
+ relazione specificata con le
+ risorse in set, ognuna con
+ attributi (ATTR) *)
+ | <set> UNION <set> (* unione *)
+ | <set> INTERSECT <set> (* intersezione *)
+
+<vvar-list> := <vvar>
+ | <vvar> , <vvar-list>
<bool> := ( <bool> ) (* parentesizzazione *)
| TRUE (* vero *)
| NOT <bool> (* negazione *)
| <bool> AND <bool> (* congiunzione *)
| <bool> OR <bool> (* disgiunzione *)
- | <string> IS <string> (* case sensitive matching *)
- | <list> SETEQUAL <list> (* uguaglianza tra liste *)
- | <list> SUBSET <list> (* operazione di sottoinsieme *)
+ | <string-set> EQ <string-set> (* uguaglianza tra insiemi
+ stringhe (case sensitive) *)
+ | <string-set> SUB <string-set> (* operazione di sottoinsieme
+ tra insiemi stringhe *)
+ | <string-set> MEET <string-set> (* operazione di meet tra
+ insiemi stringhe *)
+ | EX <bool> (* existential on attributes
+ of references *)
+
+<string-set> := {} (* insieme vuoto*)
+ | <quoted-constant-string-set> (* stringa singoletto *)
+ | {<quoted-constant-string-set>} (* insieme stringhe *)
+ | REFOF <set> (* insieme riferimenti *)
+ | <rvar>.<vvar> (* variabile per insieme
+ stringhe, relativa a
+ riferimento *)
+ | <function> <quoted-constant-string> <rvar>
+ (* applicazione di funzione
+ specificata a riferim. *)
-<string> := <'-quoted-constant-string> (* costante letterale *)
- | MAINHYPOTHESIS | HYPOTHESIS (* costanti simboliche *)
- | MAINCONCLUSION | CONCLUSION | BODY
- | <svar> (* variabile *)
- | <rvar> (* variabile *)
- | <function> <rvar> (* applicazione di funzione *)
-
-<function> := NAME (* URIREF -> nome_oggetto *)
- | TITLE (* URIREF -> valore_prop_DC *)
- | CONTRIBUTOR
- | CREATOR
- | PUBLISHER
- | SUBJECT
- | DESCRIPTION
- | DATE
- | TYPE
- | FORMAT
- | IDENTIFIER
- | LANGUAGE
- | RELATION
- | SOURCE
- | COVERAGE
- | RIGHTS
- | INSTITUTION
- | CONTACT
- | FIRSTVERSION
- | MODIFIED
+<quoted-constant-string-set> := <quoted-constant-string>
+ | <quoted-constant-string> , <quoted-constant-string-set>
+ (* lista di stringhe *)
-<pattern> := <"-quoted-constant-string> (* pattern costante *)
-<reference> := <'-quoted-constant-string> (* riferimento costante *)
+<function> := FUN (* funzione generale *)
-<rvar> := <not-reserved-identifier> (* variabile per riferimenti *)
-<svar> := $ <not-reserved-identifier> (* variabile per stringhe *)
-<lvar> := % <not-reserved-identifier> (* variabile per liste *)
+<rvar> := @ <not-reserved-identifier> (* variabile per riferimento *)
+<vvar> := $ <not-reserved-identifier> (* variabile per insiemi
+ stringhe *)
+<svar> := % <not-reserved-identifier> (* variabile per insiemi
+ riferimenti *)
-- le stringhe sono "case sensitive"
-- la funzione non definita sull'argomento restituisce la stringa nulla
-- le <rvar> si presuppongono essere istanziate come URI references costituite
+- MEET e' definito come "esiste almeno un elemento che appartiene
+ all'interserzione tra due insiemi"
+- Le stringhe sono "case sensitive"
+- La funzione non definita sull'argomento restituisce la stringa nulla
+- Le <rvar> si presuppongono essere istanziate come URI references costituite
da un URI e da un fragment identifier opzionale complete; i riferimenti
identificano risorse
-- ogni binding lega una variabile libera (nomi nuovi)
- Precedenza operatori:
NOT (+) DIFF
AND INTERSECT
OR (-) UNION
- L'ordinamento di default e' quello alfabetico crescente in base al nome
delle rvar
-- REFERENCE aumenta performance perche' NON accede al data base (costoso).
-- Note su <pattern>
- Contiene un'espressione regolare per selezionare delle "reference"
- (cioe` delle uri eventualmente seguite da un fragment identifier)
- L'espressione regolare contiene i seguenti costrutti:
-
- costrutto semanticamente fa match con
- ? un singolo carattere diverso da / # :
- * la piu' lunga sottostringa che non contiene / # :
- ** la piu' lunga sottostringa che non contiene # :
- altro carattere solo se' stesso
-
- costrutto puo' appareire in
- ? "body"
- * dovunque
- ** "body" e "fragment"
- altro carattere dovunque
-
- "body" parte compresa fra le occorrenze di ":/" e "#1" escluse
- "fragment" parte successiva all'occorrenza "#1"
\ No newline at end of file
+- REF aumenta performance perche' NON accede al data base (costoso).
+- L'argomento di PATTERN ha sintassi di una espressione regolare
+ POSIX 1003.2-1992
+- Possibili FUN (<quoted-constant-string>):
+ NAME (* URIREF -> nome_oggetto *)
+- MEET aumenta performance nel caso si verifichi (a in S) oppure
+ (b in S) = ({a,b} meet S) perche' valuta S una volta sola
+- Record <rvar>.<svar> serve per disambiguare nomi uguali di variabili
+- Operatori (come EQ) hanno nomi abbreviati rispetto ai costrutti del
+ linguaggio
+- EX verfica che la sua condizione sia vera per almeno un insieme di attributi
+ associato all'URI in rvar
+- Possibili RELATION sono:
+ USE con attributo POSITION (riferimenti backward) e valori MAINHYPOTHESIS,
+ HYPOTHESIS, MAINCONCLUSION, CONCLUSION, BODY
+ USEBY con attributo POSITION (riferimenti forward) e valori MAINHYPOTHESIS,
+ HYPOTHESIS, MAINCONCLUSION, CONCLUSION, BODY
+ CONSTRUCTORS
+ INTHEORY con attributo ITEMTYPE (riferimenti oggetti contenuti in teorie)
+ THEORYREFTO con attributo ITEMTYPE (riferimenti teorie referenti a oggetti)
\ No newline at end of file
GRAMMATICA PER QUERY SU DOCUMENTI MATEMATICI
MATHEMATICAL QUERY LANGUAGE (MathQL)
-<query> := <list> (* clausola iniziale *)
+<query> := <set> (* clausola iniziale *)
-<list> := <empty-string> (* lista vuota *)
- | ( <list> ) (* parentesizazione *)
- | <rvar> (* lista singoletto var
- (lista valori) *)
- | <lvar> (* lista singoletto var
- (lista valori) *)
- | REFERENCE <reference> (* oggetto referenziato da URI
- esplicita *)
- | PATTERN <pattern> (* espansione del pattern *)
- | SELECT <rvar> IN <list> WHERE <bool> (* selezione *)
- | LET <lvar> BE <list> IN <list> (* assegnazione a var in
+<set> := ( <set> ) (* parentesizzazione *)
+ | <rvar> (* var per insieme singoletto
+ di una risorsa *)
+ | <svar> (* var per insieme di risorse
+ (insieme di valori) *)
+ | REF <string-set> (* oggetto/i referenziato/i da
+ URI esplicita/e *)
+ | PATTERN <string-set> (* oggetto/i referenziato/i da
+ URI ottenute da espansione
+ del pattern *)
+ | SELECT <rvar> IN <set> WHERE <bool> (* selezione *)
+ | LET <svar> BE <set> IN <set> (* assegnazione a set-var in
contesto *)
- | USE <list> POSITION <svar> (* unione lista backward *)
- | USEDBY <list> POSITION <svar> (* unione lista forward *)
- | CONTRUCTORS <list> (* unione costruttori della
- lista oggetti*)
- | INTHEORY <list> ITEMTYPE <svar> (* unione oggetti lista
- teorie *)
- | THEORYREFTO <list> (* unione teorie che fanno
- riferimento a lista oggetti *)
- | <list> OFTYPE <svar> (* unione oggetti in base a
+ | RELATION <quoted-constant-string> <set> ATTR <vvar-list>
+ (* unione insieme risorse in
+ relazione specificata con le
+ risorse in set, ognuna con
+ attributi (ATTR) *)
+ | <set> OFTYPE <set> (* unione oggetti in base a
classi RDF *)
- | <list> OFSUPERTYPE <svar> (* unione oggetti in base a
+ | <set> OFSUPERTYPE <set> (* unione oggetti in base a
classi e loro superclassi *)
- | <list> OFSUBTYPE <svar> (* unione oggetti in base a
- classi e loro sottoclassi *)
- | <list> UNION <list> (* unione *)
- | <list> INTERSECT <list> (* intersezione *)
- | <list> DIFF <list> (* differenza *)
- | MINIMIZE <list> (* minimizzazione del numero
- elementi della lista *)
- | <list> SORTEDBY <function> <order> (* unione lista ordinata secondo
- valore funzione e ordine *)
-<order>:= DESC (* ordinamento decrescente *)
- | ASC (* ordinamento crescente *)
+ | <set> OFSUBTYPE <set> (* unione oggetti in base a
+ classi e loro sottoclassi *)
+ | <set> UNION <set> (* unione *)
+ | <set> INTERSECT <set> (* intersezione *)
+ | <set> DIFF <set> (* differenza *)
<bool> := ( <bool> ) (* parentesizzazione *)
| TRUE (* vero *)
| NOT <bool> (* negazione *)
| <bool> AND <bool> (* congiunzione *)
| <bool> OR <bool> (* disgiunzione *)
- | <string> IS <string> (* case sensitive matching *)
- | <list> SETEQUAL <list> (* uguaglianza tra liste *)
- | <list> SUBSET <list> (* operazione di sottoinsieme *)
- | EXISTS <rvar> IN <list> (* esistenziale *)
+ | <string-set> EQ <string-set> (* uguaglianza tra insiemi
+ stringhe (case sensitive) *)
+ | <string-set> SUB <string-set> (* operazione di sottoinsieme
+ tra insiemi stringhe *)
+ | <string-set> MEET <string-set> (* operazione di meet tra
+ insiemi stringhe *)
+ | EX <bool> (* existential on attributes
+ of references *)
-<string> := <'-quoted-constant-string> (* costante letterale *)
- | MAINHYPOTHESIS | HYPOTHESIS (* costanti simboliche *)
- | MAINCONCLUSION | CONCLUSION | BODY
- | <svar> (* variabile *)
- | <rvar> (* variabile *)
- | <function> <rvar> (* applicazione di funzione *)
-
-<function> := NAME (* URIREF -> nome_oggetto *)
- | <property> (* proprieta' RDF *)
+<vvar-list> := <vvar>
+ | <vvar> , <vvar-list>
-<property> := THEORY (* URIREF -> valore_proprieta' *)
- | TITLE (* URIREF -> valore_prop_DC *)
- | CONTRIBUTOR
- | CREATOR
- | PUBLISHER
- | SUBJECT
- | DESCRIPTION
- | DATE
- | TYPE
- | FORMAT
- | IDENTIFIER
- | LANGUAGE
- | RELATION
- | SOURCE
- | COVERAGE
- | RIGHTS
- | INSTITUTION
- | CONTACT
- | FIRSTVERSION
- | MODIFIED
- | VALUEOF <propname> (* nome_propr URIREF ->
- valore_Proprieta' *)
- | <refineprop> <property>
+<string-set> := {} (* insieme vuoto*)
+ | <quoted-constant-string-set> (* stringa singoletto *)
+ | {<quoted-constant-string-set>} (* insieme stringhe *)
+ | REFOF <set> (* insieme riferimenti *)
+ | <rvar>.<vvar> (* variabile per insieme
+ stringhe, relativa a
+ riferimento *)
+ | <function> <quoted-constant-string> <rvar>
+ (* applicazione di funzione
+ specificata a riferim. *)
-<refineprop> := SUB (* proprieta' e sotto-proprieta'
- di *)
- | SUPER (* proprieta' e super-proprieta'
- di *)
-<propname> := <'-quoted-constant-string> (* costante letterale *)
+<quoted-constant-string-list> := <quoted-constant-string>
+ | <quoted-constant-string> , <quoted-constant-string-list>
+ (* lista di stringhe *)
-<pattern> := <"-quoted-constant-string> (* pattern costante *)
-<reference> := <'-quoted-constant-string> (* riferimento costante *)
+<function> := FUN (* funzione generale *)
+ | <property>
-<rvar> := <not-reserved-identifier> (* variabile per riferimenti *)
-<svar> := $ <not-reserved-identifier> (* variabile per stringhe *)
-<lvar> := % <not-reserved-identifier> (* variabile per liste *)
+<property> := VALUEOF (* funzione proprieta': restituisce
+ suoi valori*)
+ | SUBVALUE (* restituisce valori proprieta' e
+ sotto-proprieta' di *)
+ | SUPERVALUE (* restituisce valori proprieta' e
+ super-proprieta' di *)
-- query vuota e' caso patologico: non si puo' verificare
+<rvar> := @ <not-reserved-identifier> (* variabile per riferimento *)
+<vvar> := $ <not-reserved-identifier> (* variabile per insiemi
+ stringhe *)
+<svar> := % <not-reserved-identifier> (* variabile per insiemi
+ riferimenti *)
+
+
+
+- MEET e' definito come "esiste almeno un elemento che appartiene
+ all'interserzione tra due insiemi"
- le stringhe sono "case sensitive"
- la funzione non definita sull'argomento restituisce la stringa nulla
- le <rvar> si presuppongono essere istanziate come URI references costituite
da un URI e da un fragment identifier opzionale complete; i riferimenti
identificano risorse
-- ogni binding lega una variabile libera (nomi nuovi)
- Precedenza operatori:
NOT (+) DIFF
AND INTERSECT
OR (-) UNION
-- Possibili tipi di RELATION e DEPENDENCE sono rappresentati dalle loro
- subproperties
-- FUTURO: thesauri di parole e sinonimi per ricerche testuali, ordinamenti sui
- risultati, caratteri jolly. Una volta reperito l'oggetto si possono
- visualizzare le info associate.
-- FUTURO: in output numeri ad esempio a fini statistici, aggiungendo anche
- operatori aritmetici e di confronto (< = >). Es. Quante proofs di un certo
- teorema ci sono?
- L'ordinamento di default e' quello alfabetico crescente in base al nome
delle rvar
-- REFERENCE aumenta performance perche' NON accede al data base (costoso).
-- Note su <pattern>
- Contiene un'espressione regolare per selezionare delle "reference"
- (cioe` delle uri eventualmente seguite da un fragment identifier)
- L'espressione regolare contiene i seguenti costrutti:
-
- costrutto semanticamente fa match con
- ? un singolo carattere diverso da / # :
- * la piu' lunga sottostringa che non contiene / # :
- ** la piu' lunga sottostringa che non contiene # :
- altro carattere solo se' stesso
-
- costrutto puo' appareire in
- ? "body"
- * dovunque
- ** "body" e "fragment"
- altro carattere dovunque
+- REF aumenta performance perche' NON accede al data base (costoso).
+- l'argomento di PATTERN ha sintassi di una espressione regolare
+ POSIX 1003.2-1992
+- Possibile <function> (<quoted-constant-string>):
+ NAME (* URIREF -> nome_oggetto *)
+- MEET aumenta performance nel caso si verifichi (a in S) oppure
+ (b in S) = ({a,b} meet S) perche' valuta S una volta sola
+ Il MEET codifica inoltre l'esistenziale su risorse (URI) in un certo
+ insieme che soddisfa certe condizioni
+- record <rvar>.<svar> serve per disambiguare nomi uguali di variabili
+- Operatori (come EQ) hanno nomi abbreviati rispetto ai costrutti del
+ linguaggio
+- EX verfica che la sua condizione sia vera per almeno un insieme di attributi
+ associato all'URI in rvar
+- Il costrutto di ordinamento:
+ <set> SORTEDBY <function> <order> (* unione insieme ordinato secondo
+ valore funzione e ordine *)
+ <order>:= DESC (* ordinamento decrescente *)
+ | ASC (* ordinamento crescente *)
+ perde di senso nel caso di metadati, poiche' per definizione le proprieta'
+ in RDF possono essere ripetute quindi restituiscono (come anche le funzioni
+ in generale) valori multipli per ogni riferimento (ambiguita' nell'ordine)
+- Possibili proprieta' (<quoted-constant-string>):
+ le DC: TITLE, CONTRIBUTOR, CREATOR, PUBLISHER, SUBJECT, DESCRIPTION, DATE,
+ TYPE, FORMAT, IDENTIFIER, LANGUAGE, RELATION, SOURCE, COVERAGE, RIGHTS,
+ RIGHTS; and INSTITUTION, CONTACT, FIRSTVERSION, MODIFIED, THEORY
- "body" parte compresa fra le occorrenze di ":/" e "#1" escluse
- "fragment" parte successiva all'occorrenza "#1"
-- Condizioni associate alla var dell'esisteziale possono essere espresse
- nella clausola WHERE di un SELECT nell'argomento <list> dell'EXISTS.
-- RILASSAMENTO degli operatori UNION e INTERSECT. Operatori fuzzy con
- introduzione di pesi associati ai risultati.
-- VALUEOF restituisce il valore o, ricorsivamente sulla struttura, i valori
- (delle proprieta' delle classi di valori) della proprieta' passatagli.
- Problema: e' necessario gestire sia i nomi delle classi (costrutti TYPEOF)
- sia i nomi delle proprieta' (menu a tendina di suggerimenti all'utente in
- base agli Schemi RDF relativi ai dati).
-- L'algoritmo che implementa MINIMIZE puo' ad esempio eliminare le entrate
- URI+insieme_di_attributi duplicate oppure le entrate con URI ripetute
- accorpando i diversi insieme_di_attributi per l'URI in un unica entrata
- della lista.
-
\ No newline at end of file
<MQLquery>
<Select>
<In>
- <Use>
+ <Relation name="Use">
<Pattern>
- <PPrefix><CONST>cic</CONST></PPrefix>
- <PBody>
- <SLASH/>
- <CONST>Coq</CONST>
- <SLASH/>
- <CONST>Init</CONST>
- <SLASH/>
- <CONST>Logic</CONST>
- <SLASH/>
- <CONST>Equality</CONST>
- <SLASH/>
- <CONST>eq</CONST>
- </PBody>
- <Ext><CONST>ind</CONST></Ext>
+ <CONST>cic:/Coq/Init/Logic/Equality/eq.ind</CONST>
</Pattern>
- <Position binder="$1"/>
- </Use>
+ <Attr binder="$1"/>
+ </Relation>
</In>
- <Where rvar="result">
+ <Where rvar="@result">
<AND>
- <IS>
- <BINDER name="$1"/>
- <POSITION name="MainHypothesis"/>
- </IS>
- <IS>
- <PROPERTY name="TITLE"><RVAR name="result"/></PROPERTY>
+ <EQ>
+ <BINDER name="$1"><Rvar name="@result"/></BINDER>
+ <CONST>MainHypothesis</CONST>
+ </EQ>
+ <EQ>
+ <PROPERTY name="TITLE"><Rvar name="@result"/></PROPERTY>
<CONST>Uguaglianza</CONST>
- </IS>
+ </EQ>
</AND>
</Where>
</Select>
<!--*****************************************************************-->
<!-- DTD FOR the MATHEMATICAL QUERY MARKUP LANGUAGE (XMathQL) -->
<!-- First draft: April 2002, Irene Schena -->
+<!-- Second draft: Agust 2002, Irene Schena -->
<!--*****************************************************************-->
<!--*****************************************************************-->
<!-- MathQL. -->
<!-- Operators are unambiguous (binary or unary), so there isn't any -->
<!-- grouping operator. -->
-<!-- SORTBY operator for sorting query results. -->
-<!-- CONST is the constant string; rvar is for references and lvar -->
-<!-- for list. -->
-<!-- The attributes binder, rvar, lvar declare variables which are -->
-<!-- referred to and used by means of respectively BINDER, Rvar and -->
-<!-- RVAR, Lvar and LVAR. -->
-<!-- Rvar (Lvar) is casted to a list, on the contrary the use of RVAR-->
-<!-- (LVAR) is casted to a string. -->
+<!-- CONST is the quoted constant string; rvar is for single -->
+<!-- reference and svar for sets of references, i.e. query results. -->
+<!-- The attributes binder, rvar, svar declare variables which are -->
+<!-- referred to and used by means of respectively BINDER, Rvar, Svar-->
<!-- PROPERTY works on a specified RDF property returning its value. -->
<!--*****************************************************************-->
-<!ENTITY % order '(ascendant|descendant)'>
-
-<!ENTITY % position '(MainHypothesis|Hypothesis|MainConclusion|Conclusion|
- Body)'>
-
<!ENTITY % bool '(True|False)'>
-<!ENTITY % token '(CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)'>
+<!-- MathQL query expression declaration -->
-<!-- MathQL list expression declaration -->
-
-<!ENTITY % listexpr '(Rvar|Lvar|Reference|Pattern|Select|LetIn|SortBy|
- Use|UsedBy|ConstructorsOf|InTheory|TheoryRefTo|
- TypeOf|SuperTypeOf|SubTypeOf|Union|Intersect|Diff|
- Minimize)'>
+<!ENTITY % setexpr '(Rvar|Lvar|Ref|Pattern|Select|LetIn|Relation|
+ TypeOf|SuperTypeOf|SubTypeOf|Union|Intersect|Diff)'>
<!-- MathQL boolean expression declaration -->
-<!ENTITY % boolexpr '(BOOL|NOT|AND|OR|IS|SETEQUAL|SUBSET|EXISTS)'>
+<!ENTITY % boolexpr '(BOOL|NOT|AND|OR|EQ|SUB|MEET|EX)'>
-<!-- MathQL string expression declaration -->
+<!-- MathQL string-set expression declaration -->
-<!ENTITY % functexpr '(NAME|PROPERTY|SUPERPROPERTY|SUBPROPERTY)'>
+<!ENTITY % functexpr '(FUN|PROPERTY|SUPERPROPERTY|SUBPROPERTY)'>
-<!ENTITY % stringexpr '(CONST|POSITION|RVAR|BINDER|%functexpr;)'>
+<!ENTITY % stringsetexpr '(CONST|CONSTLIST|REFOF|BINDER|%functexpr;)'>
<!-- MathQL query top-element -->
-<!ELEMENT MQLquery %listexpr;>
+<!ELEMENT MQLquery %setexpr;>
+
+<!-- MathQL set expressions -->
-<!-- MathQL list expressions -->
<!ELEMENT Rvar EMPTY>
<!ATTLIST Rvar
name CDATA #REQUIRED>
-<!ELEMENT Lvar EMPTY>
-<!ATTLIST Lvar
+<!ELEMENT Svar EMPTY>
+<!ATTLIST Svar
name CDATA #REQUIRED>
-<!ELEMENT Reference (RPrefix, RBody, Ext, (RFragmentID?))>
+<!ELEMENT Ref %stringsetexpr;>
-<!ELEMENT Pattern (PPrefix, PBody, (Ext?), (PFragmentID?))>
+<!ELEMENT Pattern %stringsetexpr;>
<!ELEMENT Select (In, Where)>
-<!ELEMENT LetIn (%listexpr;, Target)>
-
-<!ELEMENT Use (%listexpr;, Position)>
-
-<!ELEMENT UsedBy (%listexpr;, Position)>
-
-<!ELEMENT ConstructorsOf %listexpr;>
-
-<!ELEMENT InTheory (%listexpr;, ItemType)>
+<!ELEMENT LetIn (%setexpr;, Target)>
-<!ELEMENT TheoryRefTo %listexpr;>
+<!ELEMENT Relation (%setexpr;, Attr+)>
+<!ATTLIST Relation
+ name CDATA #REQUIRED>
-<!ELEMENT TypeOf %listexpr;>
+<!ELEMENT TypeOf %setexpr;>
<!ATTLIST TypeOf
binder CDATA #REQUIRED>
-<!ELEMENT SuperTypeOf %listexpr;>
+<!ELEMENT SuperTypeOf %setexpr;>
<!ATTLIST SuperTypeOf
binder CDATA #REQUIRED>
-<!ELEMENT SubTypeOf %listexpr;>
+<!ELEMENT SubTypeOf %setexpr;>
<!ATTLIST SubTypeOf
binder CDATA #REQUIRED>
-<!ELEMENT Union (%listexpr;, %listexpr;)>
-
-<!ELEMENT Intersect (%listexpr;, %listexpr;)>
-
-<!ELEMENT Diff (%listexpr;, %listexpr;)>
-
-<!ELEMENT SortBy (%listexpr;, SortField)>
-
-<!ELEMENT Minimize %listexpr;>
-
-<!-- MathQL list sub-expressions -->
-
-<!ELEMENT RPrefix (CONST)>
+<!ELEMENT Union (%setexpr;, %setexpr;)>
-<!ELEMENT RBody (CONST)>
+<!ELEMENT Intersect (%setexpr;, %setexpr;)>
-<!ELEMENT RFragmentID (NUMBER)+>
+<!ELEMENT Diff (%setexpr;, %setexpr;)>
-<!ELEMENT Ext (CONST)>
+<!-- MathQL set sub-expressions -->
-<!ELEMENT PPrefix (CONST|STAR)>
-
-<!ELEMENT PBody (%token;)+>
-
-<!-- XPointers have max depth = 2 (see CIC inductive definitions) -->
-<!ELEMENT PFragmentID (NUMBER|TWOSTARS|STAR)+>
-
-<!ELEMENT NUMBER EMPTY>
-<!ATTLIST NUMBER
- value NMTOKEN #REQUIRED>
-
-<!-- We need SLASH for grouping CONST with QUESTIONMARK -->
-<!ELEMENT SLASH EMPTY>
-
-<!-- STAR expands only to objects of the specified dir before the last "/":
- ex. cic:/Algebra/* expands to every object in Algebra only -->
-<!ELEMENT STAR EMPTY>
-
-<!-- TWOSTARS expands till the most complete name (with extension if not
- specifified) -->
-<!ELEMENT TWOSTARS EMPTY>
-
-<!-- QUESTIONMARK matches one character except "/" -->
-<!ELEMENT QUESTIONMARK EMPTY>
-
-<!ELEMENT In %listexpr;>
+<!ELEMENT In %setexpr;>
<!ELEMENT Where %boolexpr;>
<!ATTLIST Where
rvar CDATA #REQUIRED>
-<!ELEMENT Target %listexpr;>
+<!ELEMENT Target %setexpr;>
<!ATTLIST Target
- lvar CDATA #REQUIRED>
+ svar CDATA #REQUIRED>
-<!ELEMENT Position EMPTY>
-<!ATTLIST Position
+<!ELEMENT Attr EMPTY>
+<!ATTLIST Attr
binder CDATA #REQUIRED>
-<!ELEMENT ItemType EMPTY>
-<!ATTLIST ItemType
- binder CDATA #REQUIRED>
-
-<!ELEMENT SortField %functexpr;>
-<!ATTLIST SortField
- order %order; #IMPLIED>
-
<!-- MathQL boolean expressions -->
<!ELEMENT BOOL EMPTY>
<!ELEMENT OR (%boolexpr;, %boolexpr;)>
-<!ELEMENT IS (%stringexpr;, %stringexpr;)>
+<!ELEMENT EQ (%stringsetexpr;, %stringsetexpr;)>
-<!ELEMENT SETEQUAL (%listexpr;, %listexpr;)>
+<!ELEMENT SUB (%stringsetexpr;, %stringsetexpr;)>
-<!ELEMENT SUBSET (%listexpr;, %listexpr;)>
+<!ELEMENT MEET (%stringsetexpr;, %stringsetexpr;)>
-<!ELEMENT EXISTS (RVAR, %listexpr;)>
+<!ELEMENT EX %boolexpr;>
-<!-- MathQL string expressions -->
+<!-- MathQL string-set expressions -->
<!ELEMENT CONST (#PCDATA)>
-<!ELEMENT RVAR EMPTY>
-<!ATTLIST RVAR
- name CDATA #REQUIRED>
+<!ELEMENT CONSTLIST (CONST*)>
-<!ELEMENT BINDER EMPTY>
+<!ELEMENT REFOF %setexpr;>
+
+<!ELEMENT BINDER (Rvar)>
<!ATTLIST BINDER
name CDATA #REQUIRED>
-<!ELEMENT POSITION EMPTY>
-<!ATTLIST POSITION
- name %position; #REQUIRED>
-
-<!ELEMENT NAME (RVAR)>
+<!ELEMENT FUN (Rvar)>
+<!ATTLIST FUN
+ name CDATA #REQUIRED>
-<!ELEMENT PROPERTY (RVAR)>
+<!ELEMENT PROPERTY (Rvar)>
<!ATTLIST PROPERTY
name CDATA #REQUIRED>
-<!ELEMENT SUPERPROPERTY (RVAR)>
+<!ELEMENT SUPERPROPERTY (Rvar)>
<!ATTLIST SUPERPROPERTY
name CDATA #REQUIRED>
-<!ELEMENT SUBPROPERTY (RVAR)>
+<!ELEMENT SUBPROPERTY (Rvar)>
<!ATTLIST SUBPROPERTY
name CDATA #REQUIRED>
\ No newline at end of file
projects / helm.git / commitdiff