helm/nuprl_stylesheets/nuprl_abstract.xsl

   1 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
   2                               xmlns:m="http://www.w3.org/1998/Math/MathML">
   3
   4
   5 <xsl:template match="term">
   6   <xsl:choose>
   7
   8   <xsl:when test="@opid=&quot;le&quot;">
   9     <m:apply>
  10       <m:leq definitionURL="{@uri}"/>
  11         <xsl:apply-templates select="*"/>
  12     </m:apply>
  13   </xsl:when>
  14
  15   <xsl:when test="string(@opid)=&quot;exists&quot;">
  16     <m:apply>
  17       <m:exists definitionURL="{@uri}"/>
  18       <m:bvar>
  19         <m:ci>
  20           <xsl:value-of select="binder[1]/@var"/>
  21         </m:ci>
  22       </m:bvar>
  23       <m:condition>
  24         <xsl:apply-templates select="*[1]"/>
  25       </m:condition>
  26       <xsl:apply-templates select="*[3]"/>
  27     </m:apply>
  28   </xsl:when>
  29
  30   <xsl:when test="string(@opid)=&quot;all&quot;">
  31     <m:apply>
  32       <m:csymbol definitionURL="{@uri}">forall</m:csymbol>
  33       <m:bvar>
  34         <m:ci>
  35           <xsl:value-of select="binder[1]/@var"/>
  36         </m:ci>
  37         <m:type>
  38           <xsl:apply-templates select="*[1]"/>
  39         </m:type>
  40       </m:bvar>
  41       <xsl:apply-templates select="*[3]"/>
  42     </m:apply>
  43   </xsl:when>
  44
  45   <xsl:when test="string(@opid)=&quot;and&quot;">
  46     <m:apply>
  47       <m:and definitionURL="{@uri}"/>
  48       <xsl:apply-templates select="*[1]"/>
  49       <xsl:apply-templates select="*[2]"/>
  50     </m:apply>
  51   </xsl:when>
  52
  53   <xsl:when test="string(@opid)=&quot;or&quot;">
  54     <m:apply>
  55       <m:or definitionURL="{@uri}"/>
  56       <xsl:apply-templates select="*[1]"/>
  57       <xsl:apply-templates select="*[2]"/>
  58     </m:apply>
  59   </xsl:when>
  60
  61   <xsl:when test="string(@opid)=&quot;member&quot;">
  62     <m:apply>
  63       <m:in definitionURL="{@uri}"/>
  64       <xsl:apply-templates select="*[2]"/>
  65       <xsl:apply-templates select="*[1]"/>
  66     </m:apply>
  67   </xsl:when>
  68
  69   <xsl:when test="string(@opid)=&quot;implies&quot;">
  70     <m:apply>
  71       <m:implies definitionURL="{@uri}"/>
  72       <xsl:apply-templates select="*[1]"/>
  73       <xsl:apply-templates select="*[2]"/>
  74     </m:apply>
  75   </xsl:when>
  76
  77   <xsl:when test="string(@opid)=&quot;not&quot;">
  78     <m:apply>
  79       <m:not definitionURL="{@uri}"/>
  80       <xsl:apply-templates select="*[1]"/>
  81     </m:apply>
  82   </xsl:when>
  83
  84   <xsl:when test="string(@opid)=&quot;nat&quot;">
  85     <m:naturalnumbers definitionURL="{@uri}"/>
  86   </xsl:when>
  87
  88   <xsl:when test="string(@opid)=&quot;so_lambda&quot;">
  89     <m:apply>
  90       <m:csymbol definitionURL="{@uri}">so_lambda</m:csymbol>
  91       <xsl:choose>
  92       <xsl:when test="*[1]=so_variable">
  93         <m:apply>
  94         <m:ci>so_variable</m:ci>
  95         <m:ci>
  96           <xsl:value-of select="so_variable/@var"/>
  97         </m:ci>
  98         </m:apply>
  99         <!--<xsl:apply-templates select="*[2]"/>
 100         <xsl:apply-templates select="*[3]"/>-->
 101         <xsl:apply-templates/>
 102       </xsl:when>
 103       <xsl:otherwise>
 104         <xsl:apply-templates select="*[1]"/>
 105         <xsl:apply-templates select="*[2]"/>
 106       </xsl:otherwise>
 107       </xsl:choose>
 108     </m:apply>
 109   </xsl:when>
 110
 111   <xsl:when test="string(@opid)=&quot;so_apply&quot;">
 112     <m:apply>
 113       <m:csymbol definitionURL="{@uri}">so_apply</m:csymbol>
 114       <xsl:apply-templates select="*[1]"/>
 115       <xsl:apply-templates select="*[2]"/>
 116     </m:apply>
 117   </xsl:when>
 118
 119   <xsl:when test="string(@opid)=&quot;gcd_p&quot;">
 120     <m:apply>
 121       <m:ci definitionURL="{@uri}">gcd_p</m:ci>
 122       <xsl:apply-templates/>
 123     </m:apply>
 124   </xsl:when>
 125
 126   <xsl:when test="string(@opid)=&quot;decidable&quot;">
 127     <m:apply>
 128       <m:ci definitionURL="{@uri}">decidable</m:ci>
 129       <xsl:apply-templates/>
 130     </m:apply>
 131   </xsl:when>
 132
 133   <xsl:when test="string(@opid)=&quot;int_seg&quot;">
 134     <m:interval definitionURL="{@uri}">
 135       <xsl:apply-templates select="*[1]"/>
 136       <xsl:apply-templates select="*[2]"/>
 137     </m:interval>
 138   </xsl:when>
 139   <xsl:when test="string(@opid)=&quot;ge&quot;">
 140     <m:apply>
 141       <m:geq definitionURL="{@uri}"/>
 142       <xsl:apply-templates select="*[1]"/>
 143       <xsl:apply-templates select="*[2]"/>
 144     </m:apply>
 145   </xsl:when>
 146
 147   <xsl:when test="string(@opid)=&quot;false&quot;">
 148     <m:false definitionURL="{@uri}"/>
 149   </xsl:when>
 150
 151   <xsl:when test="string(@opid)=&quot;true&quot;">
 152     <m:true definitionURL="{@uri}"/>
 153   </xsl:when>
 154
 155     <!-- ALTRE ASTRAZIONI -->
 156   <xsl:otherwise>
 157     <m:apply>
 158      <m:csymbol>app</m:csymbol>
 159      <m:ci definitionURL="{@uri}">
 160        <xsl:value-of select="@opid"/>
 161      </m:ci>
 162      <xsl:apply-templates/>
 163     </m:apply>
 164   </xsl:otherwise>
 165
 166   </xsl:choose>
 167
 168 </xsl:template>
 169
 170 </xsl:stylesheet>