Add function for finding all beta redexes in a lambda term

Author: nigosto

lambda-parser.cabal

@@ -29,13 +29,14 @@ executable lambda-parser
     -- Modules included in this executable, other than Main.
     other-modules:
         Examples.Terms
+        Interaction
         Parser
         Transformer
+        Generator
         Substitution.Named
         Substitution.Nameless
-        Generator
-        Stack
-        Interaction
+        Libs.Stack
+        Libs.BetaRedexes
 
     -- LANGUAGE extensions used by modules in this package.
     -- other-extensions:

src/Examples/Terms.hs

@@ -7,7 +7,7 @@ simpleApplication :: String
 simpleApplication = "xy"
 
 complexApplication :: String
-complexApplication = "(xy)z"
+complexApplication = "xyz"
 
 simpleAbstraction :: String
 simpleAbstraction = "λx.x"
@@ -19,14 +19,23 @@ brackets :: String
 brackets = "(xy)"
 
 composed :: String
-composed = "(λx.(ab)x)(yz)"
+composed = "(λx.abx)(yz)"
 
 currySubstitution1 :: String
 currySubstitution1 = "λy.yλa.ax"
 
 currySubstitution2 :: String
 currySubstitution2 = "λy.λa.yax"
 
+betaRedexes :: String
+betaRedexes = "(λx.x)((λy.y)z)u"
+
+singleBetaRedex :: String
+singleBetaRedex = "λz.(λx.λy.x)(λu.u)(λu.uzu)z"
+
+complexBetaRedexes :: String
+complexBetaRedexes = "(λx.xz)((λy.zy)z)"
+
 allExamples :: [String]
 allExamples = [
   variable, 
@@ -37,4 +46,7 @@ allExamples = [
   brackets, 
   composed, 
   currySubstitution1, 
-  currySubstitution2 ]
+  currySubstitution2,
+  betaRedexes,
+  singleBetaRedex,
+  complexBetaRedexes ]

src/Interaction.hs

@@ -3,7 +3,7 @@ module Interaction where
 import Prelude hiding (lookup)
 import Generator (generateTerm, generateNamelessTerm)
 import Parser (parseTerm)
-import Stack (emptyStack)
+import Libs.Stack (emptyStack)
 import Substitution.Named (substitute)
 import Transformer (toNameless, toNamed)
 import Data.Map (empty, lookup)

src/Libs/BetaRedexes.hs

@@ -0,0 +1,15 @@
+module Libs.BetaRedexes where
+import Parser (Term (Variable, Application, Abstraction))
+import Generator (generateTerm)
+
+extractBetaRedexes :: Term -> [Term]
+extractBetaRedexes (Variable _) = []
+extractBetaRedexes term@(Application lhs@(Abstraction _ body) rhs) =
+  term : extractBetaRedexes body ++ extractBetaRedexes rhs
+extractBetaRedexes (Application lhs rhs) =
+  extractBetaRedexes lhs ++ extractBetaRedexes rhs
+extractBetaRedexes (Abstraction _ body) = extractBetaRedexes body
+
+displayBetaRedexes :: Term -> IO ()
+displayBetaRedexes term =
+  mapM_ (putStrLn . generateTerm) $ extractBetaRedexes term

src/Stack.hs renamed to src/Libs/Stack.hs

@@ -1,4 +1,4 @@
-module Stack where
+module Libs.Stack where
 
 type Stack t = [t]
 

src/Main.hs

@@ -1,14 +1,6 @@
 module Main where
 
-import Data.Map (empty, lookup)
-import Generator (generateNamelessTerm, generateTerm)
-import Parser (Term (Variable), parseTerm)
-import Substitution.Named (substitute)
-import Substitution.Nameless (substituteNameless)
 import System.IO (BufferMode (BlockBuffering), hSetBuffering, stdout)
-import Transformer (toNamed, toNameless)
-import Prelude hiding (lookup)
-import Stack (emptyStack)
 import Interaction (getSubstitutionType, getOutputTermType, doSubstituteNameless, TermType (Named), doSubstituteNamed)
 
 main :: IO ()

src/Parser.hs

@@ -1,7 +1,7 @@
 module Parser (parseTerm, Term(Variable, Application, Abstraction)) where
+
 import Data.Char (isAlpha)
-import Debug.Trace (trace)
-import Stack (Stack, peek, pop, emptyStack, push)
+import Libs.Stack (Stack, peek, pop, emptyStack, push)
 
 data Term =
   Variable Char |