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/getciconly?uri=</xsl:variable>
  18
  19 <!-- ************************* LOGIC *********************************-->
  20
  21 <!-- Proof objects -->
  22
  23 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
  24
  25 <!-- ALL this elements does not have inner type -->
  26 <xsl:template match="PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
  27 <xsl:apply-templates select="." mode="pure"/>
  28 </xsl:template>
  29
  30 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
  31 <xsl:template match="LAMBDA" mode="noannot">
  32  <xsl:variable name="id" select="@id"/>
  33  <xsl:choose>
  34   <xsl:when test="//InnerTypes and @sort='Prop' and name(../..) != 'LAMBDA'">
  35   <!-- <xsl:when test="@sort='Prop' and //InnerTypes/TYPE[@of=$id]"> -->
  36    <xsl:call-template name="has_inner_type"/>
  37   </xsl:when>
  38   <xsl:otherwise>
  39    <xsl:apply-templates select="." mode="pure"/>
  40   </xsl:otherwise>
  41  </xsl:choose>
  42 </xsl:template>
  43
  44 <!-- ALL this elements have inner type -->
  45 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
  46  <xsl:choose>
  47   <!-- <xsl:when test="//InnerTypes and key('typeid',@id)"> -->
  48   <!-- <xsl:when test="//InnerTypes/TYPE[@of=$id]"> -->
  49   <xsl:when test="//InnerTypes and @sort='Prop'">
  50    <xsl:call-template name="has_inner_type"/>
  51   </xsl:when>
  52   <xsl:otherwise>
  53    <xsl:apply-templates select="." mode="pure"/>
  54   </xsl:otherwise>
  55  </xsl:choose>
  56 </xsl:template>
  57
  58 <xsl:template name="has_inner_type">
  59    <xsl:variable name="id" select="@id"/>
  60    <xsl:choose>
  61     <xsl:when test="name()= 'APPLY' and CONST[
  62  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
  63  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
  64      <m:apply helm:xref="{@id}">
  65       <m:csymbol>thread</m:csymbol>
  66       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
  67       <m:apply>
  68        <m:csymbol>rw_step</m:csymbol>
  69        <xsl:apply-templates mode="pure" select="*[3]"/>
  70        <xsl:apply-templates mode="pure" select="*[6]"/>
  71        <xsl:apply-templates mode="pure" select="*[7]"/>
  72       </m:apply>
  73       <xsl:apply-templates mode="thread" select="*[5]"/>
  74      </m:apply>
  75     </xsl:when>
  76     <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
  77     <xsl:when test="name()= 'APPLY' and CONST[
  78  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
  79  and count(child::*) = 6">
  80      <m:apply helm:xref="{@id}">
  81       <m:csymbol>and_ind</m:csymbol>
  82       <xsl:apply-templates mode="noannot" select="*[6]"/>
  83       <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>
  84       <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
  85       <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>
  86       <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
  87       <xsl:apply-templates mode="noannot" select="*[5]/target/LAMBDA/target/*"/>
  88      </m:apply>
  89     </xsl:when>
  90     <xsl:when test="name()= 'APPLY' and CONST[
  91  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
  92  and count(child::*) = 7">
  93      <m:apply helm:xref="{@id}">
  94       <m:csymbol>or_ind</m:csymbol>
  95       <xsl:apply-templates mode="noannot" select="*[7]"/>
  96       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
  97       <xsl:apply-templates mode="pure" select="*[5]"/>
  98       <xsl:apply-templates mode="pure" select="*[6]"/>
  99      </m:apply>
 100     </xsl:when>
 101     <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1">
 102      <m:apply helm:xref="{@id}">
 103       <m:csymbol>thread</m:csymbol>
 104       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 105       <m:apply>
 106        <m:csymbol>app</m:csymbol>
 107        <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 108       </m:apply>
 109       <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
 110      </m:apply>
 111     </xsl:when>
 112     <xsl:otherwise>
 113      <m:apply helm:xref="{@id}">
 114       <m:csymbol>proof</m:csymbol>
 115       <xsl:apply-templates select="." mode="pure"/>
 116       <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
 117       <xsl:apply-templates select="//InnerTypes/TYPE[@of=$id]/*" mode="pure"/>
 118      </m:apply>
 119     </xsl:otherwise>
 120    </xsl:choose>
 121 </xsl:template>
 122
 123 <xsl:template match="*" mode="copy-of-no-prop">
 124  <xsl:choose>
 125   <xsl:when test="@id = //InnerTypes/TYPE/@of">
 126    <m:ci>previous</m:ci>
 127   </xsl:when>
 128   <xsl:otherwise>
 129    <xsl:apply-templates select="." mode="pure"/>
 130   </xsl:otherwise>
 131  </xsl:choose>
 132  <xsl:apply-templates mode="copy-of-no-prop" select="following-sibling::*[1]"/>
 133 </xsl:template>
 134
 135 <xsl:template match="*" mode="thread">
 136   <xsl:choose>
 137    <xsl:when test="name()= 'APPLY' and CONST[
 138  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 139  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 140     <xsl:variable name="id" select="@id"/>
 141      <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 142      <m:apply>
 143       <m:csymbol>rw_step</m:csymbol>
 144       <xsl:apply-templates mode="pure" select="*[3]"/>
 145       <xsl:apply-templates mode="pure" select="*[6]"/>
 146       <xsl:apply-templates mode="pure" select="*[7]"/>
 147      </m:apply>
 148      <xsl:apply-templates mode="thread" select="*[5]"/>
 149    </xsl:when>
 150 <!--**** Patch temporanea, per il problema dei threads ***-->
 151 <xsl:when test="(name()= 'APPLY' and CONST[
 152  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 153  and count(child::*) = 6) or
 154 (name()= 'APPLY' and CONST[
 155  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 156  and count(child::*) = 7)">
 157  <xsl:apply-templates mode="noannot" select="."/>
 158 </xsl:when>
 159 <!--**** Fine Patch temporanea, per il problema dei threads ***-->
 160    <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">
 161        <xsl:variable name="id" select="@id"/>
 162        <m:apply helm:xref="{@id}">
 163         <m:csymbol>thread</m:csymbol>
 164         <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 165         <m:apply>
 166          <m:csymbol>app</m:csymbol>
 167          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 168         </m:apply>
 169         <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
 170        </m:apply>
 171    </xsl:when>
 172    <xsl:otherwise>
 173     <xsl:apply-templates mode="noannot" select="."/>
 174    </xsl:otherwise>
 175   </xsl:choose>
 176 </xsl:template>
 177
 178
 179 <!-- Basic proof operators -->
 180
 181 <!-- non del tutto soddisfacente, ma .... -->
 182 <xsl:template match="APPLY[CONST[
 183  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 184  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con']]" mode="appflat">
 185     <xsl:choose>
 186      <xsl:when test="count(child::*) > 7">
 187       <xsl:variable name="id" select="@id"/>
 188       <xsl:variable name="ideqp" select="*[7]/@id"/>
 189       <xsl:variable name="idsubp" select="*[5]/@id"/>
 190       <xsl:variable name="leteqp" select="boolean(//InnerTypes/TYPE[@of=$ideqp])"/>
 191       <xsl:variable name="letsubp" select="boolean(//InnerTypes/TYPE[@of=$idsubp])"/>
 192       <m:apply helm:xref="{@id}">
 193        <m:csymbol>rewrite_and_apply</m:csymbol>
 194        <m:apply>
 195         <m:csymbol>rw_step</m:csymbol>
 196         <xsl:apply-templates mode="pure" select="*[3]"/>
 197         <xsl:apply-templates mode="pure" select="*[6]"/>
 198         <xsl:choose>
 199          <xsl:when test="$leteqp">
 200           <xsl:choose>
 201            <xsl:when test="$letsubp">
 202             <m:ci>
 203              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h2'"/></xsl:with-param></xsl:call-template>
 204             </m:ci>
 205            </xsl:when>
 206            <xsl:otherwise>
 207             <m:ci>
 208              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 209             </m:ci>
 210            </xsl:otherwise>
 211           </xsl:choose>
 212          </xsl:when>
 213          <xsl:otherwise>
 214           <xsl:apply-templates mode="pure" select="*[7]"/>
 215          </xsl:otherwise>
 216         </xsl:choose>
 217        </m:apply>
 218       <xsl:choose>
 219        <xsl:when test="$letsubp">
 220         <m:ci>
 221          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 222         </m:ci>
 223        </xsl:when>
 224        <xsl:otherwise>
 225         <xsl:apply-templates mode="pure" select="*[5]"/>
 226        </xsl:otherwise>
 227       </xsl:choose>
 228       <xsl:apply-templates mode="flat" select="*[8]">
 229        <xsl:with-param name="n">
 230         <xsl:value-of select="1+$letsubp+$leteqp"/>
 231        </xsl:with-param>
 232       </xsl:apply-templates>
 233      </m:apply>
 234     </xsl:when>
 235     <xsl:otherwise>
 236      <m:apply helm:xref="{@id}">
 237       <m:csymbol>app</m:csymbol>
 238       <xsl:apply-templates mode="flat" select="*[1]"/>
 239      </m:apply>
 240     </xsl:otherwise>
 241    </xsl:choose>
 242 </xsl:template>
 243
 244 <xsl:template match="APPLY[CONST[
 245  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 246     <xsl:choose>
 247      <xsl:when test="count(child::*) > 4">
 248       <m:apply helm:xref="{@id}">
 249        <m:csymbol>app</m:csymbol>
 250        <xsl:apply-templates mode="pure" select="*[1]"/>
 251        <m:ci>*</m:ci>
 252        <m:ci>*</m:ci>
 253        <m:ci>*</m:ci>
 254        <xsl:apply-templates mode="flat" select="*[5]"/>
 255       </m:apply>
 256      </xsl:when>
 257      <xsl:otherwise>
 258       <m:apply helm:xref="{@id}">
 259        <m:csymbol>app</m:csymbol>
 260        <xsl:apply-templates mode="flat" select="*[1]"/>
 261       </m:apply>
 262      </xsl:otherwise>
 263     </xsl:choose>
 264 </xsl:template>
 265
 266
 267 </xsl:stylesheet>
 268
 269
 270
 271
 272
 273