helm/dtd/cic.dtd

   1 <?xml 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 CIC OBJECTS:                                            -->
  29 <!--  First draft: September 1999, Claudio Sacerdoti Coen            -->
  30 <!--  Revised: February 3 2000, Claudio Sacerdoti Coen, Irene Schena -->
  31 <!--  Last Revision: April 4 2000, Claudio Sacerdoti Coen            -->
  32 <!--  Last Revision: June 19 2000, Claudio Sacerdoti Coen            -->
  33 <!--  Last Revision: June 20 2000, Claudio Sacerdoti Coen            -->
  34 <!--*****************************************************************-->
  35
  36 <!-- CIC term declaration -->
  37
  38 <!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST|
  39                   LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX)'>
  40
  41 <!-- CIC sorts -->
  42
  43 <!ENTITY % sort '(Prop|Set|Type)'>
  44
  45 <!-- CIC sequents -->
  46
  47 <!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'>
  48
  49 <!-- CIC objects: -->
  50
  51 <!ELEMENT Definition (body, type)>
  52 <!ATTLIST Definition
  53           name       CDATA      #REQUIRED
  54           params     CDATA      #REQUIRED
  55           paramMode  (POSSIBLE) #IMPLIED
  56           id         ID         #REQUIRED>
  57
  58 <!ELEMENT Axiom (type)>
  59 <!ATTLIST Axiom
  60           name   CDATA #REQUIRED
  61           params CDATA #REQUIRED
  62           id     ID    #REQUIRED>
  63
  64 <!ELEMENT CurrentProof (Conjecture*,body,type)>
  65 <!ATTLIST CurrentProof
  66           name CDATA #REQUIRED
  67           id   ID    #REQUIRED>
  68
  69 <!ELEMENT InductiveDefinition (InductiveType+)>
  70 <!ATTLIST InductiveDefinition
  71           noParams NMTOKEN #REQUIRED
  72           params   CDATA   #REQUIRED
  73           id       ID      #REQUIRED>
  74
  75 <!ELEMENT Variable (body?,type)>
  76 <!ATTLIST Variable
  77           name CDATA #REQUIRED
  78           id   ID    #REQUIRED>
  79
  80 <!ELEMENT Sequent %sequent;>
  81 <!ATTLIST Sequent
  82           no  NMTOKEN #REQUIRED
  83           id  ID      #REQUIRED>
  84
  85 <!-- Elements used in CIC objects, which are not terms: -->
  86
  87 <!ELEMENT InductiveType (arity,Constructor*)>
  88 <!ATTLIST InductiveType
  89           name      CDATA        #REQUIRED
  90           inductive (true|false) #REQUIRED>
  91
  92 <!ELEMENT Conjecture %sequent;>
  93 <!ATTLIST Conjecture
  94           no NMTOKEN #REQUIRED
  95           id ID      #REQUIRED>
  96
  97 <!ELEMENT Constructor %term;>
  98 <!ATTLIST Constructor
  99           name CDATA #REQUIRED>
 100
 101 <!ELEMENT Decl %term;>
 102 <!ATTLIST Decl
 103           name CDATA #IMPLIED
 104           id   ID    #REQUIRED>
 105
 106 <!ELEMENT Def %term;>
 107 <!ATTLIST Def
 108           name CDATA #IMPLIED
 109           id   ID    #REQUIRED>
 110
 111 <!ELEMENT Hidden EMPTY>
 112 <!ATTLIST Hidden
 113           id ID #REQUIRED>
 114
 115 <!ELEMENT Goal %term;>
 116
 117 <!-- CIC terms: -->
 118
 119 <!ELEMENT LAMBDA (source,target)>
 120 <!ATTLIST LAMBDA
 121           id   ID     #REQUIRED
 122           sort %sort; #REQUIRED>
 123
 124 <!ELEMENT LETIN (term,letintarget)>
 125 <!ATTLIST LETIN
 126           id   ID     #REQUIRED
 127           sort %sort; #REQUIRED>
 128
 129 <!ELEMENT PROD (source,target)>
 130 <!ATTLIST PROD
 131           id   ID     #REQUIRED
 132           type %sort; #REQUIRED>
 133
 134 <!ELEMENT CAST (term,type)>
 135 <!ATTLIST CAST
 136           id   ID     #REQUIRED
 137           sort %sort; #REQUIRED>
 138
 139 <!ELEMENT REL EMPTY>
 140 <!ATTLIST REL
 141           value  NMTOKEN #REQUIRED
 142           binder CDATA   #REQUIRED
 143           id     ID      #REQUIRED
 144           sort   %sort;  #REQUIRED>
 145
 146 <!ELEMENT SORT EMPTY>
 147 <!ATTLIST SORT
 148           value CDATA #REQUIRED
 149           id    ID    #REQUIRED>
 150
 151 <!ELEMENT APPLY (%term;)+>
 152 <!ATTLIST APPLY
 153           id   ID     #REQUIRED
 154           sort %sort; #REQUIRED>
 155
 156 <!ELEMENT VAR EMPTY>
 157 <!ATTLIST VAR
 158           relUri CDATA  #REQUIRED
 159           id     ID     #REQUIRED
 160           sort   %sort; #REQUIRED>
 161
 162 <!-- The substitutions are ordered by increasing DeBrujin  -->
 163 <!-- index. An empty substitution means that that index is -->
 164 <!-- not accessible.                                       -->
 165 <!ELEMENT META (substitution*)>
 166 <!ATTLIST META
 167           no              NMTOKEN #REQUIRED
 168           id              ID      #REQUIRED
 169           sort            %sort;  #REQUIRED>
 170
 171 <!ELEMENT IMPLICIT EMPTY>
 172 <!ATTLIST IMPLICIT
 173           id ID #REQUIRED>
 174
 175 <!ELEMENT CONST EMPTY>
 176 <!ATTLIST CONST
 177           uri  CDATA  #REQUIRED
 178           id   ID     #REQUIRED
 179           sort %sort; #REQUIRED>
 180
 181 <!ELEMENT MUTIND EMPTY>
 182 <!ATTLIST MUTIND
 183           uri    CDATA   #REQUIRED
 184           noType NMTOKEN #REQUIRED
 185           id     ID      #REQUIRED>
 186
 187 <!ELEMENT MUTCONSTRUCT EMPTY>
 188 <!ATTLIST MUTCONSTRUCT
 189           uri      CDATA   #REQUIRED
 190           noType   NMTOKEN #REQUIRED
 191           noConstr NMTOKEN #REQUIRED
 192           id       ID      #REQUIRED
 193           sort     %sort;  #REQUIRED>
 194
 195 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
 196 <!ATTLIST MUTCASE
 197           uriType CDATA   #REQUIRED
 198           noType  NMTOKEN #REQUIRED
 199           id      ID      #REQUIRED
 200           sort    %sort;  #REQUIRED>
 201
 202 <!ELEMENT FIX (FixFunction+)>
 203 <!ATTLIST FIX
 204           noFun NMTOKEN #REQUIRED
 205           id    ID      #REQUIRED
 206           sort  %sort;  #REQUIRED>
 207
 208 <!ELEMENT COFIX (CofixFunction+)>
 209 <!ATTLIST COFIX
 210           noFun NMTOKEN #REQUIRED
 211           id    ID      #REQUIRED
 212           sort  %sort;  #REQUIRED>
 213
 214 <!-- Elements used in CIC terms: -->
 215
 216 <!ELEMENT FixFunction (type,body)>
 217 <!ATTLIST FixFunction
 218           name     CDATA   #REQUIRED
 219           recIndex NMTOKEN #REQUIRED>
 220
 221 <!ELEMENT CofixFunction (type,body)>
 222 <!ATTLIST CofixFunction
 223           name     CDATA   #REQUIRED>
 224
 225 <!ELEMENT substitution ((%term;)?)>
 226
 227 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
 228
 229 <!ELEMENT source %term;>
 230
 231 <!ELEMENT target %term;>
 232 <!ATTLIST target
 233           binder CDATA #IMPLIED>
 234
 235 <!ELEMENT letintarget %term;>
 236 <!ATTLIST letintarget
 237           binder CDATA #REQUIRED>
 238
 239 <!ELEMENT term %term;>
 240
 241 <!ELEMENT type  %term;>
 242
 243 <!ELEMENT arity %term;>
 244
 245 <!ELEMENT patternsType  %term;>
 246
 247 <!ELEMENT inductiveTerm  %term;>
 248
 249 <!ELEMENT pattern  %term;>
 250
 251 <!ELEMENT body  %term;>