[llvm-commits] CVS: llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/Makefile.am Makefile.in lambda.html lambdamanual_src.html trans_xml_for_cat.pl user_manual_style.css
John Criswell
criswell at cs.uiuc.edu
Mon Dec 29 11:38:01 PST 2003
Changes in directory llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs:
Makefile.am added (r1.1)
Makefile.in added (r1.1)
lambda.html added (r1.1)
lambdamanual_src.html added (r1.1)
trans_xml_for_cat.pl added (r1.1)
user_manual_style.css added (r1.1)
---
Log message:
Adding the C++ program lambda to the test suite. This is a "real" C++
application that currently appears to work on both Linux and Solaris.
---
Diffs of the changes: (+2452 -0)
Index: llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/Makefile.am
diff -c /dev/null llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/Makefile.am:1.1
*** /dev/null Mon Dec 29 11:37:49 2003
--- llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/Makefile.am Mon Dec 29 11:37:39 2003
***************
*** 0 ****
--- 1,16 ----
+ noinst_DATA= \
+ lambdamanual.html \
+ trans_xml_for_cat.pl \
+ user_manual_style.css \
+ lambda.html
+
+ lambdamanual.html: ${srcdir}/lambdamanual_src.html ${srcdir}/trans_xml_for_cat.pl
+ ${srcdir}/trans_xml_for_cat.pl <${srcdir}/lambdamanual_src.html >lambdamanual.html
+
+ EXTRA_DIST=\
+ lambdamanual_src.html \
+ trans_xml_for_cat.pl \
+ user_manual_style.css \
+ lambda.html
+
+ CLEANFILES=lambdamanual.html
Index: llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/Makefile.in
diff -c /dev/null llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/Makefile.in:1.1
*** /dev/null Mon Dec 29 11:37:49 2003
--- llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/Makefile.in Mon Dec 29 11:37:39 2003
***************
*** 0 ****
--- 1,219 ----
+ # Makefile.in generated by automake 1.6.3 from Makefile.am.
+ # @configure_input@
+
+ # Copyright 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002
+ # Free Software Foundation, Inc.
+ # This Makefile.in is free software; the Free Software Foundation
+ # gives unlimited permission to copy and/or distribute it,
+ # with or without modifications, as long as this notice is preserved.
+
+ # This program is distributed in the hope that it will be useful,
+ # but WITHOUT ANY WARRANTY, to the extent permitted by law; without
+ # even the implied warranty of MERCHANTABILITY or FITNESS FOR A
+ # PARTICULAR PURPOSE.
+
+ @SET_MAKE@
+ SHELL = @SHELL@
+
+ srcdir = @srcdir@
+ top_srcdir = @top_srcdir@
+ VPATH = @srcdir@
+ prefix = @prefix@
+ exec_prefix = @exec_prefix@
+
+ bindir = @bindir@
+ sbindir = @sbindir@
+ libexecdir = @libexecdir@
+ datadir = @datadir@
+ sysconfdir = @sysconfdir@
+ sharedstatedir = @sharedstatedir@
+ localstatedir = @localstatedir@
+ libdir = @libdir@
+ infodir = @infodir@
+ mandir = @mandir@
+ includedir = @includedir@
+ oldincludedir = /usr/include
+ pkgdatadir = $(datadir)/@PACKAGE@
+ pkglibdir = $(libdir)/@PACKAGE@
+ pkgincludedir = $(includedir)/@PACKAGE@
+ top_builddir = ..
+
+ ACLOCAL = @ACLOCAL@
+ AUTOCONF = @AUTOCONF@
+ AUTOMAKE = @AUTOMAKE@
+ AUTOHEADER = @AUTOHEADER@
+
+ am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd
+ INSTALL = @INSTALL@
+ INSTALL_PROGRAM = @INSTALL_PROGRAM@
+ INSTALL_DATA = @INSTALL_DATA@
+ install_sh_DATA = $(install_sh) -c -m 644
+ install_sh_PROGRAM = $(install_sh) -c
+ install_sh_SCRIPT = $(install_sh) -c
+ INSTALL_SCRIPT = @INSTALL_SCRIPT@
+ INSTALL_HEADER = $(INSTALL_DATA)
+ transform = @program_transform_name@
+ NORMAL_INSTALL = :
+ PRE_INSTALL = :
+ POST_INSTALL = :
+ NORMAL_UNINSTALL = :
+ PRE_UNINSTALL = :
+ POST_UNINSTALL = :
+
+ EXEEXT = @EXEEXT@
+ OBJEXT = @OBJEXT@
+ PATH_SEPARATOR = @PATH_SEPARATOR@
+ AMTAR = @AMTAR@
+ AWK = @AWK@
+ CC = @CC@
+ CXX = @CXX@
+ DEPDIR = @DEPDIR@
+ INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@
+ PACKAGE = @PACKAGE@
+ STRIP = @STRIP@
+ VERSION = @VERSION@
+ am__include = @am__include@
+ am__quote = @am__quote@
+ install_sh = @install_sh@
+ noinst_DATA = \
+ lambdamanual.html \
+ trans_xml_for_cat.pl \
+ user_manual_style.css \
+ lambda.html
+
+
+ EXTRA_DIST = \
+ lambdamanual_src.html \
+ trans_xml_for_cat.pl \
+ user_manual_style.css \
+ lambda.html
+
+
+ CLEANFILES = lambdamanual.html
+ subdir = docs
+ mkinstalldirs = $(SHELL) $(top_srcdir)/config/mkinstalldirs
+ CONFIG_HEADER = $(top_builddir)/config.h
+ CONFIG_CLEAN_FILES =
+ DIST_SOURCES =
+ DATA = $(noinst_DATA)
+
+ DIST_COMMON = Makefile.am Makefile.in
+ all: all-am
+
+ .SUFFIXES:
+ $(srcdir)/Makefile.in: Makefile.am $(top_srcdir)/configure.ac $(ACLOCAL_M4)
+ cd $(top_srcdir) && \
+ $(AUTOMAKE) --foreign docs/Makefile
+ Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
+ cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)
+ uninstall-info-am:
+ tags: TAGS
+ TAGS:
+
+ DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
+
+ top_distdir = ..
+ distdir = $(top_distdir)/$(PACKAGE)-$(VERSION)
+
+ distdir: $(DISTFILES)
+ @list='$(DISTFILES)'; for file in $$list; do \
+ if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \
+ dir=`echo "$$file" | sed -e 's,/[^/]*$$,,'`; \
+ if test "$$dir" != "$$file" && test "$$dir" != "."; then \
+ dir="/$$dir"; \
+ $(mkinstalldirs) "$(distdir)$$dir"; \
+ else \
+ dir=''; \
+ fi; \
+ if test -d $$d/$$file; then \
+ if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \
+ cp -pR $(srcdir)/$$file $(distdir)$$dir || exit 1; \
+ fi; \
+ cp -pR $$d/$$file $(distdir)$$dir || exit 1; \
+ else \
+ test -f $(distdir)/$$file \
+ || cp -p $$d/$$file $(distdir)/$$file \
+ || exit 1; \
+ fi; \
+ done
+ check-am: all-am
+ check: check-am
+ all-am: Makefile $(DATA)
+
+ installdirs:
+
+ install: install-am
+ install-exec: install-exec-am
+ install-data: install-data-am
+ uninstall: uninstall-am
+
+ install-am: all-am
+ @$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am
+
+ installcheck: installcheck-am
+ install-strip:
+ $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
+ INSTALL_STRIP_FLAG=-s \
+ `test -z '$(STRIP)' || \
+ echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install
+ mostlyclean-generic:
+
+ clean-generic:
+ -test -z "$(CLEANFILES)" || rm -f $(CLEANFILES)
+
+ distclean-generic:
+ -rm -f Makefile $(CONFIG_CLEAN_FILES)
+
+ maintainer-clean-generic:
+ @echo "This command is intended for maintainers to use"
+ @echo "it deletes files that may require special tools to rebuild."
+ clean: clean-am
+
+ clean-am: clean-generic mostlyclean-am
+
+ distclean: distclean-am
+
+ distclean-am: clean-am distclean-generic
+
+ dvi: dvi-am
+
+ dvi-am:
+
+ info: info-am
+
+ info-am:
+
+ install-data-am:
+
+ install-exec-am:
+
+ install-info: install-info-am
+
+ install-man:
+
+ installcheck-am:
+
+ maintainer-clean: maintainer-clean-am
+
+ maintainer-clean-am: distclean-am maintainer-clean-generic
+
+ mostlyclean: mostlyclean-am
+
+ mostlyclean-am: mostlyclean-generic
+
+ uninstall-am: uninstall-info-am
+
+ .PHONY: all all-am check check-am clean clean-generic distclean \
+ distclean-generic distdir dvi dvi-am info info-am install \
+ install-am install-data install-data-am install-exec \
+ install-exec-am install-info install-info-am install-man \
+ install-strip installcheck installcheck-am installdirs \
+ maintainer-clean maintainer-clean-generic mostlyclean \
+ mostlyclean-generic uninstall uninstall-am uninstall-info-am
+
+
+ lambdamanual.html: ${srcdir}/lambdamanual_src.html ${srcdir}/trans_xml_for_cat.pl
+ ${srcdir}/trans_xml_for_cat.pl <${srcdir}/lambdamanual_src.html >lambdamanual.html
+ # Tell versions [3.59,3.63) of GNU make to not export all variables.
+ # Otherwise a system limit (for SysV at least) may be exceeded.
+ .NOEXPORT:
Index: llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/lambda.html
diff -c /dev/null llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/lambda.html:1.1
*** /dev/null Mon Dec 29 11:37:49 2003
--- llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/lambda.html Mon Dec 29 11:37:39 2003
***************
*** 0 ****
--- 1,110 ----
+ <html>
+ <head>
+ <title>Lambda - Unique Software Designs</title>
+ <meta content="text/html; charset=UTF-8" http-equiv="Content-Type" />
+ <style>
+ <!--
+ dt.outer { font-weight: bold; font-size: larger; color: blue; }
+ dt.inner { font-weight: bold; color: black; }
+ dt { font-weight: bold; color: sienna; }
+ -->
+ </style>
+ </head>
+ <body>
+ <h3>Datamaster Project</h3>
+ Lambda is a lambda calculus interpret.
+ It also will convert lambda expression into the
+ combinators S, K, and I.
+ <dl>
+ <dt class="outer">About</dt>
+ <dd class="outer">
+ <dl class="inner">
+ <dt class="inner">Current features:</dt>
+ <dd class="inner">
+ <ul>
+ <li>Load predefined lambda expression</li>
+ <li>Many definitions provided:
+ numbers Y fact map iszero list 1st 2nd 3rd
+ ADD MUL EXP
+ list suc pred . . .
+ </li>
+ <li>Automatic number definitions.</li>
+ <li>Interpret lambda expressions.</li>
+ <li>Single step interpretation.</li>
+ <li>Normal or application order reductions.</li>
+ <li>Variable extraction (Conversion to S K I)</li>
+ <li>List definitions.</li>
+ <li>Some lambda calculus theory.</li>
+ </ul>
+ </dd>
+ <dt class="inner">Current version</dt>
+ <dd class="inner">Lambda-0.1.1.</dd>
+
+ <dt class="inner">License</dt>
+ <dd class="inner">
+ Lambda is distributed as free software under GPL.
+ </dd>
+ </dl>
+ </dd>
+
+ <dt class="outer">News</dt>
+ <dd class="outer">
+ <dl>
+ <dt class="inner">Aug 19, 2003</dt>
+ <dd class="inner">Released Version 0.1.3.
+ <ul>
+ <li>Add xapp flag for ext command.</li>
+ <li>Made ext behave consistently when extracting constant expressions.</li>
+ <li>Add preprocessing for user manual.
+ This automatically inserts a table of contents
+ and does character entity translations.</li>
+ </ul>
+ </dd>
+ <dt class="inner">Aug 18, 2003</dt>
+ <dd class="inner">Released Version 0.1.2.
+ Added documentation:
+ <ul>
+ <li>Include examples for numbers.</li>
+ <li>Lists</li>
+ <li>Functional Completeness.</li>
+ </ul>
+ </dd>
+
+ <dt class="inner">Aug 17, 2003</dt>
+ <dd class="inner">Correction to definition of:
+ <code>ext x lambda-exp</code></dd>
+ <dt class="inner">Aug 15, 2003</dt>
+ <dd class="inner">Released version 0.1.1.</dd>
+ </dl>
+ </dd>
+
+ <dt class="outer">Documentation</dt>
+ <dd class="outer">
+ <a href="lambdamanual.html">User Manual.</a>
+ </dd>
+
+ <dt class="outer">Requirements</dt>
+ <dd class="outer">
+ The following software is required:
+ <ul>
+ <li>libstdc++</li>
+ </ul>
+ </dd>
+
+ <dt class="outer">Download</dt>
+ <dd class="outer">
+ <a href="http://www.uniquesoftwaredesign.com/~demo/lambda/lambda-0.1.3.tar.gz">Download Source</a>
+ </dd>
+
+ <dt class="outer">ChangeLog</dt>
+ <dd class="outer">
+ <a href="http://www.uniquesoftwaredesign.com/~demo/lambda/ChangeLog">ChangeLog</a>
+ </dd>
+
+ <dt class="outer">Contact</dt>
+ <dd class="outer">
+ <a href="mailto:usdesign at earthlink.net">usdesign at earthlink.net</a>
+ </dd>
+ </dl>
+ </body>
+ </html>
Index: llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/lambdamanual_src.html
diff -c /dev/null llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/lambdamanual_src.html:1.1
*** /dev/null Mon Dec 29 11:37:49 2003
--- llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/lambdamanual_src.html Mon Dec 29 11:37:39 2003
***************
*** 0 ****
--- 1,1756 ----
+ <html>
+ <head>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
+ <title>Lambda</title>
+ <style>
+ @import url(user_manual_style.css);
+ </style>
+ </head>
+
+ <body>
+ <p align=center>
+ <font face=helvetica size=+4><b>Lambda</b></font>
+ <table class="copying"><tr><td>
+ Permission is granted to copy, distribute and/or modify this
+ document under the terms of the GNU Free Documentation License,
+ Version 1.1 or any later version published by the Free Software
+ Foundation; with all sections Invariant Sections, with no Front-Cover
+ Texts, and with no Back-Cover Texts. A copy of the license is included
+ in the file "fdl.txt" included in this distribution.
+ <!--section entitled "GNU Free Documentation License".-->
+ </td></tr></table>
+ <p>
+ <hr>
+ <TOC>
+ <hr>
+ <h1>Commands</h1>
+ <h2>load</h2>
+ <div class="lambdacmd">load <definition-filename></div>
+
+ When lambda first starts it prints the current directory.
+ If the definition file is in this directory,
+ <directory-filename>
+ can be just the filename
+ (so long as the filename is just one word).
+ Otherwise, the filename should be enclosed in double quotes.
+ <p>
+ For example:
+ <p>
+ <code><font size=+1>
+ load definitions <br>
+ load "../share/definitions" <br>
+ </font>
+ </code>
+
+ <h2>list</h2>
+ <div class="lambdacmd">list</div>
+ <p>
+ List all current definitions in reverse order.
+ That is, the more recent definitions are printed first.
+
+ <h2>set</h2>
+ <div class="lambdacmd">
+ set [<flag>]...<br>
+ <flag> = trace | step | thru | app | body | brief | sym | eta | xapp | full <br>
+ </div>
+
+ <p>
+ Set or clear flags.
+ The flags govern the way in which expressions are evaluated and printed.
+ The set command used without any flags or with a flag
+ which it doesn't recognize will print a list the flags and their current state, after executing the commands.
+ The meaning of each flag is as follows:
+ <table>
+ <tr>
+ <td valign=top>
+ trace
+ </td>
+ <td>
+ If set, prints a sub-expression just before it is reduced.
+ Default: not set.
+ </td>
+ </tr>
+ <tr>
+ <td valign=top>
+ step
+ </td>
+ <td>
+ if set, one reduction is done at a time, the result printed,
+ and the user prompted to continue or stop reduction of this expression.
+ Default: not set.
+ </td>
+ <tr>
+ <td valign=top>
+ thru
+ </td>
+ <td>
+ Works the same as step,
+ except that the expression is reduced to normal form
+ without pausing between each reduction to print the expression
+ and prompt the user.
+ Setting one of these flags (step or thru)
+ will cause the other to be cleared.
+ If neither flag is set, the expression is reduced using a
+ recursive descent method, which should be faster.
+ This method should result in the reductions being performed
+ in the same order as the one reduction at a time method used
+ when step or thru are set.
+ However, it may not always.
+ Default: not set.
+ </td>
+ </tr>
+ <tr>
+ <td valign=top>
+ app
+ </td>
+ <td>
+ If set, do the reductions in "applicative order,"
+ which means reduce the "rand" of an application
+ before reducing the application.
+ If not set, perform the reductions in "normal order",
+ which means, do the left-most reduction in the expression first.
+ Default: not set.
+ </td>
+ </tr>
+ <tr>
+ <td valign=top>
+ body
+ </td>
+ <td>
+ If set reduce the body of a <i>abstraction,</i>
+ even though it is not the <i>rator</i> of an application.
+ Default: not set.
+ Setting body is necessary in order to make arithmetic work
+ correctly: MUL 2 2 ==> 4.
+ </td>
+ </tr>
+ <tr>
+ <td valign=top>
+ brief
+ </td>
+ <td>
+ If set, use a more compact method of printing an expression,
+ in which unnecessary parenthesis or elided.
+ If not set, extra parenthesis are printed to indicate
+ the left-to-right association nature of applications.
+ Default: set.
+ </td>
+ </tr>
+ <tr>
+ <td valign=top>
+ sym
+ </td>
+ <td>
+ If set, causes sub-expressions to be matched to definitions
+ when printing an expression.
+ Whenever a match is found,
+ the name of the definition is printed in place
+ of the value, which result in a more compact representation.
+ No attempt is made to preform alpha conversions to match expression,
+ although this would be a good idea for future versions of this program.
+ (An "alpha" conversion allows the name of the argument of an abstraction
+ to be changed.)
+ Default: set.
+ </td>
+ </tr>
+ <tr>
+ <td valign=top>eta</td>
+ <td>
+ If set:
+ <code>ext x f x ==> f</code>.
+ If not set:
+ <code>ext x f x ==> S(K f)I</code>.
+ </td>
+ </tr>
+ <tr>
+ <td valign=top>xapp</td>
+ <td>
+ If set:
+ <code>ext x f g ==>S(K f)(K g)</code>.
+ If not set:
+ <code>ext x f g ==>K(f g)</code>.
+ </td>
+ </tr>
+ <tr>
+ <td valign=top>
+ full
+ </td>
+ <td>
+ If set, causes names to be completed expanded,
+ by looping over the definitions until no more expansions
+ can be done.
+ May result in recursive loops.
+ Default: set.
+ </td>
+ </tr>
+ </table>
+
+ <h2>def</h2>
+ <div class="lambdacmd">
+ def <name> <lambda-exp>
+ </div>
+
+ <p>
+ Make a definition, associating
+ <code><font size=+1>
+ <name>
+ </font>
+ </code>
+ with
+ <code><font size=+1>
+ <lambda-exp>
+ </font>
+ </code>
+ in subsequent reductions.
+ If the name is already in use in a previous definition,
+ that definition is replaced with the new one.
+ If the lambda expression contains unbound variables,
+ they may be captured by arguments of abstractions
+ when the lambda expression is substituted for the definition name
+ in the reduction process.
+
+ <h2>ext</h2>
+ <div class="lambdacmd">
+ ext <var> <lambda-exp>
+ </div>
+ <p>
+ Extract the variable
+ <code><font size=+1><var></font></code>
+ from the lambda-exp
+ <code><font size=+1><lambda-exp></font></code>
+ so that
+ <p>
+ <code><font size=+1>
+ (ext <var> <lambda-exp>) <var>
+ == <lambda-exp><br>
+ </font></code>
+ <p>
+ If instead of a variable name
+ <code><font size=+1><var></font></code>
+ is the character
+ <code><font size=+1>^</font></code>
+ or <code><font size=+1>~</font></code>,
+ <p>
+ <code><font size=+1>
+ (ext ^ <lambda-exp>) == <lambda-exp><br>
+ (ext ~ <lambda-exp>) == <lambda-exp><br>
+ </font></code>
+ <p>
+ The
+ <lambda-exp>
+ is replaced by
+ <code><font size=+1>S</font></code>,
+ <code><font size=+1>K</font></code>,
+ and <code><font size=+1>I</font></code>
+ <i>combinators</i>, as follows:
+ <p>
+ <table border=1>
+ <tr>
+ <th>expression</th>
+ <th>result</th>
+ <th>remark</th>
+ </tr>
+ <tr>
+ <td valign="top"><code><font size=+1>ext x x</font></code></td>
+ <td valign="top"><code><font size=+1>I</font></code></td>
+ <td valign="top"> </i></td>
+ </tr>
+ <tr>
+ <td valign="top"><code><font size=+1>ext x A</font></code></td>
+ <td valign="top"><code><font size=+1>K A</font></code></td>
+ <td valign="top">A is a single symbol other than x</td>
+ </tr>
+ <tr>
+ <td valign="top"><code><font size=+1>ext x A</font></code></td>
+ <td valign="top"><code><font size=+1>K (A)</font></code></td>
+ <td valign="top">A is free in A and A is an application expression
+ and xapp is off</td>
+ </tr>
+ <tr>
+ <td valign="top"><code><font size=+1>ext x lambda-exp</font></code></td>
+ <td valign="top"><code><font size=+1>ext x (ext lambda-exp.arg lambda-exp.body)</font></code></td>
+ <td valign="top"> </i></td>
+ </tr>
+ <tr>
+ <td valign="top"><code><font size=+1>ext x exp1 exp2</font></code></td>
+ <td valign="top"><code><font size=+1>S (ext x exp1)(ext x exp2)</font></code></td>
+ <td valign="top">
+ exp1 and exp2 both constant and <i>xapp </i> is <i>on </i>
+ or<br>
+ exp1 and ext2 not both constant and exp2 is not <code>x </code>
+ or<br>
+ exp1 is x and <i>eta </i> is <i>off))</i></td>
+ </tr>
+ <tr>
+ <td valign="top"><code><font size=+1>ext x exp1 x</font></code></td>
+ <td valign="top"><code><font size=+1>S (ext x exp1)(ext x exp2)</font></code></td>
+ <td valign="top"><i>eta </i> is <i>on</i></td>
+ </tr>
+ <tr><td colspan="3"></td></tr>
+ <tr>
+ <td valign="top"><code><font size=+1>ext ^ x</font></code></td>
+ <td valign="top"><code><font size=+1>x<br></font></code></td>
+ <td valign="top"> </i></td>
+ </tr>
+ <tr>
+ <td valign="top"><code><font size=+1>ext ^ lambda-exp</font></code></td>
+ <td valign="top"><code><font size=+1>ext lambda-exp.arg lambda-exp.body</font></code></td>
+ <td valign="top"> </i></td>
+ </tr>
+ <tr>
+ <td valign="top"><code><font size=+1>ext ^ exp1 exp2</font></code></td>
+ <td valign="top"><code><font size=+1>(ext ^ exp1)(ext ^ exp2)</font></code></td>
+ <td valign="top"> </i></td>
+ </tr>
+ </table>
+ <p>
+ The definitions of S, K, and I are
+ <p>
+ <code><font size=+1>
+ I a = a <br>
+ K a b = a <br>
+ S a b c = a c( b c)<br>
+ </font></code>
+ </P>
+ <code><font size=+1>I</font></code> is often defined as
+ <code><font size=+1>S K K</font></code>.
+ <p>
+ For example,
+ <div class="lx">
+ <pre>
+ << set
+ >trace = 0
+ >step = 0
+ >thru = 0
+ >app = 0
+ >body = 0
+ >brief = 1
+ >sym = 1
+ >eta = 1
+ >xapp = 0
+ >full = 1
+ << ext x E x
+ E
+ << set eta
+ << ext x E x
+ S(K E)I
+ << ext x A B
+ K(A B)
+ << set xapp
+ << ext x A B
+ S(K A)(K B)
+ << ext x ^y.x y
+ S(S(K S)(S(K K)I))(K I)
+ << set eta
+ << ext x ^y.x y
+ I
+ << ext ^ ^x.^y.x y
+ I
+ << ext ^ ^x.^y.y x
+ S(S(K S)(K I))K
+ <<
+ </div>
+
+ <h2>lambda-expression</h2>
+ </pre>
+ <div class="lambdacmd">
+ <lambda-exp>
+ </div>
+ <p>
+ Reduce the lambda-expression.
+ However, if the lambda expression is just a single variable,
+ print its definition.
+ When a expression is reduced,
+ it is first parsed into an internal expression tree form,
+ printed (in the "non-brief" format),
+ and reduced again as directed by the flags.
+ The final result (and any intermediate results,
+ if the step flag is set) is printed as directed by the brief and sym flags.
+ When in the step mode, for each intermediate or final result,
+ an "B" is incorporated into the result cue to indicate a "beta"
+ reduction was performed, and an "H" is incorporated
+ to indicated a "eta" reduction was performed.
+ <p>
+ A user cue of
+ <p>
+ <code><font size=+1>
+ <<
+ </font></code>
+ <p>
+ used to indicate input is needed.
+ An a command is terminated by a new line.
+ However, if a lambda-expression is being reduced and a new line
+ is encountered with parentheses unbalanced,
+ the user is prompted to supply the missing right parentheses.
+ <p>
+ Parsed results are printed after the cue:
+ <p>
+ <code><font size=+1>
+ ==>
+ </font></code>
+ <p>
+ In the step mode,
+ intermediate and final results are printed after the cue:
+ <p>
+ <code><font size=+1>
+ =B==>
+ </font></code>
+ <p>
+ which indicates an "beta" reduction was peformed, or
+ <p>
+ <code><font size=+1>
+ =H==>
+ </font></code>
+ <p>
+ which means an "eta" reduction was performed. The cue
+ <p>
+ <code><font size=+1>
+ ===>
+ </font></code>
+ is used for final results when not in the step mode.
+ <p>
+
+ <h2>quit</h2>
+ <div class="lambdacmd">
+ quit
+ </div>
+ Quit.
+
+ <h1>Expressions</h1>
+
+ <h2>Syntax</h2>
+ <p>
+ <code><font size=+1>
+ <lambda-exp> = <variable> <br>
+ | ^<variable>.<lambda-exp> <br>
+ | <lambda-exp> <lambda-exp> <br>
+ | (<lambda-exp>) <br>
+ </font></code>
+
+ <h2>Semantics</h2>
+ <p>
+ The form ^<variable>.<lambda-exp>
+ is called an "abstraction."
+ The variable after the ^ and before the period is called the
+ <i>argument</i>,
+ and the lambda expression after the period is called the
+ <i>body</i>.
+ The body extends until the end of the expression,
+ or until a right parenthesis is encountered
+ which is unmatched by a corresponding left parenthesis
+ in the body expression.
+ <p>
+
+ The form
+ <code><font size=+1><lambda-exp> <lambda-exp></font></code>
+ is called an <i>application</i>.
+ The first lambda expression is called the <i>operator</i>
+ (or <i>rator</i> for short)
+ and the second is called the <i>operand</i>
+ (or <i>rand</i> for short.)
+ When an rator of an application is an abstraction,
+ an application can be <i>reduced</i>
+ by substituting the rand into the body of the abstraction
+ in place of each occurrence of the abstraction's argument.
+ This must be done in such a way
+ as to avoid an name collisions
+ with the arguments of other abstractions
+ which might be embedded in the body of the abstraction.
+ The application operation is <i>left-associative</i>,
+ which means that the expression
+ <p>
+ <code><font size=+1>
+ a b c d
+ </font></code>
+ <p>
+ means
+ <p>
+ <code><font size=+1>
+ ((a b) c) d.
+ </font></code>
+
+ <h3>Definition of "free"</h3>
+ Variable <i>x</i> occurs <b><i>free</i></b> in an expression:
+ <br>
+ 1. <i>x</i> occurs free in <i>x</i> (but not in any other variable);
+ <br>
+ 2. <i>x</i> occurs free in X Y if <i>x</i> occurs free in X or Y;
+ <br>
+ 3. <i>x</i> occurs free in ^<i>y</i>.Y if <i>x</i> and <i>y</i>
+ different and <i>x</i> occurs free in Y;
+ <br>
+ 4. <i>x</i> occurs free in (X) if <i>x</i> occurs free in X.
+ <br>
+ <h3>Definition of "bound"</h3>
+ Variable <i>x</i> occurs <b><i>bound</i></b> in an expression:
+ <br>
+ 1. No variable occurs bound in an expression consisting of
+ just a single variable;
+ <br>
+ 2. <i>x</i> occurs bound in ^<i>y</i>.Y if
+ <i>x</i> and <i>y</i> are the same variable
+ (and <i>x</i> occurs free in Y),
+ or if <i>x</i> occurs bound in Y.
+ <br>
+ 3. <i>x</i> occurs bound in X Y if it occurs bound in X or Y.
+ <br>
+ 4. <i>x</i> occurs bound in (X) if it occurs bound in X.
+
+ <h3>Substitution Rules</h3>
+ <p>
+ <b>Substitute expression M for variable <i>x</i> in expression X</b><br>
+ <b> [M/<i>x</i>]X </b><br>
+ <p>
+ <table border=1>
+ <tr>
+ <th align=left>Case</th>
+ <th align=left>Condition</th>
+ <th align=left>Rule: [M/x]X ==></th>
+ </tr>
+
+ <tr>
+ <td align=left valign=top><code><font size=+1><b>1</b></font></code></td>
+ <td align=left valign=top colspan=2><code><font size=+1>
+ <b>X is a Variable</b></td>
+ </font>
+ </tr>
+
+ <tr>
+ <td align=left valign=top><code><font size=+1>1.1</font></code></td>
+ <td align=left valign=top><code><font size=+1>X == <i>x</i></font></code></td>
+ <td align=left valign=top><code><font size=+1>M</font></code></td>
+ </tr>
+
+ <tr>
+ <td align=left valign=top><code><font size=+1>1.2</font></code></td>
+ <td align=left valign=top><code><font size=+1>X != <i>x</i></font></code></td>
+ <td align=left valign=top><code><font size=+1>X</font></code></td>
+ </tr>
+
+ <tr>
+ <td align=left valign=top><code><font size=+1><b>2</b></font></code></td>
+ <td align=left valign=top><code><font size=+1>
+ <b>X is a Application: Y Z</b></font></code></td>
+ <td align=left valign=top><code><font size=+1>
+ ([M/<i>x</i>]Y)([M/<i>x</i>]Z)</font></code></td>
+ </tr>
+
+ <tr>
+ <td align=left valign=top><code><font size=+1><b>3</b></font></code></td>
+ <td align=left valign=top colspan=2><code><font size=+1>
+ <b>X is an Abstraction: ^<i>y</i>.Y</b></font></code></td>
+ </tr>
+
+ <tr>
+ <td align=left valign=top><code><font size=+1>3.1</font></code></td>
+ <td align=left valign=top><code><font size=+1>
+ <i>y</i> == <i>x</i></font></code></td>
+ <td align=left valign=top><code><font size=+1>X</font></code></td>
+ </tr>
+
+ <tr>
+ <td align=left valign=top><code><font size=+1>3.2</font></code></td>
+ <td align=left valign=top><code><font size=+1>
+ <i>y</i> != <i>x</i></font></code></td>
+ <td align=left valign=top><code><font size=+1> </font></code></td>
+ </tr>
+
+ <tr>
+ <td align=left valign=top><code><font size=+1>3.2.1</font></code></td>
+ <td align=left valign=top><code><font size=+1>
+ <i>x</i> doesn't occur free in Y<br>
+ or <i>y</i> doesn't occur free in M</font></code></td>
+ <td align=left valign=top><code><font size=+1>
+ ^<i>y</i>.[M/<i>x</i>]Y</font></code></td>
+ </tr>
+
+ <tr>
+ <td align=left valign=top><code><font size=+1>3.2.2</font></code></td>
+ <td align=left valign=top><code><font size=+1>
+ <i>x</i> does occur free in Y<br>
+ and <i>y</i> does occur free in M
+ (a <i>collision</i>)</font></code></td>
+ <td align=left valign=top><code><font size=+1>
+ ^<i>z</i>.[M/<i>x</i>]([<i>z</i>/<i>y</i>]Y)<br>
+ where <i>z</i> is the first variable
+ in the sequence of variables
+ such that <i>z</i> doesn't occur free in M or Y.
+ <br>
+ That is, change all free occurrences of <i>y</i> in Y to <i>z</i>,
+ then replace occurrences of <i>x</i> in Y with M.
+ The argument of the abstraction is changed from
+ <i>y</i> to <i>z</i>.
+ </font></code>
+ </td>
+ </tr>
+ </table>
+ <p>
+
+ <h3>Conversion Definitions</h3>
+ <table>
+ <tr>
+ <th align=left>Conversion</th>
+ <th align=left>Definition</th>
+ </tr>
+ <tr>
+ <td>α</td>
+ <td>if <i>y</i> is not free in X,
+ then ^<i>x</i>.X cnv(&alpha) ^<i>y</i>.[<i>y</i>/<i>x</i>]X</td>
+ </tr>
+ <tr>
+ <td>β</td>
+ <td>(^<i>x</i>.M)N cnv(β) [N/<i>x</i>]M</td>
+ </tr>
+ <tr>
+ <td>η</td>
+ <td>if <i>x</i> is not free in M, then
+ ^<i>x</i>.M <i>x</i> cnv(η) M.
+ </td>
+ </tr>
+ </table>
+ <p>
+ A <i>reduction</i> means going from left to right with a β or η conversion; that is, getting rid of a ^.
+ <i>Normal order</i> means getting rid of the left most ^ first.
+ <i>Applicative order</i> means reducing the rand <i>before</i> the rator.
+
+ <h3>Variable Name Prefixes</h3>
+ <p>
+
+ <table>
+ <tr>
+ <th align=left>Prefix</th>
+ <th align=left>Meaning</th>
+ </tr>
+ <tr>
+ <td>
+ <code><font size=+1>$</font></font></code>
+ </td>
+ <td>
+ If the argument of an abstraction has
+ <code><font size=+1>$</font></font></code>
+ as its first character,
+ the abstraction,
+ when it is being reduced as part of an application,
+ will be reduced as though the step flag were off,
+ and the body flag were on.
+ </td>
+ <tr>
+ <td>
+ <code><font size=+1>&</font></font></code>
+ </td>
+ <td>
+ If the argument of an abstraction has
+ <code><font size=+1>&</font></font></code>
+ as its first character,
+ the abstraction will be reduced as though the step
+ and body flags are both off.
+ </td>
+ </tr>
+ </table>
+
+ <h1>Arithmetic</h1>
+
+ <h2>Basic Definitions</h2>
+
+ Let
+ <table>
+
+ <tr>
+ <td>
+ <code>[m]</code>
+ </td>
+ <td>
+ represent the lambda expression for the postive integer m,
+ </td>
+ </tr>
+
+ <tr>
+ <td>
+ <code>[0]</code>
+ </td>
+ <td>
+ <code>^x.^y.y</code>
+ </td>
+ </tr>
+
+ <tr>
+ <td>
+ <code>[n+1]</code>
+ </td>
+ <td>
+ <code>^x.^y.x([n] x y)</code> for all n > 0
+ </td>
+ </tr>
+
+ <tr>
+ <td>
+ <code>ADD</code>
+ </td>
+ <td>
+ <code>^m.^n.^x.^y.m x(n x y)</code>
+ </td>
+ </tr>
+
+ <tr>
+ <td>
+ <code>MUL</code>
+ </td>
+ <td>
+ <code>^m.^n.^x.m(n x)</code>
+ </td>
+ </tr>
+
+ <tr>
+ <td>
+ <code>EXP</code>
+ </td>
+ <td>
+ <code>^n.^m.m n</code>
+ </td>
+ </tr>
+ </table>
+
+ <h2>Proposition for Addition</h2>
+ <table>
+ <tr>
+ <td colspan=3 valign=top>
+ <code>ADD [m][n] = [m+n]</code>
+ </td>
+ </tr>
+ <tr>
+ <td valign="top" align=left><div class="proof">Proof</div></td>
+ <td colspan=2>By induction</td>
+ </tr>
+ <tr>
+ <th valign=top align=left>1)</th>
+ <td>
+ <code>
+ ADD [0] [n]<br>
+ = ^x.^y.[0] x.([n] x y)<br>
+ = ^x.^y.[n] x y<br>
+ = [n] = [0+n]<br>
+ </code>
+ </td>
+ </tr>
+ <tr>
+ <th valign=top align=left>2)</th>
+ <td>
+ Assume
+ <code>
+ ADD [m][n] = [m+n] <b><i>
+ </code>
+ </td>
+ <td>
+ <b><i>induction hypothesis</i></b>
+ </td>
+ </tr>
+ <tr>
+ <th valign=top align=left>3)</th>
+ <td>
+ <code>
+ ADD [m+1][n]<br>
+ = ^x.^y.[m+1] x([n] x y)<br>
+ = ^x.^y.(^a.^b.a([m] a b)) x ([n] x y)<br>
+ = ^x.^y.x([m] x ([n] x y)<br>
+ = ^x.^y.x(ADD [m] [n] x y)<br>
+ </code>
+ </td>
+ </tr>
+ <tr>
+ <th align=left valign=top>=></tn>
+ <td>
+ <code>
+ = ^x.^y.x([m+n] x y)<br>
+ </code>
+ </td>
+ </td>
+ <td valign=top>
+ <b><i>by 2) induction hypothesis</i></b><br>
+ </td>
+ </tr>
+
+ <tr>
+ <td valign=top></td>
+ <td valign=top>
+ <code>
+ = [(m+1)+n]<br>
+ </code>
+ <td valign=top></td>
+ </tr>
+ </tr>
+ </table>
+
+ <h2>Proposition for Multiplication</h2>
+ <table>
+ <tr>
+ <td colspan=3>
+ <code>MUL [m][n] = [m*n]</code>
+ </td>
+ </tr>
+ <tr>
+ <td valign="top" align=left><div class="proof">Proof</div></td>
+ <td colspan=2>By induction</td>
+ </tr>
+
+ <tr>
+ <th valign=top align=left>1)</th>
+ <td>
+ <code>
+ MUL [0] [n]<br>
+ = ^x.[0]([n] x)<br>
+ = ^x.(^a.^b.b)([n] x)<br>
+ = ^x.^b.b<br>
+ = ^x.^y.y<br>
+ = [0]<br>
+ </code>
+ </td>
+ <td valign=top></td>
+ </tr>
+ <tr>
+ <th valign=top align=left>2)</th>
+ <td valign=top>
+ Assume
+ <code>
+ MUL [m][n] = [m*n]
+ </code>
+ <td valign=top>
+ <b><i>induction hypothesis</i></b><br>
+ </td>
+ </tr>
+
+ <tr>
+ <th valign=top align=left>3)</th>
+ <td valign=top>
+ <code>
+ MUL [m+1] [n]<br>
+ = ^x.[m+1]([n] x)<br>
+ = ^x.(^a.^b.a([m] a b))([n] x)<br>
+ = ^x.^b.([n] x)([m] ([n] x) b)<br>
+ = ^x.^b.([n] x)(MUL [m] [n] x b)<br>
+ </code>
+ <td>
+ <td valign=top></td>
+ </tr>
+
+ <tr>
+ <th align=left valign=top>=></th>
+ <td valign=top>
+ <code>
+ = ^x.^b.([n] x)([m*n] x b)<br>
+ </code>
+ <td valign = top>
+ <b><i>by 2) induction hypthesis</i></b><br>
+ </td>
+ </tr>
+
+ <tr>
+ <td valign=top</td>
+ <td valign=top>
+ <code>
+ = ^x.^b.ADD [n] [m*n] x b<br>
+ = ^x.^b.[n+m*n] x b<br>
+ = [n+m*n]<br>
+ = [(m+1)*n]<br>
+ </code>
+ </td>
+ <td valign = top>
+ </td>
+ </tr>
+ </table>
+
+ <p>
+ <h2>Proposition for Exponentiation.</h2>
+ <table>
+ <tr>
+ <td colspan=3 align = top>
+ <code>EXP [n][m] = [n**m]</code>
+ </td>
+ </tr>
+ <tr>
+ <td valign="top" align=left><div class="proof">Proof</div></td>
+ <td colspan=2>By induction</td>
+ </tr>
+ <tr>
+ <th valign=top align=left>1)</th>
+ <td valign=top>
+ <code>
+ EXP [n] [0] <br>
+ = [0] [n] <br>
+ = (^x.^y.y)[n]<br>
+ = ^y.y<br>
+ = ^y.^z.y z<br>
+ = [1]<br>
+ </code>
+ </td>
+ <td valign=top> </td>
+ </tr>
+ <tr>
+ <th valign=top align=left>2)</th>
+ <td valign=top>
+ Assume
+ <code>
+ EXP [n][m] = [n**m]
+ </code>
+ </td>
+ <td valign=top>
+ <b><i>induction hypothesis</i></b><br>
+ </td>
+ </tr>
+
+ <tr>
+ <th valign=top align=left>3)</th>
+ <td valign=top>
+ <code>
+ EXP [n] [m+1]<br>
+ = [m+1] [n]<br>
+ = (^x.^y.x([m] x y))[n]<br>
+ = ^y.[n]([m] [n] y)<br>
+ = ^y.[n](EXP [n] [m] y)<br>
+ </code>
+ </td>
+ </tr>
+ <tr>
+ <th align=left valign=top>=></th>
+ <td valign=top>
+ <code>
+ = ^y.[n]([n**m] y)
+ </code>
+ </td>
+ <td valign=top>
+ <b><i>by 2) induction hypothesis</i></b><br>
+ </td>
+ </tr>
+
+ <tr>
+ <td valign=top> </td>
+ <td valign=top>
+ <code>
+ = MUL [n] [n**m]<br>
+ = [n*(n**m)]<br>
+ = [n**(m+1)]<br>
+ </code>
+ <td valign=top>
+ </td>
+ </tr>
+
+ </table>
+
+ <p>
+ <h2>Proposition for Predecessor</h2></th>
+
+ <table>
+ <tr>
+ <td colspan=3 valign=top>
+ <code>
+ pred [n] = [n-1]
+ </code>
+ <table>
+
+ <tr>
+ <th align=left valign=top>
+ Let<br>
+ </th>
+ <td>
+ <code>
+ suc = ^n.^x.^y.x(n x y)<br>
+ pair = ^f.^s.^p.(p f s)<br>
+ false = ^f.^s.s<br>
+ true = ^f.^s.f<br>
+ </code>
+ </td>
+ </tr>
+
+ <tr>
+ <th align=left valign=top>
+ and<br>
+ </th>
+ <td>
+ <code>
+ bump = ^p.pair (suc(p true)) (p true)<br>
+ pred_pair = ^n.n bump (pair 0 0)<br>
+ pred = ^n.pred_pair n false<br>
+ </code>
+ </td>
+ </tr>
+
+ <tr>
+ <th align=left valign=top>
+ then
+ </th>
+ <td>
+ <code>
+ pred_pair [n] = pair [n] [n-1]<br>
+ </code>
+ </td>
+ </tr>
+
+ <tr>
+ <tr>
+ <th align=left valign=top>
+ hence<br>
+ </th>
+ <td>
+ <code>
+ pred [n] = [n-1]<br>
+ </code>
+ </td>
+ </tr>
+ </table>
+ </td>
+ </tr>
+ <tr>
+ <td valign = align=left><div class="proof">Proof</div></td>
+ <td colspan=2>By induction</td>
+ </tr>
+
+ <tr>
+ <th valign=top align=left>1)</th>
+ <td valign=top>
+ <code>
+ pred_pair [1]<br>
+ = 1 bump (pair 0 0)<br>
+ = bump (pair 0 0)<br>
+ = pair (suc((pair 0 0) true)) ((pair 0 0) true))<br>
+ = pair 1 0<br>
+ </code>
+ </list>
+ </td>
+ <td valign=top> </td>
+ </tr>
+
+ <tr>
+ <th valign=top align=left>2)</th>
+ <td valign=top>
+ Assume
+ <code>
+ pred_pair [n] = pair [n] [n-1]<br>
+ </code>
+ </td>
+ <td valign=top>
+ <b><i>induction hypothesis</i></b><br>
+ </td>
+ </tr>
+
+ <tr>
+ <th valign=top align=left>3)</th>
+ <td valign=top>
+ <code>
+ pred_pair [n+1]<br>
+ = ^n. (n bump (pair 0 0))[n+1]<br>
+ = [n+1] bump (pair 0 0)<br>
+ = bump ([n] bump (pair 0 0))<br>
+ = bump (pred_pair [n])<br>
+ </code>
+ </td>
+ </tr>
+
+ <tr>
+ <th align=left valign=top>=></th>
+ <td valign=top>
+ <code>
+ = bump (pair [n] [n-1])<br>
+ = pair [n+1] [n]<br>
+ </code>
+ </td>
+ <td valign=top>
+ <b><i>by 2) induction hypothesis</i></b><br>
+ </td>
+ </tr>
+
+ <tr>
+ <th valign=top align=left>4)</th>
+ <td valign=top>
+ <code>
+ pred [n]<br>
+ = pred_pair [n] false<br>
+ = pair [n] [n-1] false<br>
+ = false [n] [n-1]<br>
+ = [n-1]<br>
+ </code>
+ </td>
+ <td valign=top></td>
+ </tr>
+
+ </table>
+
+ <h2>Examples</h2>
+
+ <div class="lx">
+ <pre>
+ def 0 ^m.^n.n
+ def true ^p.^q.p
+ def def false ^p.^q.q
+ def suc ^p.^m.^n.m(p m n)
+ def pred ^$k.$k(^p.(mpair(suc(p true))(p true)))(mpair 0 0)false
+ def mpair ^a.^b.^u.u a b
+ def def iszero ^n. n (true false) true
+ def ADD ^m.^n.^x.^y.m x(n x y)
+ def MUL ^m.^n.^f.m(n f)
+ def EXP ^m.^n.n m
+ def GT ^m.^n.not(iszero (n pred m))
+ def EQ ^m.^n.and (iszero (m pred n)) (iszero (n pred n))
+ def LT ^m.^n.not(iszero(m pred n))
+ def GE ^m.^n.not(LT m n)
+ << iszero 0
+ ==> iszero 0
+ ====>true
+ << iszero 5
+ ==> iszero 5
+ ====>false
+ << suc 0
+ ==> suc 0
+ ====>I
+ << suc 1
+ ==> suc 1
+ ====>2
+ << suc 2
+ ==> suc 2
+ ====>3
+ << pred 3
+ ==> pred 3
+ ====>2
+ << pred 2
+ ==> pred 2
+ ====>I
+ << pred 1
+ ==> pred 1
+ ====>0
+ << pred 0
+ ==> pred 0
+ ====>0
+ << ADD 1 2
+ ==> (ADD 1) 2
+ ====>3
+ << MUL 2 3
+ ==> (MUL 2) 3
+ ====>6
+ << EXP 2 3
+ ==> (EXP 2) 3
+ ====>8
+ << EXP 3 2
+ ==> (EXP 3) 2
+ ====>9
+ << GT 2 3
+ ==> (GT 2) 3
+ ====>false
+ << GT 3 2
+ ==> (GT 3) 2
+ ====>true
+ << EQ 4 (ADD 2 2)
+ ==> (EQ 4)((ADD 2) 2)
+ ====>true
+ << EQ 5 (ADD 3 3)
+ ==> (EQ 5)((ADD 3) 3)
+ ====>false
+ <<
+ </pre>
+ </div>
+
+ <h1>Lists</h1>
+ <h2>Nodes</h2>
+ The basis of a list is the <code>triple</code>:
+ <div class="lx">
+ <pre>
+ def mtriple ^a.^b.^c.^u.u a b c
+ def 1st ^a.^b.^c.a
+ def 2nd ^a.^b.^c.b
+ def 3rd ^a.^b.^c.c
+ </pre>
+ </div>
+ So
+ <div class="lx">
+ <pre>
+ ==> abc 2nd
+ ====>b
+ << abc 3rd
+ ==> abc 3rd
+ ====>c
+ <<
+ </pre>
+ </div>
+ A list node is a triple whose first component is the first
+ element of the list, the second component is the rest of the
+ list, and the third component is a boolean that is true if
+ the triple is the last node of the list and false otherwise.
+ <div class="lx">
+ <pre>
+ def true ^p.^q.p
+ def false ^p.^q.q
+ def mknode (^a.^b.^u.u a b false)
+ def is_end (^n.n sel_3)
+ </pre>
+ </div>
+ <h2>Empty List</h2>
+ A special node, <code>end</code> is constructed to serve as the
+ empty list, and to be the last node of a list.
+ <div class="lx">
+ <pre>
+ def renda ^e.^&u.&u e e true
+ def def rend (^x.renda(x x))(^x.renda(x x))
+ def head (^n.n sel_1)
+ def tail (^n.n sel_2)
+ def end ^&u.&u rend rend true
+ </pre>
+ </div>
+ We see that:
+ <div class="lx">
+ <pre>
+ << Y renda
+ ==> Y renda
+ ====>end
+ << renda rend
+ ==> renda rend
+ ====<end
+ << head end
+ ==> head end
+ ====>end
+ << tail end
+ ==> tail end
+ ====>end
+ << is_end end
+ ==> is_end end
+ ====>true
+ <<
+ </pre>
+ </div>
+ We define Y, the fixed-point operator,
+ in the next section, "Function Complete of Curry Algebras."
+ <p>
+ So <code>end</code>
+ <ul><li>is the fixed point of <code>renda</code>,</li>
+ <li>answers true to <code>is_end</code>, and</li>
+ <li>is its own head and tail.</li>
+ </ul>
+ <p>
+ <h2>Appending</h2>
+ The form <code>append</code> adds and element to the end of a list.
+ <div class="lx">
+ <pre>
+ def Appenda ^h.^n.^list.(is_end list)(mknode n end)(mknode(head list)(h n(tail list)))
+ def append (^x.Appenda(x x))(^x.Appenda(x x))
+ </pre>
+ </div>
+ It is easy to see that
+ <pre>
+ append = Y Appenda
+ </pre>
+ As an example of a list, we have:
+ <div class="lx">
+ <pre>
+ << def abc append c (append b (append a end)))
+ << head abc
+ ==> head abc
+ ====>a
+ << head (tail abc)
+ ==> head(tail abc)
+ ====>b
+ << head (tail (tail abc))
+ ==> head(tail(tail abc))
+ ====>c
+ << head (tail (tail (tail abc)))
+ ==> head(tail(tail(tail abc)))
+ ====>end
+ <<
+ </pre>
+ </div>
+ <h2>Mapping</h2>
+ Finally define the form <code>map</code> which applies
+ its first argument to each node of its second argument,
+ if the second argument is a list, anyway.
+ <div class="lx">
+ <pre>
+ def Mapa ^h.^f.^list.(is_end list)(end)(mknode(f (head list))(h f (tail list)))
+ def map (^x.Mapa(x x))(^x.Mapa(x x))
+ </pre>
+ </div>
+ So, for example,
+ <div class="lx">
+ <pre>
+ << def n01234 append 4 (append 3 (append 2 (append 1 (append 0 end))))
+ << head n01234
+ ==> head n01234
+ ====>0
+ << head (tail n01234)
+ ==> head(tail n01234)
+ ====>I
+ << head (tail (tail n01234))
+ ==> head(tail(tail n01234))
+ ====>2
+ << head (tail (tail (tail n01234)))
+ ==> head(tail(tail(tail n01234)))
+ ====>3
+ << head(tail(tail(tail(tail n01234))))
+ ==> head(tail(tail(tail(tail n01234))))
+ ====>4
+ << head(tail(tail(tail(tail(tail n01234)))))
+ ==> head(tail(tail(tail(tail(tail n01234)))))
+ ====>end
+ << def s01234 map suc n01234
+ << head s01234
+ ==> head s01234
+ ====>I
+ << head (tail s01234)
+ ==> head(tail s01234)
+ ====>2
+ << head (tail (tail s01234))
+ ==> head(tail(tail s01234))
+ ====>3
+ << head(tail(tail(tail s01234)))
+ ==> head(tail(tail(tail s01234)))
+ ====>4
+ << head(tail(tail(tail(tail s01234))))
+ ==> head(tail(tail(tail(tail s01234))))
+ ====>5
+ << head(tail(tail(tail(tail(tail s01234)))))
+ ==> head(tail(tail(tail(tail(tail s01234)))))
+ ====>end
+ <<
+ </pre>
+ </div>
+
+ <h1>Functional Completeness of Curry Algebras</h1>
+ The course of reasoning followed here is adapted from
+ "FROM λ-CALCULUS TO CARTESIAN CLOSED CATEGORIES",
+ J Lambek, McGill University, Montreal, P.Q. H3A 2K6, Canada.
+ <p>
+ [Note: To read this section your browser must be able to render
+ the greek character entities:
+ α(α),
+ β(β),
+ ...,
+ ≡(≡),
+ ∈(∈),
+ ∀(∀),
+ °(°).]
+ <p>
+ A Schönfinkel Algebra
+ <code>A</code> consists of a set of <i>symbols </i>
+ <code>|A|</code>,
+ a left associative binary operation <code>|A|x|A|->|A|</code>
+ (denoted here by juxtaposition),
+ and three constants in <code>|A|</code>:
+ <code>I</code>,
+ <code> K</code>, and
+ <code>S</code> such that:
+ <pre>
+ for all a, b, c, f, and g in |A|
+ (1) I a = a
+ (2) K a b = a
+ (3) S f g c = (f c)(g c)
+ </pre>
+
+ We call <code>(a b) </code> a <i>combination</i>.
+ So we can form expressions of combinations of the symbols in
+ <code>|A|</code>, and these will correspond to other symbols
+ in <code>|A|</code>. Mostly, we are interested in just those
+ symbols that can be expressed by combinations of
+ <code>S</code>, <code>K</code> and <code>I</code>.
+ <p>
+ We can say that a polynomial in <code>A </code>
+ with unknown <code>x </code> is an element of
+ the Schönfinkel Algebra <code>A[x]</code>, (which is
+ <code>A </code> with an extra element <code>x</code>
+ attached to
+ <code>|A|</code>)
+ and a mapping <pre>
+ h<sub>x</sub>: A -> A[x]
+ </pre> such for all
+ algebra's <code>B </code> and mappings
+ <code>A->B </code> and
+ <code>b ∈ |B|</code>,
+ there is an <code>f' </code> such that
+ <pre>
+ f = f'°h<sub>x</sub>
+ </pre>
+ and
+ <pre>
+ f'(x) = b.
+ </pre>
+ If
+ <pre>
+ B = A and
+ f is the identity morphism,
+ </pre>
+ then
+ <code>f' </code> is the <i>substitution </i> map that
+ replaces <code>x </code> with <code>b=a∈A</code>.
+ <p>
+ If
+ <pre>
+ B = A[x], and
+ f = h<sub>x</sub>
+ </pre>
+ then <code>f' </code> is the <i>substitution </i> map that
+ replaces <code>x </code> with <code>b=ψ(x)∈A[x]</code>.
+
+ <h2>Proposition 1 Abstractions in Schönfinkel Algebras.</h2>
+ Every polynomial φ(x) over a
+ Schönfinkel Algebra <code>A </code> can be written in the form
+ <pre>
+ f x
+ </pre>
+ where
+ <pre>
+ f ∈ |A|
+ </pre>
+
+ Polynomials in <code>A </code> are formed as words in an indeterminate
+ x and satisfy the same three identities.
+ In particular equality =<sub>x</sub> between polynomials is the
+ smallest equivalence relation ≡ that satisfies:
+ <pre>
+ (0<sub>x</sub>) φ(x) &quiv; psi;(x) and α(x) ≡ β(x) implies φ(x)ψ(x) ≡ α(x) β(x)
+ (1<sub>x</sub>) I(α(x)) ≡ α(x)
+ (2<sub>x</sub>) K(α(x))(β(x)) ≡ α(x)
+ (3<sub>x</sub>) S(α(x))(β(x))(γ(x)) ≡ (α(x))(γ(x))((β(x))(γ(x))
+ </pre>
+
+ </pre>
+ <div class="proof">Proof:</div>
+ By induction a the length of the word φ(x),
+ which must be one of
+ <pre>
+ x,
+ some constant expression (without x), or
+ ψ(x) χ(x)
+ </pre>
+ We have for these three cases:
+ <pre>
+ φ(x) =<sub>x</sub> I x
+ φ(x) =<sub>x</sub> (K a ) x,
+ φ(x) =<sub>x</sub> (g x) (h x) = (S g h x)
+ </pre>
+
+ This proof yields an algorithm for converting every polynomial
+ into the form <code>f x</code>, where the word <code>f </code>
+ is free of any occurrence of <code>x</code>. This is equivalent
+ to the
+ <span class="lambda">lambda </span>
+ command
+ <pre>
+ ext x φ(x)
+ </pre>
+ with the flag <i>eta </i> toggled off (1) and <i>xapp </i> toggle on,
+ With <i>eta </i> on, we still can make <code>ext x </code>work
+ like this algorithm if we replace all occurrences of x
+ not already in the combination <code>(I x) </code>
+ with <code>(I x)</code>.
+ <p>
+ Starting with <i>eta </i> on, such a
+ <span class="lambda">lambda </span>
+ session might look like:
+ <div class="lx">
+ <PRE>
+ << ext x x
+ I
+ << ext x I x
+ I
+ << ext x A
+ K A
+ << ext x A B
+ K(A B)
+ << ext x (A x)(B x)
+ S A B
+ << ext x A x
+ A
+ << ext x A (I x)
+ S(K A)I
+ << ext x x A
+ S I(K A)
+ << ext x I x A
+ S I(K A)
+ <<
+ </PRE>
+ </div>
+
+ <p>
+ A Curry Algebra is a Schönfinkel Algebra subject to certain
+ additional equations or identities whose conjunction is equivalent
+ to the following statement:
+ <pre>
+ (4) If f x =<sub>x</sub> g x in A[x] then f = g in A.
+ </pre>
+ For example,
+ <pre>
+ S K I x =<sub>x</sub> (K x)(I x) =<sub>x</sub> I x,
+ </pre>
+ so, (4) implies
+ <pre>
+ S K I = I
+ </pre>
+ a result that can't be obtained from (1) through (3) alone.
+ <p>
+
+ <h2>Proposition 2. Existence of Curry Algebras.</h2>
+ It is possible to add a finite collection of equations or identities to
+ the definition of a Schönfinkel Algebra to form a Curry Algebra:
+ Every polynomial <code>φ(x)</code>
+ over a Curry Algebra <code>A </code> may be
+ written uniquely in the form <code>(f x)</code>
+ with <code>f ∈ |A|</code>.
+ <div class="proof">Proof</div>
+ We need to demonstate a collection of (universally quantified)
+ equations, or better, identities, in <code>|A|</code> whose conjunction,
+ together with <code>(1)</code>, <code>(2)</code>, and <code>(3)</code>,
+ imply <code>(4)</code>.
+ <p>
+ Define the function λ<sub>x</sub> by induction on the length
+ of the word representing the polynomial, φ(x).
+ <pre>
+ (i) λ<sub>x</sub>x = I;
+ (ii) λ<sub>x</sub>x = K a, when a is a constant; and
+ (iii) λ<sub>x</sub>(φ(x))(ψ(x)) = S(λ<sub>x</sub>φ(x))(λ<sub>x</sub>ψ(x)), when φ(x) and ψ(x) are not both constant.
+ </pre>
+ <p>
+ The restriction on <code>(iii)</code> is necessary so that λ<sub>x</sub> is not ambiguous:
+ if both parts of a combination are constant then <code>(ii)</code> applies.
+ The <span class="lambda">lambda </span> command <code>ext x </code>works
+ like λ<sub>x</sub> if the both the flags <i>eta </i>
+ and <i>xapp </i> are off.
+ With <i>xapp </i> on, constant applications will be extracted by
+ <code>(iii) </code> instead of <code>(ii)</code>.
+ <p>
+ λ<sub>x</sub> maps every polynomial φ(x) in <code>A[x]</code>
+ to an element of <code>f</code> of <code>A </code> such that <code>(f x)</code> =<sub>x</sub> φ(x).
+ So the existence of <code>f</code> is assured.
+ <p>
+ We must now show that <code>f</code> is unique. We first prove that
+ <pre>
+ (*) φ(x) =<sub>x</sub> ψ(x) implies λ<sub>x</sub>(φ(x)) = λ<sub>x</sub>(ψ(x)).
+ </pre>
+ That is, if two polynomials are equal in <code>A[x]</code>, their lambda abstractions are equal in <code>A </code>.
+ <p>
+ To prove this assertion, we show that the equality
+ <pre>
+ λ<sub>x</sub>(φ(x)) = λ<sub>x</sub>(ψ(x))
+ </pre>
+ defines an equivalence relation over the polynomials in
+ <code>A[x]</code> that satisfies
+ <code>(i<sub>x</sub>)</code>,
+ <code>(ii<sub>x</sub>)</code>, and
+ <code>(iii<sub>x</sub>)</code> above,
+ when certain additional universally quantified equations in
+ <code>A </code> are assumed.
+ Since =<sub>x</sub> is assumed to be the smallest (finest grained)
+ such equivalence, the assertion must hold.
+ <p>
+ (Adding such equations can only unify partitions of an equivalence
+ relation, but never divide.
+ That is, two members of <code>|A[x]|</code> (or <code>|A|</code>)
+ that were equal without the additional equations will still be equal
+ with them. So if =<sub>x</sub> was the finest equivalence relation
+ satisfying
+ <code>(i<sub>x</sub>)</code>,
+ <code>(ii<sub>x</sub>)</code>, and
+ <code>(iii<sub>x</sub>)</code>
+ before the addition, it will remain such after the addition.)
+ <p>
+ So we must have, for all polynomials
+ <code>α(x), β(x), γ(x)</code> in <code>A[x]</code>:
+ <pre>
+ (1''') λ<sub>x</sub>I(α(x)) = λα(x)
+ (2''') λ<sub>x</sub>K(α(x))(β(x)) = λ<sub>x</sub>(α(x))
+ (3''') λ<sub>x</sub>S(α(x))(β(x))(γ(x)) = λ<sub>x</sub>(α(x))(γ(x))((β(x))(γ(x))
+ </pre>
+ For uniqueness of <code>f</code>, suppose we have
+ <pre>
+ (g x) =<sub>x</sub> φ(x).
+ </pre>
+ By (*) this implies that for all <code>g</code>∈<code>A </code>
+ <pre>
+ λ<sub>x</sub>(g x) = λ<sub>x</sub>φ(x) = f.
+ </pre>
+ So we impose the condition, for all <code>g</code>∈<code>A </code>
+ <pre>
+ (4''') λ<sub>x</sub>(g x) = g.
+ </pre>
+ We would like to remove the restriction on <code>(iii)</code> above.
+ That is, for all <code>f</code>, and <code>g</code>∈<code>A </code>,
+ <code>λ<sub>x</sub>(f g) </code> using (iii)
+ must equal <code>λ<sub>x</sub>(f g) </code> using (ii).
+ So we have:
+ <pre>
+ (5''') S(K f)(K g) = K(f g)
+ </pre>
+ Let
+ <pre>
+ a = λ<sub>x</sub>α(x)
+ b = λ<sub>x</sub>β(x)
+ c = λ<sub>x</sub>γ(x)
+ </pre>
+ If we replace
+ <code>α(x)</code>,
+ <code>β(x)</code>,
+ and <code>γ(x)</code>
+ in (1'''), (2'''), and (3''') above with:
+ <code>(a x)</code>, <code>(b x)</code>, and <code>(c x)</code>
+ then we can use the
+ <span class="lambda">lambda </span>
+ command <code>ext x </code>
+ to calculate the corresponding equations in <code>A </code>
+ <pre>
+ (1'') S(K I)a = a
+ (2'') S(S(K K)a)b = a
+ (3'') S(S(S(K S)a)b)c = S(S a c)(S b c)
+ (4'') S(K g)I = g
+ (5'') S(K f)(K g) = K(f g)
+ </pre>
+ Such a
+ <span class="lambda">lambda </span>
+ session might look like:
+ <div class="lx">
+ <pre>
+ << ext x I(a x)
+ S(K I)a
+ << ext x (a x)
+ a
+ << ext x K(a x)(b x)
+ S(S(K K)a)b
+ << ext x (a x)
+ a
+ << ext x S(a x)(b x)(c x)
+ S(S(S(K S)a)b)c
+ << ext x (a x)(c x)((b x)(c x))
+ S(S a c)(S b c)
+ << ext x g (I x)
+ S(K g)I
+ <<
+ </pre>
+ </div>
+ These equations are universally quantified in
+ <code>α(x)</code>,
+ <code>β(x)</code>,
+ <code>γ(x)</code>,
+ <code>f</code>, and
+ <code>g</code>.
+ Because every occurrence of the polynomials are bound by
+ <code>λ<sub>x</sub></code>, and
+ in light of <code>(4''')</code>, every expression
+ <code>a</code>∈<code>A </code>
+ has a corresponding polynomial in <code>A[x]</code>:
+ <code>(a x)</code>.
+ So instead of qualifying the equations in terms of polynomials
+ in <code>|A[x]|</code>, we can qualify them in terms of
+ elements in <code>|A|</code>.
+ So we have
+ <pre>
+ (1') ∀a.S(K I)a = a
+ (2') ∀a.∀b.S(S(K K)a)b = a
+ (3') ∀a.∀b.∀c.S(S(S(K S)a)b)c = S(S a c)(S b c)
+ (4') ∀g.S(K g)I = g
+ (5') ∀f.∀g.S(K f)(K g) = K(f g)
+ </pre>
+ Using the
+ <span class="lambda">lambda </span>
+ <code>ext ^ </code> command, we can turn these equations
+ into identities in <code>A</code>
+ <pre>
+ (1i) S(K I) = I
+ (2i) S(K S)(S(K K)) = K
+ (3i) S(K(S(K S)))(S(K S)(S(K S))) = S(S(K S)(S(K K)(S(K S)(S(K(S(K S)))S))))(K S)
+ (4i) S(S(K S)K)(K I) = I
+ (5i) S(S(K S)(S(K K)(S(K S)K)))(K K) = S(K K)
+ </pre>
+ Such a
+ <span class="lambda">lambda </span>
+ session might look like:
+ <div class="lx">
+ <pre>
+ << ext ^ ^a.^x.I(a x)
+ S(K I)
+ << ext ^ ^a.^x.a x
+ I
+ << ext ^ ^a.^b.^x.K(a x)(b x)
+ S(K S)(S(K K))
+ << ext ^ ^a.^b.^x.a x
+ K
+ << ext ^ ^a.^b.^c.^x.S(a x)(b x)(c x)
+ S(K(S(K S)))(S(K S)(S(K S)))
+ << ext ^ ^a.^b.^c.^x.(a x)(c x)((b x)(c x))
+ S(S(K S)(S(K K)(S(K S)(S(K(S(K S)))S))))(K S)
+ << ext ^ ^g.S(K g)I
+ S(S(K S)K)(K I)
+ << ext ^ ^g.g
+ I
+ << ext ^ ^f.^g.S(K f)(K g)
+ S(S(K S)(S(K K)(S(K S)K)))(K K)
+ << ext ^ ^f.^g.K(f g)
+ S(K K)
+ <<
+ </pre>
+ </div>
+ Let's check our work:
+ <div class="lx">
+ <pre>
+ << load definitions
+ << S(K I) a x
+ ==> ((S(K I)) a) x
+ ====>a x
+ << I a x
+ ==> (I a) x
+ ====>a x
+ << S(K S)(S(K K)) a b x
+ ==> ((((S(K S))(S(K K))) a) b) x
+ ====>a x
+ << K a b x
+ ==> ((K a) b) x
+ ====>a x
+ << S(K(S(K S)))(S(K S)(S(K S))) a b c x
+ ==> (((((S(K(S(K S))))((S(K S))(S(K S)))) a) b) c) x
+ ====>a x(c x)(b x(c x))
+ << S(S(K S)(S(K K)(S(K S)(S(K(S(K S)))S))))(K S) a b c x
+ ==> (((((S((S(K S))((S(K K))((S(K S))((S(K(S(K S)))) S)))))(K S)) a) b) c) x
+ ====>a x(c x)(b x(c x))
+ << S(S(K S)K)(K I) g x
+ ==> (((S((S(K S)) K))(K I)) g) x
+ ====>g x
+ << I g x
+ ==> (I g) x
+ ====>g x
+ << S(S(K S)(S(K K)(S(K S)K)))(K K) f g x
+ ==> ((((S((S(K S))((S(K K))((S(K S)) K))))(K K)) f) g) x
+ ====>f g
+ << S(K K) f g x
+ ==> (((S(K K)) f) g) x
+ ====>f g
+ <<
+
+ </pre>
+ </div>
+ <h2>Proposition 3 Curry Algebras ≡ Lambda Calculus.</h2>
+ A Curry Algebra is equivalent to the lambda calculus.
+ <div class="proof">Proof</div>
+ We have the following equations:
+ <pre>
+ (1) I = λ<sub>x</sub>x
+ (2) K = λ<sub>x</sub>λ<sub>y</sub>x
+ (3) S = λ<sub>x</sub>λ<sub>y</sub>λ<sub>z</sub>x z(y z)
+ (4) ∀f.f = λ<sub>x</sub>f x = f
+ (5) ∀φ(x).∀a.φ(a) = (λ<sub>x</sub>φ(x))a
+ </pre>
+ Condition (5) is true because we have by Proposition 2,
+ <pre>
+ (λ<sub>x</sub>φ(x))x = φ(x)
+ </pre>
+ and by the substitution property, we can substitute <code>a∈A </code> for the unbound occurrences of <code>x </code> on both sides of the equation.
+ <h2>Proposition 4 Fixed Points in Curry Algebras.</h2>
+ Every element of a Curry Algebra has a fixed point.
+ <div class="proof">Proof</div>
+ The fixed point is
+ <pre>
+ Y g,
+ </pre>
+ where
+ <pre>
+ Y = λ<sub>g</sub>((λ<sub>x</sub>g(x x))(λ<sub>x</sub>g(x x))).
+ </pre>
+ We have
+ <pre>
+ Y f
+ = (λ<sub>x</sub>f(x x))(λ<sub>x</sub>f(x x))
+ = f((λ<sub>x</sub>f(x x))(λ<sub>x</sub>f(x x)))
+ = f(Y f)
+ </pre>
+ so <code>(Y f) </code> is indeed a fixed point of f.
+ </body>
+ </html>
Index: llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/trans_xml_for_cat.pl
diff -c /dev/null llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/trans_xml_for_cat.pl:1.1
*** /dev/null Mon Dec 29 11:37:49 2003
--- llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/trans_xml_for_cat.pl Mon Dec 29 11:37:39 2003
***************
*** 0 ****
--- 1,239 ----
+ #!/usr/bin/perl -w -I ./
+ #####!/usr/bin/perl -T -w -I ./
+ use IO::File;
+
+ # stdin: html
+ # stdout: html with toc
+ # replace a line with "<TOC>" with table of contents
+ # generated from header elements: <h1> <h2> etc.
+ # surrounds each head element with <a name=> element
+
+ ##open (TOC, "+>DOC");
+ ##open (DOC, "+>TOC");
+ $toc = IO::File->new_tmpfile();
+ $doc = IO::File->new_tmpfile();
+
+ print ($toc "<center><b><font size=+2>Table of Contents</font></b></center>\n");
+
+ $level = 0;
+ #@paranums;
+
+ while ( <STDIN> )
+ {
+ ###if( /\s*<[hH](\d+)>([^<]*)<\/[hH]\1>/ )
+ if( /\s*<([hHlL])(\d+)>([^<]*)<\/\1\2>/ )
+ {
+ my $hdr = $1;
+ my $lvl = $2;
+ my $txt = $3;
+ if( $lvl < 1 ) { $lvl = 1; }
+ if( $lvl > $level )
+ {
+ $paranums[$lvl-1] = 0;
+ print ($toc "<dl>\n");
+ }elsif( $lvl < $level )
+ {
+ my $ndx;
+ for( $ndx=0; $lvl+$ndx < $level; $ndx++ )
+ {
+ print ($toc "</dl>\n");
+ }
+ }
+ $level = $lvl;
+ $paranums[$level-1] += 1;
+
+ my $paraname = "";
+ my $dot = "";
+ for ( $ndx=0; $ndx<$level; $ndx++ )
+ {
+ $paraname = $paraname . $dot . $paranums[$ndx];
+ $dot = ".";
+ }
+ if( "h" eq $hdr || "H" eq $hdr )
+ {
+ print ($doc "<a name=\"P$paraname\"><H$lvl>$paraname $txt</H$lvl></a>\n");
+ print ($toc "<dt><a href=\"#P$paraname\">$paraname $txt</a></dt>\n");
+ }else{
+ my @txtprt = split(/;/,$txt,2);
+ if( @txtprt == 2 )
+ {
+ print ($toc "<dt><a href=\"$txtprt[0]\">$paraname $txtprt[1]</a></dt>\n");
+ }else{
+ print ($toc "<dt>$paraname $txtprt[0]</H$lvl></dt>\n");
+ }
+ }
+ }else{
+ s/<header>([^<]*)<\/header>/<table class="header"><tr><td class="header">$1<\/td><\/tr><\/table>/g;
+ s/<cat>([^<]*)<\/cat>/<span class="cat">$1<\/span>/g;
+ s/<func>([^<]*)<\/func>/<span class="func">$1<\/span>/g;
+ s/<map>([^<]*)<\/map>/<span class="map">$1<\/span>/g;
+ s/<set>([^<]*)<\/set>/<span class="set">$1<\/span>/g;
+ s/<obj>([^<]*)<\/obj>/<span class="object">$1<\/span>/g;
+ s/<CAT>([^<]*)<\/CAT>/<span class="category">$1<\/span>/g;
+ s/<FAM>([^<]*)<\/FAM>/<span class="family">$1<\/span>/g;
+ s/<FUNC>([^<]*)<\/FUNC>/<span class="functor">$1<\/span>/g;
+
+ s/&arrow;/→/g;
+ s/&rarrow;/←/g; #reverse arrow
+ s/&monic;/↦/g; #monic arrow
+ s/&equalize;/↣/g; #equalizer arrow
+ #s/&eqlz;/∥/g; #equalizer op double bar
+ s/&eqlz;/≑/g; #equalizer op geometric equality
+
+ #s/&cover;/↠/g; #cover arrow
+ s/&cover;/−⊳/g; #cover arrow
+ #s/&cover;/⇾/g; #cover arrow
+ s/&isoarrow;/⥲/g; #isomorphism arrow
+
+ s/&darrow;/⇒/g; #double arrow
+ s/&implies;/⇒/g; #double arrow
+
+ s/&rdarrow;/⇐/g; #reverse double arrow
+ s/&impliedby;/⇐/g; #reverse double arrow
+
+ s/⇔/⇔/g; #if and only if
+
+ s/&box;/□/g; #source or target operator
+ s/&opbox;/▣/g; #opposite source or target op
+ s/&circle;/○/g; #circle
+ s/&cring;/⊚/g; #circle ring
+ s/&bullseye;/◎/g; #circle ring
+
+ s/&role;/○/g; #role
+ s/&roleop;/◎/g; #opposite role
+
+ s/∀/∀/g;
+ s/∃/∃/g;
+ s/¬exist;/∄/g;
+ s/¬equal;/≠/g;
+ s/&isomorphic;/≃/g;
+
+ s/&mul;/<font face="sans-serif">X<\/font>/g;
+ s/&add;/+/g;
+
+ s/∏/∏/g; # n-ary
+ s/∐/∐/g; # n-ary
+ s/∑/∑/g; # n-ary
+
+ s/∅/∅/g;
+ s/&incr;/∆/g;
+ s/&nable;/∇/g;
+ s/∈/∈/g;
+ s/∉/∉/g;
+ s/&smallisin;/∊/g;
+ s/&contains;/∋/g;
+ s/¬contains;/∌/g;
+ s/&smallcontains;/∍/g;
+ s/&QED;/∎/g;
+
+ s/&slash;/∕/g;
+ s/∖/∖/g;
+ s/&asterisk;/∗/g;
+ s/&compose;/∘/g;
+ s/&dcomp;/ /g;
+ s/•/∙/g;
+ s/&infinity;/∞/g;
+
+ s/&logicaland;/∧/g; s/&land;/∧/g;
+ s/&logicalor;/∨/g; s/&lor;/∨/g;
+ s/∩/∩/g; s/&intersection;/∩/g;
+ s/∪/∪/g; s/&union;/∪/g;
+
+ s/&bar;/∣/g;
+ s/⊂/⊂/g;
+ s/⊃/⊃/g;
+ s/&direq;/⇉/g; #directed equality, venturi tube
+ #s/&direq;/≔/g; # :=, directed equality, venturi tube
+ s/&colonequal;/≕/g; # :=
+ s/&equalcolon;/≕/g; # =;
+
+ s/°ree;/°/g;
+ s/·/·/g;
+ s/&inverse;/⁻¹/g;
+ s/&nland;/⋀/g;
+ s/&nlor;/⋁/g;
+ s/&nintersection;/⋂/g;
+ s/⩃/⋂/g;
+ s/&nunion;/⋃/g;
+ s/⩂/⋃/g;
+ s/⋄/⋄/g;
+ s/˙/⋅/g;
+
+ s/♯/<sup>#<\/sup>/g;
+ s/&wbullet;/◦/g;
+ s/&whitebullet;/◦/g;
+
+ s/Α/Α/g;
+ s/Β/Β/g;
+ s/Γ/Γ/g;
+ s/Δ/Δ/g;
+ s/Ε/Ε/g;
+ s/Ζ/Ζ/g;
+ s/Η/Η/g;
+ s/Θ/Θ/g;
+ s/Ι/Ι/g;
+ s/Κ/Κ/g;
+ s/Λ/Λ/g;
+ s/Μ/Μ/g;
+ s/Ν/Ν/g;
+ s/Ξ/Ξ/g;
+ s/Ο/Ο/g;
+ s/Π/Π/g;
+ s/Ρ/Ρ/g;
+ s/&Stigma;/΢/g;
+ s/Σ/Σ/g;
+ s/Τ/Τ/g;
+ s/Υ/Υ/g;
+ s/Φ/Φ/g;
+ s/Χ/Χ/g;
+ s/Ψ/Ψ/g;
+ s/Ω/Ω/g;
+
+ s/α/α/g;
+ s/β/β/g;
+ s/γ/γ/g;
+ s/δ/δ/g;
+ s/ε/ε/g;
+ s/ζ/ζ/g;
+ s/η/η/g;
+ s/θ/θ/g;
+ s/ι/ι/g;
+ s/κ/κ/g;
+ s/λ/λ/g;
+ s/μ/μ/g;
+ s/ν/ν/g;
+ s/ξ/ξ/g;
+ s/ο/ο/g;
+ s/π/π/g;
+ s/ρ/ρ/g;
+ s/&stigma;/ς/g;
+ s/σ/σ/g;
+ s/τ/τ/g;
+ s/υ/υ/g;
+ s/φ/φ/g;
+ s/χ/χ/g;
+ s/ψ/ψ/g;
+ s/ω/ω/g;
+ print $doc $_;
+ }
+ }
+ print ($toc "</dl>\n");
+
+ seek ($toc,0,0);
+ seek ($doc,0,0);
+
+ while (<$doc>)
+ {
+ if( /<[Tt][Oo][Cc]\/?>/ )
+ {
+ while ( <$toc> )
+ {
+ print;
+ }
+ }else{
+ print;
+ }
+ }
+ close $toc;
+ close $doc;
+ #unlink TOC, DOC;
Index: llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/user_manual_style.css
diff -c /dev/null llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/user_manual_style.css:1.1
*** /dev/null Mon Dec 29 11:37:49 2003
--- llvm/test/Programs/MultiSource/Applications/lambda-0.1.3/docs/user_manual_style.css Mon Dec 29 11:37:39 2003
***************
*** 0 ****
--- 1,112 ----
+ <style>
+ p.text, div.text {
+ margin-left: 0em;
+ margin-top: 1em;
+ }
+ table.header {
+ margin: auto;
+ }
+ td.header {
+ color: blue;
+ font-family: sans-serif;
+ font-weight: bold;
+ font-size: x-large;
+ }
+ div.header {
+ color: blue;
+ font-family: sans-serif;
+ font-weight: bold;
+ margin-top: 1em;
+ }
+ pre.diagramuml, code.diagramuml, div.diagramsch{
+ color: darkgreen;
+ }
+ pre.diagramsch, code.diagramsch, div.diagramsch{
+ color: brown;
+ }
+ div.term {
+ color: blue;
+ font-family: sans-serif;
+ font-weight: bold;
+ margin-top: 1em;
+ }
+ div.define {
+ color: black;
+ margin-top: 1em;
+ margin-left: 0em;
+ }
+ div.quote {
+ color: color;
+ margin-top: 1em;
+ margin-left: 4em;
+ }
+ DT {
+ font-weight: bold;
+ }
+ span.set {
+ font-family: sans-serif;
+ font-weight: bold;
+ }
+ span.cat {
+ font-family: "zapf chancery" cursive;
+ font-weight: bold;
+ font-size: larger;
+ }
+ span.func {
+ font-family: "zapf chancery" cursive;
+ font-weight: bold;
+ font-size: larger;
+ }
+ span.map {
+ }
+ span.object {
+ }
+ span.category {
+ font-family: "zapf chancery" cursive;
+ font-style: italic;
+ font-weight: bold;
+ font-size: larger;
+ }
+ span.family {
+ font-family: "zapf chancery" cursive;
+ font-style: italic;
+ font-weight: bold;
+ font-size: larger;
+ }
+ span.functor {
+ font-family: "zapf chancery" cursive;
+ font-style: italic;
+ font-weight: bold;
+ font-size: larger;
+ }
+ .copying {
+ margin: 10 10 10 10;
+ text-align: justify;
+ font-size: smaller;
+ }
+ h1 {
+ font-size: x-large;
+ }
+ div.lx {
+ margin-top: 1em;
+ margin-right: 24em;
+ margin-bottom: 1em;
+ margin-left: 4em;
+ border: 1px solid;
+ background-color: peachpuff;
+ color: sienna;
+ }
+ span.lambda {
+ font-family: sans-serif;
+ font-weight: bold;
+ }
+ div.proof {
+ font-family: sans-serif;
+ font-weight: bold;
+ }
+ div.lambdacmd {
+ font-family: monospace;
+ font-weight: bold;
+ font-size: large;
+ }
+ </style>
More information about the llvm-commits
mailing list