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 <!-- Elements used in CIC objects, which are not terms: -->
  78
  79 <!ELEMENT InductiveType (arity,Constructor*)>
  80 <!ATTLIST InductiveType
  81           name      CDATA        #REQUIRED
  82           inductive (true|false) #REQUIRED>
  83
  84 <!ELEMENT Conjecture %term;>
  85 <!ATTLIST Conjecture
  86           no NMTOKEN #REQUIRED>
  87
  88 <!ELEMENT Constructor %term;>
  89 <!ATTLIST Constructor
  90           name CDATA #REQUIRED>
  91
  92 <!-- CIC terms: -->
  93
  94 <!ELEMENT LAMBDA (source,target)>
  95 <!ATTLIST LAMBDA
  96           id   ID     #REQUIRED
  97           sort %sort; #REQUIRED>
  98
  99 <!ELEMENT LETIN (term,letintarget)>
 100 <!ATTLIST LETIN
 101           id   ID     #REQUIRED
 102           sort %sort; #REQUIRED>
 103
 104 <!ELEMENT PROD (source,target)>
 105 <!ATTLIST PROD
 106           id   ID     #REQUIRED
 107           type %sort; #REQUIRED>
 108
 109 <!ELEMENT CAST (term,type)>
 110 <!ATTLIST CAST
 111           id   ID     #REQUIRED
 112           sort %sort; #REQUIRED>
 113
 114 <!ELEMENT REL EMPTY>
 115 <!ATTLIST REL
 116           value  NMTOKEN #REQUIRED
 117           binder CDATA   #REQUIRED
 118           id     ID      #REQUIRED
 119           sort   %sort;  #REQUIRED>
 120
 121 <!ELEMENT SORT EMPTY>
 122 <!ATTLIST SORT
 123           value CDATA #REQUIRED
 124           id    ID    #REQUIRED>
 125
 126 <!ELEMENT APPLY (%term;)+>
 127 <!ATTLIST APPLY
 128           id   ID     #REQUIRED
 129           sort %sort; #REQUIRED>
 130
 131 <!ELEMENT VAR EMPTY>
 132 <!ATTLIST VAR
 133           relUri CDATA  #REQUIRED
 134           id     ID     #REQUIRED
 135           sort   %sort; #REQUIRED>
 136
 137 <!ELEMENT META EMPTY>
 138 <!ATTLIST META
 139           no   NMTOKEN #REQUIRED
 140           id   ID      #REQUIRED
 141           sort %sort;  #REQUIRED>
 142
 143 <!ELEMENT IMPLICIT EMPTY>
 144 <!ATTLIST IMPLICIT
 145           id ID #REQUIRED>
 146
 147 <!ELEMENT CONST EMPTY>
 148 <!ATTLIST CONST
 149           uri  CDATA  #REQUIRED
 150           id   ID     #REQUIRED
 151           sort %sort; #REQUIRED>
 152
 153 <!ELEMENT MUTIND EMPTY>
 154 <!ATTLIST MUTIND
 155           uri    CDATA   #REQUIRED
 156           noType NMTOKEN #REQUIRED
 157           id     ID      #REQUIRED>
 158
 159 <!ELEMENT MUTCONSTRUCT EMPTY>
 160 <!ATTLIST MUTCONSTRUCT
 161           uri      CDATA   #REQUIRED
 162           noType   NMTOKEN #REQUIRED
 163           noConstr NMTOKEN #REQUIRED
 164           id       ID      #REQUIRED
 165           sort     %sort;  #REQUIRED>
 166
 167 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
 168 <!ATTLIST MUTCASE
 169           uriType CDATA   #REQUIRED
 170           noType  NMTOKEN #REQUIRED
 171           id      ID      #REQUIRED
 172           sort    %sort;  #REQUIRED>
 173
 174 <!ELEMENT FIX (FixFunction+)>
 175 <!ATTLIST FIX
 176           noFun NMTOKEN #REQUIRED
 177           id    ID      #REQUIRED
 178           sort  %sort;  #REQUIRED>
 179
 180 <!ELEMENT COFIX (CofixFunction+)>
 181 <!ATTLIST COFIX
 182           noFun NMTOKEN #REQUIRED
 183           id    ID      #REQUIRED
 184           sort  %sort;  #REQUIRED>
 185
 186 <!-- Elements used in CIC terms: -->
 187
 188 <!ELEMENT FixFunction (type,body)>
 189 <!ATTLIST FixFunction
 190           name     CDATA   #REQUIRED
 191           recIndex NMTOKEN #REQUIRED>
 192
 193 <!ELEMENT CofixFunction (type,body)>
 194 <!ATTLIST CofixFunction
 195           name     CDATA   #REQUIRED>
 196
 197 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
 198
 199 <!ELEMENT source %term;>
 200
 201 <!ELEMENT target %term;>
 202 <!ATTLIST target
 203           binder CDATA #IMPLIED>
 204
 205 <!ELEMENT letintarget %term;>
 206 <!ATTLIST letintarget
 207           binder CDATA #REQUIRED>
 208
 209 <!ELEMENT term %term;>
 210
 211 <!ELEMENT type  %term;>
 212
 213 <!ELEMENT arity %term;>
 214
 215 <!ELEMENT patternsType  %term;>
 216
 217 <!ELEMENT inductiveTerm  %term;>
 218
 219 <!ELEMENT pattern  %term;>
 220
 221 <!ELEMENT body  %term;>