]> matita.cs.unibo.it Git - helm.git/blob - helm/nuprl_stylesheets/nuprl_term.xsl
paths trough terms implemented with a nice hack :)
[helm.git] / helm / nuprl_stylesheets / nuprl_term.xsl
1 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
2                               xmlns:m="http://www.w3.org/1998/Math/MathML">
3
4 <xsl:include href="nuprl_proof.xsl"/>
5 <xsl:include href="nuprl_abstract.xsl"/>
6 <xsl:include href="nuprl_rules.xsl"/>
7
8 <!-- NuPrl Term -->
9 <xsl:template match="var">
10   <m:ci>
11     <xsl:value-of select="@val"/>
12   </m:ci>
13 </xsl:template>
14
15
16 <xsl:template match="function">
17   <xsl:choose>
18   <xsl:when test="type_of">
19     <xsl:choose>
20     <xsl:when test="type_of/@var=&quot;&quot;">
21     <m:apply>
22       <m:csymbol>arrow</m:csymbol>
23       <xsl:apply-templates select="type_of/*"/>
24       <xsl:apply-templates select="*[2]"/>
25     </m:apply>
26   </xsl:when>
27   <xsl:otherwise>
28     <m:apply>
29       <m:csymbol>prod</m:csymbol>
30       <m:bvar>
31         <m:ci>
32           <xsl:value-of select="type_of/@var"/>
33         </m:ci>
34         <m:type>
35           <xsl:apply-templates select="type_of/*"/>
36         </m:type>
37       </m:bvar>
38       <xsl:apply-templates select="*[2]"/>
39     </m:apply>
40   </xsl:otherwise>
41   </xsl:choose>
42   </xsl:when>
43   <xsl:otherwise>
44     <m:apply>
45       <m:csymbol>arrow</m:csymbol>
46       <xsl:apply-templates select="*[1]"/>
47       <xsl:apply-templates select="*[2]"/>
48     </m:apply>
49   </xsl:otherwise>
50   </xsl:choose>
51 </xsl:template>
52
53
54 <xsl:template match="lambda">
55   <m:lambda>
56     <m:bvar>
57       <m:ci>
58         <xsl:value-of select="@binder"/>
59       </m:ci>
60     </m:bvar>
61     <xsl:apply-templates/>
62   </m:lambda>
63 </xsl:template>
64
65
66 <xsl:template match="apply">
67   <m:apply>
68     <m:csymbol>app</m:csymbol>
69     <xsl:apply-templates select="*[1]"/>
70     <xsl:apply-templates select="*[2]"/>
71   </m:apply>
72 </xsl:template>
73
74
75 <xsl:template match="product">
76   <m:apply>
77     <xsl:choose>
78       <xsl:when test="type_of">
79         <xsl:choose>
80         <xsl:when test="type_of/@var=&quot;&quot;">
81           <m:csymbol>product_ind</m:csymbol>
82           <m:type>
83             <xsl:apply-templates select="type_of/*"/>
84           </m:type>
85         </xsl:when>
86         <xsl:otherwise>
87           <m:csymbol>product</m:csymbol>
88           <m:bvar>
89             <m:ci>
90               <xsl:value-of select="type_of/@var"/>
91             </m:ci>
92           <m:type>
93             <xsl:apply-templates select="type_of/*"/>
94           </m:type>
95           </m:bvar>
96         </xsl:otherwise>
97         </xsl:choose>
98       </xsl:when>
99       <xsl:otherwise>
100         <m:csymbol>product_ind</m:csymbol>
101         <m:type>
102           <xsl:apply-templates select="*[1]"/>
103         </m:type>
104       </xsl:otherwise>
105     </xsl:choose>
106     <xsl:apply-templates select="*[2]"/>
107   </m:apply>
108 </xsl:template>
109
110
111 <xsl:template match="pair">
112   <m:apply>
113     <m:csymbol>pair</m:csymbol>
114     <xsl:apply-templates select="*[1]"/>
115     <xsl:apply-templates select="*[2]"/>
116   </m:apply>
117 </xsl:template>
118
119
120 <xsl:template match="spread">
121   <m:apply>
122   <m:csymbol>mutcase</m:csymbol>
123   <m:csymbol>NONE</m:csymbol>
124   <xsl:apply-templates select="*[1]"/>
125   <m:piecewise>
126     <m:piece>
127       <xsl:apply-templates select="*[4]"/>
128       <m:apply>
129         <m:csymbol>pair</m:csymbol>
130         <xsl:apply-templates select="binder[1]"/>
131         <xsl:apply-templates select="binder[2]"/>
132       </m:apply>
133     </m:piece>
134   </m:piecewise>
135   </m:apply>
136 </xsl:template>
137
138
139 <xsl:template match="union">
140   <m:apply>
141     <m:csymbol>union</m:csymbol>
142     <xsl:apply-templates select="*[1]"/>
143     <xsl:apply-templates select="*[2]"/>
144   </m:apply>
145 </xsl:template>
146
147
148 <xsl:template match="inl">
149   <m:apply>
150     <m:csymbol>inl</m:csymbol>
151     <xsl:apply-templates select="*[1]"/>
152   </m:apply>
153 </xsl:template>
154
155
156 <xsl:template match="inr">
157   <m:apply>
158     <m:csymbol>inr</m:csymbol>
159     <xsl:apply-templates select="*[1]"/>
160   </m:apply>
161 </xsl:template>
162
163
164 <xsl:template match="decide">
165   <m:apply>
166     <m:csymbol>mutcase</m:csymbol>
167     <m:csymbol>NONE</m:csymbol>
168     <xsl:apply-templates select="*[1]"/>
169     <m:piecewise>
170     <m:piece>
171       <xsl:apply-templates select="*[3]"/>
172       <m:apply>
173         <m:csymbol>inl</m:csymbol>
174         <xsl:apply-templates select="binder[1]"/>
175       </m:apply>
176     </m:piece>
177     <m:piece>
178       <xsl:apply-templates select="*[5]"/>
179       <m:apply>
180         <m:csymbol>inr</m:csymbol>
181         <xsl:apply-templates select="binder[2]"/>
182       </m:apply>
183     </m:piece>
184     </m:piecewise>
185   </m:apply>
186 </xsl:template>
187
188
189 <xsl:template match="universe">
190   <m:apply>
191     <m:csymbol>universe</m:csymbol>
192     <m:cn>
193       <xsl:value-of select="@level"/>
194     </m:cn>
195   </m:apply>
196 </xsl:template>
197
198
199 <xsl:template match="equal">
200   <m:apply>
201     <m:csymbol>equal</m:csymbol>
202     <xsl:apply-templates select="*[1]"/>
203     <xsl:apply-templates select="*[2]"/>
204     <xsl:apply-templates select="*[3]"/>
205   </m:apply>
206 </xsl:template>
207
208
209 <xsl:template match="axiom">
210   <m:apply>
211     <m:csymbol>Ax</m:csymbol>
212   </m:apply>
213 </xsl:template>
214
215
216 <xsl:template match="void">
217   <m:apply>
218     <m:csymbol>void</m:csymbol>
219   </m:apply>
220 </xsl:template>
221
222
223 <xsl:template match="any">
224   <m:apply>
225     <m:csymbol>mutcase</m:csymbol>
226     <m:csymbol>NONE</m:csymbol>
227     <xsl:apply-templates select="*[1]"/>
228   </m:apply>
229 </xsl:template>
230
231
232 <xsl:template match="atom">
233   <m:apply>
234     <m:csymbol>atom</m:csymbol>  
235   </m:apply>
236 </xsl:template>
237
238
239 <xsl:template match="token">
240   <m:apply>
241     <m:csymbol>token</m:csymbol>
242     <m:ci>
243       <xsl:value-of select="@val"/>
244     </m:ci>
245   </m:apply>
246 </xsl:template>
247
248
249 <xsl:template match="atom_eq">
250   <m:apply>
251     <m:csymbol>if_then_else</m:csymbol>
252     <m:where>atom_eq</m:where>
253     <xsl:apply-templates select="*[1]"/>
254     <xsl:apply-templates select="*[2]"/>
255     <xsl:apply-templates select="*[3]"/>
256     <xsl:apply-templates select="*[4]"/>
257   </m:apply>
258 </xsl:template>
259
260
261 <xsl:template match="int">
262   <m:integers/>
263 </xsl:template>
264
265
266 <xsl:template match="natural_number">
267   <m:cn>
268     <xsl:value-of select="@val"/>
269   </m:cn>
270 </xsl:template>
271
272
273 <xsl:template match="minus">
274   <m:apply>
275     <m:minus/>
276     <xsl:apply-templates select="*[1]"/>
277   </m:apply>
278 </xsl:template>
279
280
281 <xsl:template match="add">
282   <m:apply>
283     <m:plus/>
284     <xsl:apply-templates select="*[1]"/>
285     <xsl:apply-templates select="*[2]"/>
286   </m:apply>
287 </xsl:template>
288
289
290 <xsl:template match="subtract">
291   <m:apply>
292     <m:minus/>
293     <xsl:apply-templates select="*[1]"/>
294     <xsl:apply-templates select="*[2]"/>
295   </m:apply>
296 </xsl:template>
297
298
299 <xsl:template match="multiply">
300   <m:apply>
301     <m:times/>
302     <xsl:apply-templates select="*[1]"/>
303     <xsl:apply-templates select="*[2]"/>
304   </m:apply>
305 </xsl:template>
306
307
308 <xsl:template match="divide">
309   <m:apply>
310     <m:divide/>
311     <xsl:apply-templates select="*[1]"/>
312     <xsl:apply-templates select="*[2]"/>
313   </m:apply>
314 </xsl:template>
315
316
317 <xsl:template match="remainder">
318   <m:apply>
319     <m:rem/>
320     <xsl:apply-templates select="*[1]"/>
321     <xsl:apply-templates select="*[2]"/>
322   </m:apply>
323 </xsl:template>
324
325
326 <xsl:template match="int_eq">
327   <m:apply>
328     <m:csymbol>if_then_else</m:csymbol>
329     <m:where>int_eq</m:where>
330     <xsl:apply-templates select="*[1]"/>
331     <xsl:apply-templates select="*[2]"/>
332     <xsl:apply-templates select="*[3]"/>
333     <xsl:apply-templates select="*[4]"/>
334   </m:apply>
335 </xsl:template>
336
337
338 <xsl:template match="less">
339   <m:apply>
340     <m:csymbol>if_then_else</m:csymbol>
341     <m:where>less</m:where>
342     <xsl:apply-templates select="*[1]"/>
343     <xsl:apply-templates select="*[2]"/>
344     <xsl:apply-templates select="*[3]"/>
345     <xsl:apply-templates select="*[4]"/>
346   </m:apply>
347 </xsl:template>
348
349
350 <xsl:template match="ind">
351   <m:apply>
352     <m:csymbol>by_induction</m:csymbol>
353     <m:ci>ind</m:ci>
354     <m:csymbol>NONE</m:csymbol>
355     <m:apply>   <!-- CASO BASE -->
356       <m:csymbol>inductive_case</m:csymbol>
357       <m:apply>
358         <m:csymbol>case_lhs</m:csymbol>
359         <m:ci>0</m:ci>
360       </m:apply>
361       <m:apply>
362         <m:csymbol>induction_hypothesis</m:csymbol>
363       </m:apply>
364       <xsl:apply-templates select="*[5]"/>
365     </m:apply>
366         
367     <m:apply> <!--CASO INDUTTIVO PER I NUMERI POSITIVI-->
368       <m:csymbol>inductive_case</m:csymbol>
369       <m:apply>
370         <m:csymbol>case_lhs</m:csymbol>
371         <m:ci>succ</m:ci>
372         <m:bvar>
373           <xsl:apply-templates select="*[6]"/> <!-- u -->
374           <m:type>int</m:type>
375         </m:bvar>
376       </m:apply>
377       <m:apply>
378         <m:csymbol>induction_hypothesis</m:csymbol>
379         <xsl:apply-templates select="*[7]"/> <!-- v  -->
380       </m:apply>
381       <xsl:apply-templates select="*[8]"/> <!-- t -->
382     </m:apply>
383
384     <m:apply> <!--CASO INDUTTIVO PER I NUMERI NEGATIVI-->
385       <m:csymbol>inductive_case</m:csymbol>
386       <m:apply>
387         <m:csymbol>case_lhs</m:csymbol>
388         <m:ci>pred</m:ci>
389         <m:bvar>
390           <xsl:apply-templates select="*[2]"/> <!-- x -->
391           <m:type>int</m:type>
392         </m:bvar>
393       </m:apply>
394       <m:apply>
395         <m:csymbol>induction_hypothesis</m:csymbol>
396         <xsl:apply-templates select="*[3]"/> <!-- y -->
397       </m:apply>
398       <xsl:apply-templates select="*[4]"/>
399     </m:apply>
400     <m:apply> 
401       <m:csymbol>extra_args</m:csymbol>
402       <xsl:apply-templates select="*[1]"/>  <!-- a -->
403     </m:apply> 
404   </m:apply>
405 </xsl:template>
406
407
408 <xsl:template match="less_than">
409   <m:apply>
410     <m:lt/>
411     <xsl:apply-templates select="*[1]"/>
412     <xsl:apply-templates select="*[2]"/>
413   </m:apply>
414 </xsl:template>
415
416
417 <xsl:template match="list">
418   <m:ci>list</m:ci>
419 </xsl:template>
420
421
422 <xsl:template match="nil">
423   <m:apply>
424     <m:csymbol>nil</m:csymbol> 
425   </m:apply>
426 </xsl:template>
427
428
429 <xsl:template match="cons">
430   <m:apply>
431     <m:csymbol>cons</m:csymbol>
432     <xsl:apply-templates select="*[1]"/>
433     <xsl:apply-templates select="*[2]"/>
434   </m:apply>
435 </xsl:template>
436
437
438 <xsl:template match="list_ind">
439   <m:apply>
440     <m:csymbol>by_induction</m:csymbol>
441     <m:ci>list_ind</m:ci>
442     <m:csymbol>NONE</m:csymbol>
443     <m:apply>
444       <m:csymbol>inductive_case</m:csymbol>
445       <m:apply>
446         <m:csymbol>case_lhs</m:csymbol>
447         <m:ci>nil</m:ci>
448       </m:apply>
449       <m:apply>
450         <m:csymbol>induction_hypothesis</m:csymbol>
451       </m:apply>
452       <xsl:apply-templates select="*[2]"/> <!-- base -->
453     </m:apply>
454     <m:apply>
455       <m:csymbol>inductive_case</m:csymbol>
456       <m:apply>
457         <m:csymbol>case_lhs</m:csymbol>
458         <m:ci>cons</m:ci>
459         <m:bvar>
460           <xsl:apply-templates select="*[3]"/> <!-- x -->
461           <m:type>?</m:type>
462         </m:bvar>
463         <m:bvar>
464         <xsl:apply-templates select="*[4]"/> <!-- l -->
465           <m:type>?</m:type>
466         </m:bvar>
467       </m:apply>
468       <m:apply>
469         <m:csymbol>induction_hypothesis</m:csymbol>
470         <xsl:apply-templates select="*[5]"/> <!-- Fxl -->
471       </m:apply>
472       <xsl:apply-templates select="*[6]"/> <!-- t -->
473     </m:apply>
474     <m:apply>
475       <m:csymbol>extra_args</m:csymbol>
476       <xsl:apply-templates select="*[1]"/> <!-- s -->
477     </m:apply>
478   </m:apply>
479 </xsl:template>
480
481
482 <xsl:template match="rec">
483   <m:apply>
484     <m:csymbol>rec</m:csymbol>
485     <xsl:apply-templates select="*[1]"/>
486     <xsl:apply-templates select="*[2]"/>
487   </m:apply>
488 </xsl:template>
489
490
491 <xsl:template match="rec_ind">
492   <m:apply>
493     <m:csymbol>app</m:csymbol>
494     <m:apply>
495       <m:csymbol>fix</m:csymbol>
496       <m:ci>
497         <xsl:apply-templates select="*[2]"/>
498       </m:ci>
499       <m:bvar>
500         <m:ci>
501           <xsl:apply-templates select="*[2]"/>
502         </m:ci>
503         <m:type>?</m:type>
504       </m:bvar>
505       <m:lambda>
506         <m:bvar>
507          <xsl:apply-templates select="*[3]"/>
508         </m:bvar>
509         <xsl:apply-templates select="*[4]"/>
510       </m:lambda>
511     </m:apply>
512     <xsl:apply-templates select="*[1]"/>
513   </m:apply>
514 </xsl:template>
515
516
517 <xsl:template match="set">
518   <m:apply>
519     <m:csymbol>t_set</m:csymbol>
520     <m:bvar>
521       <xsl:choose>
522       <xsl:when test="type_of">
523         <m:ci>
524           <xsl:value-of select="type_of/@var"/>
525         </m:ci>
526         <m:type>
527           <xsl:apply-templates select="type_of/*"/>
528         </m:type>
529       </xsl:when>
530       <xsl:otherwise>
531         <m:type>
532           <xsl:apply-templates select="*[1]"/>
533         </m:type>
534       </xsl:otherwise>
535       </xsl:choose>
536     </m:bvar>
537     <xsl:apply-templates select="*[2]"/>
538   </m:apply>
539 </xsl:template>
540
541
542 <xsl:template match="isect">
543   <m:apply>
544     <m:csymbol>isect</m:csymbol>
545     <m:bvar>
546       <m:ci>
547         <xsl:value-of select="type_of/@var"/>
548       </m:ci>   
549       <m:type>
550         <xsl:apply-templates select="type_of/*"/>
551       </m:type>
552     </m:bvar>
553     <xsl:apply-templates select="*[1]"/>
554   </m:apply>
555 </xsl:template>
556
557
558 <xsl:template match="quotient">
559   <m:apply>
560     <m:csymbol>quotient</m:csymbol>
561     <xsl:apply-templates select="*[1]"/>
562     <m:bvar>
563       <xsl:value-of select="binder[1]/@var"/>
564     </m:bvar>
565     <m:bvar>
566       <xsl:value-of select="binder[2]/@var"/>
567     </m:bvar>
568     <xsl:apply-templates select="*[4]"/>
569   </m:apply>
570 </xsl:template>
571
572
573 <xsl:template match="type_of">
574   <m:apply>
575     <m:csymbol>type_of</m:csymbol>
576     <m:ci>
577       <xsl:value-of select="@var"/>
578     </m:ci>
579     <xsl:apply-templates select="*[1]"/>
580   </m:apply>
581 </xsl:template>
582
583 <xsl:template match="prop">
584   <m:apply>
585     <m:csymbol>prop</m:csymbol>
586     <m:cn>
587       <xsl:value-of select="@level"/>
588     </m:cn>
589   </m:apply>
590 </xsl:template>
591
592 <xsl:template match="binder">
593   <m:ci>
594     <xsl:value-of select="@var"/>
595   </m:ci>
596 </xsl:template>
597
598 </xsl:stylesheet>