diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. + + + Copyright (C) + + 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. + + , 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. diff --git a/LambdaShell.cabal b/LambdaShell.cabal new file mode 100644 --- /dev/null +++ b/LambdaShell.cabal @@ -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 diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -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/ +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 diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,3 @@ +#!/usr/bin/env runhaskell +import Distribution.Simple +main = defaultMain diff --git a/prelude.lam b/prelude.lam new file mode 100644 --- /dev/null +++ b/prelude.lam @@ -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))); diff --git a/src/CPS.hs b/src/CPS.hs new file mode 100644 --- /dev/null +++ b/src/CPS.hs @@ -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) + ) diff --git a/src/Env.hs b/src/Env.hs new file mode 100644 --- /dev/null +++ b/src/Env.hs @@ -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]) diff --git a/src/Lambda.hs b/src/Lambda.hs new file mode 100644 --- /dev/null +++ b/src/Lambda.hs @@ -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 diff --git a/src/LambdaCmdLine.hs b/src/LambdaCmdLine.hs new file mode 100644 --- /dev/null +++ b/src/LambdaCmdLine.hs @@ -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 {