<?xml version="1.0" encoding="utf-8"?>
<!--
    A crude implementation of the untyped lambda calculus.
    Unfortunately, XSLT does not allow for infinite template
    recursion, so this does not work on non-normalizing terms.

    An example term:
    <app>
      <lambda var="x">
        <app>
          <var>x</var>
          <var>x</var>
        </app>
      </lambda>
      <var>y</var>
    </app>
-->
<xsl:stylesheet version="1.0"
                xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
                xmlns:exsl="http://exslt.org/common"
                exclude-result-prefixes="exsl">
  
  <xsl:output method="xml"
              encoding="utf-8"
              indent="yes"
              omit-xml-declaration="yes"/>
  
  <xsl:template match="lambda | var">
    <xsl:copy-of select="."/>
  </xsl:template>
  
  <xsl:template match="app[*[1][self::lambda]]">
    <xsl:variable name="term">
      <xsl:apply-templates select="*[1]/*" mode="subst">
        <xsl:with-param name="v" select="*[1]/@var"/>
        <xsl:with-param name="t" select="*[2]"/>
      </xsl:apply-templates>
    </xsl:variable>
    <xsl:apply-templates select="exsl:node-set($term)"/>
  </xsl:template>

  <xsl:template match="app">
    <app>
      <xsl:apply-templates select="*[1]"/>
      <xsl:copy-of select="*[2]"/>
    </app>
  </xsl:template>

  <xsl:template match="app" mode="subst">
    <xsl:param name="v"/>
    <xsl:param name="t"/>
    <app>
      <xsl:apply-templates select="*" mode="subst">
        <xsl:with-param name="v" select="$v"/>
        <xsl:with-param name="t" select="$t"/>
      </xsl:apply-templates>
    </app>
  </xsl:template>
  
  <xsl:template match="lambda" mode="subst">
    <xsl:param name="v"/>
    <xsl:param name="t"/>
    <lambda var="@var">         <!--TODO capture avoidance-->
      <xsl:apply-templates select="*" mode="subst">
        <xsl:with-param name="v" select="$v"/>
        <xsl:with-param name="t" select="$t"/>
    </xsl:apply-templates>
    </lambda>
  </xsl:template>
  
  <xsl:template match="var" mode="subst">
    <xsl:param name="v"/>
    <xsl:param name="t"/>
    <xsl:choose>
      <xsl:when test="text() = $v">
        <xsl:copy-of select="$t"/>
      </xsl:when>
      <xsl:otherwise>
        <xsl:copy-of select="."/>
      </xsl:otherwise>
    </xsl:choose>
  </xsl:template>
 
</xsl:stylesheet>