redacted prelude solutions

.envrc

@@ -0,0 +1,2 @@
+nix_direnv_watch_file *.cabal
+use flake

.gitattributes

@@ -0,0 +1 @@
+flake.lock linguist-generated=true

.github/workflows/ci.yaml

@@ -0,0 +1,38 @@
+name: "CI"
+on:
+  # Run only when pushing to master branch, and making PRs
+  push:
+    branches:
+      - master
+  pull_request:
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - uses: nixbuild/nix-quick-install-action@v22
+        with:
+          nix_conf: |
+            experimental-features = nix-command flakes
+            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
+      - name: Cache Nix dependencies
+        run: |
+          nix develop -j 4 -c echo
+      - name: Build 🔨
+        id: build
+        run: |
+          nix build -j auto -L
+      - name: Flake checks 🧪
+        run: |
+          # Because 'nix flake check' is not system-aware
+          # See https://srid.ca/haskell-template/checks
+          nix run nixpkgs#sd \
+            'systems = nixpkgs.lib.systems.flakeExposed' \
+            'systems = [ "x86_64-linux" ]' \
+            flake.nix
+
+          # Sandbox must be disabed for:
+          # https://github.com/srid/haskell-flake/issues/21
+          nix \
+            --option sandbox false \
+            flake check -L

.github/workflows/update-flake-lock.yaml

@@ -0,0 +1,24 @@
+name: update-flake-lock
+on:
+  workflow_dispatch: # allows manual triggering
+  # schedule:
+  #   - cron: '0 0 * * 0' # runs weekly on Sunday at 00:00
+
+jobs:
+  lockfile:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v2
+      - name: Install Nix
+        uses: cachix/install-nix-action@v17
+        with:
+          extra_nix_config: |
+            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
+      - name: Update flake.lock
+        uses: DeterminateSystems/update-flake-lock@v14
+        with:
+          token: ${{ secrets.GH_TOKEN_FOR_UPDATES }}
+          pr-title: "Update flake.lock" # Title of PR to be created
+          pr-labels: |                  # Labels to be set on the PR
+            automated

.gitignore

@@ -0,0 +1,12 @@
+# cabal
+dist
+dist-*
+cabal.project.local
+cabal.project.local~
+
+# nix
+result
+result-*
+
+# direnv
+.direnv

.vscode/extensions.json

@@ -0,0 +1,9 @@
+{
+  // See https://go.microsoft.com/fwlink/?LinkId=827846
+  // for the documentation about the extensions.json format
+  "recommendations": [
+    "haskell.haskell",
+    "arrterian.nix-env-selector",
+    "bbenoist.nix",
+  ]
+}

.vscode/settings.json

@@ -0,0 +1,8 @@
+{
+  "editor.formatOnType": true,
+  "editor.formatOnSave": true,
+  "nixEnvSelector.nixFile": "${workspaceRoot}/shell.nix",
+  // "nixEnvSelector.args": "--pure"
+  "haskell.formattingProvider": "fourmolu",
+  "haskell.manageHLS": "PATH"
+}

.vscode/tasks.json

@@ -0,0 +1,27 @@
+{
+    // See https://go.microsoft.com/fwlink/?LinkId=733558
+    // for the documentation about the tasks.json format
+    "version": "2.0.0",
+    "tasks": [
+        {
+            "label": "Ghcid",
+            "type": "shell",
+            // This is useful if you often see ghost ghcid left behind by VSCode reloads.
+            "command": "nix",
+            "args": [
+                "develop",
+                "-c",
+                ",",
+                "run"
+            ],
+            "problemMatcher": [],
+            "group": {
+                "kind": "build",
+                "isDefault": true
+            },
+            "runOptions": {
+                // "runOn": "folderOpen"
+            }
+        }
+    ]
+}

LICENSE

@@ -0,0 +1,19 @@
+MIT License
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

flake.lock

@@ -0,0 +1,133 @@
+{
+  "nodes": {
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib"
+      },
+      "locked": {
+        "lastModified": 1679737941,
+        "narHash": "sha256-srSD9CwsVPnUMsIZ7Kt/UegkKUEBcTyU1Rev7mO45S0=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "3502ee99d6dade045bdeaf7b0cd8ec703484c25c",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "flake-root": {
+      "locked": {
+        "lastModified": 1671378805,
+        "narHash": "sha256-yqGxyzMN2GuppwG3dTWD1oiKxi+jGYP7D1qUSc5vKhI=",
+        "owner": "srid",
+        "repo": "flake-root",
+        "rev": "dc7ba6166e478804a9da6881aa48c45d300075cf",
+        "type": "github"
+      },
+      "original": {
+        "owner": "srid",
+        "repo": "flake-root",
+        "type": "github"
+      }
+    },
+    "haskell-flake": {
+      "locked": {
+        "lastModified": 1679690126,
+        "narHash": "sha256-u6pQejlTLC1QSKLMB/8Ch+2VvgILlxuZsBHAbDn0zHM=",
+        "owner": "srid",
+        "repo": "haskell-flake",
+        "rev": "d63943b612dbe30e2aba8aab0e60f1011c369973",
+        "type": "github"
+      },
+      "original": {
+        "owner": "srid",
+        "repo": "haskell-flake",
+        "type": "github"
+      }
+    },
+    "mission-control": {
+      "locked": {
+        "lastModified": 1679674077,
+        "narHash": "sha256-hGz63fsyRGthjE6LLqB08IHApcBvHhI87gWrFN/Uu5w=",
+        "owner": "Platonic-Systems",
+        "repo": "mission-control",
+        "rev": "d07854a616f559370b71c1c440d916ab6869f084",
+        "type": "github"
+      },
+      "original": {
+        "owner": "Platonic-Systems",
+        "repo": "mission-control",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1679734080,
+        "narHash": "sha256-z846xfGLlon6t9lqUzlNtBOmsgQLQIZvR6Lt2dImk1M=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "dbf5322e93bcc6cfc52268367a8ad21c09d76fea",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixpkgs-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-lib": {
+      "locked": {
+        "dir": "lib",
+        "lastModified": 1678375444,
+        "narHash": "sha256-XIgHfGvjFvZQ8hrkfocanCDxMefc/77rXeHvYdzBMc8=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "130fa0baaa2b93ec45523fdcde942f6844ee9f6e",
+        "type": "github"
+      },
+      "original": {
+        "dir": "lib",
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "flake-root": "flake-root",
+        "haskell-flake": "haskell-flake",
+        "mission-control": "mission-control",
+        "nixpkgs": "nixpkgs",
+        "treefmt-nix": "treefmt-nix"
+      }
+    },
+    "treefmt-nix": {
+      "inputs": {
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1679588014,
+        "narHash": "sha256-URkRSunu8HAp2vH2KgLogjAXckiufCDFrBs59g9uiLY=",
+        "owner": "numtide",
+        "repo": "treefmt-nix",
+        "rev": "af75d6efe437858f9ca5535e622cfbedad1ba717",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "treefmt-nix",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,97 @@
+{
+  description = "srid/haskell-template: Nix template for Haskell projects";
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
+    flake-parts.url = "github:hercules-ci/flake-parts";
+    haskell-flake.url = "github:srid/haskell-flake";
+    treefmt-nix.url = "github:numtide/treefmt-nix";
+    treefmt-nix.inputs.nixpkgs.follows = "nixpkgs";
+    flake-root.url = "github:srid/flake-root";
+    mission-control.url = "github:Platonic-Systems/mission-control";
+  };
+
+  outputs = inputs@{ self, nixpkgs, flake-parts, ... }:
+    flake-parts.lib.mkFlake { inherit inputs; } {
+      systems = nixpkgs.lib.systems.flakeExposed;
+      imports = [
+        inputs.haskell-flake.flakeModule
+        inputs.treefmt-nix.flakeModule
+        inputs.flake-root.flakeModule
+        inputs.mission-control.flakeModule
+      ];
+      perSystem = { self', system, lib, config, pkgs, ... }: {
+        # The "main" project. You can have multiple projects, but this template
+        # has only one.
+        haskellProjects.main = {
+          packages.lambda.root = ./.; # Auto-discovered by haskell-flake
+          overrides = self: super: { };
+          devShell = {
+            tools = hp: {
+              treefmt = config.treefmt.build.wrapper;
+            } // config.treefmt.build.programs;
+            hlsCheck.enable = true;
+          };
+        };
+
+        # Auto formatters. This also adds a flake check to ensure that the
+        # source tree was auto formatted.
+        treefmt.config = {
+          inherit (config.flake-root) projectRootFile;
+          package = pkgs.treefmt;
+          flakeFormatter = false; # For https://github.com/numtide/treefmt-nix/issues/55
+
+          programs.ormolu.enable = true;
+          programs.nixpkgs-fmt.enable = true;
+          programs.cabal-fmt.enable = true;
+          programs.hlint.enable = true;
+
+          # We use fourmolu
+          programs.ormolu.package = pkgs.haskellPackages.fourmolu;
+          settings.formatter.ormolu = {
+            options = [
+              "--ghc-opt"
+              "-XImportQualifiedPost"
+            ];
+          };
+        };
+
+        # Dev shell scripts.
+        mission-control.scripts = {
+          docs = {
+            description = "Start Hoogle server for project dependencies";
+            exec = ''
+              echo http://127.0.0.1:8888
+              hoogle serve -p 8888 --local
+            '';
+            category = "Dev Tools";
+          };
+          repl = {
+            description = "Start the cabal repl";
+            exec = ''
+              cabal repl "$@"
+            '';
+            category = "Dev Tools";
+          };
+          fmt = {
+            description = "Format the source tree";
+            exec = config.treefmt.build.wrapper;
+            category = "Dev Tools";
+          };
+          run = {
+            description = "Run the program";
+            exec = ''
+              cabal run
+            '';
+            category = "Primary";
+          };
+        };
+
+        # Default package.
+        packages.default = self'.packages.main-lambda;
+
+        # Default shell.
+        devShells.default =
+          config.mission-control.installToDevShell self'.devShells.main;
+      };
+    };
+}

fourmolu.yaml

@@ -0,0 +1,8 @@
+indentation: 2
+comma-style: leading
+record-brace-space: true 
+indent-wheres: true
+diff-friendly-import-export: true 
+respectful: true 
+haddock-style: multi-line 
+newlines-between-decls: 1 

hie.yaml

@@ -0,0 +1,4 @@
+cradle:
+  cabal:
+    - path: "src"
+      component: "exe:lambda"

lambda.cabal

@@ -0,0 +1,34 @@
+cabal-version:      2.4
+name:               lambda
+version:            0.1.0.0
+license:            MIT
+author:             Leon Vatthauer
+category:           Education
+extra-source-files:
+  LICENSE
+  README.md
+
+common shared
+  build-depends:
+    , base        >=4.13.0.0  && <4.18.0.0.0
+    , containers  >=0.5.9.1.0
+    , extra       >=1.7
+    , mtl         >=2.1.0     && <2.3
+    , parsec      >=3.1.15.0
+    , haskeline   >=0.8.0.0
+
+  default-extensions:
+    ImportQualifiedPost
+    InstanceSigs
+
+  hs-source-dirs:     src
+  default-language:   Haskell2010
+
+executable lambda
+  import:        shared
+  main-is:       Main.hs
+  other-modules:
+    Lexer
+    Parser
+    Reduction
+    Syntax

shell.nix

@@ -0,0 +1 @@
+(builtins.getFlake ("git+file://" + toString ./.)).devShells.${builtins.currentSystem}.default

src/Lexer.hs

@@ -0,0 +1,50 @@
+{-# LANGUAGE ImportQualifiedPost #-}
+
+module Lexer where
+
+import Text.Parsec.Char (alphaNum, letter, oneOf)
+import Text.Parsec.Language (emptyDef)
+import Text.Parsec.String (Parser)
+import Text.Parsec.Token qualified as Tok
+
+lexer :: Tok.TokenParser ()
+lexer = Tok.makeTokenParser style
+  where
+    ops = ["\\", "="]
+    names = []
+    style =
+      emptyDef
+        { Tok.commentLine = "#"
+        , Tok.reservedOpNames = ops
+        , Tok.reservedNames = names
+        , Tok.opLetter = oneOf "\\=."
+        , Tok.identStart = letter
+        , Tok.identLetter = alphaNum
+        }
+
+digit :: Parser Integer
+digit = Tok.natural lexer
+
+parens :: Parser a -> Parser a
+parens = Tok.parens lexer
+
+dot :: Parser String
+dot = Tok.dot lexer
+
+semi :: Parser String
+semi = Tok.semi lexer
+
+identifier :: Parser String
+identifier = Tok.identifier lexer
+
+reserved :: String -> Parser ()
+reserved = Tok.reserved lexer
+
+reservedOp :: String -> Parser ()
+reservedOp = Tok.reservedOp lexer
+
+whiteSpace :: Parser ()
+whiteSpace = Tok.whiteSpace lexer
+
+newline :: Parser String
+newline = Tok.symbol lexer "\n"

src/Main.hs

@@ -0,0 +1,75 @@
+module Main where
+
+import Control.Exception (SomeException (SomeException), catch)
+import Control.Monad.State (
+  MonadIO (liftIO),
+  MonadTrans (lift),
+  StateT,
+  evalStateT,
+  gets,
+  lift,
+  modify,
+ )
+import Data.Functor (($>))
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as Map
+import Data.Maybe (fromJust)
+import Parser (parseLine, parsePrelude, readP)
+import Reduction (reduce)
+import Syntax (Declaration (..), Term)
+import System.Console.Haskeline (
+  InputT,
+  defaultSettings,
+  getInputLine,
+  runInputT,
+ )
+import System.IO (IOMode (ReadMode), hGetContents, openFile)
+
+-- REPL
+newtype ReplState = ReplState {declarations :: Map String Term}
+insertDeclaration :: Declaration -> ReplM ()
+insertDeclaration (Declaration name term) = modify (\state -> state {declarations = Map.insert name term (declarations state)})
+type ReplM = StateT ReplState IO
+initialState :: ReplState
+initialState = ReplState . Map.fromList $ map (\(Declaration name term) -> (name, term)) []
+
+main :: IO ()
+main = evalStateT (readPrelude >> runInputT defaultSettings repl) initialState
+  where
+    repl :: InputT ReplM ()
+    repl = do
+      minput <- getInputLine "λ "
+      case minput of
+        Nothing -> return ()
+        Just line -> do
+          lift $ evalLine line
+          repl
+
+-- Try reading prelude definitions from prelude.lmd
+readPrelude :: ReplM ()
+readPrelude = do
+  decls <- liftIO $ catch getDecls handleException
+  mapM_ insertDeclaration decls
+  where
+    getDecls :: IO [Declaration]
+    getDecls = do
+      handle <- liftIO $ openFile "prelude.lmd" ReadMode
+      content <- liftIO $ hGetContents handle
+      let declsE = parsePrelude content
+      case declsE of
+        Left err -> putStrLn ("Error while parsing prelude:\n" ++ show err) $> []
+        Right decls -> putStrLn "Prelude successfully read from prelude.lmd!" $> decls
+    handleException :: SomeException -> IO [Declaration]
+    handleException e = putStrLn "Couldn't read file prelude.lmd so no prelude was loaded." >> return []
+
+-- evaluate a single line from stdin
+evalLine :: String -> ReplM ()
+evalLine "" = return ()
+evalLine line = either (liftIO . print) computeLine $ parseLine line
+
+-- do computations for a single line
+computeLine :: Either Declaration Term -> ReplM ()
+computeLine (Left decl) = insertDeclaration decl
+computeLine (Right term) = do
+  decls <- gets declarations
+  liftIO $ reduce 0 False decls term

src/Parser.hs

@@ -0,0 +1,79 @@
+module Parser (parseLine, readP, parsePrelude) where
+
+import Data.Either.Extra (eitherToMaybe)
+import Lexer (digit, dot, identifier, parens, reservedOp, semi, whiteSpace)
+import Syntax (Declaration (..), Term (..))
+import Text.Parsec (
+  ParseError,
+  endBy,
+  eof,
+  many,
+  many1,
+  newline,
+  parse,
+  sepBy,
+  try,
+  (<?>),
+  (<|>),
+ )
+import Text.Parsec.String (Parser)
+import Prelude hiding (abs)
+
+line :: Parser (Either Declaration Term)
+line = try (Left <$> declaration) <|> try (Right <$> term)
+
+declaration :: Parser Declaration
+declaration =
+  Declaration
+    <$> identifier
+    <*> (reservedOp "=" *> term)
+    <?> "declaration"
+
+term :: Parser Term
+term = abs <|> app <|> numeral <|> var
+
+atomicTerm :: Parser Term
+atomicTerm = abs <|> numeral <|> var <|> (parens term <?> "nested term")
+
+var :: Parser Term
+var =
+  Var
+    <$> identifier
+
+numeral :: Parser Term
+numeral =
+  churchEncode
+    <$> digit
+
+churchEncode :: Integer -> Term
+churchEncode n = Abs "f" (Abs "a" (go n))
+  where
+    go 0 = Var "a"
+    go n = App (Var "f") (go (n - 1))
+
+app :: Parser Term
+app = foldl1 App <$> many1 atomicTerm
+
+abs :: Parser Term
+abs =
+  Abs
+    <$> (reservedOp "\\" *> identifier)
+    <*> (dot *> term)
+    <?> "lambda abstraction"
+
+-- runners
+contents :: Parser a -> Parser a
+contents p = do
+  whiteSpace
+  r <- p
+  eof
+  return r
+
+parseLine :: String -> Either ParseError (Either Declaration Term)
+parseLine = Text.Parsec.parse (contents line) "stdin"
+
+parsePrelude :: String -> Either ParseError [Declaration]
+parsePrelude = Text.Parsec.parse (contents (declaration `endBy` semi)) "prelude.lmd"
+
+readP :: String -> Maybe Term
+readP line = eitherToMaybe (Text.Parsec.parse (contents term) "sourcefile" line)

src/Reduction.hs

@@ -0,0 +1,120 @@
+module Reduction (reduce) where
+
+import Control.Monad (when)
+import Data.Char (toLower)
+import Data.List (find)
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as Map
+import Data.Maybe (fromMaybe)
+import Data.Maybe qualified as Maybe
+import Data.Set (Set)
+import Data.Set qualified as Set
+import Syntax (Substitution, Term (..), Var)
+
+-- a stock of variablenames that is used for getting fresh variables
+vars :: [Var]
+vars = ['v' : '$' : show n | n <- [0 :: Int ..]]
+
+-- free variables
+fv :: Term -> Set Var
+fv (Var v) = Set.singleton v
+fv (App t1 t2) = Set.union (fv t1) (fv t2)
+fv (Abs v t) = Set.difference (fv t) (Set.singleton v)
+
+-- capture avoiding substitution
+substT :: Substitution -> Term -> Term
+substT o (Var x) = o x
+substT o (App t1 t2) = App (substT o t1) (substT o t2)
+substT o (Abs x t) = Abs y (substT o' t)
+  where
+    y = if isFresh x then x else fromMaybe (error "Error: no fresh variable found, cant happen!") $ find isFresh vars
+    o' v
+      | v == x = Var y
+      | otherwise = o v
+    zs = Set.map o $ fv (Abs x t)
+    isFresh :: Var -> Bool
+    isFresh e = not (any (Set.member e . fv) zs)
+
+-- do a single reduction step, implements 'normal-reduction'
+reduceStep :: Map String Term -> Term -> (Reduction, Term)
+-- abstraction: reduce the inner term
+reduceStep globals (Abs x t) = let (r, t') = reduceStep globals t in (r, Abs x t')
+-- abstraction applied to term - beta reduction!
+reduceStep globals (App (Abs x t) s) = (Beta, substT (\y -> if x == y then s else Var y) t)
+-- application, here we either reduce the left or right term
+reduceStep globals (App t s)
+  | t' == t = (rs, App t s') -- t is normal, reduce s
+  | otherwise = (rt, App t' s) -- t is not normal, reduce t
+  where
+    (rt, t') = reduceStep globals t
+    (rs, s') = reduceStep globals s
+-- variable, here we either delta-reduce (if name is known) or stop
+reduceStep globals t@(Var x)
+  | x `Map.member` globals = (Delta, globals Map.! x)
+  | otherwise = (None, t)
+
+reduce :: Int -> Bool -> Map String Term -> Term -> IO ()
+reduce 1000000 full m t = do
+  putStrLn "Evaluation reached 1.000.000 reduction steps, this might be an endless loop.\nIf you want the evaluation to continue type Y, else type something else."
+  line <- getLine
+  case line of
+    "Y" -> putStrLn "Continuing evaluation..." >> reduce 1000001 full m t
+    _ -> putStrLn "Evaluation cancelled"
+reduce count full m t = do
+  let (r, t') = reduceStep m t
+  when full $ do
+    case r of
+      Beta -> putStr "-β-> " >> print t'
+      Delta -> putStr "-δ-> " >> print t'
+      None -> showResult m t'
+  if r == None then showResult m t' else reduce (count + 1) full m t'
+
+showResult :: Map String Term -> Term -> IO ()
+showResult globals t = do
+  putStr "result: "
+  print t
+  case parseChurchNumeral t of
+    Nothing -> return ()
+    Just x -> putStr "as church-numeral: " >> print x
+  case parseChurchBoolean t of
+    Nothing -> return ()
+    Just x -> putStr "as church-boolean: " >> putStrLn (map toLower $ show x)
+  case parseFoldList t of
+    Nothing -> return ()
+    Just x -> do
+      let numeralList = mapM parseChurchNumeral x
+      case numeralList of
+        Nothing -> return ()
+        Just x -> putStr "as fold-list (numeral):" >> print x
+      let booleanList = mapM parseChurchBoolean x
+      case booleanList of
+        Nothing -> return ()
+        Just x -> putStr "as fold-list (boolean):" >> print x
+  putStrLn ""
+
+parseChurchNumeral :: Term -> Maybe Int
+parseChurchNumeral (Abs f (Abs a (Var a'))) | a == a' = Just 0
+parseChurchNumeral (Abs x (Abs y t)) = if count == Just 0 then Nothing else count
+  where
+    count = countApps t
+    countApps :: Term -> Maybe Int
+    countApps (App t1 t2) = (+ 1) <$> countApps t2
+    countApps _ = Just 0
+parseChurchNumeral _ = Nothing
+
+parseChurchBoolean :: Term -> Maybe Bool
+parseChurchBoolean (Abs x (Abs y (Var x'))) | x == x' = Just True
+parseChurchBoolean (Abs x (Abs y (Var y'))) | y == y' = Just False
+parseChurchBoolean _ = Nothing
+
+parseFoldList :: Term -> Maybe [Term]
+parseFoldList (Abs c (Abs n (Var n'))) | n == n' = Just []
+parseFoldList (Abs c (Abs n (App (App (Var c') e) t))) | c == c' = (:) e <$> parseRest c n t
+  where
+    parseRest :: String -> String -> Term -> Maybe [Term]
+    parseRest c n (App (App (Var c') e) (Var n')) | c == c' && n == n' = Just [e]
+    parseRest c n (App (App (Var c') e) t) | c == c' = (:) e <$> parseRest c n t
+    parseRest c n _ = Nothing
+parseFoldList _ = Nothing
+
+data Reduction = Beta | Delta | None deriving (Eq)

src/Syntax.hs

@@ -0,0 +1,33 @@
+module Syntax where
+
+type Var = String
+type Substitution = Var -> Term
+
+data Declaration = Declaration String Term
+
+data Term
+  = Var Var
+  | App Term Term
+  | Abs Var Term
+  deriving (Eq, Ord)
+
+instance Show Term where
+  show :: Term -> String
+  show (Var v) = v
+  show (App t1 t2) = showHelper t1 False ++ " " ++ showHelper t2 True
+    where
+      showHelper :: Term -> Bool -> String
+      showHelper (Var v) True = v
+      showHelper (App t1 t2) True = "(" ++ showHelper t1 False ++ " " ++ showHelper t2 True ++ ")"
+      showHelper t@(Abs {}) True = "(" ++ show t ++ ")"
+      showHelper t False = show t
+  show t@(Abs {}) = absHelper t True -- only outermost abstraction needs parentheses
+    where
+      absHelper :: Term -> Bool -> String
+      absHelper (Abs v t) True = "(\\" ++ v ++ "." ++ absHelper t False ++ ")"
+      absHelper (Abs v t) False = "\\" ++ v ++ "." ++ absHelper t False
+      absHelper t _ = show t
+
+instance Show Declaration where
+  show :: Declaration -> String
+  show (Declaration name term) = name ++ " = " ++ show term