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     <!-- gestire meglio il caso di and_ind quando la prova
 101          non e' della forma \x.\y.M -->
 102     <xsl:when test="name()= 'APPLY' and CONST[
 103  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 104  and count(child::*) = 6
 105  and name(*[5])='LAMBDA'
 106  and name(*[5]/target/*[1])='LAMBDA'">
 107      <m:apply helm:xref="{@id}">
 108       <m:csymbol>and_ind</m:csymbol>
 109       <xsl:apply-templates mode="noannot" select="*[6]"/>
 110       <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>
 111       <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 112       <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>
 113       <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 114       <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
 115      </m:apply>
 116     </xsl:when>
 117     <xsl:when test="name()= 'APPLY' and CONST[
 118  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 119  and count(child::*) = 7">
 120      <m:apply helm:xref="{@id}">
 121       <m:csymbol>or_ind</m:csymbol>
 122       <xsl:apply-templates mode="noannot" select="*[7]"/>
 123       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 124       <xsl:apply-templates mode="pure" select="*[5]"/>
 125       <xsl:apply-templates mode="pure" select="*[6]"/>
 126      </m:apply>
 127     </xsl:when>
 128     <!-- <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1"> -->
 129     <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">
 130      <m:apply helm:xref="{@id}">
 131       <m:csymbol>thread</m:csymbol>
 132       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 133       <m:apply>
 134        <m:csymbol>app</m:csymbol>
 135        <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 136       </m:apply>
 137       <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')]"/>
 138      </m:apply>
 139     </xsl:when>
 140     <xsl:otherwise>
 141      <m:apply helm:xref="{@id}">
 142       <m:csymbol>proof</m:csymbol>
 143       <xsl:apply-templates select="." mode="pure"/>
 144       <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
 145       <xsl:apply-templates select="//InnerTypes/TYPE[@of=$id]/*" mode="pure"/>
 146      </m:apply>
 147     </xsl:otherwise>
 148    </xsl:choose>
 149 </xsl:template>
 150
 151 <xsl:template match="*" mode="copy-of-no-prop">
 152  <xsl:choose>
 153   <!-- <xsl:when test="@id = //InnerTypes/TYPE/@of"> -->
 154   <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
 155    <m:ci>previous</m:ci>
 156   </xsl:when>
 157   <xsl:otherwise>
 158    <xsl:apply-templates select="." mode="pure"/>
 159   </xsl:otherwise>
 160  </xsl:choose>
 161  <xsl:apply-templates mode="copy-of-no-prop" select="following-sibling::*[1]"/>
 162 </xsl:template>
 163
 164 <xsl:template match="*" mode="thread">
 165   <xsl:choose>
 166    <xsl:when test="name()= 'APPLY' and CONST[
 167  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 168  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 169     <xsl:variable name="id" select="@id"/>
 170      <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 171      <m:apply>
 172       <m:csymbol>rw_step</m:csymbol>
 173       <xsl:apply-templates mode="pure" select="*[3]"/>
 174       <xsl:apply-templates mode="pure" select="*[6]"/>
 175       <xsl:apply-templates mode="pure" select="*[7]"/>
 176      </m:apply>
 177      <xsl:apply-templates mode="thread" select="*[5]"/>
 178    </xsl:when>
 179 <!--**** Patch temporanea, per il problema dei threads ***-->
 180 <xsl:when test="(name()= 'APPLY' and CONST[
 181  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 182  and count(child::*) = 6
 183  and name(*[5])='LAMBDA'
 184  and name(*[5]/target/*[1])='LAMBDA')
 185  or
 186 (name()= 'APPLY' and CONST[
 187  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 188  and count(child::*) = 7)">
 189  <xsl:apply-templates mode="noannot" select="."/>
 190 </xsl:when>
 191 <!--**** Fine Patch temporanea, per il problema dei threads ***-->
 192    <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">
 193        <xsl:variable name="id" select="@id"/>
 194        <m:apply helm:xref="{@id}">
 195         <m:csymbol>thread</m:csymbol>
 196         <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 197         <m:apply>
 198          <m:csymbol>app</m:csymbol>
 199          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 200         </m:apply>
 201         <!-- <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/> -->
 202         <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')]"/>
 203        </m:apply>
 204    </xsl:when>
 205    <xsl:otherwise>
 206     <xsl:apply-templates mode="noannot" select="."/>
 207    </xsl:otherwise>
 208   </xsl:choose>
 209 </xsl:template>
 210
 211
 212 <!-- Basic proof operators -->
 213
 214 <!-- non del tutto soddisfacente, ma .... -->
 215 <xsl:template match="APPLY[CONST[
 216  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 217  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con']]" mode="appflat">
 218     <xsl:choose>
 219      <xsl:when test="count(child::*) > 7">
 220       <xsl:variable name="id" select="@id"/>
 221       <xsl:variable name="ideqp" select="*[7]/@id"/>
 222       <xsl:variable name="idsubp" select="*[5]/@id"/>
 223 <!--
 224       <xsl:variable name="leteqp" select="boolean(//InnerTypes/TYPE[@of=$ideqp])"/>
 225       <xsl:variable name="letsubp" select="boolean(//InnerTypes/TYPE[@of=$idsubp])"/>
 226 -->
 227       <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')])"/>
 228       <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')])"/>
 229       <m:apply helm:xref="{@id}">
 230        <m:csymbol>rewrite_and_apply</m:csymbol>
 231        <m:apply>
 232         <m:csymbol>rw_step</m:csymbol>
 233         <xsl:apply-templates mode="pure" select="*[3]"/>
 234         <xsl:apply-templates mode="pure" select="*[6]"/>
 235         <xsl:choose>
 236          <xsl:when test="$leteqp">
 237           <xsl:choose>
 238            <xsl:when test="$letsubp">
 239             <m:ci>
 240              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h2'"/></xsl:with-param></xsl:call-template>
 241             </m:ci>
 242            </xsl:when>
 243            <xsl:otherwise>
 244             <m:ci>
 245              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 246             </m:ci>
 247            </xsl:otherwise>
 248           </xsl:choose>
 249          </xsl:when>
 250          <xsl:otherwise>
 251           <xsl:apply-templates mode="pure" select="*[7]"/>
 252          </xsl:otherwise>
 253         </xsl:choose>
 254        </m:apply>
 255       <xsl:choose>
 256        <xsl:when test="$letsubp">
 257         <m:ci>
 258          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 259         </m:ci>
 260        </xsl:when>
 261        <xsl:otherwise>
 262         <xsl:apply-templates mode="pure" select="*[5]"/>
 263        </xsl:otherwise>
 264       </xsl:choose>
 265       <xsl:apply-templates mode="flat" select="*[8]">
 266        <xsl:with-param name="n">
 267         <xsl:value-of select="1+$letsubp+$leteqp"/>
 268        </xsl:with-param>
 269       </xsl:apply-templates>
 270      </m:apply>
 271     </xsl:when>
 272     <xsl:otherwise>
 273      <m:apply helm:xref="{@id}">
 274       <m:csymbol>app</m:csymbol>
 275       <xsl:apply-templates mode="flat" select="*[1]"/>
 276      </m:apply>
 277     </xsl:otherwise>
 278    </xsl:choose>
 279 </xsl:template>
 280
 281 <xsl:template match="APPLY[CONST[
 282  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 283     <xsl:choose>
 284      <xsl:when test="count(child::*) > 4">
 285       <m:apply helm:xref="{@id}">
 286        <m:csymbol>app</m:csymbol>
 287        <xsl:apply-templates mode="pure" select="*[1]"/>
 288        <m:ci>*</m:ci>
 289        <m:ci>*</m:ci>
 290        <m:ci>*</m:ci>
 291        <xsl:apply-templates mode="flat" select="*[5]"/>
 292       </m:apply>
 293      </xsl:when>
 294      <xsl:otherwise>
 295       <m:apply helm:xref="{@id}">
 296        <m:csymbol>app</m:csymbol>
 297        <xsl:apply-templates mode="flat" select="*[1]"/>
 298       </m:apply>
 299      </xsl:otherwise>
 300     </xsl:choose>
 301 </xsl:template>
 302
 303
 304 </xsl:stylesheet>
 305
 306
 307
 308
 309
 310