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