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)'>
  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 %term;>
  22 <!ATTLIST ConstantType
  23           name       CDATA      #REQUIRED
  24           params     CDATA      #REQUIRED
  25           id         ID         #REQUIRED>
  26
  27 <!ELEMENT ConstantBody %term;>
  28 <!ATTLIST ConstantBody
  29           for        CDATA      #REQUIRED
  30           params     CDATA      #REQUIRED
  31           id         ID         #REQUIRED>
  32
  33 <!ELEMENT CurrentProof (Conjecture*,body)>
  34 <!ATTLIST CurrentProof
  35           of         CDATA      #REQUIRED
  36           id         ID         #REQUIRED>
  37
  38 <!ELEMENT InductiveDefinition (InductiveType+)>
  39 <!ATTLIST InductiveDefinition
  40           noParams NMTOKEN #REQUIRED
  41           params   CDATA   #REQUIRED
  42           id       ID      #REQUIRED>
  43
  44 <!ELEMENT Variable (body?,type)>
  45 <!ATTLIST Variable
  46           name CDATA #REQUIRED
  47           id   ID    #REQUIRED>
  48
  49 <!ELEMENT Sequent %sequent;>
  50 <!ATTLIST Sequent
  51           no  NMTOKEN #REQUIRED
  52           id  ID      #REQUIRED>
  53
  54 <!-- Elements used in CIC objects, which are not terms: -->
  55
  56 <!ELEMENT InductiveType (arity,Constructor*)>
  57 <!ATTLIST InductiveType
  58           name      CDATA        #REQUIRED
  59           inductive (true|false) #REQUIRED
  60           id        ID           #REQUIRED>
  61
  62 <!ELEMENT Conjecture %sequent;>
  63 <!ATTLIST Conjecture
  64           no NMTOKEN #REQUIRED
  65           id ID      #REQUIRED>
  66
  67 <!ELEMENT Constructor %term;>
  68 <!ATTLIST Constructor
  69           name CDATA #REQUIRED>
  70
  71 <!ELEMENT Decl %term;>
  72 <!ATTLIST Decl
  73           name CDATA #IMPLIED
  74           id   ID    #REQUIRED>
  75
  76 <!ELEMENT Def %term;>
  77 <!ATTLIST Def
  78           name CDATA #IMPLIED
  79           id   ID    #REQUIRED>
  80
  81 <!ELEMENT Hidden EMPTY>
  82 <!ATTLIST Hidden
  83           id ID #REQUIRED>
  84
  85 <!ELEMENT Goal %term;>
  86
  87 <!-- CIC terms: -->
  88
  89 <!ELEMENT LAMBDA (decl*,target)>
  90 <!ATTLIST LAMBDA
  91           sort %sort; #REQUIRED>
  92
  93 <!ELEMENT LETIN (def*,target)>
  94 <!ATTLIST LETIN
  95           sort %sort; #REQUIRED>
  96
  97 <!ELEMENT PROD (decl*,target)>
  98 <!ATTLIST PROD
  99           type %sort; #REQUIRED>
 100
 101 <!ELEMENT CAST (term,type)>
 102 <!ATTLIST CAST
 103           id   ID     #REQUIRED
 104           sort %sort; #REQUIRED>
 105
 106 <!ELEMENT REL EMPTY>
 107 <!ATTLIST REL
 108           value  NMTOKEN #REQUIRED
 109           binder CDATA   #REQUIRED
 110           id     ID      #REQUIRED
 111           idref  IDREF   #REQUIRED
 112           sort   %sort;  #REQUIRED>
 113
 114 <!ELEMENT SORT EMPTY>
 115 <!ATTLIST SORT
 116           value CDATA #REQUIRED
 117           id    ID    #REQUIRED>
 118
 119 <!ELEMENT APPLY (%term;)+>
 120 <!ATTLIST APPLY
 121           id   ID     #REQUIRED
 122           sort %sort; #REQUIRED>
 123
 124 <!ELEMENT VAR EMPTY>
 125 <!ATTLIST VAR
 126           uri  CDATA  #REQUIRED
 127           id   ID     #REQUIRED
 128           sort %sort; #REQUIRED>
 129
 130 <!-- The substitutions are ordered by increasing DeBrujin  -->
 131 <!-- index. An empty substitution means that that index is -->
 132 <!-- not accessible.                                       -->
 133 <!ELEMENT META (substitution*)>
 134 <!ATTLIST META
 135           no              NMTOKEN #REQUIRED
 136           id              ID      #REQUIRED
 137           sort            %sort;  #REQUIRED>
 138
 139 <!ELEMENT IMPLICIT EMPTY>
 140 <!ATTLIST IMPLICIT
 141           id ID #REQUIRED>
 142
 143 <!ELEMENT CONST EMPTY>
 144 <!ATTLIST CONST
 145           uri  CDATA  #REQUIRED
 146           id   ID     #REQUIRED
 147           sort %sort; #REQUIRED>
 148
 149 <!ELEMENT MUTIND EMPTY>
 150 <!ATTLIST MUTIND
 151           uri    CDATA   #REQUIRED
 152           noType NMTOKEN #REQUIRED
 153           id     ID      #REQUIRED>
 154
 155 <!ELEMENT MUTCONSTRUCT EMPTY>
 156 <!ATTLIST MUTCONSTRUCT
 157           uri      CDATA   #REQUIRED
 158           noType   NMTOKEN #REQUIRED
 159           noConstr NMTOKEN #REQUIRED
 160           id       ID      #REQUIRED
 161           sort     %sort;  #REQUIRED>
 162
 163 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
 164 <!ATTLIST MUTCASE
 165           uriType CDATA   #REQUIRED
 166           noType  NMTOKEN #REQUIRED
 167           id      ID      #REQUIRED
 168           sort    %sort;  #REQUIRED>
 169
 170 <!ELEMENT FIX (FixFunction+)>
 171 <!ATTLIST FIX
 172           noFun NMTOKEN #REQUIRED
 173           id    ID      #REQUIRED
 174           sort  %sort;  #REQUIRED>
 175
 176 <!ELEMENT COFIX (CofixFunction+)>
 177 <!ATTLIST COFIX
 178           noFun NMTOKEN #REQUIRED
 179           id    ID      #REQUIRED
 180           sort  %sort;  #REQUIRED>
 181
 182 <!-- Elements used in CIC terms: -->
 183
 184 <!ELEMENT FixFunction (type,body)>
 185 <!ATTLIST FixFunction
 186           name     CDATA   #REQUIRED
 187           id       ID      #REQUIRED
 188           recIndex NMTOKEN #REQUIRED>
 189
 190 <!ELEMENT CofixFunction (type,body)>
 191 <!ATTLIST CofixFunction
 192           id       ID      #REQUIRED
 193           name     CDATA   #REQUIRED>
 194
 195 <!ELEMENT substitution ((%term;)?)>
 196
 197 <!-- Explicit named substitutions: -->
 198
 199 <!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT),arg+)>
 200 <!ATTLIST instantiate
 201           id ID #IMPLIED>
 202
 203 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
 204
 205 <!ELEMENT arg %term;>
 206 <!ATTLIST arg
 207           relUri CDATA #REQUIRED>
 208
 209 <!ELEMENT decl %term;>
 210 <!ATTLIST decl
 211           id     ID     #REQUIRED
 212           type   %sort; #REQUIRED
 213           binder CDATA  #IMPLIED>
 214
 215 <!ELEMENT def %term;>
 216 <!ATTLIST def
 217           id     ID     #REQUIRED
 218           sort   %sort; #REQUIRED
 219           binder CDATA  #IMPLIED>
 220
 221 <!ELEMENT target %term;>
 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;>