First commit of the NuPRL stylesheets.

[helm.git] / helm / nuprl_stylesheets / nuprl_abstract.xsl

diff --git a/helm/nuprl_stylesheets/nuprl_abstract.xsl b/helm/nuprl_stylesheets/nuprl_abstract.xsl
new file mode 100644 (file)
index 0000000..fa6d815
--- /dev/null
+++ b/helm/nuprl_stylesheets/nuprl_abstract.xsl
@@ -0,0 +1,170 @@
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+
+<xsl:template match="term">
+  <xsl:choose>
+  
+  <xsl:when test="@opid=&quot;le&quot;">
+    <m:apply>
+      <m:leq definitionURL="{@uri}"/>
+        <xsl:apply-templates select="*"/>
+    </m:apply>
+  </xsl:when>
+ 
+  <xsl:when test="string(@opid)=&quot;exists&quot;">
+    <m:apply>
+      <m:exists definitionURL="{@uri}"/>
+      <m:bvar>
+        <m:ci>
+         <xsl:value-of select="binder[1]/@var"/>
+       </m:ci>
+      </m:bvar>
+      <m:condition>
+        <xsl:apply-templates select="*[1]"/>
+      </m:condition>
+      <xsl:apply-templates select="*[3]"/>
+    </m:apply>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;all&quot;">
+    <m:apply>
+      <m:csymbol definitionURL="{@uri}">forall</m:csymbol>
+      <m:bvar>
+        <m:ci>
+          <xsl:value-of select="binder[1]/@var"/>
+        </m:ci>
+        <m:type>
+          <xsl:apply-templates select="*[1]"/>
+        </m:type>
+      </m:bvar>
+      <xsl:apply-templates select="*[3]"/>
+    </m:apply>
+  </xsl:when>
+
+  <xsl:when test="string(@opid)=&quot;and&quot;">
+    <m:apply>
+      <m:and definitionURL="{@uri}"/>
+      <xsl:apply-templates select="*[1]"/>
+      <xsl:apply-templates select="*[2]"/>
+    </m:apply>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;or&quot;">
+    <m:apply>
+      <m:or definitionURL="{@uri}"/>
+      <xsl:apply-templates select="*[1]"/>
+      <xsl:apply-templates select="*[2]"/>
+    </m:apply>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;member&quot;">
+    <m:apply>
+      <m:in definitionURL="{@uri}"/>
+      <xsl:apply-templates select="*[2]"/>
+      <xsl:apply-templates select="*[1]"/>
+    </m:apply>
+  </xsl:when>
+    
+  <xsl:when test="string(@opid)=&quot;implies&quot;">
+    <m:apply>
+      <m:implies definitionURL="{@uri}"/>
+      <xsl:apply-templates select="*[1]"/>
+      <xsl:apply-templates select="*[2]"/>
+    </m:apply>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;not&quot;">
+    <m:apply>
+      <m:not definitionURL="{@uri}"/>
+      <xsl:apply-templates select="*[1]"/>
+    </m:apply>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;nat&quot;">
+    <m:naturalnumbers definitionURL="{@uri}"/>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;so_lambda&quot;">
+    <m:apply>
+      <m:csymbol definitionURL="{@uri}">so_lambda</m:csymbol>
+      <xsl:choose>
+      <xsl:when test="*[1]=so_variable">
+        <m:apply>
+        <m:ci>so_variable</m:ci>
+        <m:ci>
+          <xsl:value-of select="so_variable/@var"/>
+       </m:ci>
+        </m:apply>
+        <!--<xsl:apply-templates select="*[2]"/>
+        <xsl:apply-templates select="*[3]"/>-->
+        <xsl:apply-templates/>
+      </xsl:when>
+      <xsl:otherwise>
+        <xsl:apply-templates select="*[1]"/>
+        <xsl:apply-templates select="*[2]"/>
+      </xsl:otherwise>
+      </xsl:choose>
+    </m:apply>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;so_apply&quot;">
+    <m:apply>
+      <m:csymbol definitionURL="{@uri}">so_apply</m:csymbol>
+      <xsl:apply-templates select="*[1]"/>
+      <xsl:apply-templates select="*[2]"/>
+    </m:apply>
+  </xsl:when>  
+  
+  <xsl:when test="string(@opid)=&quot;gcd_p&quot;">
+    <m:apply>
+      <m:ci definitionURL="{@uri}">gcd_p</m:ci>
+      <xsl:apply-templates/>
+    </m:apply>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;decidable&quot;">
+    <m:apply>
+      <m:ci definitionURL="{@uri}">decidable</m:ci>
+      <xsl:apply-templates/>
+    </m:apply>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;int_seg&quot;">
+    <m:interval definitionURL="{@uri}">
+      <xsl:apply-templates select="*[1]"/>
+      <xsl:apply-templates select="*[2]"/>
+    </m:interval>
+  </xsl:when>
+  <xsl:when test="string(@opid)=&quot;ge&quot;">
+    <m:apply>
+      <m:geq definitionURL="{@uri}"/>
+      <xsl:apply-templates select="*[1]"/>
+      <xsl:apply-templates select="*[2]"/>
+    </m:apply>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;false&quot;">
+    <m:false definitionURL="{@uri}"/>
+  </xsl:when>
+  
+  <xsl:when test="string(@opid)=&quot;true&quot;">
+    <m:true definitionURL="{@uri}"/>
+  </xsl:when>
+  
+    <!-- ALTRE ASTRAZIONI -->
+  <xsl:otherwise>
+    <m:apply>
+     <m:csymbol>app</m:csymbol>
+     <m:ci definitionURL="{@uri}">
+       <xsl:value-of select="@opid"/>
+     </m:ci>
+     <xsl:apply-templates/>
+    </m:apply>
+  </xsl:otherwise>
+  
+  </xsl:choose>
+  
+</xsl:template>
+
+</xsl:stylesheet>