+++ /dev/null
-<?xml version="1.0"?>
-<!-- Copyright (C) 2000, HELM Team -->
-<!-- -->
-<!-- This file is part of HELM, an Hypertextual, Electronic -->
-<!-- Library of Mathematics, developed at the Computer Science -->
-<!-- Department, University of Bologna, Italy. -->
-<!-- -->
-<!-- HELM is free software; you can redistribute it and/or -->
-<!-- modify it under the terms of the GNU General Public License -->
-<!-- as published by the Free Software Foundation; either version 2 -->
-<!-- of the License, or (at your option) any later version. -->
-<!-- -->
-<!-- HELM is distributed in the hope that it will be useful, -->
-<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
-<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
-<!-- GNU General Public License for more details. -->
-<!-- -->
-<!-- You should have received a copy of the GNU General Public License -->
-<!-- along with HELM; if not, write to the Free Software -->
-<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
-<!-- MA 02111-1307, USA. -->
-<!-- -->
-<!-- For details, see the HELM World-Wide-Web page, -->
-<!-- http://cs.unibo.it/helm/. -->
-
-<!--******************************************************************-->
-<!-- Lambda Calculus -->
-<!-- First draft: March 20 2001, Andrea Asperti -->
-<!--******************************************************************-->
-
-<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
- xmlns:m="http://www.w3.org/1998/Math/MathML"
- xmlns:helm="http://www.cs.unibo.it/helm">
-
-<!-- ************************** LAMBDA ****************************** -->
-
-<!-- subst -->
-<xsl:template match="APPLY[CONST[(attribute::uri='cic:/Rocq/LAMBDA/Terms/subst_rec.con' or attribute::uri='cic:/Rocq/LAMBDA/Substitution/subst_rec_r.con')] and count(child::*) = 4]" mode="pure">
- <m:apply>
- <m:csymbol definitionURL="{CONST/@uri}">subst</m:csymbol>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[4]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[CONST[(attribute::uri='cic:/Rocq/LAMBDA/Terms/subst.con' or attribute::uri='cic:/Rocq/LAMBDA/Substitution/subst_r.con')] and count(child::*) = 3]" mode="pure">
- <m:apply>
- <m:csymbol definitionURL="{CONST/@uri}">subst</m:csymbol>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- <m:ci>0</m:ci>
- </m:apply>
-</xsl:template>
-
-<!-- lift -->
-<xsl:template match="APPLY[CONST[(attribute::uri='cic:/Rocq/LAMBDA/Terms/lift_rec.con' or attribute::uri='cic:/Rocq/LAMBDA/Substitution/lift_rec_r.con')] and count(child::*) = 4]" mode="pure">
- <m:apply>
- <m:csymbol definitionURL="{CONST/@uri}">lift_with_base</m:csymbol>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- <xsl:apply-templates select="*[4]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[CONST[(attribute::uri='cic:/Rocq/LAMBDA/Terms/lift.con' or attribute::uri='cic:/Rocq/LAMBDA/Substitution/lift_r.con')] and count(child::*) = 3]" mode="pure">
- <m:apply>
- <m:csymbol definitionURL="{CONST/@uri}">lift</m:csymbol>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<!-- reduction -->
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Reduction/red1.ind')] and count(child::*) = 3]" mode="pure">
- <m:apply>
- <m:csymbol definitionURL="{MUTIND/@uri}">beta_red1</m:csymbol>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Reduction/red.ind')] and count(child::*) = 3]" mode="pure">
- <m:apply>
- <m:csymbol definitionURL="{MUTIND/@uri}">beta_red</m:csymbol>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Reduction/par_red1.ind')] and count(child::*) = 3]" mode="pure">
- <m:apply>
- <m:csymbol definitionURL="{MUTIND/@uri}">par_beta_red1</m:csymbol>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Reduction/par_red.ind')] and count(child::*) = 3]" mode="pure">
- <m:apply>
- <m:csymbol definitionURL="{MUTIND/@uri}">par_beta_red</m:csymbol>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<!-- unmark -->
-
-<xsl:template match="APPLY[CONST[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Marks/unmark.con')] and count(child::*) = 2]" mode="pure">
- <m:apply>
- <m:csymbol definitionURL="{CONST/@uri}">forgetful</m:csymbol>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<!-- boolean algebra of redexes -->
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Redexes/sub.ind')] and count(child::*) = 3]" mode="pure">
- <m:apply>
- <m:subset definitionURL="{MUTIND/@uri}"/>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Redexes/union.ind')] and count(child::*) = 4]" mode="pure">
- <m:apply>
- <m:eq definitionURL="{MUTIND/@uri}"/>
- <m:apply>
- <m:union definitionURL="{MUTIND/@uri}"/>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- </m:apply>
- <xsl:apply-templates select="*[4]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Redexes/comp.ind')] and count(child::*) = 3]" mode="pure">
- <m:apply>
- <m:csymbol definitionURL="{MUTIND/@uri}">isomorphic</m:csymbol>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Residuals/residuals.ind')] and count(child::*) = 4]" mode="pure">
- <m:apply>
- <m:eq definitionURL="{MUTIND/@uri}"/>
- <m:apply>
- <m:setdiff definitionURL="{MUTIND/@uri}"/>
- <xsl:apply-templates select="*[2]" mode="pure"/>
- <xsl:apply-templates select="*[3]" mode="pure"/>
- </m:apply>
- <xsl:apply-templates select="*[4]" mode="pure"/>
- </m:apply>
-</xsl:template>
-
-</xsl:stylesheet>
projects / helm.git / blobdiff