helm/dtd/cic.dtd

   1 <?xml encoding="ISO-8859-1"?>
   2
   3 <!--*****************************************************************-->
   4 <!-- DTD FOR CIC OBJECTS:                                            -->
   5 <!--  First draft: September 1999, Claudio Sacerdoti Coen            -->
   6 <!--  Revised: February 3 2000, Claudio Sacerdoti Coen, Irene Schena -->
   7 <!--  Last Revision: April 4 2000, Claudio Sacerdoti Coen            -->
   8 <!--  Last Revision: June 19 2000, Claudio Sacerdoti Coen            -->
   9 <!--  Last Revision: June 20 2000, Claudio Sacerdoti Coen            -->
  10 <!--*****************************************************************-->
  11
  12 <!-- CIC term declaration -->
  13
  14 <!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST|
  15                   LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX)'>
  16
  17 <!-- CIC sorts -->
  18
  19 <!ENTITY % sort '(Prop|Set|Type)'>
  20
  21
  22 <!-- CIC objects: -->
  23
  24 <!ELEMENT Definition (body, type)>
  25 <!ATTLIST Definition
  26           name       CDATA      #REQUIRED
  27           params     CDATA      #REQUIRED
  28           paramMode  (POSSIBLE) #IMPLIED
  29           id         ID         #REQUIRED>
  30
  31 <!ELEMENT Axiom (type)>
  32 <!ATTLIST Axiom
  33           name   CDATA #REQUIRED
  34           params CDATA #REQUIRED
  35           id     ID    #REQUIRED>
  36
  37 <!ELEMENT CurrentProof (Conjecture*,body,type)>
  38 <!ATTLIST CurrentProof
  39           name CDATA #REQUIRED
  40           id   ID    #REQUIRED>
  41
  42 <!ELEMENT InductiveDefinition (InductiveType+)>
  43 <!ATTLIST InductiveDefinition
  44           noParams NMTOKEN #REQUIRED
  45           params   CDATA   #REQUIRED
  46           id       ID      #REQUIRED>
  47
  48 <!ELEMENT Variable (body?,type)>
  49 <!ATTLIST Variable
  50           name CDATA #REQUIRED
  51           id   ID    #REQUIRED>
  52
  53 <!-- Elements used in CIC objects, which are not terms: -->
  54
  55 <!ELEMENT InductiveType (arity,Constructor*)>
  56 <!ATTLIST InductiveType
  57           name      CDATA        #REQUIRED
  58           inductive (true|false) #REQUIRED>
  59
  60 <!ELEMENT Conjecture %term;>
  61 <!ATTLIST Conjecture
  62           no NMTOKEN #REQUIRED>
  63
  64 <!ELEMENT Constructor %term;>
  65 <!ATTLIST Constructor
  66           name CDATA #REQUIRED>
  67
  68 <!-- CIC terms: -->
  69
  70 <!ELEMENT LAMBDA (source,target)>
  71 <!ATTLIST LAMBDA
  72           id   ID     #REQUIRED
  73           sort %sort; #REQUIRED>
  74
  75 <!ELEMENT LETIN (term,letintarget)>
  76 <!ATTLIST LETIN
  77           id   ID     #REQUIRED
  78           sort %sort; #REQUIRED>
  79
  80 <!ELEMENT PROD (source,target)>
  81 <!ATTLIST PROD
  82           id ID #REQUIRED>
  83
  84 <!ELEMENT CAST (term,type)>
  85 <!ATTLIST CAST
  86           id   ID     #REQUIRED
  87           sort %sort; #REQUIRED>
  88
  89 <!ELEMENT REL EMPTY>
  90 <!ATTLIST REL
  91           value  NMTOKEN #REQUIRED
  92           binder CDATA   #REQUIRED
  93           id     ID      #REQUIRED
  94           sort   %sort;  #REQUIRED>
  95
  96 <!ELEMENT SORT EMPTY>
  97 <!ATTLIST SORT
  98           value CDATA #REQUIRED
  99           id    ID    #REQUIRED>
 100
 101 <!ELEMENT APPLY (%term;)+>
 102 <!ATTLIST APPLY
 103           id   ID     #REQUIRED
 104           sort %sort; #REQUIRED>
 105
 106 <!ELEMENT VAR EMPTY>
 107 <!ATTLIST VAR
 108           relUri CDATA  #REQUIRED
 109           id     ID     #REQUIRED
 110           sort   %sort; #REQUIRED>
 111
 112 <!ELEMENT META EMPTY>
 113 <!ATTLIST META
 114           no   NMTOKEN #REQUIRED
 115           id   ID      #REQUIRED
 116           sort %sort;  #REQUIRED>
 117
 118 <!ELEMENT IMPLICIT EMPTY>
 119 <!ATTLIST IMPLICIT
 120           id ID #REQUIRED>
 121
 122 <!ELEMENT CONST EMPTY>
 123 <!ATTLIST CONST
 124           uri  CDATA  #REQUIRED
 125           id   ID     #REQUIRED
 126           sort %sort; #REQUIRED>
 127
 128 <!ELEMENT MUTIND EMPTY>
 129 <!ATTLIST MUTIND
 130           uri    CDATA   #REQUIRED
 131           noType NMTOKEN #REQUIRED
 132           id     ID      #REQUIRED>
 133
 134 <!ELEMENT MUTCONSTRUCT EMPTY>
 135 <!ATTLIST MUTCONSTRUCT
 136           uri      CDATA   #REQUIRED
 137           noType   NMTOKEN #REQUIRED
 138           noConstr NMTOKEN #REQUIRED
 139           id       ID      #REQUIRED
 140           sort     %sort;  #REQUIRED>
 141
 142 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
 143 <!ATTLIST MUTCASE
 144           uriType CDATA   #REQUIRED
 145           noType  NMTOKEN #REQUIRED
 146           id      ID      #REQUIRED
 147           sort    %sort;  #REQUIRED>
 148
 149 <!ELEMENT FIX (FixFunction+)>
 150 <!ATTLIST FIX
 151           noFun NMTOKEN #REQUIRED
 152           id    ID      #REQUIRED
 153           sort  %sort;  #REQUIRED>
 154
 155 <!ELEMENT COFIX (CofixFunction+)>
 156 <!ATTLIST COFIX
 157           noFun NMTOKEN #REQUIRED
 158           id    ID      #REQUIRED
 159           sort  %sort;  #REQUIRED>
 160
 161 <!-- Elements used in CIC terms: -->
 162
 163 <!ELEMENT FixFunction (type,body)>
 164 <!ATTLIST FixFunction
 165           name     CDATA   #REQUIRED
 166           recIndex NMTOKEN #REQUIRED>
 167
 168 <!ELEMENT CofixFunction (type,body)>
 169 <!ATTLIST CofixFunction
 170           name     CDATA   #REQUIRED>
 171
 172 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
 173
 174 <!ELEMENT source %term;>
 175
 176 <!ELEMENT target %term;>
 177 <!ATTLIST target
 178           binder CDATA #IMPLIED>
 179
 180 <!ELEMENT letintarget %term;>
 181 <!ATTLIST letintarget
 182           binder CDATA #REQUIRED>
 183
 184 <!ELEMENT term %term;>
 185
 186 <!ELEMENT type  %term;>
 187
 188 <!ELEMENT arity %term;>
 189
 190 <!ELEMENT patternsType  %term;>
 191
 192 <!ELEMENT inductiveTerm  %term;>
 193
 194 <!ELEMENT pattern  %term;>
 195
 196 <!ELEMENT body  %term;>