helm/style/proof31-10-00.xsl

   1 <?xml version="1.0"?>
   2
   3 <!--******************************************************************-->
   4 <!-- Basic Logic                                                      -->
   5 <!-- First draft: April 3 2000                                        -->
   6 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
   7 <!--******************************************************************-->
   8
   9 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  10                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  11                               xmlns:helm="http://www.cs.unibo.it/helm">
  12
  13 <!--******************************************************************-->
  14 <!-- Variable containing the absolute path of the CIC file            -->
  15 <!--******************************************************************-->
  16
  17 <xsl:variable name="absPath">http://localhost:8081/get?url=</xsl:variable>
  18
  19 <!-- ************************* LOGIC *********************************-->
  20
  21 <!-- Proof objects -->
  22
  23 <!-- <xsl:key name="typeid" use="@id" match="TYPE"/> -->
  24
  25 <xsl:template match="LAMBDA|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX" mode="noannot">
  26   <xsl:choose>
  27    <xsl:when test="@id">
  28     <xsl:variable name="id" select="@id"/>
  29     <xsl:choose>
  30      <!-- <xsl:when test="//ALLTYPES and key('typeid',@id)"> -->
  31      <xsl:when test="//ALLTYPES/TYPE[@id=$id]">
  32      <xsl:choose>
  33       <xsl:when test="name()= 'APPLY' and CONST[
  34  attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
  35  attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
  36        <m:apply helm:xref="{@id}">
  37         <m:csymbol>rewrite</m:csymbol>
  38         <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
  39         <m:apply>
  40          <m:csymbol>rw_step</m:csymbol>
  41          <xsl:apply-templates mode="pure" select="*[3]"/>
  42          <xsl:apply-templates mode="pure" select="*[6]"/>
  43          <xsl:apply-templates mode="pure" select="*[7]"/>
  44         </m:apply>
  45         <xsl:apply-templates mode="rewrite" select="*[5]"/>
  46        </m:apply>
  47       </xsl:when>
  48       <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
  49       <xsl:when test="name()= 'APPLY' and CONST[
  50  attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']
  51  and count(child::*) = 6">
  52        <m:apply helm:xref="{@id}">
  53         <m:csymbol>and_ind</m:csymbol>
  54         <xsl:apply-templates mode="noannot" select="*[6]"/>
  55         <m:ci><xsl:value-of select="*[5]/target/@binder"/></m:ci>
  56         <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
  57         <m:ci><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></m:ci>
  58         <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
  59         <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
  60        </m:apply>
  61       </xsl:when>
  62       <xsl:when test="name()= 'APPLY' and CONST[
  63  attribute::uri='cic:/coq/INIT/Logic/Disjunction/or_ind.con']
  64  and count(child::*) = 7">
  65        <m:apply helm:xref="{@id}">
  66         <m:csymbol>or_ind</m:csymbol>
  67         <xsl:apply-templates mode="noannot" select="*[7]"/>
  68         <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
  69         <xsl:apply-templates mode="pure" select="*[5]"/>
  70         <xsl:apply-templates mode="pure" select="*[6]"/>
  71        </m:apply>
  72       </xsl:when>
  73       <xsl:otherwise>
  74        <m:apply helm:xref="{@id}">
  75         <m:csymbol>proof</m:csymbol>
  76         <xsl:apply-templates select="." mode="pure"/>
  77         <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
  78         <xsl:apply-templates select="//ALLTYPES/TYPE[@id=$id]" mode="pure"/>
  79        </m:apply>
  80       </xsl:otherwise>
  81      </xsl:choose>
  82      </xsl:when>
  83      <xsl:otherwise>
  84       <xsl:apply-templates select="." mode="pure"/>
  85      </xsl:otherwise>
  86     </xsl:choose>
  87    </xsl:when>
  88    <xsl:otherwise>
  89     <xsl:apply-templates select="." mode="pure"/>
  90    </xsl:otherwise>
  91   </xsl:choose>
  92 </xsl:template>
  93
  94 <xsl:template match="*" mode="rewrite">
  95   <xsl:choose>
  96    <xsl:when test="name()= 'APPLY' and CONST[
  97  attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
  98  attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
  99     <xsl:variable name="id" select="@id"/>
 100      <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
 101      <m:apply>
 102       <m:csymbol>rw_step</m:csymbol>
 103       <xsl:apply-templates mode="pure" select="*[3]"/>
 104       <xsl:apply-templates mode="pure" select="*[6]"/>
 105       <xsl:apply-templates mode="pure" select="*[7]"/>
 106      </m:apply>
 107      <xsl:apply-templates mode="rewrite" select="*[5]"/>
 108    </xsl:when>
 109    <xsl:otherwise>
 110     <xsl:apply-templates mode="noannot" select="."/>
 111    </xsl:otherwise>
 112   </xsl:choose>
 113 </xsl:template>
 114
 115
 116 <!-- Basic proof operators -->
 117
 118 <!-- non del tutto soddisfacente, ma .... -->
 119 <xsl:template match="APPLY[CONST[
 120  attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
 121  attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con']]" mode="appflat">
 122     <xsl:choose>
 123      <xsl:when test="count(child::*) > 7">
 124       <xsl:variable name="id" select="@id"/>
 125       <xsl:variable name="ideqp" select="*[7]/@id"/>
 126       <xsl:variable name="idsubp" select="*[5]/@id"/>
 127       <xsl:variable name="leteqp" select="boolean(//ALLTYPES/TYPE[@id=$ideqp])"/>
 128       <xsl:variable name="letsubp" select="boolean(//ALLTYPES/TYPE[@id=$idsubp])"/>
 129       <m:apply helm:xref="{@id}">
 130        <m:csymbol>rewrite_and_apply</m:csymbol>
 131        <m:apply>
 132         <m:csymbol>rw_step</m:csymbol>
 133         <xsl:apply-templates mode="pure" select="*[3]"/>
 134         <xsl:apply-templates mode="pure" select="*[6]"/>
 135         <xsl:choose>
 136          <xsl:when test="$leteqp">
 137           <xsl:choose>
 138            <xsl:when test="$letsubp">
 139             <m:ci>
 140              <xsl:value-of select="'h2'"/>
 141             </m:ci>
 142            </xsl:when>
 143            <xsl:otherwise>
 144             <m:ci>
 145              <xsl:value-of select="'h1'"/>
 146             </m:ci>
 147            </xsl:otherwise>
 148           </xsl:choose>
 149          </xsl:when>
 150          <xsl:otherwise>
 151           <xsl:apply-templates mode="pure" select="*[7]"/>
 152          </xsl:otherwise>
 153         </xsl:choose>
 154        </m:apply>
 155       <xsl:choose>
 156        <xsl:when test="$letsubp">
 157         <m:ci>
 158          <xsl:value-of select="'h1'"/>
 159         </m:ci>
 160        </xsl:when>
 161        <xsl:otherwise>
 162         <xsl:apply-templates mode="pure" select="*[5]"/>
 163        </xsl:otherwise>
 164       </xsl:choose>
 165       <xsl:apply-templates mode="flat" select="*[8]">
 166        <xsl:with-param name="n">
 167         <xsl:value-of select="1+$letsubp+$leteqp"/>
 168        </xsl:with-param>
 169       </xsl:apply-templates>
 170      </m:apply>
 171     </xsl:when>
 172     <xsl:otherwise>
 173      <m:apply helm:xref="{@id}">
 174       <m:csymbol>app</m:csymbol>
 175       <xsl:apply-templates mode="flat" select="*[1]"/>
 176      </m:apply>
 177     </xsl:otherwise>
 178    </xsl:choose>
 179 </xsl:template>
 180
 181 <xsl:template match="APPLY[CONST[
 182  attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']]" mode="appflat">
 183     <xsl:choose>
 184      <xsl:when test="count(child::*) > 4">
 185       <m:apply helm:xref="{@id}">
 186        <m:csymbol>app</m:csymbol>
 187        <xsl:apply-templates mode="pure" select="*[1]"/>
 188        <m:ci>*</m:ci>
 189        <m:ci>*</m:ci>
 190        <m:ci>*</m:ci>
 191        <xsl:apply-templates mode="flat" select="*[5]"/>
 192       </m:apply>
 193      </xsl:when>
 194      <xsl:otherwise>
 195       <m:apply helm:xref="{@id}">
 196        <m:csymbol>app</m:csymbol>
 197        <xsl:apply-templates mode="flat" select="*[1]"/>
 198       </m:apply>
 199      </xsl:otherwise>
 200     </xsl:choose>
 201 </xsl:template>
 202
 203
 204 </xsl:stylesheet>
 205
 206
 207
 208
 209
 210