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                   ABST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX)'>
  16
  17 <!-- CIC objects: -->
  18
  19 <!ELEMENT Definition (body, type)>
  20 <!ATTLIST Definition
  21           name       CDATA      #REQUIRED
  22           params     CDATA      #REQUIRED
  23           paramMode  (POSSIBLE) #IMPLIED
  24           id         ID         #REQUIRED>
  25
  26 <!ELEMENT Axiom (type)>
  27 <!ATTLIST Axiom
  28           name   CDATA #REQUIRED
  29           params CDATA #REQUIRED
  30           id     ID    #REQUIRED>
  31
  32 <!ELEMENT CurrentProof (Conjecture*,body,type)>
  33 <!ATTLIST CurrentProof
  34           name CDATA #REQUIRED
  35           id   ID    #REQUIRED>
  36
  37 <!ELEMENT InductiveDefinition (InductiveType+)>
  38 <!ATTLIST InductiveDefinition
  39           noParams NMTOKEN #REQUIRED
  40           params   CDATA   #REQUIRED
  41           id       ID      #REQUIRED>
  42
  43 <!ELEMENT Variable (type)>
  44 <!ATTLIST Variable
  45           name CDATA #REQUIRED
  46           id   ID    #REQUIRED>
  47
  48 <!-- Elements used in CIC objects, which are not terms: -->
  49
  50 <!ELEMENT InductiveType (arity,Constructor*)>
  51 <!ATTLIST InductiveType
  52           name      CDATA        #REQUIRED
  53           inductive (true|false) #REQUIRED>
  54
  55 <!ELEMENT Conjecture %term;>
  56 <!ATTLIST Conjecture
  57           no NMTOKEN #REQUIRED>
  58
  59 <!ELEMENT Constructor %term;>
  60 <!ATTLIST Constructor
  61           name CDATA #REQUIRED>
  62
  63 <!-- CIC terms: -->
  64
  65 <!ELEMENT LAMBDA (source,target)>
  66 <!ATTLIST LAMBDA
  67           id ID #REQUIRED>
  68
  69 <!ELEMENT PROD (source,target)>
  70 <!ATTLIST PROD
  71           id ID #REQUIRED>
  72
  73 <!ELEMENT CAST (term,type)>
  74 <!ATTLIST CAST
  75           id ID #REQUIRED>
  76
  77 <!ELEMENT REL EMPTY>
  78 <!ATTLIST REL
  79           value  NMTOKEN #REQUIRED
  80           binder CDATA   #REQUIRED
  81           id     ID      #REQUIRED>
  82
  83 <!ELEMENT SORT EMPTY>
  84 <!ATTLIST SORT
  85           value CDATA #REQUIRED
  86           id    ID    #REQUIRED>
  87
  88 <!ELEMENT APPLY (%term;)+>
  89 <!ATTLIST APPLY
  90           id ID #REQUIRED>
  91
  92 <!ELEMENT VAR EMPTY>
  93 <!ATTLIST VAR
  94           relUri CDATA #REQUIRED
  95           id     ID    #REQUIRED>
  96
  97 <!ELEMENT META EMPTY>
  98 <!ATTLIST META
  99           no NMTOKEN #REQUIRED
 100           id ID      #REQUIRED>
 101
 102 <!ELEMENT IMPLICIT EMPTY>
 103 <!ATTLIST IMPLICIT
 104           id ID #REQUIRED>
 105
 106 <!ELEMENT CONST EMPTY>
 107 <!ATTLIST CONST
 108           uri CDATA #REQUIRED
 109           id  ID    #REQUIRED>
 110
 111 <!ELEMENT ABST EMPTY>
 112 <!ATTLIST ABST
 113           uri CDATA #REQUIRED
 114           id  ID    #REQUIRED>
 115
 116 <!ELEMENT MUTIND EMPTY>
 117 <!ATTLIST MUTIND
 118           uri    CDATA   #REQUIRED
 119           noType NMTOKEN #REQUIRED
 120           id     ID      #REQUIRED>
 121
 122 <!ELEMENT MUTCONSTRUCT EMPTY>
 123 <!ATTLIST MUTCONSTRUCT
 124           uri      CDATA   #REQUIRED
 125           noType   NMTOKEN #REQUIRED
 126           noConstr NMTOKEN #REQUIRED
 127           id       ID      #REQUIRED>
 128
 129 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
 130 <!ATTLIST MUTCASE
 131           uriType CDATA   #REQUIRED
 132           noType  NMTOKEN #REQUIRED
 133           id      ID      #REQUIRED>
 134
 135 <!ELEMENT FIX (FixFunction+)>
 136 <!ATTLIST FIX
 137           noFun NMTOKEN #REQUIRED
 138           id    ID      #REQUIRED>
 139
 140 <!ELEMENT COFIX (CofixFunction+)>
 141 <!ATTLIST COFIX
 142           noFun NMTOKEN #REQUIRED
 143           id    ID      #REQUIRED>
 144
 145 <!-- Elements used in CIC terms: -->
 146
 147 <!ELEMENT FixFunction (type,body)>
 148 <!ATTLIST FixFunction
 149           name     CDATA   #REQUIRED
 150           recIndex NMTOKEN #REQUIRED>
 151
 152 <!ELEMENT CofixFunction (type,body)>
 153 <!ATTLIST CofixFunction
 154           name     CDATA   #REQUIRED>
 155
 156 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
 157
 158 <!ELEMENT source %term;>
 159
 160 <!ELEMENT target %term;>
 161 <!ATTLIST target
 162           binder CDATA #IMPLIED>
 163
 164 <!ELEMENT term %term;>
 165
 166 <!ELEMENT type  %term;>
 167
 168 <!ELEMENT arity %term;>
 169
 170 <!ELEMENT patternsType  %term;>
 171
 172 <!ELEMENT inductiveTerm  %term;>
 173
 174 <!ELEMENT pattern  %term;>
 175
 176 <!ELEMENT body  %term;>