3 <!--******************************************************************-->
5 <!-- First draft: April 3 2000 -->
6 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
7 <!--******************************************************************-->
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">
13 <!--******************************************************************-->
14 <!-- Variable containing the absolute path of the CIC file -->
15 <!--******************************************************************-->
17 <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
19 <!-- ************************* LOGIC *********************************-->
21 <!-- Proof objects -->
23 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
25 <xsl:template match="LAMBDA|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX" mode="noannot">
28 <xsl:variable name="id" select="@id"/>
30 <!-- <xsl:when test="//InnerTypes and key('typeid',@id)"> -->
31 <xsl:when test="//InnerTypes/TYPE[@of=$id]">
33 <xsl:when test="name()= 'APPLY' and CONST[
34 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
35 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
36 <m:apply helm:xref="{@id}">
37 <m:csymbol>thread</m:csymbol>
38 <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
40 <m:csymbol>rw_step</m:csymbol>
41 <xsl:apply-templates mode="pure" select="*[3]"/>
42 <xsl:apply-templates mode="pure" select="*[6]"/>
43 <xsl:apply-templates mode="pure" select="*[7]"/>
45 <xsl:apply-templates mode="thread" select="*[5]"/>
48 <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
49 <xsl:when test="name()= 'APPLY' and CONST[
50 attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
51 and count(child::*) = 6">
52 <m:apply helm:xref="{@id}">
53 <m:csymbol>and_ind</m:csymbol>
54 <xsl:apply-templates mode="noannot" select="*[6]"/>
55 <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>
56 <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
57 <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>
58 <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
59 <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
62 <xsl:when test="name()= 'APPLY' and CONST[
63 attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
64 and count(child::*) = 7">
65 <m:apply helm:xref="{@id}">
66 <m:csymbol>or_ind</m:csymbol>
67 <xsl:apply-templates mode="noannot" select="*[7]"/>
68 <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
69 <xsl:apply-templates mode="pure" select="*[5]"/>
70 <xsl:apply-templates mode="pure" select="*[6]"/>
73 <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1">
74 <m:apply helm:xref="{@id}">
75 <m:csymbol>thread</m:csymbol>
76 <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
78 <m:csymbol>app</m:csymbol>
79 <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
81 <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
85 <m:apply helm:xref="{@id}">
86 <m:csymbol>proof</m:csymbol>
87 <xsl:apply-templates select="." mode="pure"/>
88 <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
89 <xsl:apply-templates select="//InnerTypes/TYPE[@of=$id]" mode="pure"/>
95 <xsl:apply-templates select="." mode="pure"/>
100 <xsl:apply-templates select="." mode="pure"/>
105 <xsl:template match="*" mode="copy-of-no-prop">
107 <xsl:when test="@id = //InnerTypes/TYPE/@of">
108 <m:ci>previous</m:ci>
111 <xsl:apply-templates select="." mode="pure"/>
114 <xsl:apply-templates mode="copy-of-no-prop" select="following-sibling::*[1]"/>
117 <xsl:template match="*" mode="thread">
119 <xsl:when test="name()= 'APPLY' and CONST[
120 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
121 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
122 <xsl:variable name="id" select="@id"/>
123 <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
125 <m:csymbol>rw_step</m:csymbol>
126 <xsl:apply-templates mode="pure" select="*[3]"/>
127 <xsl:apply-templates mode="pure" select="*[6]"/>
128 <xsl:apply-templates mode="pure" select="*[7]"/>
130 <xsl:apply-templates mode="thread" select="*[5]"/>
132 <!--**** Patch temporanea, per il problema dei threads ***-->
133 <xsl:when test="(name()= 'APPLY' and CONST[
134 attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
135 and count(child::*) = 6) or
136 (name()= 'APPLY' and CONST[
137 attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
138 and count(child::*) = 7)">
139 <xsl:apply-templates mode="noannot" select="."/>
141 <!--**** Fine Patch temporanea, per il problema dei threads ***-->
142 <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1">
143 <xsl:variable name="id" select="@id"/>
144 <m:apply helm:xref="{@id}">
145 <m:csymbol>thread</m:csymbol>
146 <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
148 <m:csymbol>app</m:csymbol>
149 <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
151 <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
155 <xsl:apply-templates mode="noannot" select="."/>
161 <!-- Basic proof operators -->
163 <!-- non del tutto soddisfacente, ma .... -->
164 <xsl:template match="APPLY[CONST[
165 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
166 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con']]" mode="appflat">
168 <xsl:when test="count(child::*) > 7">
169 <xsl:variable name="id" select="@id"/>
170 <xsl:variable name="ideqp" select="*[7]/@id"/>
171 <xsl:variable name="idsubp" select="*[5]/@id"/>
172 <xsl:variable name="leteqp" select="boolean(//InnerTypes/TYPE[@of=$ideqp])"/>
173 <xsl:variable name="letsubp" select="boolean(//InnerTypes/TYPE[@of=$idsubp])"/>
174 <m:apply helm:xref="{@id}">
175 <m:csymbol>rewrite_and_apply</m:csymbol>
177 <m:csymbol>rw_step</m:csymbol>
178 <xsl:apply-templates mode="pure" select="*[3]"/>
179 <xsl:apply-templates mode="pure" select="*[6]"/>
181 <xsl:when test="$leteqp">
183 <xsl:when test="$letsubp">
185 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h2'"/></xsl:with-param></xsl:call-template>
190 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
196 <xsl:apply-templates mode="pure" select="*[7]"/>
201 <xsl:when test="$letsubp">
203 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
207 <xsl:apply-templates mode="pure" select="*[5]"/>
210 <xsl:apply-templates mode="flat" select="*[8]">
211 <xsl:with-param name="n">
212 <xsl:value-of select="1+$letsubp+$leteqp"/>
214 </xsl:apply-templates>
218 <m:apply helm:xref="{@id}">
219 <m:csymbol>app</m:csymbol>
220 <xsl:apply-templates mode="flat" select="*[1]"/>
226 <xsl:template match="APPLY[CONST[
227 attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
229 <xsl:when test="count(child::*) > 4">
230 <m:apply helm:xref="{@id}">
231 <m:csymbol>app</m:csymbol>
232 <xsl:apply-templates mode="pure" select="*[1]"/>
236 <xsl:apply-templates mode="flat" select="*[5]"/>
240 <m:apply helm:xref="{@id}">
241 <m:csymbol>app</m:csymbol>
242 <xsl:apply-templates mode="flat" select="*[1]"/>