helm/style/rewrite.xsl

   1 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
   2 <!-- GNU General Public License for more details.                      -->
   3 <!--                                                                   -->
   4 <!-- You should have received a copy of the GNU General Public License -->
   5 <!-- along with HELM; if not, write to the Free Software               -->
   6 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
   7 <!-- MA  02111-1307, USA.                                              -->
   8 <!--                                                                   -->
   9 <!-- For details, see the HELM World-Wide-Web page,                    -->
  10 <!-- http://cs.unibo.it/helm/.                                         -->
  11
  12 <!--******************************************************************-->
  13 <!-- Basic Logic                                                      -->
  14 <!-- (completely) Revisited: february 2001, Andrea Asperti            -->
  15 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
  16 <!--******************************************************************-->
  17
  18 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  19                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  20                               xmlns:helm="http://www.cs.unibo.it/helm">
  21
  22 <xsl:template mode="proof_transform" match="APPLY[CONST[
  23  attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
  24  attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
  25  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
  26  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
  27  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7]">
  28  <xsl:variable name="id" select="@id"/>
  29   <m:apply>
  30    <m:csymbol>rw_step</m:csymbol>
  31    <xsl:apply-templates mode="noannot" select="*[5]"/>
  32    <xsl:apply-templates mode="pure" select="*[3]"/>
  33    <xsl:apply-templates mode="pure" select="*[6]"/>
  34    <xsl:call-template name="generate_side_proof">
  35     <xsl:with-param name="proof" select="*[7]"/>
  36    </xsl:call-template>
  37   </m:apply>
  38 </xsl:template>
  39
  40 <xsl:template mode="proof_transform" match="APPLY[CONST[
  41  attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
  42  attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
  43  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
  44  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
  45  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7]">
  46  <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
  47  <xsl:choose>
  48   <xsl:when test="$no_extraproofs=0">
  49    <m:apply>
  50     <m:csymbol>rewrite_and_apply</m:csymbol>
  51     <m:apply>
  52      <m:csymbol>rw_step</m:csymbol>
  53      <xsl:apply-templates mode="noannot" select="*[5]"/>
  54      <xsl:apply-templates mode="pure" select="*[3]"/>
  55      <xsl:apply-templates mode="pure" select="*[6]"/>
  56      <xsl:call-template name="generate_side_proof">
  57       <xsl:with-param name="proof" select="*[7]"/>
  58      </xsl:call-template>
  59     </m:apply>
  60     <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
  61    </m:apply>
  62   </xsl:when>
  63   <xsl:otherwise>
  64    <xsl:choose>
  65     <xsl:when test="*[5]/@sort='Prop'">
  66      <m:apply helm:xref="{@id}">
  67       <m:csymbol>letin</m:csymbol>
  68       <m:apply>
  69        <m:csymbol>let</m:csymbol>
  70        <m:ci>
  71         <xsl:call-template name="insert_subscript">
  72          <xsl:with-param name="node_value" select="'h1'"/>
  73         </xsl:call-template>
  74        </m:ci>
  75        <xsl:apply-templates mode="noannot" select="*[5]"/>
  76       </m:apply>
  77       <xsl:call-template name="gen_let">
  78        <xsl:with-param name="init_pos" select="1"/>
  79        <xsl:with-param name="from" select="7"/>
  80       </xsl:call-template>
  81       <m:apply>
  82        <m:csymbol>rewrite_and_apply</m:csymbol>
  83        <m:apply>
  84         <m:csymbol>rw_step</m:csymbol>
  85         <m:ci>
  86          <xsl:call-template name="insert_subscript">
  87           <xsl:with-param name="node_value" select="'h1'"/>
  88          </xsl:call-template>
  89         </m:ci>
  90         <xsl:apply-templates mode="pure" select="*[3]"/>
  91         <xsl:apply-templates mode="pure" select="*[6]"/>
  92         <xsl:call-template name="generate_side_proof">
  93          <xsl:with-param name="proof" select="*[7]"/>
  94         </xsl:call-template>
  95        </m:apply>
  96        <xsl:apply-templates mode="flat" select="*[8]">
  97         <xsl:with-param name="n">
  98          <xsl:value-of select="2"/>
  99         </xsl:with-param>
 100        </xsl:apply-templates>
 101       </m:apply>
 102      </m:apply>
 103     </xsl:when>
 104     <xsl:otherwise>
 105      <m:apply helm:xref="{@id}">
 106       <m:csymbol>letin</m:csymbol>
 107       <xsl:call-template name="gen_let">
 108        <xsl:with-param name="init_pos" select="0"/>
 109        <xsl:with-param name="form" select="7"/>
 110       </xsl:call-template>
 111       <m:apply>
 112        <m:csymbol>rewrite_and_apply</m:csymbol>
 113        <m:apply>
 114         <m:csymbol>rw_step</m:csymbol>
 115         <xsl:apply-templates mode="pure" select="*[5]"/>
 116         <xsl:apply-templates mode="pure" select="*[3]"/>
 117         <xsl:apply-templates mode="pure" select="*[6]"/>
 118         <xsl:call-template name="generate_side_proof">
 119          <xsl:with-param name="proof" select="*[7]"/>
 120         </xsl:call-template>
 121        </m:apply>
 122        <xsl:apply-templates mode="flat" select="*[8]">
 123         <xsl:with-param name="n">
 124          <xsl:value-of select="1"/>
 125         </xsl:with-param>
 126        </xsl:apply-templates>
 127       </m:apply>
 128      </m:apply>
 129     </xsl:otherwise>
 130    </xsl:choose>
 131   </xsl:otherwise>
 132  </xsl:choose>
 133 </xsl:template>
 134
 135 </xsl:stylesheet>