]> matita.cs.unibo.it Git - helm.git/blob - helm/style/proofs.xsl
Bug fixed
[helm.git] / helm / style / proofs.xsl
1 <?xml version="1.0"?>
2
3 <!--******************************************************************--> 
4 <!-- Basic Logic                                                      -->
5 <!-- First draft: April 3 2000                                        -->
6 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
7 <!--******************************************************************-->
8
9 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
10                               xmlns:m="http://www.w3.org/1998/Math/MathML"
11                               xmlns:helm="http://www.cs.unibo.it/helm">
12
13 <!--******************************************************************-->
14 <!-- Variable containing the absolute path of the CIC file            -->
15 <!--******************************************************************-->
16
17 <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
18
19 <!-- ************************* LOGIC *********************************-->
20
21 <!-- Proof objects -->
22
23 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
24
25 <!-- ALL this elements does not have inner type -->
26 <xsl:template match="PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
27 <xsl:apply-templates select="." mode="pure"/>
28 </xsl:template>
29
30 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
31 <xsl:template match="LAMBDA" mode="noannot">
32  <xsl:variable name="id" select="@id"/>
33  <xsl:choose>
34   <xsl:when test="@sort='Prop' and name(../..) != 'LAMBDA'">
35   <!-- <xsl:when test="@sort='Prop' and //InnerTypes/TYPE[@of=$id]"> -->
36    <xsl:call-template name="has_inner_type"/>
37   </xsl:when>
38   <xsl:otherwise>
39    <xsl:apply-templates select="." mode="pure"/>
40   </xsl:otherwise>
41  </xsl:choose>
42 </xsl:template>
43
44 <!-- ALL this elements have inner type -->
45 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
46  <xsl:choose>
47   <!-- <xsl:when test="//InnerTypes and key('typeid',@id)"> -->
48   <!-- <xsl:when test="//InnerTypes/TYPE[@of=$id]"> -->
49   <xsl:when test="@sort='Prop'">
50    <xsl:call-template name="has_inner_type"/>
51   </xsl:when>
52   <xsl:otherwise>
53    <xsl:apply-templates select="." mode="pure"/>
54   </xsl:otherwise>
55  </xsl:choose>
56 </xsl:template>
57
58 <xsl:template name="has_inner_type">
59    <xsl:variable name="id" select="@id"/>
60    <xsl:choose>
61     <xsl:when test="name()= 'APPLY' and CONST[
62  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
63  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
64      <m:apply helm:xref="{@id}">
65       <m:csymbol>thread</m:csymbol>
66       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
67       <m:apply>
68        <m:csymbol>rw_step</m:csymbol>
69        <xsl:apply-templates mode="pure" select="*[3]"/>
70        <xsl:apply-templates mode="pure" select="*[6]"/>
71        <xsl:apply-templates mode="pure" select="*[7]"/>
72       </m:apply>
73       <xsl:apply-templates mode="thread" select="*[5]"/>
74      </m:apply>
75     </xsl:when>
76     <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
77     <xsl:when test="name()= 'APPLY' and CONST[
78  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] 
79  and count(child::*) = 6">
80      <m:apply helm:xref="{@id}">
81       <m:csymbol>and_ind</m:csymbol>
82       <xsl:apply-templates mode="noannot" select="*[6]"/>
83       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
84       <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
85       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
86       <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
87       <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
88      </m:apply>
89     </xsl:when>
90     <xsl:when test="name()= 'APPLY' and CONST[
91  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con'] 
92  and count(child::*) = 7">
93      <m:apply helm:xref="{@id}">
94       <m:csymbol>or_ind</m:csymbol>
95       <xsl:apply-templates mode="noannot" select="*[7]"/>
96       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
97       <xsl:apply-templates mode="pure" select="*[5]"/>
98       <xsl:apply-templates mode="pure" select="*[6]"/>
99      </m:apply>
100     </xsl:when>
101     <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1">
102      <m:apply helm:xref="{@id}">
103       <m:csymbol>thread</m:csymbol>
104       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
105       <m:apply>
106        <m:csymbol>app</m:csymbol>
107        <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
108       </m:apply>
109       <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
110      </m:apply>
111     </xsl:when>
112     <xsl:otherwise>
113      <m:apply helm:xref="{@id}">
114       <m:csymbol>proof</m:csymbol>
115       <xsl:apply-templates select="." mode="pure"/>
116       <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
117       <xsl:apply-templates select="//InnerTypes/TYPE[@of=$id]" mode="pure"/>
118      </m:apply>
119     </xsl:otherwise>
120    </xsl:choose>
121 </xsl:template>
122
123 <xsl:template match="*" mode="copy-of-no-prop">
124  <xsl:choose>
125   <xsl:when test="@id = //InnerTypes/TYPE/@of">
126    <m:ci>previous</m:ci>
127   </xsl:when>
128   <xsl:otherwise>
129    <xsl:apply-templates select="." mode="pure"/>
130   </xsl:otherwise>
131  </xsl:choose>
132  <xsl:apply-templates mode="copy-of-no-prop" select="following-sibling::*[1]"/>
133 </xsl:template>
134
135 <xsl:template match="*" mode="thread">
136   <xsl:choose>
137    <xsl:when test="name()= 'APPLY' and CONST[
138  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
139  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
140     <xsl:variable name="id" select="@id"/>
141      <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
142      <m:apply>
143       <m:csymbol>rw_step</m:csymbol>
144       <xsl:apply-templates mode="pure" select="*[3]"/>
145       <xsl:apply-templates mode="pure" select="*[6]"/>
146       <xsl:apply-templates mode="pure" select="*[7]"/>
147      </m:apply>
148      <xsl:apply-templates mode="thread" select="*[5]"/>
149    </xsl:when>
150 <!--**** Patch temporanea, per il problema dei threads ***-->
151 <xsl:when test="(name()= 'APPLY' and CONST[
152  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] 
153  and count(child::*) = 6) or
154 (name()= 'APPLY' and CONST[
155  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con'] 
156  and count(child::*) = 7)">
157  <xsl:apply-templates mode="noannot" select="."/>
158 </xsl:when>
159 <!--**** Fine Patch temporanea, per il problema dei threads ***-->
160    <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1">
161        <xsl:variable name="id" select="@id"/>
162        <m:apply helm:xref="{@id}">
163         <m:csymbol>thread</m:csymbol>
164         <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
165         <m:apply>
166          <m:csymbol>app</m:csymbol>
167          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
168         </m:apply>
169         <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
170        </m:apply>
171    </xsl:when>
172    <xsl:otherwise>
173     <xsl:apply-templates mode="noannot" select="."/>
174    </xsl:otherwise>
175   </xsl:choose>
176 </xsl:template>
177
178
179 <!-- Basic proof operators -->
180
181 <!-- non del tutto soddisfacente, ma .... -->
182 <xsl:template match="APPLY[CONST[
183  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
184  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con']]" mode="appflat">
185     <xsl:choose>
186      <xsl:when test="count(child::*) > 7">
187       <xsl:variable name="id" select="@id"/>
188       <xsl:variable name="ideqp" select="*[7]/@id"/>
189       <xsl:variable name="idsubp" select="*[5]/@id"/>
190       <xsl:variable name="leteqp" select="boolean(//InnerTypes/TYPE[@of=$ideqp])"/>
191       <xsl:variable name="letsubp" select="boolean(//InnerTypes/TYPE[@of=$idsubp])"/>
192       <m:apply helm:xref="{@id}">
193        <m:csymbol>rewrite_and_apply</m:csymbol>
194        <m:apply>
195         <m:csymbol>rw_step</m:csymbol>
196         <xsl:apply-templates mode="pure" select="*[3]"/>
197         <xsl:apply-templates mode="pure" select="*[6]"/>
198         <xsl:choose>
199          <xsl:when test="$leteqp">
200           <xsl:choose>
201            <xsl:when test="$letsubp">
202             <m:ci>
203              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h2'"/></xsl:with-param></xsl:call-template>
204             </m:ci>
205            </xsl:when>
206            <xsl:otherwise>
207             <m:ci>
208              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
209             </m:ci>
210            </xsl:otherwise>
211           </xsl:choose>
212          </xsl:when>
213          <xsl:otherwise>
214           <xsl:apply-templates mode="pure" select="*[7]"/>
215          </xsl:otherwise>
216         </xsl:choose>
217        </m:apply>
218       <xsl:choose>
219        <xsl:when test="$letsubp">
220         <m:ci>
221          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
222         </m:ci>
223        </xsl:when>
224        <xsl:otherwise>
225         <xsl:apply-templates mode="pure" select="*[5]"/>
226        </xsl:otherwise>
227       </xsl:choose>
228       <xsl:apply-templates mode="flat" select="*[8]">
229        <xsl:with-param name="n">
230         <xsl:value-of select="1+$letsubp+$leteqp"/>
231        </xsl:with-param>
232       </xsl:apply-templates>
233      </m:apply>
234     </xsl:when>
235     <xsl:otherwise>
236      <m:apply helm:xref="{@id}">
237       <m:csymbol>app</m:csymbol>
238       <xsl:apply-templates mode="flat" select="*[1]"/>
239      </m:apply>
240     </xsl:otherwise>
241    </xsl:choose>
242 </xsl:template> 
243
244 <xsl:template match="APPLY[CONST[
245  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
246     <xsl:choose>
247      <xsl:when test="count(child::*) > 4">
248       <m:apply helm:xref="{@id}">
249        <m:csymbol>app</m:csymbol>
250        <xsl:apply-templates mode="pure" select="*[1]"/>
251        <m:ci>*</m:ci>
252        <m:ci>*</m:ci>
253        <m:ci>*</m:ci>
254        <xsl:apply-templates mode="flat" select="*[5]"/>
255       </m:apply>
256      </xsl:when>
257      <xsl:otherwise>
258       <m:apply helm:xref="{@id}">
259        <m:csymbol>app</m:csymbol>
260        <xsl:apply-templates mode="flat" select="*[1]"/>
261       </m:apply>
262      </xsl:otherwise>
263     </xsl:choose>
264 </xsl:template> 
265
266
267 </xsl:stylesheet>
268
269
270
271
272
273