First commit of the NuPRL stylesheets.

[helm.git] / helm / nuprl_stylesheets / nuprl_proof.xsl
diff --git a/helm/nuprl_stylesheets/nuprl_proof.xsl b/helm/nuprl_stylesheets/nuprl_proof.xsl

new file mode 100644 (file)

index 0000000..343cafd
--- /dev/null
+++ b/helm/nuprl_stylesheets/nuprl_proof.xsl
@@ -0,0 +1,74 @@
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML"
+                              xmlns:cn="http://www.......">
+
+
+<xsl:template match="NuPrlProof">
+  <Definition>
+    <Params />
+    <body>
+      <xsl:apply-templates/>
+    </body>
+    <type>
+      <xsl:apply-templates select="node/sequent/conclusion/*[1]"/>
+    </type>
+  </Definition>
+</xsl:template>
+
+<xsl:template match="node">
+  <xsl:element name="Node">
+    <xsl:apply-templates/>
+  </xsl:element>
+</xsl:template>
+
+<xsl:template match="sequent">
+  <xsl:element name="Sequent">
+    <xsl:attribute name="id">
+      <xsl:value-of select="@number"/>
+    </xsl:attribute>
+    <xsl:apply-templates/>
+  </xsl:element>
+</xsl:template>
+
+<xsl:template match="hypothesis">
+  <xsl:element name="Decl">
+    <xsl:if test="@var!=&quot;&quot;">
+      <xsl:attribute name="name">
+        <xsl:value-of select="@var"/>
+      </xsl:attribute>
+    </xsl:if>
+    <xsl:apply-templates/>
+  </xsl:element>
+</xsl:template>
+
+<xsl:template match="conclusion">
+  <xsl:element name="Goal">
+    <xsl:apply-templates/>
+  </xsl:element>
+</xsl:template>
+
+<xsl:template match="ruleinstance">
+  <xsl:element name="Rule">
+    <xsl:apply-templates/>
+  </xsl:element>
+</xsl:template>
+
+<xsl:template match="tacticinstance">
+  <TacticInstance name="{@name}">
+    <xsl:apply-templates select="extra_info"/>
+  </TacticInstance>
+</xsl:template>
+
+<xsl:template match="extra_info">
+ <extra_info>
+  <xsl:copy-of select="*|@*|text()"/>
+ </extra_info>
+</xsl:template>
+
+<xsl:template match="tacticproof">
+  <xsl:element name="TacticProof">
+    <xsl:apply-templates/>
+  </xsl:element>
+</xsl:template>
+
+</xsl:stylesheet>