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>rewrite</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="rewrite" 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:value-of select="*[5]/target/@binder"/></m:ci>
56 <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
57 <m:ci><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></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="//ALLTYPES/TYPE[@id=$id]"/>
69 <xsl:apply-templates mode="pure" select="*[5]"/>
70 <xsl:apply-templates mode="pure" select="*[6]"/>
74 <m:apply helm:xref="{@id}">
75 <m:csymbol>proof</m:csymbol>
76 <xsl:apply-templates select="." mode="pure"/>
77 <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
78 <xsl:apply-templates select="//ALLTYPES/TYPE[@id=$id]" mode="pure"/>
84 <xsl:apply-templates select="." mode="pure"/>
89 <xsl:apply-templates select="." mode="pure"/>
94 <xsl:template match="*" mode="rewrite">
96 <xsl:when test="name()= 'APPLY' and CONST[
97 attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
98 attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
99 <xsl:variable name="id" select="@id"/>
100 <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
102 <m:csymbol>rw_step</m:csymbol>
103 <xsl:apply-templates mode="pure" select="*[3]"/>
104 <xsl:apply-templates mode="pure" select="*[6]"/>
105 <xsl:apply-templates mode="pure" select="*[7]"/>
107 <xsl:apply-templates mode="rewrite" select="*[5]"/>
110 <xsl:apply-templates mode="noannot" select="."/>
116 <!-- Basic proof operators -->
118 <!-- non del tutto soddisfacente, ma .... -->
119 <xsl:template match="APPLY[CONST[
120 attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
121 attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con']]" mode="appflat">
123 <xsl:when test="count(child::*) > 7">
124 <xsl:variable name="id" select="@id"/>
125 <xsl:variable name="ideqp" select="*[7]/@id"/>
126 <xsl:variable name="idsubp" select="*[5]/@id"/>
127 <xsl:variable name="leteqp" select="boolean(//ALLTYPES/TYPE[@id=$ideqp])"/>
128 <xsl:variable name="letsubp" select="boolean(//ALLTYPES/TYPE[@id=$idsubp])"/>
129 <m:apply helm:xref="{@id}">
130 <m:csymbol>rewrite_and_apply</m:csymbol>
132 <m:csymbol>rw_step</m:csymbol>
133 <xsl:apply-templates mode="pure" select="*[3]"/>
134 <xsl:apply-templates mode="pure" select="*[6]"/>
136 <xsl:when test="$leteqp">
138 <xsl:when test="$letsubp">
140 <xsl:value-of select="'h2'"/>
145 <xsl:value-of select="'h1'"/>
151 <xsl:apply-templates mode="pure" select="*[7]"/>
156 <xsl:when test="$letsubp">
158 <xsl:value-of select="'h1'"/>
162 <xsl:apply-templates mode="pure" select="*[5]"/>
165 <xsl:apply-templates mode="flat" select="*[8]">
166 <xsl:with-param name="n">
167 <xsl:value-of select="1+$letsubp+$leteqp"/>
169 </xsl:apply-templates>
173 <m:apply helm:xref="{@id}">
174 <m:csymbol>app</m:csymbol>
175 <xsl:apply-templates mode="flat" select="*[1]"/>
181 <xsl:template match="APPLY[CONST[
182 attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']]" mode="appflat">
184 <xsl:when test="count(child::*) > 4">
185 <m:apply helm:xref="{@id}">
186 <m:csymbol>app</m:csymbol>
187 <xsl:apply-templates mode="pure" select="*[1]"/>
191 <xsl:apply-templates mode="flat" select="*[5]"/>
195 <m:apply helm:xref="{@id}">
196 <m:csymbol>app</m:csymbol>
197 <xsl:apply-templates mode="flat" select="*[1]"/>