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="@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: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>
  56         <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
  57         <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>
  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>previous</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          <m:csymbol>app</m:csymbol>
 149          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
 150         </m:apply>
 151         <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
 152        </m:apply>
 153    </xsl:when>
 154    <xsl:otherwise>
 155     <xsl:apply-templates mode="noannot" select="."/>
 156    </xsl:otherwise>
 157   </xsl:choose>
 158 </xsl:template>
 159
 160
 161 <!-- Basic proof operators -->
 162
 163 <!-- non del tutto soddisfacente, ma .... -->
 164 <xsl:template match="APPLY[CONST[
 165  attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
 166  attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con']]" mode="appflat">
 167     <xsl:choose>
 168      <xsl:when test="count(child::*) > 7">
 169       <xsl:variable name="id" select="@id"/>
 170       <xsl:variable name="ideqp" select="*[7]/@id"/>
 171       <xsl:variable name="idsubp" select="*[5]/@id"/>
 172       <xsl:variable name="leteqp" select="boolean(//ALLTYPES/TYPE[@id=$ideqp])"/>
 173       <xsl:variable name="letsubp" select="boolean(//ALLTYPES/TYPE[@id=$idsubp])"/>
 174       <m:apply helm:xref="{@id}">
 175        <m:csymbol>rewrite_and_apply</m:csymbol>
 176        <m:apply>
 177         <m:csymbol>rw_step</m:csymbol>
 178         <xsl:apply-templates mode="pure" select="*[3]"/>
 179         <xsl:apply-templates mode="pure" select="*[6]"/>
 180         <xsl:choose>
 181          <xsl:when test="$leteqp">
 182           <xsl:choose>
 183            <xsl:when test="$letsubp">
 184             <m:ci>
 185              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h2'"/></xsl:with-param></xsl:call-template>
 186             </m:ci>
 187            </xsl:when>
 188            <xsl:otherwise>
 189             <m:ci>
 190              <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="'h1'"/></xsl:with-param></xsl:call-template>
 191             </m:ci>
 192            </xsl:otherwise>
 193           </xsl:choose>
 194          </xsl:when>
 195          <xsl:otherwise>
 196           <xsl:apply-templates mode="pure" select="*[7]"/>
 197          </xsl:otherwise>
 198         </xsl:choose>
 199        </m:apply>
 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="'h1'"/></xsl:with-param></xsl:call-template>
 204         </m:ci>
 205        </xsl:when>
 206        <xsl:otherwise>
 207         <xsl:apply-templates mode="pure" select="*[5]"/>
 208        </xsl:otherwise>
 209       </xsl:choose>
 210       <xsl:apply-templates mode="flat" select="*[8]">
 211        <xsl:with-param name="n">
 212         <xsl:value-of select="1+$letsubp+$leteqp"/>
 213        </xsl:with-param>
 214       </xsl:apply-templates>
 215      </m:apply>
 216     </xsl:when>
 217     <xsl:otherwise>
 218      <m:apply helm:xref="{@id}">
 219       <m:csymbol>app</m:csymbol>
 220       <xsl:apply-templates mode="flat" select="*[1]"/>
 221      </m:apply>
 222     </xsl:otherwise>
 223    </xsl:choose>
 224 </xsl:template>
 225
 226 <xsl:template match="APPLY[CONST[
 227  attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']]" mode="appflat">
 228     <xsl:choose>
 229      <xsl:when test="count(child::*) > 4">
 230       <m:apply helm:xref="{@id}">
 231        <m:csymbol>app</m:csymbol>
 232        <xsl:apply-templates mode="pure" select="*[1]"/>
 233        <m:ci>*</m:ci>
 234        <m:ci>*</m:ci>
 235        <m:ci>*</m:ci>
 236        <xsl:apply-templates mode="flat" select="*[5]"/>
 237       </m:apply>
 238      </xsl:when>
 239      <xsl:otherwise>
 240       <m:apply helm:xref="{@id}">
 241        <m:csymbol>app</m:csymbol>
 242        <xsl:apply-templates mode="flat" select="*[1]"/>
 243       </m:apply>
 244      </xsl:otherwise>
 245     </xsl:choose>
 246 </xsl:template>
 247
 248
 249 </xsl:stylesheet>
 250
 251
 252
 253
 254
 255