helm/style/proofs.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   6 <!-- Library of Mathematics, developed at the Computer Science         -->
   7 <!-- Department, University of Bologna, Italy.                         -->
   8 <!--                                                                   -->
   9 <!-- HELM is free software; you can redistribute it and/or             -->
  10 <!-- modify it under the terms of the GNU General Public License       -->
  11 <!-- as published by the Free Software Foundation; either version 2    -->
  12 <!-- of the License, or (at your option) any later version.            -->
  13 <!--                                                                   -->
  14 <!-- HELM is distributed in the hope that it will be useful,           -->
  15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  17 <!-- GNU General Public License for more details.                      -->
  18 <!--                                                                   -->
  19 <!-- You should have received a copy of the GNU General Public License -->
  20 <!-- along with HELM; if not, write to the Free Software               -->
  21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  22 <!-- MA  02111-1307, USA.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <!--******************************************************************-->
  28 <!-- Basic Logic                                                      -->
  29 <!-- First draft: April 3 2000                                        -->
  30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
  31 <!--******************************************************************-->
  32
  33 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  34                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  35                               xmlns:helm="http://www.cs.unibo.it/helm">
  36
  37 <!--******************************************************************-->
  38 <!-- Variable containing the absolute path of the CIC file            -->
  39 <!--******************************************************************-->
  40
  41 <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
  42
  43 <!-- ************************* LOGIC *********************************-->
  44
  45 <!-- Proof objects -->
  46
  47 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
  48
  49 <!-- ALL this elements does not have inner type -->
  50 <xsl:template match="LETIN|PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
  51 <xsl:apply-templates select="." mode="pure"/>
  52 </xsl:template>
  53
  54 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
  55 <xsl:template match="LAMBDA" mode="noannot">
  56  <xsl:variable name="id" select="@id"/>
  57  <xsl:choose>
  58   <xsl:when test="//InnerTypes and @sort='Prop' and name(../..) != 'LAMBDA'">
  59   <!-- <xsl:when test="@sort='Prop' and //InnerTypes/TYPE[@of=$id]"> -->
  60    <xsl:call-template name="has_inner_type"/>
  61   </xsl:when>
  62   <xsl:otherwise>
  63    <xsl:apply-templates select="." mode="pure"/>
  64   </xsl:otherwise>
  65  </xsl:choose>
  66 </xsl:template>
  67
  68 <!-- ALL this elements have inner type -->
  69 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
  70  <xsl:choose>
  71   <!-- <xsl:when test="//InnerTypes and key('typeid',@id)"> -->
  72   <!-- <xsl:when test="//InnerTypes/TYPE[@of=$id]"> -->
  73   <xsl:when test="//InnerTypes and @sort='Prop'">
  74    <xsl:call-template name="has_inner_type"/>
  75   </xsl:when>
  76   <xsl:otherwise>
  77    <xsl:apply-templates select="." mode="pure"/>
  78   </xsl:otherwise>
  79  </xsl:choose>
  80 </xsl:template>
  81
  82 <xsl:template name="has_inner_type">
  83    <xsl:variable name="id" select="@id"/>
  84    <xsl:choose>
  85     <xsl:when test="name()= 'APPLY' and CONST[
  86  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
  87  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
  88      <m:apply helm:xref="{@id}">
  89       <m:csymbol>thread</m:csymbol>
  90       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
  91       <m:apply>
  92        <m:csymbol>rw_step</m:csymbol>
  93        <xsl:apply-templates mode="pure" select="*[3]"/>
  94        <xsl:apply-templates mode="pure" select="*[6]"/>
  95        <xsl:apply-templates mode="pure" select="*[7]"/>
  96       </m:apply>
  97       <xsl:apply-templates mode="thread" select="*[5]"/>
  98      </m:apply>
  99     </xsl:when>
 100     <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
 101     <xsl:when test="name()= 'APPLY' and CONST[
 102  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 103  and count(child::*) = 6">
 104      <m:apply helm:xref="{@id}">
 105       <m:csymbol>and_ind</m:csymbol>
 106       <xsl:apply-templates mode="noannot" select="*[6]"/>
 107       <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>
 108       <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 109       <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>
 110       <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 111       <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
 112      </m:apply>
 113     </xsl:when>
 114     <xsl:when test="name()= 'APPLY' and CONST[
 115  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 116  and count(child::*) = 7">
 117      <m:apply helm:xref="{@id}">
 118       <m:csymbol>or_ind</m:csymbol>
 119       <xsl:apply-templates mode="noannot" select="*[7]"/>
 120       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 121       <xsl:apply-templates mode="pure" select="*[5]"/>
 122       <xsl:apply-templates mode="pure" select="*[6]"/>
 123      </m:apply>
 124     </xsl:when>
 125     <!-- <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1"> -->
 126     <xsl:when test="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 1">
 127      <m:apply helm:xref="{@id}">
 128       <m:csymbol>thread</m:csymbol>
 129       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 130       <m:apply>
 131        <m:csymbol>app</m:csymbol>
 132        <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 133       </m:apply>
 134       <xsl:apply-templates mode="thread" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
 135      </m:apply>
 136     </xsl:when>
 137     <xsl:otherwise>
 138      <m:apply helm:xref="{@id}">
 139       <m:csymbol>proof</m:csymbol>
 140       <xsl:apply-templates select="." mode="pure"/>
 141       <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
 142       <xsl:apply-templates select="//InnerTypes/TYPE[@of=$id]/*" mode="pure"/>
 143      </m:apply>
 144     </xsl:otherwise>
 145    </xsl:choose>
 146 </xsl:template>
 147
 148 <xsl:template match="*" mode="copy-of-no-prop">
 149  <xsl:choose>
 150   <!-- <xsl:when test="@id = //InnerTypes/TYPE/@of"> -->
 151   <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
 152    <m:ci>previous</m:ci>
 153   </xsl:when>
 154   <xsl:otherwise>
 155    <xsl:apply-templates select="." mode="pure"/>
 156   </xsl:otherwise>
 157  </xsl:choose>
 158  <xsl:apply-templates mode="copy-of-no-prop" select="following-sibling::*[1]"/>
 159 </xsl:template>
 160
 161 <xsl:template match="*" mode="thread">
 162   <xsl:choose>
 163    <xsl:when test="name()= 'APPLY' and CONST[
 164  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 165  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 166     <xsl:variable name="id" select="@id"/>
 167      <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 168      <m:apply>
 169       <m:csymbol>rw_step</m:csymbol>
 170       <xsl:apply-templates mode="pure" select="*[3]"/>
 171       <xsl:apply-templates mode="pure" select="*[6]"/>
 172       <xsl:apply-templates mode="pure" select="*[7]"/>
 173      </m:apply>
 174      <xsl:apply-templates mode="thread" select="*[5]"/>
 175    </xsl:when>
 176 <!--**** Patch temporanea, per il problema dei threads ***-->
 177 <xsl:when test="(name()= 'APPLY' and CONST[
 178  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 179  and count(child::*) = 6) or
 180 (name()= 'APPLY' and CONST[
 181  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 182  and count(child::*) = 7)">
 183  <xsl:apply-templates mode="noannot" select="."/>
 184 </xsl:when>
 185 <!--**** Fine Patch temporanea, per il problema dei threads ***-->
 186    <xsl:when test="//InnerTypes and count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 1">
 187        <xsl:variable name="id" select="@id"/>
 188        <m:apply helm:xref="{@id}">
 189         <m:csymbol>thread</m:csymbol>
 190         <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 191         <m:apply>
 192          <m:csymbol>app</m:csymbol>
 193          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 194         </m:apply>
 195         <!-- <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/> -->
 196         <xsl:apply-templates mode="thread" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
 197        </m:apply>
 198    </xsl:when>
 199    <xsl:otherwise>
 200     <xsl:apply-templates mode="noannot" select="."/>
 201    </xsl:otherwise>
 202   </xsl:choose>
 203 </xsl:template>
 204
 205
 206 <!-- Basic proof operators -->
 207
 208 <!-- non del tutto soddisfacente, ma .... -->
 209 <xsl:template match="APPLY[CONST[
 210  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 211  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con']]" mode="appflat">
 212     <xsl:choose>
 213      <xsl:when test="count(child::*) > 7">
 214       <xsl:variable name="id" select="@id"/>
 215       <xsl:variable name="ideqp" select="*[7]/@id"/>
 216       <xsl:variable name="idsubp" select="*[5]/@id"/>
 217 <!--
 218       <xsl:variable name="leteqp" select="boolean(//InnerTypes/TYPE[@of=$ideqp])"/>
 219       <xsl:variable name="letsubp" select="boolean(//InnerTypes/TYPE[@of=$idsubp])"/>
 220 -->
 221       <xsl:variable name="leteqp" select="boolean(*[7][@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
 222       <xsl:variable name="letsubp" select="boolean(*[5][@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
 223       <m:apply helm:xref="{@id}">
 224        <m:csymbol>rewrite_and_apply</m:csymbol>
 225        <m:apply>
 226         <m:csymbol>rw_step</m:csymbol>
 227         <xsl:apply-templates mode="pure" select="*[3]"/>
 228         <xsl:apply-templates mode="pure" select="*[6]"/>
 229         <xsl:choose>
 230          <xsl:when test="$leteqp">
 231           <xsl:choose>
 232            <xsl:when test="$letsubp">
 233             <m:ci>
 234              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h2'"/></xsl:with-param></xsl:call-template>
 235             </m:ci>
 236            </xsl:when>
 237            <xsl:otherwise>
 238             <m:ci>
 239              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 240             </m:ci>
 241            </xsl:otherwise>
 242           </xsl:choose>
 243          </xsl:when>
 244          <xsl:otherwise>
 245           <xsl:apply-templates mode="pure" select="*[7]"/>
 246          </xsl:otherwise>
 247         </xsl:choose>
 248        </m:apply>
 249       <xsl:choose>
 250        <xsl:when test="$letsubp">
 251         <m:ci>
 252          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 253         </m:ci>
 254        </xsl:when>
 255        <xsl:otherwise>
 256         <xsl:apply-templates mode="pure" select="*[5]"/>
 257        </xsl:otherwise>
 258       </xsl:choose>
 259       <xsl:apply-templates mode="flat" select="*[8]">
 260        <xsl:with-param name="n">
 261         <xsl:value-of select="1+$letsubp+$leteqp"/>
 262        </xsl:with-param>
 263       </xsl:apply-templates>
 264      </m:apply>
 265     </xsl:when>
 266     <xsl:otherwise>
 267      <m:apply helm:xref="{@id}">
 268       <m:csymbol>app</m:csymbol>
 269       <xsl:apply-templates mode="flat" select="*[1]"/>
 270      </m:apply>
 271     </xsl:otherwise>
 272    </xsl:choose>
 273 </xsl:template>
 274
 275 <xsl:template match="APPLY[CONST[
 276  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 277     <xsl:choose>
 278      <xsl:when test="count(child::*) > 4">
 279       <m:apply helm:xref="{@id}">
 280        <m:csymbol>app</m:csymbol>
 281        <xsl:apply-templates mode="pure" select="*[1]"/>
 282        <m:ci>*</m:ci>
 283        <m:ci>*</m:ci>
 284        <m:ci>*</m:ci>
 285        <xsl:apply-templates mode="flat" select="*[5]"/>
 286       </m:apply>
 287      </xsl:when>
 288      <xsl:otherwise>
 289       <m:apply helm:xref="{@id}">
 290        <m:csymbol>app</m:csymbol>
 291        <xsl:apply-templates mode="flat" select="*[1]"/>
 292       </m:apply>
 293      </xsl:otherwise>
 294     </xsl:choose>
 295 </xsl:template>
 296
 297
 298 </xsl:stylesheet>
 299
 300
 301
 302
 303
 304