helm/style/style_prima_del_linguaggio_naturale/basic.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 <!-- AND -->
  22
  23 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/Conjunction/and.ind'] and (count(child::*) = 3)]" mode="noannot">
  24     <m:apply helm:xref="{@id}">
  25     <m:and definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
  26      <xsl:apply-templates select="*[2]" mode="noannot"/>
  27      <xsl:apply-templates select="*[3]" mode="noannot"/>
  28     </m:apply>
  29 </xsl:template>
  30
  31 <!-- OR -->
  32
  33 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/Disjunction/or.ind'] and (count(child::*) = 3)]" mode="noannot">
  34     <m:apply helm:xref="{@id}">
  35     <m:or definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
  36      <xsl:apply-templates select="*[2]" mode="noannot"/>
  37      <xsl:apply-templates select="*[3]" mode="noannot"/>
  38     </m:apply>
  39 </xsl:template>
  40
  41 <!-- NOT -->
  42
  43 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/not.con'] and (count(child::*) = 2)]" mode="noannot">
  44     <m:apply helm:xref="{@id}">
  45     <m:not definitionURL="{CONST/@uri}" helm:xref="{MUTIND/@id}"/>
  46      <xsl:apply-templates select="*[2]" mode="noannot"/>
  47     </m:apply>
  48 </xsl:template>
  49
  50 <!-- IFF -->
  51 <!--
  52 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/Equivalence/iff.ind'] and (count(child::*) = 3)]" mode="noannot">
  53     <m:apply helm:xref="{@id}">
  54     <m:iff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
  55      <xsl:apply-templates select="*[2]" mode="noannot"/>
  56      <xsl:apply-templates select="*[3]" mode="noannot"/>
  57     </m:apply>
  58 </xsl:template>
  59 -->
  60
  61 <!-- EXISTS -->
  62
  63 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/First_order_quantifiers/ex.ind' or attribute::uri='cic:/coq/INIT/Logic_Type/exT.ind'] and (count(child::*) = 3)]" mode="noannot">
  64     <m:apply helm:xref="{@id}">
  65      <m:exists definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
  66      <xsl:choose>
  67       <xsl:when test="name(*[3]) = 'LAMBDA'">
  68        <m:bvar>
  69         <m:ci><xsl:value-of select="LAMBDA/target/@binder"/></m:ci>
  70        </m:bvar>
  71        <xsl:apply-templates select="LAMBDA/target" mode="noannot"/>
  72       </xsl:when>
  73       <xsl:otherwise>
  74        <m:bvar>
  75         <m:ci>$x</m:ci>
  76        </m:bvar>
  77        <m:apply>
  78         <m:csymbol>app</m:csymbol>
  79         <xsl:apply-templates select="*[3]" mode="noannot"/>
  80         <m:ci>$x</m:ci>
  81        </m:apply>
  82       </xsl:otherwise>
  83      </xsl:choose>
  84     </m:apply>
  85 </xsl:template>
  86
  87 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/First_order_quantifiers/ex2.ind' or attribute::uri='cic:/coq/INIT/Logic_Type/exT2.ind'] and (count(child::*) = 4)]" mode="noannot">
  88     <m:apply helm:xref="{@id}">
  89     <m:exists definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
  90      <xsl:choose>
  91       <xsl:when test="name(*[3]) = 'LAMBDA'">
  92        <xsl:variable name="bvarname" select="*[3]/target/@binder"/>
  93        <m:bvar>
  94         <m:ci><xsl:value-of select="$bvarname"/></m:ci>
  95        </m:bvar>
  96        <m:condition>
  97         <xsl:apply-templates select="LAMBDA[1]/target" mode="noannot"/>
  98        </m:condition>
  99        <xsl:choose>
 100         <xsl:when test="(name(*[4]) = 'LAMBDA') and
 101            ($bvarname = *[4]/target/@binder)">
 102          <xsl:apply-templates select="LAMBDA[2]/target" mode="noannot"/>
 103         </xsl:when>
 104         <xsl:otherwise>
 105          <m:apply>
 106           <m:csymbol>app</m:csymbol>
 107           <xsl:apply-templates select="*[4]" mode="noannot"/>
 108           <m:ci><xsl:value-of select="$bvarname"/></m:ci>
 109          </m:apply>
 110         </xsl:otherwise>
 111        </xsl:choose>
 112       </xsl:when>
 113       <xsl:otherwise>
 114        <xsl:choose>
 115         <xsl:when test="name(*[4]) = 'LAMBDA'">
 116          <xsl:variable name="bvarname" select="*[4]/target/@binder"/>
 117          <m:bvar>
 118           <m:ci><xsl:value-of select="$bvarname"/></m:ci>
 119          </m:bvar>
 120          <m:condition>
 121           <m:apply>
 122            <m:csymbol>app</m:csymbol>
 123            <xsl:apply-templates select="*[3]" mode="noannot"/>
 124            <m:ci><xsl:value-of select="$bvarname"/></m:ci>
 125           </m:apply>
 126          </m:condition>
 127          <xsl:apply-templates select="*[4]/target" mode="noannot"/>
 128         </xsl:when>
 129         <xsl:otherwise>
 130          <m:bvar>
 131           <m:ci>x</m:ci>
 132          </m:bvar>
 133          <m:condition>
 134           <m:apply>
 135            <m:csymbol>app</m:csymbol>
 136            <xsl:apply-templates select="*[3]" mode="noannot"/>
 137            <m:ci>x</m:ci>
 138           </m:apply>
 139          </m:condition>
 140          <m:apply>
 141           <m:csymbol>app</m:csymbol>
 142           <xsl:apply-templates select="*[4]" mode="noannot"/>
 143           <m:ci>x</m:ci>
 144          </m:apply>
 145         </xsl:otherwise>
 146        </xsl:choose>
 147       </xsl:otherwise>
 148      </xsl:choose>
 149     </m:apply>
 150 </xsl:template>
 151
 152 <!-- EQUALITY -->
 153
 154 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/Equality/eq.ind'] and (count(child::*) = 4)]" mode="noannot">
 155     <m:apply helm:xref="{@id}">
 156     <m:eq definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 157      <xsl:apply-templates select="*[3]" mode="noannot"/>
 158      <xsl:apply-templates select="*[4]" mode="noannot"/>
 159     </m:apply>
 160 </xsl:template>
 161
 162
 163 <!-- TYPE EQUALITY -->
 164
 165 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic_Type/eqT.ind'] and (count(child::*) = 4)]" mode="noannot">
 166     <m:apply helm:xref="{@id}">
 167     <m:eq definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 168      <xsl:apply-templates select="*[3]" mode="noannot"/>
 169      <xsl:apply-templates select="*[4]" mode="noannot"/>
 170     </m:apply>
 171 </xsl:template>
 172
 173 <!-- NOT-EQ -->
 174 <!-- NOT and EQ have no parameters -->
 175 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/not.con']
 176 and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/Equality/eq.ind']]]" mode="noannot">
 177     <xsl:choose>
 178      <xsl:when test="count(APPLY/child::*) = 4">
 179       <m:apply helm:xref="{@id}">
 180        <m:neq/>
 181        <xsl:apply-templates select="*[2]/*[3]" mode="noannot"/>
 182        <xsl:apply-templates select="*[2]/*[4]" mode="set"/>
 183       </m:apply>
 184      </xsl:when>
 185      <xsl:otherwise>
 186       <xsl:apply-imports/>
 187      </xsl:otherwise>
 188     </xsl:choose>
 189 </xsl:template>
 190
 191 <!-- NOT-EQT -->
 192 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/not.con']
 193 and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic_Type/eqT.ind']]]" mode="noannot">
 194     <xsl:choose>
 195      <xsl:when test="count(APPLY/child::*) = 4">
 196       <m:apply helm:xref="{@id}">
 197        <m:neq/>
 198        <xsl:apply-templates select="*[2]/*[3]" mode="noannot"/>
 199        <xsl:apply-templates select="*[2]/*[4]" mode="set"/>
 200       </m:apply>
 201      </xsl:when>
 202      <xsl:otherwise>
 203       <xsl:apply-imports/>
 204      </xsl:otherwise>
 205     </xsl:choose>
 206 </xsl:template>
 207
 208 <!-- ************************ DATATYPES ******************************* -->
 209
 210 <!-- no datatypes in MathML content -->
 211
 212
 213 <!-- *************************** PEANO ********************************* -->
 214
 215 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Peano/le.ind'] and (count(child::*) = 3)]" mode="noannot">
 216     <m:apply helm:xref="{@id}">
 217     <m:leq definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 218      <xsl:apply-templates select="*[2]" mode="noannot"/>
 219      <xsl:apply-templates select="*[3]" mode="noannot"/>
 220     </m:apply>
 221 </xsl:template>
 222
 223 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Peano/lt.con'] and (count(child::*) = 3)]" mode="noannot">
 224     <m:apply helm:xref="{@id}">
 225     <m:lt definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 226      <xsl:apply-templates select="*[2]" mode="noannot"/>
 227      <xsl:apply-templates select="*[3]" mode="noannot"/>
 228     </m:apply>
 229 </xsl:template>
 230
 231 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Peano/ge.con'] and (count(child::*) = 3)]" mode="noannot">
 232     <m:apply helm:xref="{@id}">
 233     <m:geq definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 234      <xsl:apply-templates select="*[2]" mode="noannot"/>
 235      <xsl:apply-templates select="*[3]" mode="noannot"/>
 236     </m:apply>
 237 </xsl:template>
 238
 239 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Peano/gt.con'] and (count(child::*) = 3)]" mode="noannot">
 240     <m:apply helm:xref="{@id}">
 241     <m:gt definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 242      <xsl:apply-templates select="*[2]" mode="noannot"/>
 243      <xsl:apply-templates select="*[3]" mode="noannot"/>
 244     </m:apply>
 245 </xsl:template>
 246
 247 </xsl:stylesheet>
 248
 249
 250
 251
 252
 253