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