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           type %sort; #REQUIRED>
  84
  85 <!ELEMENT CAST (term,type)>
  86 <!ATTLIST CAST
  87           id   ID     #REQUIRED
  88           sort %sort; #REQUIRED>
  89
  90 <!ELEMENT REL EMPTY>
  91 <!ATTLIST REL
  92           value  NMTOKEN #REQUIRED
  93           binder CDATA   #REQUIRED
  94           id     ID      #REQUIRED
  95           sort   %sort;  #REQUIRED>
  96
  97 <!ELEMENT SORT EMPTY>
  98 <!ATTLIST SORT
  99           value CDATA #REQUIRED
 100           id    ID    #REQUIRED>
 101
 102 <!ELEMENT APPLY (%term;)+>
 103 <!ATTLIST APPLY
 104           id   ID     #REQUIRED
 105           sort %sort; #REQUIRED>
 106
 107 <!ELEMENT VAR EMPTY>
 108 <!ATTLIST VAR
 109           relUri CDATA  #REQUIRED
 110           id     ID     #REQUIRED
 111           sort   %sort; #REQUIRED>
 112
 113 <!ELEMENT META EMPTY>
 114 <!ATTLIST META
 115           no   NMTOKEN #REQUIRED
 116           id   ID      #REQUIRED
 117           sort %sort;  #REQUIRED>
 118
 119 <!ELEMENT IMPLICIT EMPTY>
 120 <!ATTLIST IMPLICIT
 121           id ID #REQUIRED>
 122
 123 <!ELEMENT CONST EMPTY>
 124 <!ATTLIST CONST
 125           uri  CDATA  #REQUIRED
 126           id   ID     #REQUIRED
 127           sort %sort; #REQUIRED>
 128
 129 <!ELEMENT MUTIND EMPTY>
 130 <!ATTLIST MUTIND
 131           uri    CDATA   #REQUIRED
 132           noType NMTOKEN #REQUIRED
 133           id     ID      #REQUIRED>
 134
 135 <!ELEMENT MUTCONSTRUCT EMPTY>
 136 <!ATTLIST MUTCONSTRUCT
 137           uri      CDATA   #REQUIRED
 138           noType   NMTOKEN #REQUIRED
 139           noConstr NMTOKEN #REQUIRED
 140           id       ID      #REQUIRED
 141           sort     %sort;  #REQUIRED>
 142
 143 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
 144 <!ATTLIST MUTCASE
 145           uriType CDATA   #REQUIRED
 146           noType  NMTOKEN #REQUIRED
 147           id      ID      #REQUIRED
 148           sort    %sort;  #REQUIRED>
 149
 150 <!ELEMENT FIX (FixFunction+)>
 151 <!ATTLIST FIX
 152           noFun NMTOKEN #REQUIRED
 153           id    ID      #REQUIRED
 154           sort  %sort;  #REQUIRED>
 155
 156 <!ELEMENT COFIX (CofixFunction+)>
 157 <!ATTLIST COFIX
 158           noFun NMTOKEN #REQUIRED
 159           id    ID      #REQUIRED
 160           sort  %sort;  #REQUIRED>
 161
 162 <!-- Elements used in CIC terms: -->
 163
 164 <!ELEMENT FixFunction (type,body)>
 165 <!ATTLIST FixFunction
 166           name     CDATA   #REQUIRED
 167           recIndex NMTOKEN #REQUIRED>
 168
 169 <!ELEMENT CofixFunction (type,body)>
 170 <!ATTLIST CofixFunction
 171           name     CDATA   #REQUIRED>
 172
 173 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
 174
 175 <!ELEMENT source %term;>
 176
 177 <!ELEMENT target %term;>
 178 <!ATTLIST target
 179           binder CDATA #IMPLIED>
 180
 181 <!ELEMENT letintarget %term;>
 182 <!ATTLIST letintarget
 183           binder CDATA #REQUIRED>
 184
 185 <!ELEMENT term %term;>
 186
 187 <!ELEMENT type  %term;>
 188
 189 <!ELEMENT arity %term;>
 190
 191 <!ELEMENT patternsType  %term;>
 192
 193 <!ELEMENT inductiveTerm  %term;>
 194
 195 <!ELEMENT pattern  %term;>
 196
 197 <!ELEMENT body  %term;>