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
  46 <!-- CIC objects: -->
  47
  48 <!ELEMENT Definition (body, type)>
  49 <!ATTLIST Definition
  50           name       CDATA      #REQUIRED
  51           params     CDATA      #REQUIRED
  52           paramMode  (POSSIBLE) #IMPLIED
  53           id         ID         #REQUIRED>
  54
  55 <!ELEMENT Axiom (type)>
  56 <!ATTLIST Axiom
  57           name   CDATA #REQUIRED
  58           params CDATA #REQUIRED
  59           id     ID    #REQUIRED>
  60
  61 <!ELEMENT CurrentProof (Conjecture*,body,type)>
  62 <!ATTLIST CurrentProof
  63           name CDATA #REQUIRED
  64           id   ID    #REQUIRED>
  65
  66 <!ELEMENT InductiveDefinition (InductiveType+)>
  67 <!ATTLIST InductiveDefinition
  68           noParams NMTOKEN #REQUIRED
  69           params   CDATA   #REQUIRED
  70           id       ID      #REQUIRED>
  71
  72 <!ELEMENT Variable (body?,type)>
  73 <!ATTLIST Variable
  74           name CDATA #REQUIRED
  75           id   ID    #REQUIRED>
  76
  77 <!ELEMENT Sequent ((Decl|Def)*,Goal)>
  78 <!ATTLIST Sequent
  79           id   ID    #REQUIRED>
  80
  81 <!-- Elements used in CIC objects, which are not terms: -->
  82
  83 <!ELEMENT InductiveType (arity,Constructor*)>
  84 <!ATTLIST InductiveType
  85           name      CDATA        #REQUIRED
  86           inductive (true|false) #REQUIRED>
  87
  88 <!ELEMENT Conjecture %term;>
  89 <!ATTLIST Conjecture
  90           no NMTOKEN #REQUIRED>
  91
  92 <!ELEMENT Constructor %term;>
  93 <!ATTLIST Constructor
  94           name CDATA #REQUIRED>
  95
  96 <!ELEMENT Decl %term;>
  97 <!ATTLIST Decl
  98           name CDATA #REQUIRED>
  99
 100 <!ELEMENT Def %term;>
 101 <!ATTLIST Def
 102           name CDATA #REQUIRED>
 103
 104 <!ELEMENT Goal %term;>
 105
 106 <!-- CIC terms: -->
 107
 108 <!ELEMENT LAMBDA (source,target)>
 109 <!ATTLIST LAMBDA
 110           id   ID     #REQUIRED
 111           sort %sort; #REQUIRED>
 112
 113 <!ELEMENT LETIN (term,letintarget)>
 114 <!ATTLIST LETIN
 115           id   ID     #REQUIRED
 116           sort %sort; #REQUIRED>
 117
 118 <!ELEMENT PROD (source,target)>
 119 <!ATTLIST PROD
 120           id   ID     #REQUIRED
 121           type %sort; #REQUIRED>
 122
 123 <!ELEMENT CAST (term,type)>
 124 <!ATTLIST CAST
 125           id   ID     #REQUIRED
 126           sort %sort; #REQUIRED>
 127
 128 <!ELEMENT REL EMPTY>
 129 <!ATTLIST REL
 130           value  NMTOKEN #REQUIRED
 131           binder CDATA   #REQUIRED
 132           id     ID      #REQUIRED
 133           sort   %sort;  #REQUIRED>
 134
 135 <!ELEMENT SORT EMPTY>
 136 <!ATTLIST SORT
 137           value CDATA #REQUIRED
 138           id    ID    #REQUIRED>
 139
 140 <!ELEMENT APPLY (%term;)+>
 141 <!ATTLIST APPLY
 142           id   ID     #REQUIRED
 143           sort %sort; #REQUIRED>
 144
 145 <!ELEMENT VAR EMPTY>
 146 <!ATTLIST VAR
 147           relUri CDATA  #REQUIRED
 148           id     ID     #REQUIRED
 149           sort   %sort; #REQUIRED>
 150
 151 <!ELEMENT META EMPTY>
 152 <!ATTLIST META
 153           no   NMTOKEN #REQUIRED
 154           id   ID      #REQUIRED
 155           sort %sort;  #REQUIRED>
 156
 157 <!ELEMENT IMPLICIT EMPTY>
 158 <!ATTLIST IMPLICIT
 159           id ID #REQUIRED>
 160
 161 <!ELEMENT CONST EMPTY>
 162 <!ATTLIST CONST
 163           uri  CDATA  #REQUIRED
 164           id   ID     #REQUIRED
 165           sort %sort; #REQUIRED>
 166
 167 <!ELEMENT MUTIND EMPTY>
 168 <!ATTLIST MUTIND
 169           uri    CDATA   #REQUIRED
 170           noType NMTOKEN #REQUIRED
 171           id     ID      #REQUIRED>
 172
 173 <!ELEMENT MUTCONSTRUCT EMPTY>
 174 <!ATTLIST MUTCONSTRUCT
 175           uri      CDATA   #REQUIRED
 176           noType   NMTOKEN #REQUIRED
 177           noConstr NMTOKEN #REQUIRED
 178           id       ID      #REQUIRED
 179           sort     %sort;  #REQUIRED>
 180
 181 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
 182 <!ATTLIST MUTCASE
 183           uriType CDATA   #REQUIRED
 184           noType  NMTOKEN #REQUIRED
 185           id      ID      #REQUIRED
 186           sort    %sort;  #REQUIRED>
 187
 188 <!ELEMENT FIX (FixFunction+)>
 189 <!ATTLIST FIX
 190           noFun NMTOKEN #REQUIRED
 191           id    ID      #REQUIRED
 192           sort  %sort;  #REQUIRED>
 193
 194 <!ELEMENT COFIX (CofixFunction+)>
 195 <!ATTLIST COFIX
 196           noFun NMTOKEN #REQUIRED
 197           id    ID      #REQUIRED
 198           sort  %sort;  #REQUIRED>
 199
 200 <!-- Elements used in CIC terms: -->
 201
 202 <!ELEMENT FixFunction (type,body)>
 203 <!ATTLIST FixFunction
 204           name     CDATA   #REQUIRED
 205           recIndex NMTOKEN #REQUIRED>
 206
 207 <!ELEMENT CofixFunction (type,body)>
 208 <!ATTLIST CofixFunction
 209           name     CDATA   #REQUIRED>
 210
 211 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
 212
 213 <!ELEMENT source %term;>
 214
 215 <!ELEMENT target %term;>
 216 <!ATTLIST target
 217           binder CDATA #IMPLIED>
 218
 219 <!ELEMENT letintarget %term;>
 220 <!ATTLIST letintarget
 221           binder CDATA #REQUIRED>
 222
 223 <!ELEMENT term %term;>
 224
 225 <!ELEMENT type  %term;>
 226
 227 <!ELEMENT arity %term;>
 228
 229 <!ELEMENT patternsType  %term;>
 230
 231 <!ELEMENT inductiveTerm  %term;>
 232
 233 <!ELEMENT pattern  %term;>
 234
 235 <!ELEMENT body  %term;>