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     <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">
 103      <m:apply helm:xref="{@id}">
 104       <m:csymbol>thread</m:csymbol>
 105       <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 106       <m:apply>
 107        <m:csymbol>app</m:csymbol>
 108        <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 109       </m:apply>
 110       <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')]"/>
 111      </m:apply>
 112     </xsl:when>
 113     <xsl:otherwise>
 114      <m:apply helm:xref="{@id}">
 115       <m:csymbol>proof</m:csymbol>
 116       <xsl:apply-templates select="." mode="pure"/>
 117       <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
 118       <xsl:apply-templates select="//InnerTypes/TYPE[@of=$id]/*" mode="pure"/>
 119      </m:apply>
 120     </xsl:otherwise>
 121    </xsl:choose>
 122 </xsl:template>
 123
 124 <xsl:template match="*" mode="copy-of-no-prop">
 125  <xsl:choose>
 126   <!-- <xsl:when test="@id = //InnerTypes/TYPE/@of"> -->
 127   <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
 128    <m:ci>previous</m:ci>
 129   </xsl:when>
 130   <xsl:otherwise>
 131    <xsl:apply-templates select="." mode="pure"/>
 132   </xsl:otherwise>
 133  </xsl:choose>
 134  <xsl:apply-templates mode="copy-of-no-prop" select="following-sibling::*[1]"/>
 135 </xsl:template>
 136
 137 <xsl:template match="*" mode="thread">
 138   <xsl:choose>
 139    <xsl:when test="name()= 'APPLY' and CONST[
 140  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 141  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 142     <xsl:variable name="id" select="@id"/>
 143      <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 144      <m:apply>
 145       <m:csymbol>rw_step</m:csymbol>
 146       <xsl:apply-templates mode="pure" select="*[3]"/>
 147       <xsl:apply-templates mode="pure" select="*[6]"/>
 148       <xsl:apply-templates mode="pure" select="*[7]"/>
 149      </m:apply>
 150      <xsl:apply-templates mode="thread" select="*[5]"/>
 151    </xsl:when>
 152 <!--**** Patch temporanea, per il problema dei threads ***-->
 153 <xsl:when test="(name()= 'APPLY' and CONST[
 154  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 155  and count(child::*) = 6) or
 156 (name()= 'APPLY' and CONST[
 157  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 158  and count(child::*) = 7)">
 159  <xsl:apply-templates mode="noannot" select="."/>
 160 </xsl:when>
 161 <!--**** Fine Patch temporanea, per il problema dei threads ***-->
 162    <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">
 163        <xsl:variable name="id" select="@id"/>
 164        <m:apply helm:xref="{@id}">
 165         <m:csymbol>thread</m:csymbol>
 166         <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
 167         <m:apply>
 168          <m:csymbol>app</m:csymbol>
 169          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 170         </m:apply>
 171         <!-- <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/> -->
 172         <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')]"/>
 173        </m:apply>
 174    </xsl:when>
 175    <xsl:otherwise>
 176     <xsl:apply-templates mode="noannot" select="."/>
 177    </xsl:otherwise>
 178   </xsl:choose>
 179 </xsl:template>
 180
 181
 182 <!-- Basic proof operators -->
 183
 184 <!-- non del tutto soddisfacente, ma .... -->
 185 <xsl:template match="APPLY[CONST[
 186  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 187  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con']]" mode="appflat">
 188     <xsl:choose>
 189      <xsl:when test="count(child::*) > 7">
 190       <xsl:variable name="id" select="@id"/>
 191       <xsl:variable name="ideqp" select="*[7]/@id"/>
 192       <xsl:variable name="idsubp" select="*[5]/@id"/>
 193 <!--
 194       <xsl:variable name="leteqp" select="boolean(//InnerTypes/TYPE[@of=$ideqp])"/>
 195       <xsl:variable name="letsubp" select="boolean(//InnerTypes/TYPE[@of=$idsubp])"/>
 196 -->
 197       <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')])"/>
 198       <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')])"/>
 199       <m:apply helm:xref="{@id}">
 200        <m:csymbol>rewrite_and_apply</m:csymbol>
 201        <m:apply>
 202         <m:csymbol>rw_step</m:csymbol>
 203         <xsl:apply-templates mode="pure" select="*[3]"/>
 204         <xsl:apply-templates mode="pure" select="*[6]"/>
 205         <xsl:choose>
 206          <xsl:when test="$leteqp">
 207           <xsl:choose>
 208            <xsl:when test="$letsubp">
 209             <m:ci>
 210              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h2'"/></xsl:with-param></xsl:call-template>
 211             </m:ci>
 212            </xsl:when>
 213            <xsl:otherwise>
 214             <m:ci>
 215              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 216             </m:ci>
 217            </xsl:otherwise>
 218           </xsl:choose>
 219          </xsl:when>
 220          <xsl:otherwise>
 221           <xsl:apply-templates mode="pure" select="*[7]"/>
 222          </xsl:otherwise>
 223         </xsl:choose>
 224        </m:apply>
 225       <xsl:choose>
 226        <xsl:when test="$letsubp">
 227         <m:ci>
 228          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 229         </m:ci>
 230        </xsl:when>
 231        <xsl:otherwise>
 232         <xsl:apply-templates mode="pure" select="*[5]"/>
 233        </xsl:otherwise>
 234       </xsl:choose>
 235       <xsl:apply-templates mode="flat" select="*[8]">
 236        <xsl:with-param name="n">
 237         <xsl:value-of select="1+$letsubp+$leteqp"/>
 238        </xsl:with-param>
 239       </xsl:apply-templates>
 240      </m:apply>
 241     </xsl:when>
 242     <xsl:otherwise>
 243      <m:apply helm:xref="{@id}">
 244       <m:csymbol>app</m:csymbol>
 245       <xsl:apply-templates mode="flat" select="*[1]"/>
 246      </m:apply>
 247     </xsl:otherwise>
 248    </xsl:choose>
 249 </xsl:template>
 250
 251 <xsl:template match="APPLY[CONST[
 252  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 253     <xsl:choose>
 254      <xsl:when test="count(child::*) > 4">
 255       <m:apply helm:xref="{@id}">
 256        <m:csymbol>app</m:csymbol>
 257        <xsl:apply-templates mode="pure" select="*[1]"/>
 258        <m:ci>*</m:ci>
 259        <m:ci>*</m:ci>
 260        <m:ci>*</m:ci>
 261        <xsl:apply-templates mode="flat" select="*[5]"/>
 262       </m:apply>
 263      </xsl:when>
 264      <xsl:otherwise>
 265       <m:apply helm:xref="{@id}">
 266        <m:csymbol>app</m:csymbol>
 267        <xsl:apply-templates mode="flat" select="*[1]"/>
 268       </m:apply>
 269      </xsl:otherwise>
 270     </xsl:choose>
 271 </xsl:template>
 272
 273
 274 </xsl:stylesheet>
 275
 276
 277
 278
 279
 280