LambdaShell (empty) → 0.9

raw patch · 13 files changed

+2624/−0 lines, 13 filesdep +Shellacdep +Shellac-readlinedep +basebuild-type:Customsetup-changed

Dependencies added: Shellac, Shellac-readline, base, haskell98, mtl, parsec, readline

Files

• LICENSE +340/−0
• LambdaShell.cabal +32/−0
• README +123/−0
• Setup.hs +3/−0
• prelude.lam +155/−0
• src/CPS.hs +198/−0
• src/Env.hs +45/−0
• src/Lambda.hs +382/−0
• src/LambdaCmdLine.hs +302/−0
• src/LambdaParser.hs +253/−0
• src/LambdaShell.hs +358/−0
• src/Version.hs +409/−0
• src/main.hs +24/−0

@@ -0,0 +1,340 @@+		    GNU GENERAL PUBLIC LICENSE+		       Version 2, June 1991++ Copyright (C) 1989, 1991 Free Software Foundation, Inc.+                       51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.++			    Preamble++  The licenses for most software are designed to take away your+freedom to share and change it.  By contrast, the GNU General Public+License is intended to guarantee your freedom to share and change free+software--to make sure the software is free for all its users.  This+General Public License applies to most of the Free Software+Foundation's software and to any other program whose authors commit to+using it.  (Some other Free Software Foundation software is covered by+the GNU Library General Public License instead.)  You can apply it to+your programs, too.++  When we speak of free software, we are referring to freedom, not+price.  Our General Public Licenses are designed to make sure that you+have the freedom to distribute copies of free software (and charge for+this service if you wish), that you receive source code or can get it+if you want it, that you can change the software or use pieces of it+in new free programs; and that you know you can do these things.++  To protect your rights, we need to make restrictions that forbid+anyone to deny you these rights or to ask you to surrender the rights.+These restrictions translate to certain responsibilities for you if you+distribute copies of the software, or if you modify it.++  For example, if you distribute copies of such a program, whether+gratis or for a fee, you must give the recipients all the rights that+you have.  You must make sure that they, too, receive or can get the+source code.  And you must show them these terms so they know their+rights.++  We protect your rights with two steps: (1) copyright the software, and+(2) offer you this license which gives you legal permission to copy,+distribute and/or modify the software.++  Also, for each author's protection and ours, we want to make certain+that everyone understands that there is no warranty for this free+software.  If the software is modified by someone else and passed on, we+want its recipients to know that what they have is not the original, so+that any problems introduced by others will not reflect on the original+authors' reputations.++  Finally, any free program is threatened constantly by software+patents.  We wish to avoid the danger that redistributors of a free+program will individually obtain patent licenses, in effect making the+program proprietary.  To prevent this, we have made it clear that any+patent must be licensed for everyone's free use or not licensed at all.++  The precise terms and conditions for copying, distribution and+modification follow.++		    GNU GENERAL PUBLIC LICENSE+   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION++  0. This License applies to any program or other work which contains+a notice placed by the copyright holder saying it may be distributed+under the terms of this General Public License.  The "Program", below,+refers to any such program or work, and a "work based on the Program"+means either the Program or any derivative work under copyright law:+that is to say, a work containing the Program or a portion of it,+either verbatim or with modifications and/or translated into another+language.  (Hereinafter, translation is included without limitation in+the term "modification".)  Each licensee is addressed as "you".++Activities other than copying, distribution and modification are not+covered by this License; they are outside its scope.  The act of+running the Program is not restricted, and the output from the Program+is covered only if its contents constitute a work based on the+Program (independent of having been made by running the Program).+Whether that is true depends on what the Program does.++  1. You may copy and distribute verbatim copies of the Program's+source code as you receive it, in any medium, provided that you+conspicuously and appropriately publish on each copy an appropriate+copyright notice and disclaimer of warranty; keep intact all the+notices that refer to this License and to the absence of any warranty;+and give any other recipients of the Program a copy of this License+along with the Program.++You may charge a fee for the physical act of transferring a copy, and+you may at your option offer warranty protection in exchange for a fee.++  2. You may modify your copy or copies of the Program or any portion+of it, thus forming a work based on the Program, and copy and+distribute such modifications or work under the terms of Section 1+above, provided that you also meet all of these conditions:++    a) You must cause the modified files to carry prominent notices+    stating that you changed the files and the date of any change.++    b) You must cause any work that you distribute or publish, that in+    whole or in part contains or is derived from the Program or any+    part thereof, to be licensed as a whole at no charge to all third+    parties under the terms of this License.++    c) If the modified program normally reads commands interactively+    when run, you must cause it, when started running for such+    interactive use in the most ordinary way, to print or display an+    announcement including an appropriate copyright notice and a+    notice that there is no warranty (or else, saying that you provide+    a warranty) and that users may redistribute the program under+    these conditions, and telling the user how to view a copy of this+    License.  (Exception: if the Program itself is interactive but+    does not normally print such an announcement, your work based on+    the Program is not required to print an announcement.)++These requirements apply to the modified work as a whole.  If+identifiable sections of that work are not derived from the Program,+and can be reasonably considered independent and separate works in+themselves, then this License, and its terms, do not apply to those+sections when you distribute them as separate works.  But when you+distribute the same sections as part of a whole which is a work based+on the Program, the distribution of the whole must be on the terms of+this License, whose permissions for other licensees extend to the+entire whole, and thus to each and every part regardless of who wrote it.++Thus, it is not the intent of this section to claim rights or contest+your rights to work written entirely by you; rather, the intent is to+exercise the right to control the distribution of derivative or+collective works based on the Program.++In addition, mere aggregation of another work not based on the Program+with the Program (or with a work based on the Program) on a volume of+a storage or distribution medium does not bring the other work under+the scope of this License.++  3. You may copy and distribute the Program (or a work based on it,+under Section 2) in object code or executable form under the terms of+Sections 1 and 2 above provided that you also do one of the following:++    a) Accompany it with the complete corresponding machine-readable+    source code, which must be distributed under the terms of Sections+    1 and 2 above on a medium customarily used for software interchange; or,++    b) Accompany it with a written offer, valid for at least three+    years, to give any third party, for a charge no more than your+    cost of physically performing source distribution, a complete+    machine-readable copy of the corresponding source code, to be+    distributed under the terms of Sections 1 and 2 above on a medium+    customarily used for software interchange; or,++    c) Accompany it with the information you received as to the offer+    to distribute corresponding source code.  (This alternative is+    allowed only for noncommercial distribution and only if you+    received the program in object code or executable form with such+    an offer, in accord with Subsection b above.)++The source code for a work means the preferred form of the work for+making modifications to it.  For an executable work, complete source+code means all the source code for all modules it contains, plus any+associated interface definition files, plus the scripts used to+control compilation and installation of the executable.  However, as a+special exception, the source code distributed need not include+anything that is normally distributed (in either source or binary+form) with the major components (compiler, kernel, and so on) of the+operating system on which the executable runs, unless that component+itself accompanies the executable.++If distribution of executable or object code is made by offering+access to copy from a designated place, then offering equivalent+access to copy the source code from the same place counts as+distribution of the source code, even though third parties are not+compelled to copy the source along with the object code.++  4. You may not copy, modify, sublicense, or distribute the Program+except as expressly provided under this License.  Any attempt+otherwise to copy, modify, sublicense or distribute the Program is+void, and will automatically terminate your rights under this License.+However, parties who have received copies, or rights, from you under+this License will not have their licenses terminated so long as such+parties remain in full compliance.++  5. You are not required to accept this License, since you have not+signed it.  However, nothing else grants you permission to modify or+distribute the Program or its derivative works.  These actions are+prohibited by law if you do not accept this License.  Therefore, by+modifying or distributing the Program (or any work based on the+Program), you indicate your acceptance of this License to do so, and+all its terms and conditions for copying, distributing or modifying+the Program or works based on it.++  6. Each time you redistribute the Program (or any work based on the+Program), the recipient automatically receives a license from the+original licensor to copy, distribute or modify the Program subject to+these terms and conditions.  You may not impose any further+restrictions on the recipients' exercise of the rights granted herein.+You are not responsible for enforcing compliance by third parties to+this License.++  7. If, as a consequence of a court judgment or allegation of patent+infringement or for any other reason (not limited to patent issues),+conditions are imposed on you (whether by court order, agreement or+otherwise) that contradict the conditions of this License, they do not+excuse you from the conditions of this License.  If you cannot+distribute so as to satisfy simultaneously your obligations under this+License and any other pertinent obligations, then as a consequence you+may not distribute the Program at all.  For example, if a patent+license would not permit royalty-free redistribution of the Program by+all those who receive copies directly or indirectly through you, then+the only way you could satisfy both it and this License would be to+refrain entirely from distribution of the Program.++If any portion of this section is held invalid or unenforceable under+any particular circumstance, the balance of the section is intended to+apply and the section as a whole is intended to apply in other+circumstances.++It is not the purpose of this section to induce you to infringe any+patents or other property right claims or to contest validity of any+such claims; this section has the sole purpose of protecting the+integrity of the free software distribution system, which is+implemented by public license practices.  Many people have made+generous contributions to the wide range of software distributed+through that system in reliance on consistent application of that+system; it is up to the author/donor to decide if he or she is willing+to distribute software through any other system and a licensee cannot+impose that choice.++This section is intended to make thoroughly clear what is believed to+be a consequence of the rest of this License.++  8. If the distribution and/or use of the Program is restricted in+certain countries either by patents or by copyrighted interfaces, the+original copyright holder who places the Program under this License+may add an explicit geographical distribution limitation excluding+those countries, so that distribution is permitted only in or among+countries not thus excluded.  In such case, this License incorporates+the limitation as if written in the body of this License.++  9. The Free Software Foundation may publish revised and/or new versions+of the General Public License from time to time.  Such new versions will+be similar in spirit to the present version, but may differ in detail to+address new problems or concerns.++Each version is given a distinguishing version number.  If the Program+specifies a version number of this License which applies to it and "any+later version", you have the option of following the terms and conditions+either of that version or of any later version published by the Free+Software Foundation.  If the Program does not specify a version number of+this License, you may choose any version ever published by the Free Software+Foundation.++  10. If you wish to incorporate parts of the Program into other free+programs whose distribution conditions are different, write to the author+to ask for permission.  For software which is copyrighted by the Free+Software Foundation, write to the Free Software Foundation; we sometimes+make exceptions for this.  Our decision will be guided by the two goals+of preserving the free status of all derivatives of our free software and+of promoting the sharing and reuse of software generally.++			    NO WARRANTY++  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,+REPAIR OR CORRECTION.++  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE+POSSIBILITY OF SUCH DAMAGES.++		     END OF TERMS AND CONDITIONS++	    How to Apply These Terms to Your New Programs++  If you develop a new program, and you want it to be of the greatest+possible use to the public, the best way to achieve this is to make it+free software which everyone can redistribute and change under these terms.++  To do so, attach the following notices to the program.  It is safest+to attach them to the start of each source file to most effectively+convey the exclusion of warranty; and each file should have at least+the "copyright" line and a pointer to where the full notice is found.++    <one line to give the program's name and a brief idea of what it does.>+    Copyright (C) <year>  <name of author>++    This program 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.++    This program 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 this program; if not, write to the Free Software+    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA+++Also add information on how to contact you by electronic and paper mail.++If the program is interactive, make it output a short notice like this+when it starts in an interactive mode:++    Gnomovision version 69, Copyright (C) year name of author+    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.+    This is free software, and you are welcome to redistribute it+    under certain conditions; type `show c' for details.++The hypothetical commands `show w' and `show c' should show the appropriate+parts of the General Public License.  Of course, the commands you use may+be called something other than `show w' and `show c'; they could even be+mouse-clicks or menu items--whatever suits your program.++You should also get your employer (if you work as a programmer) or your+school, if any, to sign a "copyright disclaimer" for the program, if+necessary.  Here is a sample; alter the names:++  Yoyodyne, Inc., hereby disclaims all copyright interest in the program+  `Gnomovision' (which makes passes at compilers) written by James Hacker.++  <signature of Ty Coon>, 1 April 1989+  Ty Coon, President of Vice++This General Public License does not permit incorporating your program into+proprietary programs.  If your program is a subroutine library, you may+consider it more useful to permit linking proprietary applications with the+library.  If this is what you want to do, use the GNU Library General+Public License instead of this License.

@@ -0,0 +1,32 @@+Name:            LambdaShell+Version:         0.9+License:         GPL+License-file:    LICENSE+Author:          Robert Dockins+Maintainer:      robdockins AT fastmail DOT fm+Stability:       Beta+Category:        Compilers/Interpreters+Synopsis:        Simple shell for evaluating lambda expressions+Description:+  The lambda shell is a feature-rich shell environment and command-line tool for+  evaluating terms of the pure, untyped lambda calculus.  The Lambda+  Shell builds on the shell creation framework Shellac, and showcases+  most of Shellac's features.+Build-Depends:+    base >= 1.0,+    haskell98 >= 1.0,+    parsec >= 1.0,+    mtl >= 1.0,+    readline >= 1.0,+    Shellac >= 0.9,+    Shellac-readline >= 0.9++Executable:      lambdaShell+Main-Is:         main.hs+Hs-Source-Dirs:+    src+Extensions:+    MultiParamTypeClasses+Extra-libraries:+    readline+GHC-Options: -O

@@ -0,0 +1,123 @@++  The Lambda Shell+-==================-++== What is it?++It is a feature-rich shell environment and command-line tool for+evaluating terms of the pure, untyped lambda calculus.  The Lambda+Shell builds on the shell creation framework Shellac, and showcases+most of Shellac's features.++Features:+  -- evalutate lambda terms directly from the shell prompt using+     normal or applicative order.  In normal order, one can evaluate+     to normal form, head normal form, or weak head normal form.+  -- define aliases for lambda terms using a top level, non-recursive+     'let' construct.+  -- Show traces of term evaluation, or dump the trace to a file+  -- Count the number of reductions when evaluating terms+  -- test two lambda terms for confluence (that is; if two+     terms, when evaluated to normal form, are alpha equivalant)+  -- programs can be entered from the command line (using the -e option)+     or piped into stdin (using the -s option)+  -- perform Continuation Passing Style (CPS) transforms on terms before+     evaluation using the syntax  '[[ five ]]'+++An example session:+-------------------------------++$ lambdaShell++The Lambda Shell, version 0.3+Copyright 2005-2006, Robert Dockins+++The Lambda Shell comes with ABSOLUTELY NO WARRANTY; for details+type ':nowarranty'.  This is free software, and you are welcome to+redistribute it under certain conditions; type ':gpl'+for details++> (\x y. x) (\a. a) (\b. b)+\a. a+> :load prelude.lam+> :show four+four = succ three+> four+\f x. f (f (f (f x)))+> mul two three+\f x. f (f (f (f (f (f x)))))+> let x = plus six two+> x == eight+equal+> x == nine+not equal+> one+\f x. f x+> [[ one ]]+\f k. k (\x k_0. f x k_0)+> :showcount+showcount on+> sub seven two+\f x. f (f (f (f (f x))))+<<90 reductions>>+> let l = insertSort (cons two (cons three (cons one nil)))+> index zero l+one+<<463 reductions>>+> index one l+two+<<2135 reductions>>+> index two l+three+<<5720 reductions>>+> :quit+++-----------------------------------------------+++== Why do I care?++Because you are a lambda calculus nut, and you just can't get enough.+Or, the lambda shell could be a worthwhile teaching tool.  The command+line features (especially confluence testing) could lend themselves to+automatic grading.  Also, the lambda shell is a good example of+how to write a shell using Shellac.++++== How is it licensed?++The Lambda Shell is licensed under the GNU GPL version 2.  See+the LICENSE file for details.++++== How do I build it?++The lambda shell uses a Cabal build system.  The follwing+commands assume you have a haskell interpreter in your system+path named 'runhaskell'.  All commands are run from+this directory.  If Shellac is installed as a user package, you+will need to add the '--user' flag to your configure commands.++To install for the whole system:++runhaskell Setup.hs configure+runhaskell Setup.hs build+runhaskell Setup.hs install++To install for a single user:++runhaskell Setup.hs configure --prefix=/home/<username>+runhaskell Setup.hs build+runhaskell Setup.hs install --user+++== Who is responsable for this mess?++You can send bug reports, rants and comments to:++  Robert Dockins <robdockins AT fastmail.fm>

@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,155 @@+# the church encoding for booleans+true    = \t f. t;+false   = \t f. f;+if      = \b x y. b x y;+not     = \x.   if x false true;+and     = \x y. if x y false;+or      = \x y. if x true y;+xor     = \x y. if x (not y) y;++# the church encoding for peano numbers+zero    = \f x. x;+succ    = \n f x. f (n f x);+pred    = \n f x. n (\g h. h (g f)) (\u. x) (\u. u);++# addition, subtraction and multiplication+plus    = \m n f x. m f (n f x);+sub     = \m n. (n pred) m;+mul     = \m n f. m (n f);++# some useful predicates on church numerals+even    = \n. n not true;+iszero  = \m. m (\x. false) true;+lte     = \m n. iszero (sub m n);+gte     = \m n. iszero (sub n m);+eq      = \m n. and (lte m n) (gte m n);+lt      = \m n. and (lte m n) (not (gte m n));+gt      = \m n. and (gte m n) (not (lte m n));++# aliases for the church numerals up to ten+one   = succ zero;+two   = succ one;+three = succ two;+four  = succ three;+five  = succ four;+six   = succ five;+seven = succ six;+eight = succ seven;+nine  = succ eight;+ten   = succ nine;++# integer exponentation+pow     = \m n. n (\x. mul m x) one;+++# Turner's combinators+I = \x .x;+K = \x y. x;+S = \f g x. (f x) (g x);+W = \f x. f x x;+B = \f g x. f (g x);+C = \f x y. f x y;++# the fixpoint combinator+Y = \f. (\x. f (x x)) \x. f (x x);++# a divergent labmda term+omega = (\x. x x) \x. x x;++# factorial+fac = Y (\facF n. if (iszero n)+                     one +                     (mul n (facF (pred n))));++# the church encoding for pairs+pair = \x y f. f x y;+fst  = \p. p (\x y. x);+snd  = \p. p (\x y. y);++# now, encode ADTs+match = \x pats. x (\n f. f (fst ((n snd) pats)));++# the ADT representation of lists+nil  = \    w. w zero (\f. f);+cons = \h t w. w one  (\f. f h t);++# head and tail, by pattern matching+head = \l. match l (pair nil+                   (pair (\h t. h)+                    zero));++tail = \l. match l (pair nil+                   (pair (\h t. t)+                    zero));++# the ith element of a list+index = \n l. head (n tail l);++# right fold on a list+foldr = \f z. Y (\foldF l. match l (pair z+                                   (pair (\h t. f h (foldF t))+                                    zero)));++# left fold on a list+foldl = \f. Y (\foldF r l. match l (pair r+                                   (pair (\h t. foldF (f r h) t)+                                    zero)));++# the length of a list+len = foldl (\x h. succ x) zero;++# the mapping function on a list+map = \f. Y (\mapF l. match l (pair nil+                              (pair (\h t. cons (f h) (mapF t))+                               zero)));++# list generator+unfold = \g until. Y (\unfoldF x. if (until x)+                                       (cons x nil)+                                       (cons x (unfoldF (g x))));++# some other interesting list functions....++iterate = \g. unfold g (K false);+nats = iterate succ zero;++upTo = \n. unfold succ (\x. gte x n) zero;++zipWith = \f. Y (\zipF l1 l2. match l1+                     (pair nil+                     (pair (\h1 t1. match l2+                        (pair nil+                        (pair (\h2 t2.+                           cons (f h1 h2) (zipF t1 t2))+                         zero)))+                       zero)));++zip = zipWith pair;++take = \n l. zipWith K l (tail (upTo n));+drop = \n l. n tail l;++minAux = foldl (\x y. if (lt y x) y x);++min  = \l. match l+             (pair nil+             (pair minAux+              zero));++maxAux = foldl (\x y. if (gt y x) y x);++max  = \l. match l+             (pair nil+             (pair maxAux+              zero));++remove = \x. Y (\removeF l. match l+              (pair nil+              (pair (\h t.+                 if (eq h x) t (cons h (removeF t)))+               zero)));++insertSort = Y (\sortF l. match l+             (pair nil+             (pair (\h t. (\x. cons x (sortF (remove x l))) (minAux h t))+              zero)));

@@ -0,0 +1,198 @@+{-+ -   The Lambda Shell, an interactive environment for evaluating pure untyped lambda terms.+ -   Copyright (C) 2005-2007, Robert Dockins+ -+ -   This program 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.+ -+ -   This program 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 this program; if not, write to the Free Software+ -   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA+ -}++{- |+  This module defines CPS transformations on lambda terms.+-}++module CPS+( simple_cps+, eta_cps+, onepass_cps+, CPS+) where++import Lambda++type CPS m+     = Bindings () String+    -> PureLambda () String+    -> m (PureLambda () String)++-- | The simple CPS transform defined by Plotkin+simple_cps :: Monad m => CPS m++simple_cps b t = do+    x <- do_simple_cps b t+    return (App () x (Lam () "q" (Var () 0)))++do_simple_cps :: Monad m => CPS m++do_simple_cps b (Binding _ name) =+    lookupBindingM name b >>= \t -> do_simple_cps b t++do_simple_cps b (Var _ i) =+    return (Lam () "k" $ App () (Var () 0) $ (Var () (i+1)))++do_simple_cps b (Lam _ l t) = do+    t' <- do_simple_cps b (lamShift 1 1 t)+    return+      (Lam () "k" $ App () (Var () 0) $ Lam () l t')++do_simple_cps b (App _ t1 t2) = do+    t1' <- do_simple_cps b (lamShift 0 1 t1)+    t2' <- do_simple_cps b (lamShift 0 2 t2)+    return+      (Lam () "k" $ App () t1' $+         Lam () "m" $ App () t2' $+           Lam () "n" $+             App () (App () (Var () 1) (Var () 0)) (Var () 2))+++-- | A version of Plotkin's CPS transform with additional+--   eta expansions, preparing for the one-pass+--   simplifying transform+eta_cps :: Monad m => CPS m+eta_cps b t = do+   x <- do_eta_cps b t+   return (App () x (Lam () "q" (Var () 0)))++do_eta_cps :: Monad m => CPS m++do_eta_cps b (Binding _ name) =+    lookupBindingM name b >>= \t -> do_simple_cps b t++do_eta_cps b (Var _ i) =+    return (Lam () "k" $ App () (Var () 0) $ (Var () (i+1)))+++do_eta_cps b (Lam _ l t) = do+    t' <- do_eta_cps b (lamShift 2 1 (lamShift 0 1 t))+    return+      (Lam () "k" $ App () (Var () 0) $+        Lam () l $+          Lam () "kk" $ App () t' $+            Lam () "m" $ App () (Var () 1) (Var () 0)+      )+++do_eta_cps b (App _ t1 t2) = do+    t1' <- do_eta_cps b (lamShift 0 1 t1)+    t2' <- do_eta_cps b (lamShift 0 2 t2)+    return+      (Lam () "k" $ App () t1' $+        Lam () "m" $ App () t2' $+          Lam () "n" $+            App () (App () (Var () 1) (Var () 0)) $+              Lam () "a" $ App () (Var () 3) (Var () 0)+      )+++++-- | The \"one-pass\" properly-tail-recursive CPS tranform due to Danvy and Filinski,+--   from the paper \"Representing Control: A Study of the CPS Transformation\",+--   in /Mathematical Structures in Computer Science/, 1991.+--+--   Here is is actually implemented as a two-pass tranform.+--   In the first pass we create the eta-expanded version and note+--   which redexes are adminstrative.  In the second pass all administrative+--   redexes are reduced, leaving only the dynamic redexes.++onepass_cps :: Monad m => CPS m+onepass_cps b t = do+   x <- do_onepass_cps b t+   simplify_onepass (App True x (Lam True "q" (Var True 0)))+++simplify_onepass+    :: Monad m+    => PureLambda Bool String+    -> m (PureLambda () String)++simplify_onepass (Binding _ _) = fail "bug: binding found in simplify_onepass"++simplify_onepass (Var False i)     = return (Var () i)+simplify_onepass (Lam False l t)   = simplify_onepass t >>= \t' -> return (Lam () l t')+simplify_onepass (App False t1 t2) = do+    t1' <- simplify_onepass t1+    t2' <- simplify_onepass t2+    return (App () t1' t2')++simplify_onepass (App True (Lam True _ t) s) = simplify_onepass (lamSubst s t)+simplify_onepass t  = fail $ "bug: found unexpected administrative terms in simplify_onepass\n"++(show t)+++do_onepass_cps+    :: Monad m+    => Bindings () String+    -> PureLambda () String+    -> m (PureLambda Bool String)++do_onepass_cps b (Binding _ name) =+     lookupBindingM name b >>= \t -> do_onepass_cps b t++do_onepass_cps b (Var _ i) =+     return (Lam True "k" $ App True (Var True 0) $ (Var False (i+1)))++do_onepass_cps b (Lam _ l t) = do+    t' <- do_onepass_cps_tail b (lamShift 2 1 (lamShift 0 1 t))+    return+       (Lam True "k0" $ App True (Var True 0) $+          Lam False l $ Lam False "k" $ App True t' $ (Var False 0)+       )++do_onepass_cps b (App _ t1 t2) = do+    t1' <- do_onepass_cps b (lamShift 0 1 t1)+    t2' <- do_onepass_cps b (lamShift 0 2 t2)+    return+        (Lam True "k0" $ App True t1' $+           Lam True "m0" $ App True t2' $+             Lam True "n" $+               App False (App False (Var True 1) (Var True 0)) $+                 Lam False "a" $ App True (Var True 3) (Var False 0)+        )+++do_onepass_cps_tail+    :: Monad m+    => Bindings () String+    -> PureLambda () String+    -> m (PureLambda Bool String)++do_onepass_cps_tail b (Var _ i) =+    return (Lam True "k0" (App False (Var True 0) (Var False (i+1))))++do_onepass_cps_tail b (Lam _ l t) = do+    t' <- do_onepass_cps_tail b (lamShift 2 1 (lamShift 0 1 t))+    return+      (Lam True "k0" $ App False (Var True 0) $+         Lam False l $ Lam False "k" $ App True t' $ (Var False 0)+      )++do_onepass_cps_tail b (App _ t1 t2) = do+    t1' <- do_onepass_cps b (lamShift 0 1 t1)+    t2' <- do_onepass_cps b (lamShift 0 2 t2)+    return+      (Lam True "k0" $ App True t1' $+         Lam True "m" $ App True t2' $+           Lam True "n" $+             App False (App False (Var True 1) (Var True 0))+               (Var True 2)+      )

@@ -0,0 +1,45 @@+{-+ -   The Lambda Shell, an interactive environment for evaluating pure untyped lambda terms.+ -   Copyright (C) 2005-2007, Robert Dockins+ -+ -   This program 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.+ -+ -   This program 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 this program; if not, write to the Free Software+ -   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA+ -}++module Env+( Env+, empty+, insert+, lookup+) where++import Prelude hiding (lookup)+import qualified Data.Set as Set++data Env = Env !Int ![String] !(Set.Set String)++empty :: Env+empty = Env 0 [] (Set.empty)++insert :: String -> Env -> Env+insert label (Env z labels set)+    | label `Set.member` set = Env (z+1) ( (label++"_"++(show z)) : labels) set+    | otherwise              = Env z     ( label : labels )                 (Set.insert label set)++lookup :: Int -> Env -> String++lookup x (Env z labels set) =+   case drop x labels of+      l:_ -> l+      []  -> error (concat ["'",show x,"' out of bounds in environment ",show labels])

@@ -0,0 +1,382 @@+{-+ -   The Lambda Shell, an interactive environment for evaluating pure untyped lambda terms.+ -   Copyright (C) 2005-2007, Robert Dockins+ -+ -   This program 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.+ -+ -   This program 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 this program; if not, write to the Free Software+ -   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA+ -}++{- |+ This module defines the pure lambda calculus and+ some associated operations.++ Lambda terms are represented with de Brujin indicies.  Lambdas+ are annotated with a label for the variable that is used when+ displaying.  Lambda terms may be references to let-bindings;+ these are unfolded in explicit reduction steps.  Let bindings are+ non-recursive; that is, the bound name is not in scope during+ the definition.+-}++module Lambda (+-- * Type Definitions+  Bindings+, ReductionStrategy++-- * Lamda Term Datatype+, PureLambda (..)++-- * Comparison Functions+, alphaEq+, normalEq++-- * Auxilary Functions+, lookupBinding+, lookupBindingM+, printLam+, showLam+, lamSubst+, lamShift+, unfoldTop++-- * Reduction Strategies+, lamReduceNull+, lamReduceWHNF+, lamReduceHNF+, lamReduceNF+, lamStrictNF++-- * Evaluation Functions+, lamEvalF+, lamEval+, lamEvalCount+, lamEvalTrace++) where++import Data.List+import qualified Env as Env+import qualified Data.Map as Map+import Control.Monad (MonadPlus (..))+import Control.Monad.Identity++type Bindings a l = Map.Map String (PureLambda a l)++lookupBinding :: String -> Bindings a l -> PureLambda a l+lookupBinding name b  = runIdentity (lookupBindingM name b)++lookupBindingM :: Monad m => String -> Bindings a l -> m (PureLambda a l)+lookupBindingM name b =+   case Map.lookup name b of+      Just x  -> return x+      Nothing -> fail (concat ["'",name,"' not bound"])+++----------------------------------------------------------------+-- | The type of lambda terms;+--   they are polymorphic in an annotation type \'a\' and the type+--   of labels \'l\'.++data PureLambda a l+   = Lam a l (PureLambda a l)+   | App a (PureLambda a l) (PureLambda a l)+   | Var a Int+   | Binding a String+ deriving (Show)++------------------------------------------------------------------+-- | Alpha equivalance on lambda terms.  Defined in the usual+--   way, except that bindings are compared by name.++alphaEq      :: PureLambda a l+             -> PureLambda a l+             -> Bool++alphaEq (Lam _ _ t1)   (Lam _ _ t2)   = alphaEq t1 t2+alphaEq (App _ x1 y1)  (App _ x2 y2)  = alphaEq x1 x2 && alphaEq y1 y2+alphaEq (Var _ i1)     (Var _ i2)     = i1 == i2+alphaEq (Binding _ n1) (Binding _ n2) = n1 == n2+alphaEq _              _              = False+++-------------------------------------------------------------------+-- | Defines an eqivalance predicate on normalizing terms, where+--   terms with alpha-equivalant normal forms are in the relation.+--   This function will diverge for non-normalizing terms.++normalEq     :: Bindings a l    -- ^ Let bindings in scope+             -> PureLambda a l+             -> PureLambda a l+             -> Bool++normalEq binds t1 t2 =+    let n1 = lamEval binds True lamReduceNF t1+        n2 = lamEval binds True lamReduceNF t2+    in alphaEq n1 n2++-------------------------------------------------------------------+-- | Show a lambda term, minimizing parenthises and disambiguating+--   variables in nested scopes with identical labels.++printLam :: PureLambda a String -> String+printLam lam = showLam lam []++showLam :: PureLambda a String -> ShowS+showLam = showLam_ Env.empty TopContext 0+++data LamContext+   = TopContext+   | AppLeft+   | AppRight+ deriving (Eq)+++showLam_     :: Env.Env+             -> LamContext+             -> Int+             -> PureLambda a String+             -> ShowS++showLam_ env c x lam = case lam of++  Binding _ name -> showLambdas env x . showString name++  Var _ v        -> showLambdas env x . showString (Env.lookup v env)++  Lam _ label t  ->+       showParen (c /= TopContext)+       ( showLam_ (Env.insert label env) TopContext (x+1) t )++  App _ t1 t2    ->+       showParen (c == AppRight)+       ( showLambdas env x+       . showLam_ env AppLeft 0 t1+       . showChar ' '+       . showLam_ env AppRight 0 t2+       )+++showLambdas :: Env.Env+            -> Int+            -> ShowS++showLambdas env 0 = id+showLambdas env x =+    ( showChar '\\'+    . showString+          (concat . intersperse " " . map (\i -> Env.lookup i env) $ [x-1, x-2 .. 0])+    . showString ". "+    )+++-----------------------------------------------------------------------------+-- shifts all free variables by a specified amount+-- ancillary function for substitution++lamShift     :: Int+             -> Int+             -> PureLambda a l+             -> PureLambda a l++lamShift c d v@(Var a x)+   | x >= c    = Var a (x+d)+   | otherwise = v++lamShift c d (Lam a label t)  = Lam a label (lamShift (c+1) d t)+lamShift c d (App a t1 t2)    = App a (lamShift c d t1) (lamShift c d t2)+lamShift c d b@(Binding _ _)  = b+++------------------------------------------------------------------------------+-- | Capture-avoiding substitution;+--   substitute \'s\' into \'t\', replacing all free variables with index 0.++lamSubst     :: PureLambda a l -- ^ s+             -> PureLambda a l -- ^ t+             -> PureLambda a l++lamSubst s t = lamShift 0 (-1) (lamSubst' (lamShift 0 1 s) 0 0 t)++++lamSubst'    :: PureLambda a l+             -> Int+             -> Int+             -> PureLambda a l+             -> PureLambda a l++lamSubst' s var c v@(Var _ x)+   | x == (var+c) = lamShift 0 c s+   | otherwise    = v++lamSubst' s var c (Lam a label t)  = Lam a label (lamSubst' s var (c+1) t)+lamSubst' s var c (App a t1 t2)    = App a (lamSubst' s var c t1) (lamSubst' s var c t2)+lamSubst' s var c b@(Binding _ _)  = b+++-------------------------------------------------------------------------------------+-- | The type of reduction strategies.++type ReductionStrategy a l+     = Bindings a l+    -> Bool+    -> PureLambda a l+    -> Maybe (PureLambda a l)+++-------------------------------------------------------------------------------------+-- | The \'null\' reduction strategy, which does no reduction+lamReduceNull :: ReductionStrategy a l+lamReduceNull _ _ _ = Nothing++-------------------------------------------------------------------------------------+-- | Single-step normal order reduction to Weak Head Normal Form (WHNF)++lamReduceWHNF :: ReductionStrategy a l++lamReduceWHNF b unfold (App _ (Lam _ _ t1) t2) = Just (lamSubst t2 t1)+lamReduceWHNF b unfold (App a t1 t2)           = lamReduceWHNF b True t1   >>= \t1' -> return (App a t1' t2)+lamReduceWHNF b unfold (Lam a l t)             = Nothing+lamReduceWHNF b unfold (Var _ _)               = Nothing+lamReduceWHNF b unfold (Binding a name)        = if unfold then Just (lookupBinding name b) else Nothing+++-------------------------------------------------------------------------------------+-- | Single-step normal order reduction to Head Normal Form (HNF)++lamReduceHNF :: ReductionStrategy a l++lamReduceHNF b unfold (App _ (Lam _ _ t1) t2)  = Just (lamSubst t2 t1)+lamReduceHNF b unfold (App a t1 t2)            = lamReduceHNF b True t1   >>= \t1' -> return (App a t1' t2)+lamReduceHNF b unfold (Lam a l t)              = lamReduceHNF b unfold t  >>= \t'  -> return (Lam a l t')+lamReduceHNF b unfold (Var _ _)                = Nothing+lamReduceHNF b unfold (Binding a name)         = if unfold then Just (lookupBinding name b) else Nothing++++--------------------------------------------------------------------------------------+-- | Single-step normal order reduction to Normal Form (NF)++lamReduceNF :: ReductionStrategy a l++lamReduceNF b unfold (App _ (Lam _ _ t1) t2)   = Just (lamSubst t2 t1)+lamReduceNF b unfold (App a t1 t2)             = (lamReduceNF b True t1   >>= \t1' -> return (App a t1' t2))+                                                   `mplus`+                                                 (lamReduceNF b unfold t2 >>= \t2' -> return (App a t1 t2'))+lamReduceNF b unfold (Lam a l t)               = lamReduceNF b unfold t   >>= \t'  -> return (Lam a l t')+lamReduceNF b unfold (Var _ _)                 = Nothing+lamReduceNF b unfold (Binding a name)          = if unfold then Just (lookupBinding name b) else Nothing++++---------------------------------------------------------------------------------------+-- | Single-step applicative order reduction to Normal Form (NF)++lamStrictNF :: ReductionStrategy a l++lamStrictNF b unfold (App a (Lam al l t1) t2)  = (lamStrictNF b True t2 >>= \t2' -> return (App a (Lam al l t1) t2'))+                                                   `mplus`+                                                 (Just (lamSubst t2 t1))+lamStrictNF b unfold (App a t1 t2)             = (lamStrictNF b True t1   >>= \t1' -> return (App a t1' t2))+                                                   `mplus`+                                                 (lamStrictNF b unfold t2 >>= \t2' -> return (App a t1 t2'))+lamStrictNF b unfold (Lam a l t)               = lamStrictNF b unfold t   >>= \t'  -> return (Lam a l t')+lamStrictNF b unfold (Var _ _)                 = Nothing+lamStrictNF b unfold (Binding a name)          = if unfold then Just (lookupBinding name b) else Nothing++++---------------------------------------------------------------------------------------+-- | Helper for various kinds of evaluation.  Applies the function \'z\' if+--   the evaluation strategy has terminated, and applies \'f\' to the+--   reduced term otherwise.++lamEvalF     :: Bindings a l             -- ^ A set of bindings for unfolding+             -> Bool                     -- ^ Apply full unfolding?+             -> ReductionStrategy a l    -- ^ Reduction strategy to use+             -> (PureLambda a l -> b)    -- ^ f+             -> (PureLambda a l -> b)    -- ^ z+             -> PureLambda a l           -- ^ The term to reduce+             -> b++lamEvalF b unfold reduce f z x =+   case reduce b unfold x of+        Just x' -> f x'+        Nothing -> z x+++++-------------------------------------------------------------------------------------+-- | Big-step reduction; that is, apply the reduction strategy until+--   it fails to reduce any futher.++lamEval     :: Bindings a l            -- ^ A set of bindings for unfolding+             -> Bool                   -- ^ Apply full unfolding ?+             -> ReductionStrategy a l  -- ^ Reduction strategy to use+             -> PureLambda a l         -- ^ The term to reduce+             -> PureLambda a l         -- ^ The evaluated term++lamEval bind unfold red = eval+  where evalF  = lamEvalF bind unfold red+        eval x = evalF eval id x++++-------------------------------------------------------------------------------------+-- | Big-step reduction that counts the number of reductions performed++lamEvalCount :: Bindings a l           -- ^ A set of bindings for unfolding+             -> Bool                   -- ^ Apply full unfolding ?+             -> ReductionStrategy a l  -- ^ Reduction strategy to use+             -> PureLambda a l         -- ^ The term to reduce+             -> (PureLambda a l,Integer) -- ^ The evaluated term and reduction count++lamEvalCount bind unfold red = eval 0+  where evalF     = lamEvalF bind unfold red+        eval n x  = evalF (\t -> eval (succ n) t) (\t -> (t,n)) x+++-------------------------------------------------------------------------------------+-- | Traced evaluation; the result is a list of the reduction+--   steps taken by the given reduction stragegy.  A non-terminating+--   term (under the given strategy) will result in an infinite list.+--   For a normalizing term, the last element in the list will be the+--   normal  form.++lamEvalTrace :: Bindings a l          -- ^ A set of bindings for unfolding+             -> Bool                  -- ^ Apply full unfolding ?+             -> ReductionStrategy a l -- ^ Reduction strategy to use+             -> PureLambda a l        -- ^ The term to reduce+             -> [PureLambda a l]      -- ^ The list of intermediate reductions++lamEvalTrace bind unfold red = eval+  where evalF  = lamEvalF bind unfold red+        eval x = evalF ((x:) . eval) (:[]) x++++++-----------------------------------------------------------------------------------------+-- | If a lambda term is just a let binding, this function will unfold it; otherwise+--   it will return the term unchanged.  It will result in bottom if the term is not bound.++unfoldTop     :: Bindings () String+              -> PureLambda () String+              -> PureLambda () String++unfoldTop binds (Binding a x) = Map.findWithDefault (error $ concat ["'",x,"' not bound"]) x binds+unfoldTop binds x             = x

@@ -0,0 +1,302 @@+{-+ -   The Lambda Shell, an interactive environment for evaluating pure untyped lambda terms.+ -   Copyright (C) 2005-2007, Robert Dockins+ -+ -   This program 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.+ -+ -   This program 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 this program; if not, write to the Free Software+ -   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA+ -}+++module LambdaCmdLine+( lambdaCmdLine+) where++import Data.IORef+import Numeric+import Maybe+import Data.List+import Data.Char+import qualified Data.Map as Map+import System.IO+import System.Exit+import System.Console.GetOpt+import Text.ParserCombinators.Parsec (runParser)++import Lambda+import CPS+import LambdaParser+import LambdaShell+import Version++-----------------------------------------------------------------------+-- Main entry point for the command line tool++-- | Parse command line options and run the lambda shell+lambdaCmdLine :: [String] -> IO ()+lambdaCmdLine argv =+   do st <- parseCmdLine argv+      case (cmd_print st) of+         PrintNothing    -> doCmdLine st+         PrintHelp       -> putStr (printUsage usageNotes)+         PrintVersion    -> putStr versionInfo+         PrintNoWarranty -> putStr noWarranty+         PrintGPL        -> putStr gpl+++doCmdLine :: LambdaCmdLineState -> IO ()+doCmdLine st =+   case (cmd_input st) of+       Just expr -> evalInput st expr+       Nothing ->+           if (cmd_stdin st)+              then evalStdin st+              else runShell st++--------------------------------------------------------------+-- Holds important values parsed from the command line++data LambdaCmdLineState+   = LambdaCmdLineState+     { cmd_unfold  :: Bool+     , cmd_stdin   :: Bool+     , cmd_input   :: Maybe String+     , cmd_binds   :: Bindings () String+     , cmd_print   :: PrintWhat+     , cmd_trace   :: Maybe (Maybe Int)+     , cmd_red     :: RS+     , cmd_count   :: Bool+     , cmd_extsyn  :: Bool+     , cmd_cps     :: CPS LamParser+     , cmd_history :: Maybe String+     }++initialCmdLineState =+  LambdaCmdLineState+  { cmd_unfold  = False+  , cmd_stdin   = False+  , cmd_input   = Nothing+  , cmd_binds   = Map.empty+  , cmd_print   = PrintNothing+  , cmd_trace   = Nothing+  , cmd_red     = lamReduceNF+  , cmd_count   = False+  , cmd_extsyn  = True+  , cmd_cps     = simple_cps+  , cmd_history = Just "lambda.history"+  }++data PrintWhat+   = PrintNothing+   | PrintVersion+   | PrintHelp+   | PrintNoWarranty+   | PrintGPL++-------------------------------------------------------------+-- Set up the command line options++data LambdaCmdLineArgs+  = FullUnfold+  | ReadStdIn+  | Program String+  | Trace (Maybe String)+  | Print PrintWhat+  | Reduction String+  | Cps String+  | ShowCount+  | NoExtSyn+  | History String+  | NoHistory++options :: [OptDescr LambdaCmdLineArgs]+options =+  [ Option ['u']     ["unfold"]      (NoArg FullUnfold)              "perform full unfolding of let-bound terms"+  , Option ['s']     ["stdin"]       (NoArg ReadStdIn)               "read from standard in"+  , Option ['e']     ["program"]     (ReqArg Program "PROGRAM")      "evaluate statements from command line"+  , Option ['r']     ["trace"]       (OptArg Trace "TRACE_NUM")      "set tracing (and optional trace display length)"+  , Option ['h','?'] ["help"]        (NoArg (Print PrintHelp))       "print this message"+  , Option ['v']     ["version"]     (NoArg (Print PrintVersion))    "print version information"+  , Option ['g']     ["gpl"]         (NoArg (Print PrintGPL))        "print the GNU GPLv2, under which this software is licensed"+  , Option ['w']     ["nowarranty"]  (NoArg (Print PrintNoWarranty)) "print the warranty disclamer"+  , Option ['c']     ["count"]       (NoArg ShowCount)               "turn on printing of reduction counts"+  , Option ['x']     ["extsyn"]      (NoArg NoExtSyn)                "turn off extended syntax"+  , Option ['t']     ["strategy"]    (ReqArg Reduction "REDUCTION_STRATEGY")+           "set the reduction strategy (one of 'whnf', 'hnf', 'nf', 'strict')"+  , Option ['w']     ["history"]     (ReqArg History "HISTORY_FILE")  "set the command history file (default: 'lambda.history')"+  , Option ['q']     ["nohistory"]   (NoArg NoHistory)                "disable command history file"++  , Option ['p']     ["cps"]         (ReqArg Cps "CPS_STRATEGY")+           "set the CPS strategy (one of 'simple', 'onepass')"++  ]++++-----------------------------------------------------------------+-- Parser for the command line+-- yeah, I know its ugly++parseCmdLine :: [String] -> IO LambdaCmdLineState+parseCmdLine argv =+   case getOpt RequireOrder options argv of+     (opts,files,[]) -> (foldl (>>=) (return initialCmdLineState) $ map applyFlag opts) >>= \st ->+                        (foldl (>>=) (return st)                  $ map loadDefs files)++     (_,_,errs)      -> fail (errMsg errs)++  where errMsg errs = printUsage (concat (intersperse "\n" errs))++        applyFlag :: LambdaCmdLineArgs -> LambdaCmdLineState -> IO LambdaCmdLineState+        applyFlag FullUnfold            st = return st{ cmd_unfold  = True }+        applyFlag ReadStdIn             st = return st{ cmd_stdin   = True }+        applyFlag ShowCount             st = return st{ cmd_count   = True }+        applyFlag NoExtSyn              st = return st{ cmd_extsyn  = False }+        applyFlag NoHistory             st = return st{ cmd_history = Nothing }+        applyFlag (History nm)          st = return st{ cmd_history = Just nm }+        applyFlag (Print printWhat)     st = return st{ cmd_print   = printWhat }+        applyFlag (Trace Nothing)       st = return st{ cmd_trace   = Just Nothing }+        applyFlag (Trace (Just num))    st = case readDec num of+                                                ((n,[]):_) -> return st{ cmd_trace = Just (Just n) }+                                                _          -> fail (errMsg [concat ["'",num,"' must be a positive integer"]])++        applyFlag (Program pgm)         st = case cmd_input st of+                                                Nothing -> return st{ cmd_input = Just pgm }+                                                _       -> fail (errMsg ["'-e' option may only occur once"])++        applyFlag (Cps str) st =+            case map toLower str of+                "simple"  -> return st{ cmd_cps = simple_cps }+                "onepass" -> return st{ cmd_cps = onepass_cps }+                _         -> fail (concat ["'",str,"' is not a valid CPS strategy"])++        applyFlag (Reduction str) st =+            case map toLower str of+                "whnf"   -> return st{ cmd_red = lamReduceWHNF }+                "hnf"    -> return st{ cmd_red = lamReduceHNF }+                "nf"     -> return st{ cmd_red = lamReduceNF }+                "strict" -> return st{ cmd_red = lamStrictNF }+                _        -> fail (concat ["'",str,"' is not a valid reduction strategy"])+++-----------------------------------------------------------------------+-- Actually run the shell++mapToShellState :: LambdaCmdLineState -> LambdaShellState+mapToShellState st =+  initialShellState+  { letBindings = cmd_binds st+  , fullUnfold  = cmd_unfold st+  , trace       = isJust (cmd_trace st)+  , traceNum    = let x = traceNum initialShellState+                  in maybe x (maybe x id) (cmd_trace st)+  , redStrategy = cmd_red st+  , showCount   = cmd_count st+  , cpsStrategy = cmd_cps st+  , histFile    = cmd_history st+  }++runShell :: LambdaCmdLineState -> IO ()+runShell st = do+--   putStrLn versionInfo+--   putStrLn shellMessage+   lambdaShell (mapToShellState st)+   return ()++++--------------------------------------------------------------------------+-- For dealing with input from stdin or the command line++evalStdin :: LambdaCmdLineState -> IO ()+evalStdin st = hGetContents stdin >>= evalInput st++evalInput :: LambdaCmdLineState -> String -> IO ()+evalInput st expr = do+    exitCode <- newIORef ExitSuccess+    let parseSt = LamParseState (cmd_cps st) (cmd_extsyn st)+    case runParser (statementsParser (cmd_binds st)) parseSt "" expr of+       Left msg    -> fail (show msg)+       Right stmts -> foldl (>>=) (return st) $ map (flip (evalStmt exitCode)) $ stmts+    code <- readIORef exitCode+    exitWith code++setSucc :: IORef ExitCode -> IO ()+setSucc ec = writeIORef ec ExitSuccess++setFail :: IORef ExitCode -> IO ()+setFail ec = writeIORef ec (ExitFailure 100)++evalStmt :: IORef ExitCode -> LambdaCmdLineState -> Statement -> IO LambdaCmdLineState+evalStmt ec st (Stmt_eval t)     = evalTerm st t >> setSucc ec >> return st+evalStmt ec st (Stmt_isEq t1 t2) = compareTerms ec st t1 t2 >> return st+evalStmt ec st (Stmt_let name t) = setSucc ec >> return st{ cmd_binds = Map.insert name t (cmd_binds st) }+evalStmt ec st (Stmt_empty)      = setSucc ec >> return st+++evalTerm :: LambdaCmdLineState -> PureLambda () String -> IO ()+evalTerm st t = doEval (unfoldTop (cmd_binds st) t)+ where doEval t =+         case cmd_trace st of+            Nothing       -> putStrLn (printLam (eval t))+            Just Nothing  -> printTrace 50 t+            Just (Just x) -> printTrace x t++       printTrace x t = putStr $ unlines $ map printLam $ take x $ trace t++       eval t  = lamEval      (cmd_binds st) (cmd_unfold st) (cmd_red st) t+       trace t = lamEvalTrace (cmd_binds st) (cmd_unfold st) (cmd_red st) t+++compareTerms :: IORef ExitCode+            -> LambdaCmdLineState+            -> PureLambda () String+            -> PureLambda () String+            -> IO ()++compareTerms ec st t1 t2 = do+  if normalEq (cmd_binds st) t1 t2+     then putStrLn "equal"     >> setSucc ec+     else putStrLn "not equal" >> setFail ec+++-------------------------------------------------------------------------+-- Read definitions from a file++loadDefs :: FilePath -> LambdaCmdLineState -> IO LambdaCmdLineState+loadDefs path st = do+  let parseSt = LamParseState (cmd_cps st) (cmd_extsyn st)+  binds <- readDefinitionFile parseSt (cmd_binds st) path+  return st{ cmd_binds = Map.union binds (cmd_binds st) }+++-----------------------------------------------------------------------+-- Printing stuff++printUsage :: String -> String+printUsage str = unlines+   [ ""+   , ""+   , usageInfo "usage: lambdaShell {<option>} [{<file>}]\n" options+   , ""+   , ""+   ,str+   , ""+   ]++usageNotes :: String+usageNotes = unlines+   [ "Any files listed after the options will be parsed as a series of"+   , "\"let\" definitions, which will be in scope when the shell starts"+   , "(or when the -e expression is evaluated)"+   ]

@@ -0,0 +1,253 @@+{-+ -   The Lambda Shell, an interactive environment for evaluating pure untyped lambda terms.+ -   Copyright (C) 2005-2007, Robert Dockins+ -+ -   This program 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.+ -+ -   This program 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 this program; if not, write to the Free Software+ -   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA+ -}+++-- | This module defines parsers for lambda terms+--   and for \"let\" bound definitions.++module LambdaParser+( nameParser+, lambdaParser+, definitionFileParser+, stripComments+, Statement (..)+, statementParser+, statementsParser+, LamParseState (..)+, LamParser+)+where++import Data.List+import qualified Data.Map as Map+import Text.ParserCombinators.Parsec++import Lambda+import CPS++-- | A type representing "statements".  A statement is+--   either a lambda form to reduce, a let binding,+--   a confluence test, a cps transform,+--   or the empty statement.++data Statement+  = Stmt_eval (PureLambda () String)+  | Stmt_let String (PureLambda () String)+  | Stmt_isEq (PureLambda () String)+              (PureLambda () String)+  | Stmt_empty++data LamParseState+   = LamParseState+   { cpsTransform   :: CPS LamParser+   , extendedSyntax :: Bool+   }++type LamParser = GenParser Char LamParseState++-- | Parser for an identifier.  An identifier is+--   a letter followed by zero or more alphanumeric characters (or underscores).+nameParser :: LamParser String+nameParser =+  do a  <- letter+     as <- many (char '_' <|> alphaNum)+     return (a:as)++-- | Parser for a lambda term.  Function application is left associative.+--+-- @+--   lambda -\> name+--   lambda -\> \'(\' lambda \')\'+--   lambda -\> lambda lambda+--   lambda -\> \'\\\' {name} \'.\' lambda+-- @++lambdaParser :: Bindings () String -> LamParser (PureLambda () String)+lambdaParser b = do+    st <- getState+    let p = if (extendedSyntax st) then extSyntax else basicSyntax+    spaces+    e <- appParser p b []+    spaces+    return e+++-- | Parser for multiple statements.+--+-- @+--   stmts -\> stmt ';' stmts+--   stmts -\>+-- @+statementsParser :: Bindings () String -> LamParser [Statement]+statementsParser b = do spaces; x <- p b; eof; return x++ where p b = do x <- stmtParser b+                let b' = case x of+                          (Stmt_let name t) -> Map.insert name t b+                          _ -> b+                spaces+                ( do char ';'+                     spaces+                     xs <- p b'+                     return (x:xs))+                 <|> (return [x])+++++-- | Parser for a statement.+--+-- @+--    stmt -\> \'let\' name \'=\' lambda+--    stmt -\> lambda+-- @+statementParser :: Bindings () String -> LamParser Statement+statementParser b = do+   spaces+   x <- stmtParser b+   spaces+   eof+   return x++++stmtParser :: Bindings () String -> LamParser Statement+stmtParser b =+       try (letDefParser b     >>= return . uncurry Stmt_let)+   <|> try (compParser b       >>= return . uncurry Stmt_isEq)+   <|> (lambdaParser b         >>= return . Stmt_eval)+   <|> (return Stmt_empty)++compParser :: Bindings () String -> LamParser (PureLambda () String,PureLambda () String)+compParser b = do+    x <- lambdaParser b+    spaces+    string "=="+    spaces+    y <- lambdaParser b+    spaces+    return (x,y)+++letDefParser :: Bindings () String -> LamParser (String,PureLambda () String)+letDefParser b = do+    string "let"+    many1 space+    n <- nameParser+    spaces+    char '='+    e <- lambdaParser b+    return (n,e)++stripComments :: String -> String+stripComments (x:xs)+  | x == '#'  = stripComments (dropWhile (/= '\n') xs)+  | otherwise = x : stripComments xs+stripComments [] = []++-- | Parser a file of definitions.  Each definition takes the form+--+-- @+--  def -\> \'let\' name \'=\' lambda \';\'+-- @++definitionFileParser :: Bindings () String -> LamParser (Bindings () String)+definitionFileParser b =+  (do spaces+      (n,t) <- definitionParser b+      spaces+      let b' = Map.insert n t b+      definitionFileParser b'+  )+  <|> (eof >> return b)++++definitionParser :: Bindings () String -> LamParser (String,PureLambda () String)+definitionParser b =+   do n <- nameParser+      spaces+      char '='+      e <- lambdaParser b+      char ';'+      return (n,e)++type P = Bindings () String -> [String] -> LamParser (PureLambda () String)+++cpsParser :: P -> P+cpsParser p b l = do+    string "[["+    spaces+    x <- (appParser p) b l+    spaces+    string "]]"+    st <- getState+    cpsTransform st b x++parensParser :: P -> P+parensParser p b l = do+    char '('+    spaces+    e <- (appParser p) b l+    spaces+    char ')'+    return e++varParser :: P+varParser b labels = do+    var <- nameParser+    let i = elemIndex var labels+    case i of+       Just i  -> return (Var () i)+       Nothing -> if Map.member var b+                     then return (Binding () var)+                     else fail ("variable '"++var++"' not in scope")+++absParser :: P -> P+absParser p b labels = do+    char '\\'+    spaces+    vars <- sepEndBy1 nameParser spaces+    char '.'+    spaces+    let labels' = foldr (:) labels (reverse vars)+    exp <- (appParser p) b labels'+    let expr = foldr (Lam ()) exp vars+    return expr+++appParser :: P -> P+appParser p b l = do+    exprs <- sepEndBy1 (p b l) (many1 space)+    return (foldl1 (App ()) exprs)++basicSyntax :: P+basicSyntax b l =+    parensParser basicSyntax b l <|>+    absParser    basicSyntax b l <|>+    varParser b l++extSyntax :: P+extSyntax b l =+    parensParser extSyntax b l <|>+    absParser    extSyntax b l <|>+    cpsParser    extSyntax b l <|>+    varParser b l

@@ -0,0 +1,358 @@+{-+ -   The Lambda Shell, an interactive environment for evaluating pure untyped lambda terms.+ -   Copyright (C) 2005-2007, Robert Dockins+ -+ -   This program 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.+ -+ -   This program 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 this program; if not, write to the Free Software+ -   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA+ -}+++module LambdaShell+( LambdaShellState (..)+, initialShellState+, lambdaShell+, readDefinitionFile+, RS+)+where++import Control.Monad.Trans+import System.IO+import Data.List (isPrefixOf)++import Lambda+import LambdaParser+import CPS+import Version++import qualified Data.Map as Map+import Text.ParserCombinators.Parsec (runParser)++import System.Console.Shell+import System.Console.Shell.ShellMonad+import System.Console.Shell.Backend.Readline+--import System.Console.Shell.Backend.Basic++defaultBackend = readlineBackend++type RS = ReductionStrategy () String+++-------------------------------------------------------+-- Define types to allow completion of let-bound names++completeLetBindings :: LambdaShellState -> String -> IO [String]+completeLetBindings st prefix =+    return . filter (prefix `isPrefixOf`) . Map.keys . letBindings $ st++data LetBinding = LetBinding++instance Completion LetBinding LambdaShellState where+  complete _         = completeLetBindings+  completableLabel _ = "<name>"++++----------------------------------------------------------+-- Define the shell state++-- | Keeps track of all the state that is needed for the+--   operation of the lambda shell.++data LambdaShellState =+  LambdaShellState+  { trace       :: Bool      -- ^ Step through the reduction one redex at a time+  , traceNum    :: Int       -- ^ Number of reduction steps to display during tracing+  , letBindings :: Map.Map String (PureLambda () String)+                             -- ^ All \"let\" bindings currently in scope+  , fullUnfold  :: Bool      -- ^ Should binding names be eagerly unfolded?+  , redStrategy :: RS        -- ^ The reduction strategy currently in use+  , showCount   :: Bool      -- ^ If true, show the number of reductions at each step+  , cpsStrategy :: CPS LamParser -- ^ The current CPS strategy+  , extSyntax   :: Bool      -- ^ Is extended syntax enabled?+  , histFile    :: Maybe String -- ^ A file for command history+  }+++-- | Default settings for all elements of shell state.+initialShellState =+  LambdaShellState+  { trace       = False+  , traceNum    = 10+  , letBindings = Map.empty+  , fullUnfold  = False+  , redStrategy = lamReduceWHNF+  , showCount   = False+  , cpsStrategy = simple_cps+  , extSyntax   = True+  , histFile    = Nothing+  }++-----------------------------------------------------------------+-- Main entry point to the shell++-- | Run an interactive shell starting with the+--   given shell state and returning the final,+--   possibly modified, state.+lambdaShell :: LambdaShellState -> IO LambdaShellState+lambdaShell init = do+    let+      desc =+         (mkShellDescription commands evaluate)+         { defaultCompletions = Just completeLetBindings+         , historyFile        = histFile init+         , greetingText       = Just (versionInfo ++ shellMessage)+         , secondaryPrompt    = Just $ \_ -> return "] "+         }+    runShell desc defaultBackend init++++-----------------------------------------------------------------+-- read definitions from a file++readDefinitionFile :: LamParseState+                   -> Bindings () String+                   -> String+                   -> IO (Bindings () String)+readDefinitionFile parseSt b file = do+    str  <- openFile file ReadMode >>= hGetContents+    let str' = stripComments str+    case runParser (definitionFileParser b) parseSt file str' of+        Left err -> fail (show err)+        Right b' -> return b'++++----------------------------------------------------------------+-- Definition of all the shell commands++commands :: [ShellCommand LambdaShellState]+commands =+  [ exitCommand "quit"+  , exitCommand "exit"+  , helpCommand "help"+  , toggle "trace"     "Toggle the trace mode"      trace      (\x st -> st { trace = x })+  , toggle "unfold"    "Toggle the unfold mode"     fullUnfold (\x st -> st { fullUnfold = x })+  , toggle "showcount" "Toggle the show count mode" showCount  (\x st -> st { showCount = x })+  , toggle "extsyn"    "Toggle extended syntax"     extSyntax  (\x st -> st { extSyntax = x })++  , cmd "tracestep"  setTraceStep    "Set the number of steps shown in trace mode"+  , cmd "dumptrace"  dumpTrace       "Dump a trace of the named term into a file"+  , cmd "showall"    showBindings    "Show all let bindings"+  , cmd "show"       showBinding     "Show a let binding"+  , cmd "whnf"       setRedWHNF      "Set reduction strategy to weak head normal form"+  , cmd "hnf"        setRedHNF       "Set reduction strategy to head normal form"+  , cmd "nf"         setRedNF        "Set reduction strategy to normal form"+  , cmd "null"       setRedNull      "Set the null reduction strategy (no reduction)"+  , cmd "strict"     setRedStrict    "Use applicative order (strict) reduction"+  , cmd "load"       loadDefFile     "Load definitions from a file"+  , cmd "clear"      clearBindings   "Clear all let bindings"++  , cmd "nowarranty" (shellPutInfo noWarranty)  "Print the warranty disclaimer"+  , cmd "gpl"        (shellPutInfo gpl)         "Print the GNU GPLv2, under which this software is licensed"+  , cmd "version"    (shellPutInfo versionInfo) "Print version info"+  , cmd "simple_cps"  setCPSSimple   "Use the simple CPS strategy"+  , cmd "onepass_cps" setCPSOnepass  "Use the onepass optimizing CPS strategy"+  ]+++dumpTrace :: File -> Int -> Completable LetBinding -> Sh LambdaShellState ()+dumpTrace (File f) steps (Completable termStr) = do+   st <- getShellSt+   let parseSt = LamParseState (cpsStrategy st) (extSyntax st)+   case runParser (lambdaParser (letBindings st)) parseSt "" termStr of+      Left msg   -> shellPutErrLn (show msg)+      Right term -> do+         let trace = lamEvalTrace (letBindings st) (fullUnfold st)+                                  (redStrategy st)+                                  (unfoldTop (letBindings st) term)+         liftIO (writeFile f (unlines . map printLam . take steps $ trace))+++setTraceStep :: Int -> Sh LambdaShellState ()+setTraceStep step = getShellSt >>= \st -> putShellSt st{ traceNum = step }++showBinding :: Completable LetBinding -> Sh LambdaShellState ()+showBinding (Completable name) = do+    st <- getShellSt+    case Map.lookup name (letBindings st) of+        Nothing -> shellPutErrLn  $ concat ["'",name,"' not bound"]+        Just t  -> shellPutInfoLn $ concat [name," = ",printLam t]++showBindings :: Sh LambdaShellState ()+showBindings = do+   st <- getShellSt+   shellPutStrLn $+     Map.foldWithKey+       (\name t x -> concat [name," = ",printLam t,"\n",x])+       ""+       (letBindings st)++clearBindings :: Sh LambdaShellState ()+clearBindings = modifyShellSt (\st -> st{ letBindings = Map.empty })++loadDefFile :: File -> Sh LambdaShellState ()+loadDefFile (File path) = do+   st <- getShellSt+   let parseSt = LamParseState (cpsStrategy st) (extSyntax st)+   newBinds <- liftIO (readDefinitionFile parseSt (letBindings st) path)+   putShellSt st{ letBindings = newBinds }+++setRedWHNF :: Sh LambdaShellState ()+setRedWHNF = setRed lamReduceWHNF "weak head normal form"++setRedHNF :: Sh LambdaShellState ()+setRedHNF = setRed lamReduceHNF "head normal form"++setRedNF :: Sh LambdaShellState ()+setRedNF = setRed lamReduceNF "normal form"++setRedStrict :: Sh LambdaShellState ()+setRedStrict = setRed lamStrictNF "applicative order"++setRedNull :: Sh LambdaShellState ()+setRedNull = setRed lamReduceNull "no reduction"++setRed :: RS -> String -> Sh LambdaShellState ()+setRed strategy name = do+   shellPutInfoLn $ concat ["using reduction strategy: ",name]+   modifyShellSt (\st -> st{ redStrategy = strategy })++setCPSSimple :: Sh LambdaShellState ()+setCPSSimple = setCPS simple_cps "simple"++setCPSOnepass :: Sh LambdaShellState ()+setCPSOnepass = setCPS onepass_cps "onepass"++setCPS :: CPS LamParser -> String -> Sh LambdaShellState ()+setCPS cps name = do+   shellPutInfoLn $ concat ["unsing CPS strategy: ",name]+   modifyShellSt (\st -> st{ cpsStrategy = cps })++----------------------------------------------------------------+-- Normal statement evaluation++evaluate :: String -> Sh LambdaShellState ()+evaluate str = do+  case reverse str of+   '@':_ -> shellSpecial (ShellContinueLine (init str))+   _ -> do+      st <- getShellSt+      let parseSt = LamParseState (cpsStrategy st) (extSyntax st)+      case runParser (statementParser (letBindings st)) parseSt "" str of+        Left err   -> shellPutErrLn (show err)+        Right stmt ->+          case stmt of+           Stmt_eval expr      -> evalExpr expr+           Stmt_isEq x y       -> compareExpr x y+           Stmt_let nm expr    -> modifyShellSt (\st -> st{ letBindings = Map.insert nm expr (letBindings st) })+           Stmt_empty          -> return ()+++evalExpr :: PureLambda () String -> Sh LambdaShellState ()+evalExpr t = getShellSt >>= \st -> doEval (unfoldTop (letBindings st) t) st++ where+   doEval x st+    | trace st     = traceEval x+    | showCount st = evalCount x st+    | otherwise    = eval x st++   traceEval x = do+      subshell <- liftIO (traceSubshell x)+      shellSpecial (ExecSubshell subshell)++   evalCount t st = do+      let (z,n) = lamEvalCount (letBindings st) (fullUnfold st) (redStrategy st) t+      shellPutStrLn $ printLam z+      shellPutInfoLn $ concat ["<<",show n," reductions>>"]++   eval t st = do+      let z = lamEval (letBindings st) (fullUnfold st) (redStrategy st) t+      shellPutStrLn $ printLam z+++compareExpr :: PureLambda () String+            -> PureLambda () String+            -> Sh LambdaShellState ()++compareExpr x y = do+    st <- getShellSt+    if normalEq (letBindings st) x y+        then shellPutInfoLn "equal"+        else shellPutInfoLn "not equal"+++----------------------------------------------------------------+-- All the stuff for the tracing subshell++data TraceShellState+   = TraceShellState+     { tracePos  :: Int+     , traceStep :: Int+     , traceList :: [PureLambda () String]+     }++mkTraceDesc :: ShellDescription TraceShellState+mkTraceDesc =+  initialShellDescription+      { prompt         = \_ -> return "  ]"+      , commandStyle   = SingleCharCommands+      , shellCommands  = traceShellCommands+      , beforePrompt   = printTrace+      , historyEnabled = False+      }++traceShellCommands :: [ShellCommand TraceShellState]+traceShellCommands =+  [ cmd "p" tracePrev "previous"+  , cmd "n" traceNext "next"+  , helpCommand "h"+  , helpCommand "?"+  , exitCommand "q"+  ]++printTrace :: Sh TraceShellState ()+printTrace = do+  st <- getShellSt+  shellPutStr $ unlines $ map (\(n,t) -> concat[show n,") ",printLam t]) $+        take (traceStep st) $ drop (tracePos st) $ zip [1..] (traceList st)++tracePrev :: Sh TraceShellState ()+tracePrev = do+  modifyShellSt $ \st ->+      let x = max 0 (tracePos st - traceStep st) in+      st{ tracePos = x }++traceNext :: Sh TraceShellState ()+traceNext = do+  st <- getShellSt+  let x = tracePos st + traceStep st+  if null (drop (tracePos st) (traceList st))+     then return ()+     else putShellSt st{ tracePos = x }++mkTraceState :: PureLambda () String -> LambdaShellState -> IO TraceShellState+mkTraceState term st =+   return TraceShellState+          { tracePos  = 0+          , traceStep = traceNum st+          , traceList = lamEvalTrace (letBindings st) (fullUnfold st) (redStrategy st) term+          }++traceSubshell :: PureLambda () String -> IO (Subshell LambdaShellState TraceShellState)+traceSubshell term =+   simpleSubshell (mkTraceState term) mkTraceDesc

@@ -0,0 +1,409 @@+{-+ -   The Lambda Shell, an interactive environment for evaluating pure untyped lambda terms.+ -   Copyright (C) 2005-2007, Robert Dockins+ -+ -   This program 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.+ -+ -   This program 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 this program; if not, write to the Free Software+ -   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA+ -}+++module Version where++import Data.Version+import Paths_LambdaShell (version)++versionInfo :: String+versionInfo = unlines+  [ ""+  , "The Lambda Shell, version "++(showVersion version)+  , "Copyright 2005-2007, Robert Dockins"+  , ""+  ]++shellMessage :: String+shellMessage = unlines+  [ "The Lambda Shell comes with ABSOLUTELY NO WARRANTY; for details"+  , "type ':nowarranty'.  This is free software, and you are welcome to"+  , "redistribute it under certain conditions; type ':gpl'"+  , "for details"+  ]++noWarranty :: String  +noWarranty = unlines+  [ "			    NO WARRANTY"+  , ""+  , "  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY"+  , "FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN"+  , "OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES"+  , "PROVIDE THE PROGRAM \"AS IS\" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED"+  , "OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF"+  , "MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS"+  , "TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE"+  , "PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,"+  , "REPAIR OR CORRECTION."+  , ""+  , "  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING"+  , "WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR"+  , "REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,"+  , "INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING"+  , "OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED"+  , "TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY"+  , "YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER"+  , "PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE"+  , "POSSIBILITY OF SUCH DAMAGES."+  ]++gpl :: String+gpl = unlines+  ["		    GNU GENERAL PUBLIC LICENSE"+  ,"		       Version 2, June 1991"+  ,""+  ," Copyright (C) 1989, 1991 Free Software Foundation, Inc."+  ,"                       51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA"+  ," Everyone is permitted to copy and distribute verbatim copies"+  ," of this license document, but changing it is not allowed."+  ,""+  ,"			    Preamble"+  ,""+  ,"  The licenses for most software are designed to take away your"+  ,"freedom to share and change it.  By contrast, the GNU General Public"+  ,"License is intended to guarantee your freedom to share and change free"+  ,"software--to make sure the software is free for all its users.  This"+  ,"General Public License applies to most of the Free Software"+  ,"Foundation's software and to any other program whose authors commit to"+  ,"using it.  (Some other Free Software Foundation software is covered by"+  ,"the GNU Library General Public License instead.)  You can apply it to"+  ,"your programs, too."+  ,""+  ,"  When we speak of free software, we are referring to freedom, not"+  ,"price.  Our General Public Licenses are designed to make sure that you"+  ,"have the freedom to distribute copies of free software (and charge for"+  ,"this service if you wish), that you receive source code or can get it"+  ,"if you want it, that you can change the software or use pieces of it"+  ,"in new free programs; and that you know you can do these things."+  ,""+  ,"  To protect your rights, we need to make restrictions that forbid"+  ,"anyone to deny you these rights or to ask you to surrender the rights."+  ,"These restrictions translate to certain responsibilities for you if you"+  ,"distribute copies of the software, or if you modify it."+  ,""+  ,"  For example, if you distribute copies of such a program, whether"+  ,"gratis or for a fee, you must give the recipients all the rights that"+  ,"you have.  You must make sure that they, too, receive or can get the"+  ,"source code.  And you must show them these terms so they know their"+  ,"rights."+  ,""+  ,"  We protect your rights with two steps: (1) copyright the software, and"+  ,"(2) offer you this license which gives you legal permission to copy,"+  ,"distribute and/or modify the software."+  ,""+  ,"  Also, for each author's protection and ours, we want to make certain"+  ,"that everyone understands that there is no warranty for this free"+  ,"software.  If the software is modified by someone else and passed on, we"+  ,"want its recipients to know that what they have is not the original, so"+  ,"that any problems introduced by others will not reflect on the original"+  ,"authors' reputations."+  ,""+  ,"  Finally, any free program is threatened constantly by software"+  ,"patents.  We wish to avoid the danger that redistributors of a free"+  ,"program will individually obtain patent licenses, in effect making the"+  ,"program proprietary.  To prevent this, we have made it clear that any"+  ,"patent must be licensed for everyone's free use or not licensed at all."+  ,""+  ,"  The precise terms and conditions for copying, distribution and"+  ,"modification follow."+  ,""+  ,"		    GNU GENERAL PUBLIC LICENSE"+  ,"   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION"+  ,""+  ,"  0. This License applies to any program or other work which contains"+  ,"a notice placed by the copyright holder saying it may be distributed"+  ,"under the terms of this General Public License.  The \"Program\", below,"+  ,"refers to any such program or work, and a \"work based on the Program\""+  ,"means either the Program or any derivative work under copyright law:"+  ,"that is to say, a work containing the Program or a portion of it,"+  ,"either verbatim or with modifications and/or translated into another"+  ,"language.  (Hereinafter, translation is included without limitation in"+  ,"the term \"modification\".)  Each licensee is addressed as \"you\"."+  ,""+  ,"Activities other than copying, distribution and modification are not"+  ,"covered by this License; they are outside its scope.  The act of"+  ,"running the Program is not restricted, and the output from the Program"+  ,"is covered only if its contents constitute a work based on the"+  ,"Program (independent of having been made by running the Program)."+  ,"Whether that is true depends on what the Program does."+  ,""+  ,"  1. You may copy and distribute verbatim copies of the Program's"+  ,"source code as you receive it, in any medium, provided that you"+  ,"conspicuously and appropriately publish on each copy an appropriate"+  ,"copyright notice and disclaimer of warranty; keep intact all the"+  ,"notices that refer to this License and to the absence of any warranty;"+  ,"and give any other recipients of the Program a copy of this License"+  ,"along with the Program."+  ,""+  ,"You may charge a fee for the physical act of transferring a copy, and"+  ,"you may at your option offer warranty protection in exchange for a fee."+  ,""+  ,"  2. You may modify your copy or copies of the Program or any portion"+  ,"of it, thus forming a work based on the Program, and copy and"+  ,"distribute such modifications or work under the terms of Section 1"+  ,"above, provided that you also meet all of these conditions:"+  ,""+  ,"    a) You must cause the modified files to carry prominent notices"+  ,"    stating that you changed the files and the date of any change."+  ,""+  ,"    b) You must cause any work that you distribute or publish, that in"+  ,"    whole or in part contains or is derived from the Program or any"+  ,"    part thereof, to be licensed as a whole at no charge to all third"+  ,"    parties under the terms of this License."+  ,""+  ,"    c) If the modified program normally reads commands interactively"+  ,"    when run, you must cause it, when started running for such"+  ,"    interactive use in the most ordinary way, to print or display an"+  ,"    announcement including an appropriate copyright notice and a"+  ,"    notice that there is no warranty (or else, saying that you provide"+  ,"    a warranty) and that users may redistribute the program under"+  ,"    these conditions, and telling the user how to view a copy of this"+  ,"    License.  (Exception: if the Program itself is interactive but"+  ,"    does not normally print such an announcement, your work based on"+  ,"    the Program is not required to print an announcement.)"+  ,""+  ,"These requirements apply to the modified work as a whole.  If"+  ,"identifiable sections of that work are not derived from the Program,"+  ,"and can be reasonably considered independent and separate works in"+  ,"themselves, then this License, and its terms, do not apply to those"+  ,"sections when you distribute them as separate works.  But when you"+  ,"distribute the same sections as part of a whole which is a work based"+  ,"on the Program, the distribution of the whole must be on the terms of"+  ,"this License, whose permissions for other licensees extend to the"+  ,"entire whole, and thus to each and every part regardless of who wrote it."+  ,""+  ,"Thus, it is not the intent of this section to claim rights or contest"+  ,"your rights to work written entirely by you; rather, the intent is to"+  ,"exercise the right to control the distribution of derivative or"+  ,"collective works based on the Program."+  ,""+  ,"In addition, mere aggregation of another work not based on the Program"+  ,"with the Program (or with a work based on the Program) on a volume of"+  ,"a storage or distribution medium does not bring the other work under"+  ,"the scope of this License."+  ,""+  ,"  3. You may copy and distribute the Program (or a work based on it,"+  ,"under Section 2) in object code or executable form under the terms of"+  ,"Sections 1 and 2 above provided that you also do one of the following:"+  ,""+  ,"    a) Accompany it with the complete corresponding machine-readable"+  ,"    source code, which must be distributed under the terms of Sections"+  ,"    1 and 2 above on a medium customarily used for software interchange; or,"+  ,""+  ,"    b) Accompany it with a written offer, valid for at least three"+  ,"    years, to give any third party, for a charge no more than your"+  ,"    cost of physically performing source distribution, a complete"+  ,"    machine-readable copy of the corresponding source code, to be"+  ,"    distributed under the terms of Sections 1 and 2 above on a medium"+  ,"    customarily used for software interchange; or,"+  ,""+  ,"    c) Accompany it with the information you received as to the offer"+  ,"    to distribute corresponding source code.  (This alternative is"+  ,"    allowed only for noncommercial distribution and only if you"+  ,"    received the program in object code or executable form with such"+  ,"    an offer, in accord with Subsection b above.)"+  ,""+  ,"The source code for a work means the preferred form of the work for"+  ,"making modifications to it.  For an executable work, complete source"+  ,"code means all the source code for all modules it contains, plus any"+  ,"associated interface definition files, plus the scripts used to"+  ,"control compilation and installation of the executable.  However, as a"+  ,"special exception, the source code distributed need not include"+  ,"anything that is normally distributed (in either source or binary"+  ,"form) with the major components (compiler, kernel, and so on) of the"+  ,"operating system on which the executable runs, unless that component"+  ,"itself accompanies the executable."+  ,""+  ,"If distribution of executable or object code is made by offering"+  ,"access to copy from a designated place, then offering equivalent"+  ,"access to copy the source code from the same place counts as"+  ,"distribution of the source code, even though third parties are not"+  ,"compelled to copy the source along with the object code."+  ,""+  ,"  4. You may not copy, modify, sublicense, or distribute the Program"+  ,"except as expressly provided under this License.  Any attempt"+  ,"otherwise to copy, modify, sublicense or distribute the Program is"+  ,"void, and will automatically terminate your rights under this License."+  ,"However, parties who have received copies, or rights, from you under"+  ,"this License will not have their licenses terminated so long as such"+  ,"parties remain in full compliance."+  ,""+  ,"  5. You are not required to accept this License, since you have not"+  ,"signed it.  However, nothing else grants you permission to modify or"+  ,"distribute the Program or its derivative works.  These actions are"+  ,"prohibited by law if you do not accept this License.  Therefore, by"+  ,"modifying or distributing the Program (or any work based on the"+  ,"Program), you indicate your acceptance of this License to do so, and"+  ,"all its terms and conditions for copying, distributing or modifying"+  ,"the Program or works based on it."+  ,""+  ,"  6. Each time you redistribute the Program (or any work based on the"+  ,"Program), the recipient automatically receives a license from the"+  ,"original licensor to copy, distribute or modify the Program subject to"+  ,"these terms and conditions.  You may not impose any further"+  ,"restrictions on the recipients' exercise of the rights granted herein."+  ,"You are not responsible for enforcing compliance by third parties to"+  ,"this License."+  ,""+  ,"  7. If, as a consequence of a court judgment or allegation of patent"+  ,"infringement or for any other reason (not limited to patent issues),"+  ,"conditions are imposed on you (whether by court order, agreement or"+  ,"otherwise) that contradict the conditions of this License, they do not"+  ,"excuse you from the conditions of this License.  If you cannot"+  ,"distribute so as to satisfy simultaneously your obligations under this"+  ,"License and any other pertinent obligations, then as a consequence you"+  ,"may not distribute the Program at all.  For example, if a patent"+  ,"license would not permit royalty-free redistribution of the Program by"+  ,"all those who receive copies directly or indirectly through you, then"+  ,"the only way you could satisfy both it and this License would be to"+  ,"refrain entirely from distribution of the Program."+  ,""+  ,"If any portion of this section is held invalid or unenforceable under"+  ,"any particular circumstance, the balance of the section is intended to"+  ,"apply and the section as a whole is intended to apply in other"+  ,"circumstances."+  ,""+  ,"It is not the purpose of this section to induce you to infringe any"+  ,"patents or other property right claims or to contest validity of any"+  ,"such claims; this section has the sole purpose of protecting the"+  ,"integrity of the free software distribution system, which is"+  ,"implemented by public license practices.  Many people have made"+  ,"generous contributions to the wide range of software distributed"+  ,"through that system in reliance on consistent application of that"+  ,"system; it is up to the author/donor to decide if he or she is willing"+  ,"to distribute software through any other system and a licensee cannot"+  ,"impose that choice."+  ,""+  ,"This section is intended to make thoroughly clear what is believed to"+  ,"be a consequence of the rest of this License."+  ,""+  ,"  8. If the distribution and/or use of the Program is restricted in"+  ,"certain countries either by patents or by copyrighted interfaces, the"+  ,"original copyright holder who places the Program under this License"+  ,"may add an explicit geographical distribution limitation excluding"+  ,"those countries, so that distribution is permitted only in or among"+  ,"countries not thus excluded.  In such case, this License incorporates"+  ,"the limitation as if written in the body of this License."+  ,""+  ,"  9. The Free Software Foundation may publish revised and/or new versions"+  ,"of the General Public License from time to time.  Such new versions will"+  ,"be similar in spirit to the present version, but may differ in detail to"+  ,"address new problems or concerns."+  ,""+  ,"Each version is given a distinguishing version number.  If the Program"+  ,"specifies a version number of this License which applies to it and \"any"+  ,"later version\", you have the option of following the terms and conditions"+  ,"either of that version or of any later version published by the Free"+  ,"Software Foundation.  If the Program does not specify a version number of"+  ,"this License, you may choose any version ever published by the Free Software"+  ,"Foundation."+  ,""+  ,"  10. If you wish to incorporate parts of the Program into other free"+  ,"programs whose distribution conditions are different, write to the author"+  ,"to ask for permission.  For software which is copyrighted by the Free"+  ,"Software Foundation, write to the Free Software Foundation; we sometimes"+  ,"make exceptions for this.  Our decision will be guided by the two goals"+  ,"of preserving the free status of all derivatives of our free software and"+  ,"of promoting the sharing and reuse of software generally."+  ,""+  ,"			    NO WARRANTY"+  ,""+  ,"  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY"+  ,"FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN"+  ,"OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES"+  ,"PROVIDE THE PROGRAM \"AS IS\" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED"+  ,"OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF"+  ,"MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS"+  ,"TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE"+  ,"PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,"+  ,"REPAIR OR CORRECTION."+  ,""+  ,"  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING"+  ,"WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR"+  ,"REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,"+  ,"INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING"+  ,"OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED"+  ,"TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY"+  ,"YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER"+  ,"PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE"+  ,"POSSIBILITY OF SUCH DAMAGES."+  ,""+  ,"		     END OF TERMS AND CONDITIONS"+  ,""+  ,"	    How to Apply These Terms to Your New Programs"+  ,""+  ,"  If you develop a new program, and you want it to be of the greatest"+  ,"possible use to the public, the best way to achieve this is to make it"+  ,"free software which everyone can redistribute and change under these terms."+  ,""+  ,"  To do so, attach the following notices to the program.  It is safest"+  ,"to attach them to the start of each source file to most effectively"+  ,"convey the exclusion of warranty; and each file should have at least"+  ,"the \"copyright\" line and a pointer to where the full notice is found."+  ,""+  ,"    <one line to give the program's name and a brief idea of what it does.>"+  ,"    Copyright (C) <year>  <name of author>"+  ,""+  ,"    This program 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."+  ,""+  ,"    This program 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 this program; if not, write to the Free Software"+  ,"    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA"+  ,""+  ,""+  ,"Also add information on how to contact you by electronic and paper mail."+  ,""+  ,"If the program is interactive, make it output a short notice like this"+  ,"when it starts in an interactive mode:"+  ,""+  ,"    Gnomovision version 69, Copyright (C) year name of author"+  ,"    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'."+  ,"    This is free software, and you are welcome to redistribute it"+  ,"    under certain conditions; type `show c' for details."+  ,""+  ,"The hypothetical commands `show w' and `show c' should show the appropriate"+  ,"parts of the General Public License.  Of course, the commands you use may"+  ,"be called something other than `show w' and `show c'; they could even be"+  ,"mouse-clicks or menu items--whatever suits your program."+  ,""+  ,"You should also get your employer (if you work as a programmer) or your"+  ,"school, if any, to sign a \"copyright disclaimer\" for the program, if"+  ,"necessary.  Here is a sample; alter the names:"+  ,""+  ,"  Yoyodyne, Inc., hereby disclaims all copyright interest in the program"+  ,"  `Gnomovision' (which makes passes at compilers) written by James Hacker."+  ,""+  ,"  <signature of Ty Coon>, 1 April 1989"+  ,"  Ty Coon, President of Vice"+  ,""+  ,"This General Public License does not permit incorporating your program into"+  ,"proprietary programs.  If your program is a subroutine library, you may"+  ,"consider it more useful to permit linking proprietary applications with the"+  ,"library.  If this is what you want to do, use the GNU Library General"+  ,"Public License instead of this License."+  ]

@@ -0,0 +1,24 @@+{-+ -   The Lambda Shell, an interactive environment for evaluating pure untyped lambda terms.+ -   Copyright (C) 2005-2007, Robert Dockins+ -+ -   This program 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.+ -+ -   This program 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 this program; if not, write to the Free Software+ -   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA+ -}++import System.Environment+import LambdaCmdLine++main :: IO ()+main = getArgs >>= lambdaCmdLine