X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fxmathql.dtd;h=63c0145655b51ab407aafb1b39fe9964814adc62;hb=86ec68f575f6f781572d14d0aba9a98a860c94a6;hp=e32b0299fb7dbe57b8a7289fb0de99288cc6273e;hpb=11ca09baa5979991650a11878ce807a21ba978ea;p=helm.git

diff --git a/helm/mathql/xmathql.dtd b/helm/mathql/xmathql.dtd
index e32b0299f..63c014565 100644
--- a/helm/mathql/xmathql.dtd
+++ b/helm/mathql/xmathql.dtd
@@ -25,8 +25,9 @@
 <!-- http://cs.unibo.it/helm/.                                         -->
 
 <!--*****************************************************************-->
-<!-- DTD FOR the MATHEMATICAL QUERY MARKUP LANGUAGE (MathQML)        -->
+<!-- DTD FOR the MATHEMATICAL QUERY MARKUP LANGUAGE (XMathQL)        -->
 <!-- First draft: April 2002, Irene Schena                           -->
+<!-- Second draft: Agust 2002, Irene Schena                          -->
 <!--*****************************************************************-->
 
 <!--*****************************************************************-->
@@ -38,165 +39,119 @@
 <!-- 3) reusing queries saved in a standard format                   -->
 <!-- The syntax reflects the structure of the grammar productions of -->
 <!-- MathQL.                                                         -->
-<!-- The %queryexpr parameter entity is used to allow all query      -->
-<!-- expression types to occur                                       -->
 <!-- Operators are unambiguous (binary or unary), so there isn't any -->
 <!-- grouping operator.                                              -->
-<!-- CONST is the constant string.                                   -->
-<!-- The attributes binder and rvar declare variables which are      -->
-<!-- referred to and used by means of respectively BINDER and RVAR   -->
+<!-- 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 % position '(Conclusion|Hypothesis|Body|MainConclusion|
-                        MainHypothesis)'>
-
-<!ENTITY % order '(ascendant|descendant)'>
-
 <!ENTITY % bool '(True|False)'>
 
 <!-- MathQL query expression declaration -->
 
-<!ENTITY % queryexpr '(Union|Intersect|Diff|SortBy|Select|Exists|Use|UsedBy|
-                   ConstructorsOf|Pattern|InTheory|TheoryRefTo|TypeOf|
-                   SuperTypeOf|SubTypeOf|Group)'>
+<!ENTITY % setexpr '(Rvar|Svar|Ref|Pattern|Select|LetIn|Relation|
+                     Union|Intersect|Diff)'>
 
 <!-- MathQL boolean expression declaration -->
 
-<!ENTITY % boolexpr '(AND|OR|NOT|BOOL|IS|GROUP)'>
+<!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)'>
 
-<!ENTITY % stringexpr '(CONST|POSITION|RVAR|BINDER|%functexpr;)'>
+<!ENTITY % stringsetexpr '(CONST|CONSTLIST|REFOF|BINDER|%functexpr;)'>
 
 
-<!-- MathQL top-element -->
+<!-- MathQL query top-element -->
 
-<!ELEMENT MathQL %queryexpr;>
+<!ELEMENT MQLquery %setexpr;>
 
-<!-- MathQL query expressions -->
+<!-- MathQL set expressions -->
 
-<!ELEMENT Union (%queryexpr;, %queryexpr;)>
+<!ELEMENT Rvar EMPTY>
+<!ATTLIST Rvar
+          name CDATA #REQUIRED>
 
-<!ELEMENT Intersect (%queryexpr;, %queryexpr;)>
+<!ELEMENT Svar EMPTY>
+<!ATTLIST Svar
+          name CDATA #REQUIRED>
 
-<!ELEMENT Diff (%queryexpr;, %queryexpr;)>
+<!ELEMENT Ref %stringsetexpr;>
 
-<!ELEMENT SortBy (%queryexpr;, SortField)>
+<!ELEMENT Pattern %stringsetexpr;>
 
 <!ELEMENT Select (In, Where)>
 
-<!ELEMENT Exists (In, Where)>
+<!ELEMENT LetIn (%setexpr;, Target)>
 
-<!ELEMENT Use (%queryexpr;, Position)>
+<!ELEMENT Relation (Refine?,%setexpr;, Attr+)>
+<!ATTLIST Relation
+          name CDATA #REQUIRED
+          refine (sub|super) #IMPLIED>
 
-<!ELEMENT Position EMPTY>
-<!ATTLIST Position
-          binder CDATA #REQUIRED>
+<!ELEMENT Union (%setexpr;, %setexpr;)>
 
-<!ELEMENT UsedBy (%queryexpr;, Position)>
+<!ELEMENT Intersect (%setexpr;, %setexpr;)>
 
-<!ELEMENT ConstructorsOf %queryexpr;>
+<!ELEMENT Diff (%setexpr;, %setexpr;)>
 
-<!ELEMENT Pattern (Prefix, TokenList, (FragmentID?))>
+<!-- MathQL set sub-expressions -->
 
-<!ELEMENT InTheory (%queryexpr;, ItemType)>
-
-<!ELEMENT ItemType EMPTY>
-<!ATTLIST ItemType
-          binder CDATA #REQUIRED>
-
-<!ELEMENT TheoryRefTo %queryexpr;>
-
-<!ELEMENT TypeOf %queryexpr;>
-<!ATTLIST TypeOf
-          binder CDATA #REQUIRED>
-
-<!ELEMENT SuperTypeOf %queryexpr;>
-<!ATTLIST SuperTypeOf
-          binder CDATA #REQUIRED>
-
-<!ELEMENT SubTypeOf %queryexpr;>
-<!ATTLIST SubTypeOf
-          binder CDATA #REQUIRED>
-
-<!-- MathQL query sub-expressions -->
-
-<!ELEMENT SortField %functexpr;>
-<!ATTLIST SortField 
-          order %order; #IMPLIED>
-
-<!ELEMENT In %queryexpr;>
+<!ELEMENT In %setexpr;>
 
 <!ELEMENT Where %boolexpr;>
 <!ATTLIST Where
           rvar CDATA #REQUIRED>
 
-<!ELEMENT STAR EMPTY>
-
-<!ELEMENT TWOSTARS EMPTY>
-
-<!ELEMENT SLASH EMPTY>
-
-<!ELEMENT QUESTIONMARK EMPTY>
-
-<!ELEMENT NUMBER EMPTY>
-<!ATTLIST NUMBER
-          value NMTOKEN #REQUIRED>
+<!ELEMENT Target %setexpr;>
+<!ATTLIST Target
+          svar CDATA #REQUIRED>
 
-<!-- STAR expands only to objects of the specified dir before the last "/": 
-     ex. cic:/Algebra/* expands to every object in Algebra only            -->
-<!-- TWOSTARS expands till the most complete name (with extension if not 
-     specifified)                                                          -->
-<!-- QUESTIONMARK matches one character except "/"                         --> 
-<!ELEMENT TokenList (CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)+>
+<!ELEMENT Attr EMPTY>
+<!ATTLIST Attr 
+          binder CDATA #REQUIRED>
 
-<!ELEMENT Prefix (#PCDATA)>
+<!-- MathQL boolean expressions -->
 
-<!-- XPointers have max depth = 2 (see CIC inductive definitions) -->
-<!ELEMENT FragmentID ((NUMBER|STAR), (NUMBER|STAR)?)>
+<!ELEMENT BOOL EMPTY>
+<!ATTLIST BOOL
+          value %bool; #REQUIRED>
 
-<!-- MathQL boolean expressions -->
+<!ELEMENT NOT %boolexpr;>
 
 <!ELEMENT AND (%boolexpr;, %boolexpr;)>
 
 <!ELEMENT OR (%boolexpr;, %boolexpr;)>
 
-<!ELEMENT NOT %boolexpr;>
+<!ELEMENT EQ (%stringsetexpr;, %stringsetexpr;)>
 
-<!ELEMENT IS (%stringexpr;, %stringexpr;)>
-
-<!ELEMENT BOOL EMPTY>
-<!ATTLIST BOOL
-          value %bool; #REQUIRED>
+<!ELEMENT SUB (%stringsetexpr;, %stringsetexpr;)>
 
-<!-- MathQL string expressions -->
+<!ELEMENT MEET (%stringsetexpr;, %stringsetexpr;)>
 
-<!ELEMENT CONST (#PCDATA)>
+<!ELEMENT EX %boolexpr;>
 
-<!ELEMENT RVAR EMPTY>
-<!ATTLIST RVAR
-          name CDATA #REQUIRED>
+<!-- MathQL string-set expressions -->
 
-<!ELEMENT BINDER EMPTY>
-<!ATTLIST BINDER
-          name CDATA #REQUIRED>
+<!ELEMENT CONST (#PCDATA)>
 
-<!ELEMENT POSITION EMPTY>
-<!ATTLIST POSITION
-          name %position; #REQUIRED>
+<!ELEMENT CONSTLIST (CONST*)>
 
-<!ELEMENT NAME (RVAR)>
+<!ELEMENT REFOF %setexpr;>
 
-<!ELEMENT PROPERTY (RVAR)>
-<!ATTLIST PROPERTY
+<!ELEMENT BINDER (Rvar)>
+<!ATTLIST BINDER
           name CDATA #REQUIRED>
 
-<!ELEMENT SUPERPROPERTY (RVAR)>
-<!ATTLIST SUPERPROPERTY
+<!ELEMENT FUN %stringsetexpr;>
+<!ATTLIST FUN
           name CDATA #REQUIRED>
 
-<!ELEMENT SUBPROPERTY (RVAR)>
-<!ATTLIST SUBPROPERTY
-          name CDATA #REQUIRED>
\ No newline at end of file
+<!ELEMENT PROPERTY %stringsetexpr;>
+<!ATTLIST PROPERTY
+          name CDATA #REQUIRED
+          refine (sub|super) #IMPLIED>
\ No newline at end of file