X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fxmathql.dtd;h=96b52a22b17c4f3a2a2a155374c597026748d883;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a5bd242e7b108bd98d09e8386aba45db3527edcf;hpb=14a126b578b2c9a26d849553c65cec5e381df8fb;p=helm.git

diff --git a/helm/mathql/xmathql.dtd b/helm/mathql/xmathql.dtd
index a5bd242e7..96b52a22b 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,127 @@
 <!-- 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|LetSIn|LetVIn|Relation|
+                     Union|Intersect|Diff)'>
 
 <!-- MathQL boolean expression declaration -->
 
-<!ENTITY % boolexpr '(AND|OR|NOT|BOOL|IS|GROUP)'>
-
-<!-- MathQL string expression declaration -->
+<!ENTITY % boolexpr '(BOOL|NOT|AND|OR|EQ|SUB|MEET|EX)'>
 
-<!ENTITY % functexpr '(NAME|PROPERTY|SUPERPROPERTY|SUBPROPERTY)'>
+<!-- MathQL string-set expression declaration -->
 
-<!ENTITY % stringexpr '(CONST|POSITION|RVAR|BINDER|%functexpr;)'>
+<!ENTITY % functexpr '(FUN|PROPERTY)'>
 
+<!ENTITY % stringsetexpr '(CONST|CONSTLIST|REFOF|BINDER|VVAR|%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 Use (%queryexpr;, Position)>
-
-<!ELEMENT Position EMPTY>
-<!ATTLIST Position
-          binder CDATA #REQUIRED>
-
-<!ELEMENT UsedBy (%queryexpr;, Position)>
-
-<!ELEMENT ConstructorsOf %queryexpr;>
+<!ELEMENT LetSIn (%setexpr;, Starget)>
 
-<!ELEMENT Pattern (Prefix, TokenList, (FragmentID?))>
+<!ELEMENT LetVIn (%stringsetexpr;, Vtarget)>
 
-<!ELEMENT InTheory (%queryexpr;, ItemType)>
+<!ELEMENT Relation (PName?,%setexpr;, Attr+)>
+<!ATTLIST Relation
+          name CDATA #REQUIRED
+          refine (sub|super) #IMPLIED>
 
-<!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 Union (%setexpr;, %setexpr;)>
 
-<!ELEMENT SubTypeOf %queryexpr;>
-<!ATTLIST SubTypeOf
-          binder CDATA #REQUIRED>
+<!ELEMENT Intersect (%setexpr;, %setexpr;)>
 
-<!-- MathQL query sub-expressions -->
+<!ELEMENT Diff (%setexpr;, %setexpr;)>
 
-<!ELEMENT SortField %functexpr;>
-<!ATTLIST SortField 
-          order %order; #IMPLIED>
+<!-- MathQL set sub-expressions -->
 
-<!ELEMENT In %queryexpr;>
+<!ELEMENT In %setexpr;>
 
 <!ELEMENT Where %boolexpr;>
 <!ATTLIST Where
           rvar CDATA #REQUIRED>
 
-<!ELEMENT STAR EMPTY>
-
-<!ELEMENT TWOSTARS EMPTY>
+<!ELEMENT Starget %setexpr;>
+<!ATTLIST Starget
+          svar CDATA #REQUIRED>
 
-<!ELEMENT SLASH EMPTY>
+<!ELEMENT Vtarget %setexpr;>
+<!ATTLIST Vtarget
+          vvar CDATA #REQUIRED>
 
-<!ELEMENT QUESTIONMARK EMPTY>
-
-<!ELEMENT NUMBER EMPTY>
-<!ATTLIST NUMBER
-          value NMTOKEN #REQUIRED>
+<!ELEMENT Attr EMPTY>
+<!ATTLIST Attr 
+          binder 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 PName (CONST+)>
 
-<!ELEMENT Prefix (CONST|STAR)>
+<!-- MathQL boolean expressions -->
 
-<!-- XPointers have max depth = 2 (see CIC inductive definitions) -->
-<!ELEMENT FragmentID (NUMBER|TWOSTARS|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 SUB (%stringsetexpr;, %stringsetexpr;)>
 
-<!ELEMENT BOOL EMPTY>
-<!ATTLIST BOOL
-          value %bool; #REQUIRED>
+<!ELEMENT MEET (%stringsetexpr;, %stringsetexpr;)>
 
-<!-- MathQL string expressions -->
+<!ELEMENT EX %boolexpr;>
 
-<!ELEMENT CONST (#PCDATA)>
+<!-- MathQL string-set expressions -->
 
-<!ELEMENT RVAR EMPTY>
-<!ATTLIST RVAR
-          name CDATA #REQUIRED>
+<!ELEMENT CONST (#PCDATA)>
 
-<!ELEMENT BINDER EMPTY>
-<!ATTLIST BINDER
-          name CDATA #REQUIRED>
+<!ELEMENT CONSTLIST (CONST*)>
 
-<!ELEMENT POSITION EMPTY>
-<!ATTLIST POSITION
-          name %position; #REQUIRED>
+<!ELEMENT REFOF %setexpr;>
 
-<!ELEMENT NAME (RVAR)>
+<!ELEMENT VVAR %stringsetexpr;>
 
-<!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 (Refine?,%stringsetexpr;)>
+<!ATTLIST PROPERTY
+          name CDATA #REQUIRED>