helm/dtd/cic.dtd

   1 <?xml encoding="ISO-8859-1"?>
   2
   3 <!-- DTD FOR CIC OBJECTS: -->
   4
   5 <!-- CIC term declaration -->
   6
   7 <!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST|
   8                   LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'>
   9
  10 <!-- CIC sorts -->
  11
  12 <!ENTITY % sort '(Prop|Set|Type|CProp)'>
  13
  14 <!-- CIC sequents -->
  15
  16 <!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'>
  17
  18 <!-- CIC objects: -->
  19
  20 <!-- CSC: so far params is equal to the one of the only body.  -->
  21 <!ELEMENT ConstantType (attributes?,%term;)>
  22 <!ATTLIST ConstantType
  23           name       CDATA      #REQUIRED
  24           params     CDATA      #REQUIRED
  25           id         ID         #REQUIRED>
  26
  27 <!ELEMENT ConstantBody (attributes?,%term;)>
  28 <!ATTLIST ConstantBody
  29           for        CDATA      #REQUIRED
  30           params     CDATA      #REQUIRED
  31           id         ID         #REQUIRED>
  32
  33 <!ELEMENT CurrentProof (attributes?,Conjecture*,body)>
  34 <!ATTLIST CurrentProof
  35           of         CDATA      #REQUIRED
  36           id         ID         #REQUIRED>
  37
  38 <!ELEMENT InductiveDefinition (attributes?,InductiveType+)>
  39 <!ATTLIST InductiveDefinition
  40           noParams NMTOKEN #REQUIRED
  41           params   CDATA   #REQUIRED
  42           id       ID      #REQUIRED>
  43
  44 <!ELEMENT Variable (attributes?,body?,type)>
  45 <!ATTLIST Variable
  46           name   CDATA #REQUIRED
  47           params CDATA #REQUIRED
  48           id     ID    #REQUIRED>
  49
  50 <!ELEMENT Sequent %sequent;>
  51 <!ATTLIST Sequent
  52           no  NMTOKEN #REQUIRED
  53           id  ID      #REQUIRED>
  54
  55 <!ELEMENT attributes ((class,generated?)|(generated,class?))?>
  56
  57 <!ELEMENT generated EMPTY>
  58
  59 <!-- the fields are allowed only when @value = "record"
  60      the SORT is allowed only when @value = "elim" -->
  61 <!ELEMENT class (field*|SORT)>
  62 <!ATTLIST class
  63           value (coercion|elim|record|projection) #REQUIRED>
  64
  65 <!-- Elements used in CIC objects, which are not terms: -->
  66
  67 <!ELEMENT InductiveType (arity,Constructor*)>
  68 <!ATTLIST InductiveType
  69           name      CDATA        #REQUIRED
  70           inductive (true|false) #REQUIRED
  71           id        ID           #REQUIRED>
  72
  73 <!ELEMENT Conjecture %sequent;>
  74 <!ATTLIST Conjecture
  75           no NMTOKEN #REQUIRED
  76           id ID      #REQUIRED>
  77
  78 <!ELEMENT Constructor %term;>
  79 <!ATTLIST Constructor
  80           name CDATA #REQUIRED>
  81
  82 <!ELEMENT Decl %term;>
  83 <!ATTLIST Decl
  84           name CDATA #IMPLIED
  85           id   ID    #REQUIRED>
  86
  87 <!ELEMENT Def %term;>
  88 <!ATTLIST Def
  89           name CDATA #IMPLIED
  90           id   ID    #REQUIRED>
  91
  92 <!ELEMENT Hidden EMPTY>
  93 <!ATTLIST Hidden
  94           id ID #REQUIRED>
  95
  96 <!ELEMENT Goal %term;>
  97
  98 <!-- CIC terms: -->
  99
 100 <!ELEMENT LAMBDA (decl*,target)>
 101 <!ATTLIST LAMBDA
 102           sort %sort; #REQUIRED>
 103
 104 <!ELEMENT LETIN (def*,target)>
 105 <!ATTLIST LETIN
 106           sort %sort; #REQUIRED>
 107
 108 <!ELEMENT PROD (decl*,target)>
 109 <!ATTLIST PROD
 110           type %sort; #REQUIRED>
 111
 112 <!ELEMENT CAST (term,type)>
 113 <!ATTLIST CAST
 114           id   ID     #REQUIRED
 115           sort %sort; #REQUIRED>
 116
 117 <!ELEMENT REL EMPTY>
 118 <!ATTLIST REL
 119           value  NMTOKEN #REQUIRED
 120           binder CDATA   #REQUIRED
 121           id     ID      #REQUIRED
 122           idref  IDREF   #REQUIRED
 123           sort   %sort;  #REQUIRED>
 124
 125 <!ELEMENT SORT EMPTY>
 126 <!ATTLIST SORT
 127           value CDATA #REQUIRED
 128           id    ID    #REQUIRED>
 129
 130 <!ELEMENT APPLY (%term;)+>
 131 <!ATTLIST APPLY
 132           id   ID     #REQUIRED
 133           sort %sort; #REQUIRED>
 134
 135 <!ELEMENT VAR EMPTY>
 136 <!ATTLIST VAR
 137           uri  CDATA  #REQUIRED
 138           id   ID     #REQUIRED
 139           sort %sort; #REQUIRED>
 140
 141 <!-- The substitutions are ordered by increasing DeBrujin  -->
 142 <!-- index. An empty substitution means that that index is -->
 143 <!-- not accessible.                                       -->
 144 <!ELEMENT META (substitution*)>
 145 <!ATTLIST META
 146           no              NMTOKEN #REQUIRED
 147           id              ID      #REQUIRED
 148           sort            %sort;  #REQUIRED>
 149
 150 <!ELEMENT IMPLICIT EMPTY>
 151 <!ATTLIST IMPLICIT
 152           id ID #REQUIRED
 153           annotation (closed|type|hole) #IMPLIED>
 154
 155 <!ELEMENT CONST EMPTY>
 156 <!ATTLIST CONST
 157           uri  CDATA  #REQUIRED
 158           id   ID     #REQUIRED
 159           sort %sort; #REQUIRED>
 160
 161 <!ELEMENT MUTIND EMPTY>
 162 <!ATTLIST MUTIND
 163           uri    CDATA   #REQUIRED
 164           noType NMTOKEN #REQUIRED
 165           id     ID      #REQUIRED>
 166
 167 <!ELEMENT MUTCONSTRUCT EMPTY>
 168 <!ATTLIST MUTCONSTRUCT
 169           uri      CDATA   #REQUIRED
 170           noType   NMTOKEN #REQUIRED
 171           noConstr NMTOKEN #REQUIRED
 172           id       ID      #REQUIRED
 173           sort     %sort;  #REQUIRED>
 174
 175 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
 176 <!ATTLIST MUTCASE
 177           uriType CDATA   #REQUIRED
 178           noType  NMTOKEN #REQUIRED
 179           id      ID      #REQUIRED
 180           sort    %sort;  #REQUIRED>
 181
 182 <!ELEMENT FIX (FixFunction+)>
 183 <!ATTLIST FIX
 184           noFun NMTOKEN #REQUIRED
 185           id    ID      #REQUIRED
 186           sort  %sort;  #REQUIRED>
 187
 188 <!ELEMENT COFIX (CofixFunction+)>
 189 <!ATTLIST COFIX
 190           noFun NMTOKEN #REQUIRED
 191           id    ID      #REQUIRED
 192           sort  %sort;  #REQUIRED>
 193
 194 <!-- Elements used in CIC terms: -->
 195
 196 <!ELEMENT FixFunction (type,body)>
 197 <!ATTLIST FixFunction
 198           name     CDATA   #REQUIRED
 199           id       ID      #REQUIRED
 200           recIndex NMTOKEN #REQUIRED>
 201
 202 <!ELEMENT CofixFunction (type,body)>
 203 <!ATTLIST CofixFunction
 204           id       ID      #REQUIRED
 205           name     CDATA   #REQUIRED>
 206
 207 <!ELEMENT substitution ((%term;)?)>
 208
 209 <!-- Explicit named substitutions: -->
 210
 211 <!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT|VAR),arg+)>
 212 <!ATTLIST instantiate
 213           id ID #IMPLIED>
 214
 215 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
 216
 217 <!ELEMENT arg %term;>
 218 <!ATTLIST arg
 219           relUri CDATA #REQUIRED>
 220
 221 <!ELEMENT decl %term;>
 222 <!ATTLIST decl
 223           id     ID     #REQUIRED
 224           type   %sort; #REQUIRED
 225           binder CDATA  #IMPLIED>
 226
 227 <!ELEMENT def %term;>
 228 <!ATTLIST def
 229           id     ID     #REQUIRED
 230           sort   %sort; #REQUIRED
 231           binder CDATA  #IMPLIED>
 232
 233 <!ELEMENT target %term;>
 234
 235 <!ELEMENT term %term;>
 236
 237 <!ELEMENT type  %term;>
 238
 239 <!ELEMENT arity %term;>
 240
 241 <!ELEMENT patternsType  %term;>
 242
 243 <!ELEMENT inductiveTerm  %term;>
 244
 245 <!ELEMENT pattern  %term;>
 246
 247 <!ELEMENT body  %term;>