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