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/get?url=</xsl:variable>
19 <!-- ************************* LOGIC *********************************-->
21 <!-- Proof objects -->
23 <!-- <xsl:key name="typeid" use="@id" 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="//ALLTYPES and key('typeid',@id)"> -->
31 <xsl:when test="//ALLTYPES/TYPE[@id=$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="//ALLTYPES/TYPE[@id=$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 <xsl:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
49 <m:apply helm:xref="{@id}">
50 <m:csymbol>thread</m:csymbol>
51 <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
53 <m:csymbol>app</m:csymbol>
54 <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
56 <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
59 <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
60 <xsl:when test="name()= 'APPLY' and CONST[
61 attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']
62 and count(child::*) = 6">
63 <m:apply helm:xref="{@id}">
64 <m:csymbol>and_ind</m:csymbol>
65 <xsl:apply-templates mode="noannot" select="*[6]"/>
66 <m:ci><xsl:value-of select="*[5]/target/@binder"/></m:ci>
67 <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
68 <m:ci><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></m:ci>
69 <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
70 <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
73 <xsl:when test="name()= 'APPLY' and CONST[
74 attribute::uri='cic:/coq/INIT/Logic/Disjunction/or_ind.con']
75 and count(child::*) = 7">
76 <m:apply helm:xref="{@id}">
77 <m:csymbol>or_ind</m:csymbol>
78 <xsl:apply-templates mode="noannot" select="*[7]"/>
79 <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
80 <xsl:apply-templates mode="pure" select="*[5]"/>
81 <xsl:apply-templates mode="pure" select="*[6]"/>
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="//ALLTYPES/TYPE[@id=$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 = //ALLTYPES/TYPE/@id">
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="//ALLTYPES/TYPE[@id=$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 <xsl:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
133 <m:apply helm:xref="{@id}">
134 <m:csymbol>thread</m:csymbol>
135 <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
137 <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
139 <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
143 <xsl:apply-templates mode="noannot" select="."/>
149 <!-- Basic proof operators -->
151 <!-- non del tutto soddisfacente, ma .... -->
152 <xsl:template match="APPLY[CONST[
153 attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
154 attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con']]" mode="appflat">
156 <xsl:when test="count(child::*) > 7">
157 <xsl:variable name="id" select="@id"/>
158 <xsl:variable name="ideqp" select="*[7]/@id"/>
159 <xsl:variable name="idsubp" select="*[5]/@id"/>
160 <xsl:variable name="leteqp" select="boolean(//ALLTYPES/TYPE[@id=$ideqp])"/>
161 <xsl:variable name="letsubp" select="boolean(//ALLTYPES/TYPE[@id=$idsubp])"/>
162 <m:apply helm:xref="{@id}">
163 <m:csymbol>rewrite_and_apply</m:csymbol>
165 <m:csymbol>rw_step</m:csymbol>
166 <xsl:apply-templates mode="pure" select="*[3]"/>
167 <xsl:apply-templates mode="pure" select="*[6]"/>
169 <xsl:when test="$leteqp">
171 <xsl:when test="$letsubp">
173 <xsl:value-of select="'h2'"/>
178 <xsl:value-of select="'h1'"/>
184 <xsl:apply-templates mode="pure" select="*[7]"/>
189 <xsl:when test="$letsubp">
191 <xsl:value-of select="'h1'"/>
195 <xsl:apply-templates mode="pure" select="*[5]"/>
198 <xsl:apply-templates mode="flat" select="*[8]">
199 <xsl:with-param name="n">
200 <xsl:value-of select="1+$letsubp+$leteqp"/>
202 </xsl:apply-templates>
206 <m:apply helm:xref="{@id}">
207 <m:csymbol>app</m:csymbol>
208 <xsl:apply-templates mode="flat" select="*[1]"/>
214 <xsl:template match="APPLY[CONST[
215 attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']]" mode="appflat">
217 <xsl:when test="count(child::*) > 4">
218 <m:apply helm:xref="{@id}">
219 <m:csymbol>app</m:csymbol>
220 <xsl:apply-templates mode="pure" select="*[1]"/>
224 <xsl:apply-templates mode="flat" select="*[5]"/>
228 <m:apply helm:xref="{@id}">
229 <m:csymbol>app</m:csymbol>
230 <xsl:apply-templates mode="flat" select="*[1]"/>