helm/mathql/xmathql.dtd

   1 <?xml version="1.0" encoding="ISO-8859-1"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   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.                         -->
   8 <!--                                                                   -->
   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.            -->
  13 <!--                                                                   -->
  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.                      -->
  18 <!--                                                                   -->
  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.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <!--*****************************************************************-->
  28 <!-- DTD FOR the MATHEMATICAL QUERY MARKUP LANGUAGE (XMathQL)        -->
  29 <!-- First draft: April 2002, Irene Schena                           -->
  30 <!--*****************************************************************-->
  31
  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 -->
  40 <!-- MathQL.                                                         -->
  41 <!-- Operators are unambiguous (binary or unary), so there isn't any -->
  42 <!-- grouping operator.                                              -->
  43 <!-- CONST is the constant string; rvar is for references and lvar   -->
  44 <!-- for list.                                                       -->
  45 <!-- The attributes binder, rvar, lvar declare variables which are   -->
  46 <!-- referred to and used by means of respectively BINDER, Rvar and  -->
  47 <!-- RVAR, Lvar and LVAR.                                            -->
  48 <!-- Rvar (Lvar) is casted to a list, on the contrary the use of RVAR-->
  49 <!-- (LVAR) is casted to a string.                                   -->
  50 <!-- PROPERTY works on a specified RDF property returning its value. -->
  51 <!--*****************************************************************-->
  52
  53 <!ENTITY % position '(MainHypothesis|Hypothesis|MainConclusion|Conclusion|
  54                       Body)'>
  55
  56 <!ENTITY % bool '(True|False)'>
  57
  58 <!ENTITY % token '(CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)'>
  59
  60 <!-- MathQL list expression declaration -->
  61
  62 <!ENTITY % listexpr '(Rvar|Lvar|Reference|Pattern|Select|Exists|LetIn|
  63                       Use|UsedBy|ConstructorsOf|InTheory|TheoryRefTo|
  64                       TypeOf|SuperTypeOf|SubTypeOf|Union|Intersect|Diff)'>
  65
  66 <!-- MathQL boolean expression declaration -->
  67
  68 <!ENTITY % boolexpr '(BOOL|NOT|AND|OR|IS|SETEQUAL|SUBSET)'>
  69
  70 <!-- MathQL string expression declaration -->
  71
  72 <!ENTITY % functexpr '(NAME|PROPERTY|SUPERPROPERTY|SUBPROPERTY)'>
  73
  74 <!ENTITY % stringexpr '(CONST|POSITION|RVAR|BINDER|%functexpr;)'>
  75
  76
  77 <!-- MathQL query top-element -->
  78
  79 <!ELEMENT MQLquery %listexpr;>
  80
  81 <!-- MathQL list expressions -->
  82 <!ELEMENT Rvar EMPTY>
  83 <!ATTLIST Rvar
  84           name CDATA #REQUIRED>
  85
  86 <!ELEMENT Lvar EMPTY>
  87 <!ATTLIST Lvar
  88           name CDATA #REQUIRED>
  89
  90 <!ELEMENT Reference (RPrefix, RBody, Ext, (RFragmentID?))>
  91
  92 <!ELEMENT Pattern (PPrefix, PBody, (Ext?), (PFragmentID?))>
  93
  94 <!ELEMENT Select (In, Where)>
  95
  96 <!ELEMENT Exists (In, Where)>
  97
  98 <!ELEMENT LetIn (%listexpr;, Target)>
  99
 100 <!ELEMENT Use (%listexpr;, Position)>
 101
 102 <!ELEMENT UsedBy (%listexpr;, Position)>
 103
 104 <!ELEMENT ConstructorsOf %listexpr;>
 105
 106 <!ELEMENT InTheory (%listexpr;, ItemType)>
 107
 108 <!ELEMENT TheoryRefTo %listexpr;>
 109
 110 <!ELEMENT TypeOf %listexpr;>
 111 <!ATTLIST TypeOf
 112           binder CDATA #REQUIRED>
 113
 114 <!ELEMENT SuperTypeOf %listexpr;>
 115 <!ATTLIST SuperTypeOf
 116           binder CDATA #REQUIRED>
 117
 118 <!ELEMENT SubTypeOf %listexpr;>
 119 <!ATTLIST SubTypeOf
 120           binder CDATA #REQUIRED>
 121
 122 <!ELEMENT Union (%listexpr;, %listexpr;)>
 123
 124 <!ELEMENT Intersect (%listexpr;, %listexpr;)>
 125
 126 <!ELEMENT Diff (%listexpr;, %listexpr;)>
 127
 128 <!-- MathQL list sub-expressions -->
 129
 130 <!ELEMENT RPrefix (CONST)>
 131
 132 <!ELEMENT RBody (CONST)>
 133
 134 <!ELEMENT RFragmentID (NUMBER)+>
 135
 136 <!ELEMENT Ext (CONST)>
 137
 138 <!ELEMENT PPrefix (CONST|STAR)>
 139
 140 <!ELEMENT PBody (%token;)+>
 141
 142 <!-- XPointers have max depth = 2 (see CIC inductive definitions) -->
 143 <!ELEMENT PFragmentID (NUMBER|TWOSTARS|STAR)+>
 144
 145 <!ELEMENT NUMBER EMPTY>
 146 <!ATTLIST NUMBER
 147           value NMTOKEN #REQUIRED>
 148
 149 <!-- We need SLASH for grouping CONST with QUESTIONMARK -->
 150 <!ELEMENT SLASH EMPTY>
 151
 152 <!-- STAR expands only to objects of the specified dir before the last "/":
 153      ex. cic:/Algebra/* expands to every object in Algebra only            -->
 154 <!ELEMENT STAR EMPTY>
 155
 156 <!-- TWOSTARS expands till the most complete name (with extension if not
 157      specifified)                                                          -->
 158 <!ELEMENT TWOSTARS EMPTY>
 159
 160 <!-- QUESTIONMARK matches one character except "/"                         -->
 161 <!ELEMENT QUESTIONMARK EMPTY>
 162
 163 <!ELEMENT In %listexpr;>
 164
 165 <!ELEMENT Where %boolexpr;>
 166 <!ATTLIST Where
 167           rvar CDATA #REQUIRED>
 168
 169 <!ELEMENT Target %listexpr;>
 170 <!ATTLIST Target
 171           lvar CDATA #REQUIRED>
 172
 173 <!ELEMENT Position EMPTY>
 174 <!ATTLIST Position
 175           binder CDATA #REQUIRED>
 176
 177 <!ELEMENT ItemType EMPTY>
 178 <!ATTLIST ItemType
 179           binder CDATA #REQUIRED>
 180
 181 <!-- MathQL boolean expressions -->
 182
 183 <!ELEMENT BOOL EMPTY>
 184 <!ATTLIST BOOL
 185           value %bool; #REQUIRED>
 186
 187 <!ELEMENT NOT %boolexpr;>
 188
 189 <!ELEMENT AND (%boolexpr;, %boolexpr;)>
 190
 191 <!ELEMENT OR (%boolexpr;, %boolexpr;)>
 192
 193 <!ELEMENT IS (%stringexpr;, %stringexpr;)>
 194
 195 <!ELEMENT SETEQUAL (%listexpr;, %listexpr;)>
 196
 197 <!ELEMENT SUBSET (%listexpr;, %listexpr;)>
 198
 199 <!-- MathQL string expressions -->
 200
 201 <!ELEMENT CONST (#PCDATA)>
 202
 203 <!ELEMENT RVAR EMPTY>
 204 <!ATTLIST RVAR
 205           name CDATA #REQUIRED>
 206
 207 <!ELEMENT BINDER EMPTY>
 208 <!ATTLIST BINDER
 209           name CDATA #REQUIRED>
 210
 211 <!ELEMENT POSITION EMPTY>
 212 <!ATTLIST POSITION
 213           name %position; #REQUIRED>
 214
 215 <!ELEMENT NAME (RVAR)>
 216
 217 <!ELEMENT PROPERTY (RVAR)>
 218 <!ATTLIST PROPERTY
 219           name CDATA #REQUIRED>
 220
 221 <!ELEMENT SUPERPROPERTY (RVAR)>
 222 <!ATTLIST SUPERPROPERTY
 223           name CDATA #REQUIRED>
 224
 225 <!ELEMENT SUBPROPERTY (RVAR)>
 226 <!ATTLIST SUBPROPERTY
 227           name CDATA #REQUIRED>