1 <?xml version="1.0" encoding="ISO-8859-1"?>
3 <!-- Copyright (C) 2000, HELM Team -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic -->
6 <!-- Library of Mathematics, developed at the Computer Science -->
7 <!-- Department, University of Bologna, Italy. -->
9 <!-- HELM is free software; you can redistribute it and/or -->
10 <!-- modify it under the terms of the GNU General Public License -->
11 <!-- as published by the Free Software Foundation; either version 2 -->
12 <!-- of the License, or (at your option) any later version. -->
14 <!-- HELM is distributed in the hope that it will be useful, -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
17 <!-- GNU General Public License for more details. -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
22 <!-- MA 02111-1307, USA. -->
24 <!-- For details, see the HELM World-Wide-Web page, -->
25 <!-- http://cs.unibo.it/helm/. -->
27 <!--*****************************************************************-->
28 <!-- DTD FOR the MATHEMATICAL QUERY MARKUP LANGUAGE (MathQML) -->
29 <!-- First draft: April 2002, Irene Schena -->
30 <!--*****************************************************************-->
32 <!--*****************************************************************-->
33 <!-- This syntax is not convenient for humans to read and write, but -->
34 <!-- it is for programs. -->
35 <!-- XMathQL is useful for: -->
36 <!-- 1) generating queries in a XML-orienting programming environment-->
37 <!-- 2) embedding queries in XML documents -->
38 <!-- 3) reusing queries saved in a standard format -->
39 <!-- The syntax reflects the structure of the grammar productions of -->
41 <!-- The %queryexpr parameter entity is used to allow all query -->
42 <!-- expression types to occur -->
43 <!-- Operators are unambiguous (binary or unary), so there isn't any -->
44 <!-- grouping operator. -->
45 <!-- CONST is the constant string. -->
46 <!-- The attributes binder and rvar declare variables which are -->
47 <!-- referred to and used by means of respectively BINDER and RVAR -->
48 <!--*****************************************************************-->
50 <!ENTITY % position '(Conclusion|Hypothesis|Body|MainConclusion|
53 <!ENTITY % order '(ascendant|descendant)'>
55 <!ENTITY % bool '(True|False)'>
57 <!-- MathQL query expression declaration -->
59 <!ENTITY % queryexpr '(Union|Intersect|Diff|SortBy|Select|Exists|Use|UsedBy|
60 ConstructorsOf|Pattern|InTheory|TheoryRefTo|TypeOf|
61 SuperTypeOf|SubTypeOf|Group)'>
63 <!-- MathQL boolean expression declaration -->
65 <!ENTITY % boolexpr '(AND|OR|NOT|BOOL|IS|GROUP)'>
67 <!-- MathQL string expression declaration -->
69 <!ENTITY % functexpr '(NAME|PROPERTY|SUPERPROPERTY|SUBPROPERTY)'>
71 <!ENTITY % stringexpr '(CONST|POSITION|RVAR|BINDER|%functexpr;)'>
74 <!-- MathQL top-element -->
76 <!ELEMENT MathQL %queryexpr;>
78 <!-- MathQL query expressions -->
80 <!ELEMENT Union (%queryexpr;, %queryexpr;)>
82 <!ELEMENT Intersect (%queryexpr;, %queryexpr;)>
84 <!ELEMENT Diff (%queryexpr;, %queryexpr;)>
86 <!ELEMENT SortBy (%queryexpr;, SortField)>
88 <!ELEMENT Select (In, Where)>
90 <!ELEMENT Exists (In, Where)>
92 <!ELEMENT Use (%queryexpr;, Position)>
94 <!ELEMENT Position EMPTY>
96 binder CDATA #REQUIRED>
98 <!ELEMENT UsedBy (%queryexpr;, Position)>
100 <!ELEMENT ConstructorsOf %queryexpr;>
102 <!ELEMENT Pattern (Prefix, TokenList, (FragmentID?))>
104 <!ELEMENT InTheory (%queryexpr;, ItemType)>
106 <!ELEMENT ItemType EMPTY>
108 binder CDATA #REQUIRED>
110 <!ELEMENT TheoryRefTo %queryexpr;>
112 <!ELEMENT TypeOf %queryexpr;>
114 binder CDATA #REQUIRED>
116 <!ELEMENT SuperTypeOf %queryexpr;>
117 <!ATTLIST SuperTypeOf
118 binder CDATA #REQUIRED>
120 <!ELEMENT SubTypeOf %queryexpr;>
122 binder CDATA #REQUIRED>
124 <!-- MathQL query sub-expressions -->
126 <!ELEMENT SortField %functexpr;>
128 order %order; #IMPLIED>
130 <!ELEMENT In %queryexpr;>
132 <!ELEMENT Where %boolexpr;>
134 rvar CDATA #REQUIRED>
136 <!ELEMENT STAR EMPTY>
138 <!ELEMENT TWOSTARS EMPTY>
140 <!ELEMENT SLASH EMPTY>
142 <!ELEMENT QUESTIONMARK EMPTY>
144 <!ELEMENT NUMBER EMPTY>
146 value NMTOKEN #REQUIRED>
148 <!-- STAR expands only to objects of the specified dir before the last "/":
149 ex. cic:/Algebra/* expands to every object in Algebra only -->
150 <!-- TWOSTARS expands till the most complete name (with extension if not
152 <!-- QUESTIONMARK matches one character except "/" -->
153 <!ELEMENT TokenList (CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)+>
155 <!ELEMENT Prefix (CONST|STAR)>
157 <!-- XPointers have max depth = 2 (see CIC inductive definitions) -->
158 <!ELEMENT FragmentID (NUMBER|TWOSTARS|STAR)+>
160 <!-- MathQL boolean expressions -->
162 <!ELEMENT AND (%boolexpr;, %boolexpr;)>
164 <!ELEMENT OR (%boolexpr;, %boolexpr;)>
166 <!ELEMENT NOT %boolexpr;>
168 <!ELEMENT IS (%stringexpr;, %stringexpr;)>
170 <!ELEMENT BOOL EMPTY>
172 value %bool; #REQUIRED>
174 <!-- MathQL string expressions -->
176 <!ELEMENT CONST (#PCDATA)>
178 <!ELEMENT RVAR EMPTY>
180 name CDATA #REQUIRED>
182 <!ELEMENT BINDER EMPTY>
184 name CDATA #REQUIRED>
186 <!ELEMENT POSITION EMPTY>
188 name %position; #REQUIRED>
190 <!ELEMENT NAME (RVAR)>
192 <!ELEMENT PROPERTY (RVAR)>
194 name CDATA #REQUIRED>
196 <!ELEMENT SUPERPROPERTY (RVAR)>
197 <!ATTLIST SUPERPROPERTY
198 name CDATA #REQUIRED>
200 <!ELEMENT SUBPROPERTY (RVAR)>
201 <!ATTLIST SUBPROPERTY
202 name CDATA #REQUIRED>