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       <xsl:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
  49        <m:apply helm:xref="{@id}">
  50         <m:csymbol>thread</m:csymbol>
  51         <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
  52         <m:apply>
  53          <m:csymbol>app</m:csymbol>
  54          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
  55         </m:apply>
  56         <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
  57        </m:apply>
  58       </xsl:when>
  59       <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
  60       <xsl:when test="name()= 'APPLY' and CONST[
  61  attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']
  62  and count(child::*) = 6">
  63        <m:apply helm:xref="{@id}">
  64         <m:csymbol>and_ind</m:csymbol>
  65         <xsl:apply-templates mode="noannot" select="*[6]"/>
  66         <m:ci><xsl:value-of select="*[5]/target/@binder"/></m:ci>
  67         <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
  68         <m:ci><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></m:ci>
  69         <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
  70         <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
  71        </m:apply>
  72       </xsl:when>
  73       <xsl:when test="name()= 'APPLY' and CONST[
  74  attribute::uri='cic:/coq/INIT/Logic/Disjunction/or_ind.con']
  75  and count(child::*) = 7">
  76        <m:apply helm:xref="{@id}">
  77         <m:csymbol>or_ind</m:csymbol>
  78         <xsl:apply-templates mode="noannot" select="*[7]"/>
  79         <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
  80         <xsl:apply-templates mode="pure" select="*[5]"/>
  81         <xsl:apply-templates mode="pure" select="*[6]"/>
  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    <xsl:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
 133        <m:apply helm:xref="{@id}">
 134         <m:csymbol>thread</m:csymbol>
 135         <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
 136         <m:apply>
 137          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 138         </m:apply>
 139         <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
 140        </m:apply>
 141    </xsl:when>
 142    <xsl:otherwise>
 143     <xsl:apply-templates mode="noannot" select="."/>
 144    </xsl:otherwise>
 145   </xsl:choose>
 146 </xsl:template>
 147
 148
 149 <!-- Basic proof operators -->
 150
 151 <!-- non del tutto soddisfacente, ma .... -->
 152 <xsl:template match="APPLY[CONST[
 153  attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
 154  attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con']]" mode="appflat">
 155     <xsl:choose>
 156      <xsl:when test="count(child::*) > 7">
 157       <xsl:variable name="id" select="@id"/>
 158       <xsl:variable name="ideqp" select="*[7]/@id"/>
 159       <xsl:variable name="idsubp" select="*[5]/@id"/>
 160       <xsl:variable name="leteqp" select="boolean(//ALLTYPES/TYPE[@id=$ideqp])"/>
 161       <xsl:variable name="letsubp" select="boolean(//ALLTYPES/TYPE[@id=$idsubp])"/>
 162       <m:apply helm:xref="{@id}">
 163        <m:csymbol>rewrite_and_apply</m:csymbol>
 164        <m:apply>
 165         <m:csymbol>rw_step</m:csymbol>
 166         <xsl:apply-templates mode="pure" select="*[3]"/>
 167         <xsl:apply-templates mode="pure" select="*[6]"/>
 168         <xsl:choose>
 169          <xsl:when test="$leteqp">
 170           <xsl:choose>
 171            <xsl:when test="$letsubp">
 172             <m:ci>
 173              <xsl:value-of select="'h2'"/>
 174             </m:ci>
 175            </xsl:when>
 176            <xsl:otherwise>
 177             <m:ci>
 178              <xsl:value-of select="'h1'"/>
 179             </m:ci>
 180            </xsl:otherwise>
 181           </xsl:choose>
 182          </xsl:when>
 183          <xsl:otherwise>
 184           <xsl:apply-templates mode="pure" select="*[7]"/>
 185          </xsl:otherwise>
 186         </xsl:choose>
 187        </m:apply>
 188       <xsl:choose>
 189        <xsl:when test="$letsubp">
 190         <m:ci>
 191          <xsl:value-of select="'h1'"/>
 192         </m:ci>
 193        </xsl:when>
 194        <xsl:otherwise>
 195         <xsl:apply-templates mode="pure" select="*[5]"/>
 196        </xsl:otherwise>
 197       </xsl:choose>
 198       <xsl:apply-templates mode="flat" select="*[8]">
 199        <xsl:with-param name="n">
 200         <xsl:value-of select="1+$letsubp+$leteqp"/>
 201        </xsl:with-param>
 202       </xsl:apply-templates>
 203      </m:apply>
 204     </xsl:when>
 205     <xsl:otherwise>
 206      <m:apply helm:xref="{@id}">
 207       <m:csymbol>app</m:csymbol>
 208       <xsl:apply-templates mode="flat" select="*[1]"/>
 209      </m:apply>
 210     </xsl:otherwise>
 211    </xsl:choose>
 212 </xsl:template>
 213
 214 <xsl:template match="APPLY[CONST[
 215  attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']]" mode="appflat">
 216     <xsl:choose>
 217      <xsl:when test="count(child::*) > 4">
 218       <m:apply helm:xref="{@id}">
 219        <m:csymbol>app</m:csymbol>
 220        <xsl:apply-templates mode="pure" select="*[1]"/>
 221        <m:ci>*</m:ci>
 222        <m:ci>*</m:ci>
 223        <m:ci>*</m:ci>
 224        <xsl:apply-templates mode="flat" select="*[5]"/>
 225       </m:apply>
 226      </xsl:when>
 227      <xsl:otherwise>
 228       <m:apply helm:xref="{@id}">
 229        <m:csymbol>app</m:csymbol>
 230        <xsl:apply-templates mode="flat" select="*[1]"/>
 231       </m:apply>
 232      </xsl:otherwise>
 233     </xsl:choose>
 234 </xsl:template>
 235
 236
 237 </xsl:stylesheet>
 238
 239
 240
 241
 242
 243