]> matita.cs.unibo.it Git - helm.git/blob - helm/style/proofs.xsl
3b653ad15aa38b1f64713976d8a901a61c4fec59
[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 <xsl:template match="PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
26 <xsl:apply-templates select="." mode="pure"/>
27 </xsl:template>
28
29 <xsl:template match="LAMBDA|CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
30     <xsl:variable name="id" select="@id"/>
31     <xsl:choose>
32      <!-- <xsl:when test="//InnerTypes and key('typeid',@id)"> -->
33      <!-- <xsl:when test="//InnerTypes/TYPE[@of=$id]"> -->
34      <xsl:when test="@sort='Prop'">
35      <xsl:choose>
36       <xsl:when test="name()= 'APPLY' and CONST[
37  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
38  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
39        <m:apply helm:xref="{@id}">
40         <m:csymbol>thread</m:csymbol>
41         <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
42         <m:apply>
43          <m:csymbol>rw_step</m:csymbol>
44          <xsl:apply-templates mode="pure" select="*[3]"/>
45          <xsl:apply-templates mode="pure" select="*[6]"/>
46          <xsl:apply-templates mode="pure" select="*[7]"/>
47         </m:apply>
48         <xsl:apply-templates mode="thread" select="*[5]"/>
49        </m:apply>
50       </xsl:when>
51       <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
52       <xsl:when test="name()= 'APPLY' and CONST[
53  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] 
54  and count(child::*) = 6">
55        <m:apply helm:xref="{@id}">
56         <m:csymbol>and_ind</m:csymbol>
57         <xsl:apply-templates mode="noannot" select="*[6]"/>
58         <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>
59         <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
60         <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>
61         <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
62         <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
63        </m:apply>
64       </xsl:when>
65       <xsl:when test="name()= 'APPLY' and CONST[
66  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con'] 
67  and count(child::*) = 7">
68        <m:apply helm:xref="{@id}">
69         <m:csymbol>or_ind</m:csymbol>
70         <xsl:apply-templates mode="noannot" select="*[7]"/>
71         <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
72         <xsl:apply-templates mode="pure" select="*[5]"/>
73         <xsl:apply-templates mode="pure" select="*[6]"/>
74        </m:apply>
75       </xsl:when>
76       <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1">
77        <m:apply helm:xref="{@id}">
78         <m:csymbol>thread</m:csymbol>
79         <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
80         <m:apply>
81          <m:csymbol>app</m:csymbol>
82          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
83         </m:apply>
84         <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
85        </m:apply>
86       </xsl:when>
87       <xsl:otherwise>
88        <m:apply helm:xref="{@id}">
89         <m:csymbol>proof</m:csymbol>
90         <xsl:apply-templates select="." mode="pure"/>
91         <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
92         <xsl:apply-templates select="//InnerTypes/TYPE[@of=$id]" mode="pure"/>
93        </m:apply>
94       </xsl:otherwise>
95      </xsl:choose>
96      </xsl:when>
97      <xsl:otherwise>
98       <xsl:apply-templates select="." mode="pure"/>
99      </xsl:otherwise>
100     </xsl:choose>
101 </xsl:template>
102
103 <xsl:template match="*" mode="copy-of-no-prop">
104  <xsl:choose>
105   <xsl:when test="@id = //InnerTypes/TYPE/@of">
106    <m:ci>previous</m:ci>
107   </xsl:when>
108   <xsl:otherwise>
109    <xsl:apply-templates select="." mode="pure"/>
110   </xsl:otherwise>
111  </xsl:choose>
112  <xsl:apply-templates mode="copy-of-no-prop" select="following-sibling::*[1]"/>
113 </xsl:template>
114
115 <xsl:template match="*" mode="thread">
116   <xsl:choose>
117    <xsl:when test="name()= 'APPLY' and CONST[
118  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
119  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
120     <xsl:variable name="id" select="@id"/>
121      <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
122      <m:apply>
123       <m:csymbol>rw_step</m:csymbol>
124       <xsl:apply-templates mode="pure" select="*[3]"/>
125       <xsl:apply-templates mode="pure" select="*[6]"/>
126       <xsl:apply-templates mode="pure" select="*[7]"/>
127      </m:apply>
128      <xsl:apply-templates mode="thread" select="*[5]"/>
129    </xsl:when>
130 <!--**** Patch temporanea, per il problema dei threads ***-->
131 <xsl:when test="(name()= 'APPLY' and CONST[
132  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] 
133  and count(child::*) = 6) or
134 (name()= 'APPLY' and CONST[
135  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con'] 
136  and count(child::*) = 7)">
137  <xsl:apply-templates mode="noannot" select="."/>
138 </xsl:when>
139 <!--**** Fine Patch temporanea, per il problema dei threads ***-->
140    <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1">
141        <xsl:variable name="id" select="@id"/>
142        <m:apply helm:xref="{@id}">
143         <m:csymbol>thread</m:csymbol>
144         <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
145         <m:apply>
146          <m:csymbol>app</m:csymbol>
147          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
148         </m:apply>
149         <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
150        </m:apply>
151    </xsl:when>
152    <xsl:otherwise>
153     <xsl:apply-templates mode="noannot" select="."/>
154    </xsl:otherwise>
155   </xsl:choose>
156 </xsl:template>
157
158
159 <!-- Basic proof operators -->
160
161 <!-- non del tutto soddisfacente, ma .... -->
162 <xsl:template match="APPLY[CONST[
163  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
164  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con']]" mode="appflat">
165     <xsl:choose>
166      <xsl:when test="count(child::*) > 7">
167       <xsl:variable name="id" select="@id"/>
168       <xsl:variable name="ideqp" select="*[7]/@id"/>
169       <xsl:variable name="idsubp" select="*[5]/@id"/>
170       <xsl:variable name="leteqp" select="boolean(//InnerTypes/TYPE[@of=$ideqp])"/>
171       <xsl:variable name="letsubp" select="boolean(//InnerTypes/TYPE[@of=$idsubp])"/>
172       <m:apply helm:xref="{@id}">
173        <m:csymbol>rewrite_and_apply</m:csymbol>
174        <m:apply>
175         <m:csymbol>rw_step</m:csymbol>
176         <xsl:apply-templates mode="pure" select="*[3]"/>
177         <xsl:apply-templates mode="pure" select="*[6]"/>
178         <xsl:choose>
179          <xsl:when test="$leteqp">
180           <xsl:choose>
181            <xsl:when test="$letsubp">
182             <m:ci>
183              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h2'"/></xsl:with-param></xsl:call-template>
184             </m:ci>
185            </xsl:when>
186            <xsl:otherwise>
187             <m:ci>
188              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
189             </m:ci>
190            </xsl:otherwise>
191           </xsl:choose>
192          </xsl:when>
193          <xsl:otherwise>
194           <xsl:apply-templates mode="pure" select="*[7]"/>
195          </xsl:otherwise>
196         </xsl:choose>
197        </m:apply>
198       <xsl:choose>
199        <xsl:when test="$letsubp">
200         <m:ci>
201          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
202         </m:ci>
203        </xsl:when>
204        <xsl:otherwise>
205         <xsl:apply-templates mode="pure" select="*[5]"/>
206        </xsl:otherwise>
207       </xsl:choose>
208       <xsl:apply-templates mode="flat" select="*[8]">
209        <xsl:with-param name="n">
210         <xsl:value-of select="1+$letsubp+$leteqp"/>
211        </xsl:with-param>
212       </xsl:apply-templates>
213      </m:apply>
214     </xsl:when>
215     <xsl:otherwise>
216      <m:apply helm:xref="{@id}">
217       <m:csymbol>app</m:csymbol>
218       <xsl:apply-templates mode="flat" select="*[1]"/>
219      </m:apply>
220     </xsl:otherwise>
221    </xsl:choose>
222 </xsl:template> 
223
224 <xsl:template match="APPLY[CONST[
225  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
226     <xsl:choose>
227      <xsl:when test="count(child::*) > 4">
228       <m:apply helm:xref="{@id}">
229        <m:csymbol>app</m:csymbol>
230        <xsl:apply-templates mode="pure" select="*[1]"/>
231        <m:ci>*</m:ci>
232        <m:ci>*</m:ci>
233        <m:ci>*</m:ci>
234        <xsl:apply-templates mode="flat" select="*[5]"/>
235       </m:apply>
236      </xsl:when>
237      <xsl:otherwise>
238       <m:apply helm:xref="{@id}">
239        <m:csymbol>app</m:csymbol>
240        <xsl:apply-templates mode="flat" select="*[1]"/>
241       </m:apply>
242      </xsl:otherwise>
243     </xsl:choose>
244 </xsl:template> 
245
246
247 </xsl:stylesheet>
248
249
250
251
252
253