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