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

diff --git a/helm/mathql/xmathql.dtd b/helm/mathql/xmathql.dtd
index 88462d5d2..63c014565 100644
--- a/helm/mathql/xmathql.dtd
+++ b/helm/mathql/xmathql.dtd
@@ -27,6 +27,7 @@
 <!--*****************************************************************-->
 <!-- DTD FOR the MATHEMATICAL QUERY MARKUP LANGUAGE (XMathQL)        -->
 <!-- First draft: April 2002, Irene Schena                           -->
+<!-- Second draft: Agust 2002, Irene Schena                          -->
 <!--*****************************************************************-->
 
 <!--*****************************************************************-->
@@ -40,142 +41,78 @@
 <!-- MathQL.                                                         -->
 <!-- Operators are unambiguous (binary or unary), so there isn't any -->
 <!-- grouping operator.                                              -->
-<!-- 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 % position '(MainHypothesis|Hypothesis|MainConclusion|Conclusion|
-                      Body)'>
-
 <!ENTITY % bool '(True|False)'>
 
-<!ENTITY % token '(CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)'>
-
-<!-- MathQL list expression declaration -->
+<!-- MathQL query expression declaration -->
 
-<!ENTITY % listexpr '(Rvar|Lvar|Reference|Pattern|Select|Exists|LetIn|
-                      Use|UsedBy|ConstructorsOf|InTheory|TheoryRefTo|
-                      TypeOf|SuperTypeOf|SubTypeOf|Union|Intersect|Diff)'>
+<!ENTITY % setexpr '(Rvar|Svar|Ref|Pattern|Select|LetIn|Relation|
+                     Union|Intersect|Diff)'>
 
 <!-- MathQL boolean expression declaration -->
 
-<!ENTITY % boolexpr '(BOOL|NOT|AND|OR|IS|SETEQUAL|SUBSET)'>
+<!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 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 Exists (In, Where)>
-
-<!ELEMENT LetIn (%listexpr;, Target)>
-
-<!ELEMENT Use (%listexpr;, Position)>
-
-<!ELEMENT UsedBy (%listexpr;, Position)>
-
-<!ELEMENT ConstructorsOf %listexpr;>
-
-<!ELEMENT InTheory (%listexpr;, ItemType)>
-
-<!ELEMENT TheoryRefTo %listexpr;>
-
-<!ELEMENT TypeOf %listexpr;>
-<!ATTLIST TypeOf
-          binder CDATA #REQUIRED>
-
-<!ELEMENT SuperTypeOf %listexpr;>
-<!ATTLIST SuperTypeOf
-          binder CDATA #REQUIRED>
-
-<!ELEMENT SubTypeOf %listexpr;>
-<!ATTLIST SubTypeOf
-          binder CDATA #REQUIRED>
-
-<!ELEMENT Union (%listexpr;, %listexpr;)>
-
-<!ELEMENT Intersect (%listexpr;, %listexpr;)>
-
-<!ELEMENT Diff (%listexpr;, %listexpr;)>
-
-<!-- MathQL list sub-expressions -->
+<!ELEMENT LetIn (%setexpr;, Target)>
 
-<!ELEMENT RPrefix (CONST)>
+<!ELEMENT Relation (Refine?,%setexpr;, Attr+)>
+<!ATTLIST Relation
+          name CDATA #REQUIRED
+          refine (sub|super) #IMPLIED>
 
-<!ELEMENT RBody (CONST)>
+<!ELEMENT Union (%setexpr;, %setexpr;)>
 
-<!ELEMENT RFragmentID (NUMBER)+>
+<!ELEMENT Intersect (%setexpr;, %setexpr;)>
 
-<!ELEMENT Ext (CONST)>
+<!ELEMENT Diff (%setexpr;, %setexpr;)>
 
-<!ELEMENT PPrefix (CONST|STAR)>
+<!-- MathQL set sub-expressions -->
 
-<!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>
-
-<!ELEMENT Position EMPTY>
-<!ATTLIST Position
-          binder CDATA #REQUIRED>
+          svar CDATA #REQUIRED>
 
-<!ELEMENT ItemType EMPTY>
-<!ATTLIST ItemType
+<!ELEMENT Attr EMPTY>
+<!ATTLIST Attr 
           binder CDATA #REQUIRED>
 
 <!-- MathQL boolean expressions -->
@@ -190,38 +127,31 @@
 
 <!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;)>
 
-<!-- MathQL string expressions -->
+<!ELEMENT EX %boolexpr;>
 
-<!ELEMENT CONST (#PCDATA)>
-
-<!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