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