helm/style/proofs.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>thread</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="thread" 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:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
  74        <m:apply helm:xref="{@id}">
  75         <m:csymbol>thread</m:csymbol>
  76         <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
  77         <m:apply>
  78          <m:csymbol>app</m:csymbol>
  79          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
  80         </m:apply>
  81         <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
  82        </m:apply>
  83       </xsl:when>
  84       <xsl:otherwise>
  85        <m:apply helm:xref="{@id}">
  86         <m:csymbol>proof</m:csymbol>
  87         <xsl:apply-templates select="." mode="pure"/>
  88         <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
  89         <xsl:apply-templates select="//ALLTYPES/TYPE[@id=$id]" mode="pure"/>
  90        </m:apply>
  91       </xsl:otherwise>
  92      </xsl:choose>
  93      </xsl:when>
  94      <xsl:otherwise>
  95       <xsl:apply-templates select="." mode="pure"/>
  96      </xsl:otherwise>
  97     </xsl:choose>
  98    </xsl:when>
  99    <xsl:otherwise>
 100     <xsl:apply-templates select="." mode="pure"/>
 101    </xsl:otherwise>
 102   </xsl:choose>
 103 </xsl:template>
 104
 105 <xsl:template match="*" mode="copy-of-no-prop">
 106  <xsl:choose>
 107   <xsl:when test="@id = //ALLTYPES/TYPE/@id">
 108    <m:ci>prev</m:ci>
 109   </xsl:when>
 110   <xsl:otherwise>
 111    <xsl:apply-templates select="." mode="pure"/>
 112   </xsl:otherwise>
 113  </xsl:choose>
 114  <xsl:apply-templates mode="copy-of-no-prop" select="following-sibling::*[1]"/>
 115 </xsl:template>
 116
 117 <xsl:template match="*" mode="thread">
 118   <xsl:choose>
 119    <xsl:when test="name()= 'APPLY' and CONST[
 120  attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
 121  attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 122     <xsl:variable name="id" select="@id"/>
 123      <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
 124      <m:apply>
 125       <m:csymbol>rw_step</m:csymbol>
 126       <xsl:apply-templates mode="pure" select="*[3]"/>
 127       <xsl:apply-templates mode="pure" select="*[6]"/>
 128       <xsl:apply-templates mode="pure" select="*[7]"/>
 129      </m:apply>
 130      <xsl:apply-templates mode="thread" select="*[5]"/>
 131    </xsl:when>
 132 <!--**** Patch temporanea, per il problema dei threads ***-->
 133 <xsl:when test="(name()= 'APPLY' and CONST[
 134  attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']
 135  and count(child::*) = 6) or
 136 (name()= 'APPLY' and CONST[
 137  attribute::uri='cic:/coq/INIT/Logic/Disjunction/or_ind.con']
 138  and count(child::*) = 7)">
 139  <xsl:apply-templates mode="noannot" select="."/>
 140 </xsl:when>
 141 <!--**** Fine Patch temporanea, per il problema dei threads ***-->
 142    <xsl:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
 143        <xsl:variable name="id" select="@id"/>
 144        <m:apply helm:xref="{@id}">
 145         <m:csymbol>thread</m:csymbol>
 146         <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
 147         <m:apply>
 148          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 149         </m:apply>
 150         <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
 151        </m:apply>
 152    </xsl:when>
 153    <xsl:otherwise>
 154     <xsl:apply-templates mode="noannot" select="."/>
 155    </xsl:otherwise>
 156   </xsl:choose>
 157 </xsl:template>
 158
 159
 160 <!-- Basic proof operators -->
 161
 162 <!-- non del tutto soddisfacente, ma .... -->
 163 <xsl:template match="APPLY[CONST[
 164  attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
 165  attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con']]" mode="appflat">
 166     <xsl:choose>
 167      <xsl:when test="count(child::*) > 7">
 168       <xsl:variable name="id" select="@id"/>
 169       <xsl:variable name="ideqp" select="*[7]/@id"/>
 170       <xsl:variable name="idsubp" select="*[5]/@id"/>
 171       <xsl:variable name="leteqp" select="boolean(//ALLTYPES/TYPE[@id=$ideqp])"/>
 172       <xsl:variable name="letsubp" select="boolean(//ALLTYPES/TYPE[@id=$idsubp])"/>
 173       <m:apply helm:xref="{@id}">
 174        <m:csymbol>rewrite_and_apply</m:csymbol>
 175        <m:apply>
 176         <m:csymbol>rw_step</m:csymbol>
 177         <xsl:apply-templates mode="pure" select="*[3]"/>
 178         <xsl:apply-templates mode="pure" select="*[6]"/>
 179         <xsl:choose>
 180          <xsl:when test="$leteqp">
 181           <xsl:choose>
 182            <xsl:when test="$letsubp">
 183             <m:ci>
 184              <xsl:value-of select="'h2'"/>
 185             </m:ci>
 186            </xsl:when>
 187            <xsl:otherwise>
 188             <m:ci>
 189              <xsl:value-of select="'h1'"/>
 190             </m:ci>
 191            </xsl:otherwise>
 192           </xsl:choose>
 193          </xsl:when>
 194          <xsl:otherwise>
 195           <xsl:apply-templates mode="pure" select="*[7]"/>
 196          </xsl:otherwise>
 197         </xsl:choose>
 198        </m:apply>
 199       <xsl:choose>
 200        <xsl:when test="$letsubp">
 201         <m:ci>
 202          <xsl:value-of select="'h1'"/>
 203         </m:ci>
 204        </xsl:when>
 205        <xsl:otherwise>
 206         <xsl:apply-templates mode="pure" select="*[5]"/>
 207        </xsl:otherwise>
 208       </xsl:choose>
 209       <xsl:apply-templates mode="flat" select="*[8]">
 210        <xsl:with-param name="n">
 211         <xsl:value-of select="1+$letsubp+$leteqp"/>
 212        </xsl:with-param>
 213       </xsl:apply-templates>
 214      </m:apply>
 215     </xsl:when>
 216     <xsl:otherwise>
 217      <m:apply helm:xref="{@id}">
 218       <m:csymbol>app</m:csymbol>
 219       <xsl:apply-templates mode="flat" select="*[1]"/>
 220      </m:apply>
 221     </xsl:otherwise>
 222    </xsl:choose>
 223 </xsl:template>
 224
 225 <xsl:template match="APPLY[CONST[
 226  attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']]" mode="appflat">
 227     <xsl:choose>
 228      <xsl:when test="count(child::*) > 4">
 229       <m:apply helm:xref="{@id}">
 230        <m:csymbol>app</m:csymbol>
 231        <xsl:apply-templates mode="pure" select="*[1]"/>
 232        <m:ci>*</m:ci>
 233        <m:ci>*</m:ci>
 234        <m:ci>*</m:ci>
 235        <xsl:apply-templates mode="flat" select="*[5]"/>
 236       </m:apply>
 237      </xsl:when>
 238      <xsl:otherwise>
 239       <m:apply helm:xref="{@id}">
 240        <m:csymbol>app</m:csymbol>
 241        <xsl:apply-templates mode="flat" select="*[1]"/>
 242       </m:apply>
 243      </xsl:otherwise>
 244     </xsl:choose>
 245 </xsl:template>
 246
 247
 248 </xsl:stylesheet>
 249
 250
 251
 252
 253
 254