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
  96 <!ELEMENT Constructor %term;>
  97 <!ATTLIST Constructor
  98           name CDATA #REQUIRED>
  99
 100 <!ELEMENT Decl %term;>
 101 <!ATTLIST Decl
 102           name CDATA #IMPLIED>
 103
 104 <!ELEMENT Def %term;>
 105 <!ATTLIST Def
 106           name CDATA #IMPLIED>
 107
 108 <!ELEMENT Hidden EMPTY>
 109
 110 <!ELEMENT Goal %term;>
 111
 112 <!-- CIC terms: -->
 113
 114 <!ELEMENT LAMBDA (source,target)>
 115 <!ATTLIST LAMBDA
 116           id   ID     #REQUIRED
 117           sort %sort; #REQUIRED>
 118
 119 <!ELEMENT LETIN (term,letintarget)>
 120 <!ATTLIST LETIN
 121           id   ID     #REQUIRED
 122           sort %sort; #REQUIRED>
 123
 124 <!ELEMENT PROD (source,target)>
 125 <!ATTLIST PROD
 126           id   ID     #REQUIRED
 127           type %sort; #REQUIRED>
 128
 129 <!ELEMENT CAST (term,type)>
 130 <!ATTLIST CAST
 131           id   ID     #REQUIRED
 132           sort %sort; #REQUIRED>
 133
 134 <!ELEMENT REL EMPTY>
 135 <!ATTLIST REL
 136           value  NMTOKEN #REQUIRED
 137           binder CDATA   #REQUIRED
 138           id     ID      #REQUIRED
 139           sort   %sort;  #REQUIRED>
 140
 141 <!ELEMENT SORT EMPTY>
 142 <!ATTLIST SORT
 143           value CDATA #REQUIRED
 144           id    ID    #REQUIRED>
 145
 146 <!ELEMENT APPLY (%term;)+>
 147 <!ATTLIST APPLY
 148           id   ID     #REQUIRED
 149           sort %sort; #REQUIRED>
 150
 151 <!ELEMENT VAR EMPTY>
 152 <!ATTLIST VAR
 153           relUri CDATA  #REQUIRED
 154           id     ID     #REQUIRED
 155           sort   %sort; #REQUIRED>
 156
 157 <!-- The substitutions are ordered by increasing DeBrujin  -->
 158 <!-- index. An empty substitution means that that index is -->
 159 <!-- not accessible.                                       -->
 160 <!ELEMENT META (substitution*)>
 161 <!ATTLIST META
 162           no              NMTOKEN #REQUIRED
 163           id              ID      #REQUIRED
 164           sort            %sort;  #REQUIRED>
 165
 166 <!ELEMENT IMPLICIT EMPTY>
 167 <!ATTLIST IMPLICIT
 168           id ID #REQUIRED>
 169
 170 <!ELEMENT CONST EMPTY>
 171 <!ATTLIST CONST
 172           uri  CDATA  #REQUIRED
 173           id   ID     #REQUIRED
 174           sort %sort; #REQUIRED>
 175
 176 <!ELEMENT MUTIND EMPTY>
 177 <!ATTLIST MUTIND
 178           uri    CDATA   #REQUIRED
 179           noType NMTOKEN #REQUIRED
 180           id     ID      #REQUIRED>
 181
 182 <!ELEMENT MUTCONSTRUCT EMPTY>
 183 <!ATTLIST MUTCONSTRUCT
 184           uri      CDATA   #REQUIRED
 185           noType   NMTOKEN #REQUIRED
 186           noConstr NMTOKEN #REQUIRED
 187           id       ID      #REQUIRED
 188           sort     %sort;  #REQUIRED>
 189
 190 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
 191 <!ATTLIST MUTCASE
 192           uriType CDATA   #REQUIRED
 193           noType  NMTOKEN #REQUIRED
 194           id      ID      #REQUIRED
 195           sort    %sort;  #REQUIRED>
 196
 197 <!ELEMENT FIX (FixFunction+)>
 198 <!ATTLIST FIX
 199           noFun NMTOKEN #REQUIRED
 200           id    ID      #REQUIRED
 201           sort  %sort;  #REQUIRED>
 202
 203 <!ELEMENT COFIX (CofixFunction+)>
 204 <!ATTLIST COFIX
 205           noFun NMTOKEN #REQUIRED
 206           id    ID      #REQUIRED
 207           sort  %sort;  #REQUIRED>
 208
 209 <!-- Elements used in CIC terms: -->
 210
 211 <!ELEMENT FixFunction (type,body)>
 212 <!ATTLIST FixFunction
 213           name     CDATA   #REQUIRED
 214           recIndex NMTOKEN #REQUIRED>
 215
 216 <!ELEMENT CofixFunction (type,body)>
 217 <!ATTLIST CofixFunction
 218           name     CDATA   #REQUIRED>
 219
 220 <!ELEMENT substitution ((%term;)?)>
 221
 222 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
 223
 224 <!ELEMENT source %term;>
 225
 226 <!ELEMENT target %term;>
 227 <!ATTLIST target
 228           binder CDATA #IMPLIED>
 229
 230 <!ELEMENT letintarget %term;>
 231 <!ATTLIST letintarget
 232           binder CDATA #REQUIRED>
 233
 234 <!ELEMENT term %term;>
 235
 236 <!ELEMENT type  %term;>
 237
 238 <!ELEMENT arity %term;>
 239
 240 <!ELEMENT patternsType  %term;>
 241
 242 <!ELEMENT inductiveTerm  %term;>
 243
 244 <!ELEMENT pattern  %term;>
 245
 246 <!ELEMENT body  %term;>