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