commit 692d839c34fb3f2097200504ecbdda3b6260a9f7 Author: reijix Date: Mon Apr 17 08:55:09 2023 +0200 redacted prelude solutions diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..cc94b51 --- /dev/null +++ b/.envrc @@ -0,0 +1,2 @@ +nix_direnv_watch_file *.cabal +use flake diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..af4fe8b --- /dev/null +++ b/.gitattributes @@ -0,0 +1 @@ +flake.lock linguist-generated=true diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml new file mode 100644 index 0000000..c25917a --- /dev/null +++ b/.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 diff --git a/.github/workflows/update-flake-lock.yaml b/.github/workflows/update-flake-lock.yaml new file mode 100644 index 0000000..795c278 --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..f2d40f4 --- /dev/null +++ b/.gitignore @@ -0,0 +1,12 @@ +# cabal +dist +dist-* +cabal.project.local +cabal.project.local~ + +# nix +result +result-* + +# direnv +.direnv \ No newline at end of file diff --git a/.vscode/extensions.json b/.vscode/extensions.json new file mode 100644 index 0000000..61dc1f3 --- /dev/null +++ b/.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", + ] +} \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..121ca83 --- /dev/null +++ b/.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" +} \ No newline at end of file diff --git a/.vscode/tasks.json b/.vscode/tasks.json new file mode 100644 index 0000000..dcfb5e3 --- /dev/null +++ b/.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" + } + } + ] +} \ No newline at end of file diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..9cf1062 --- /dev/null +++ b/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. diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..10de5af --- /dev/null +++ b/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 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..eeada23 --- /dev/null +++ b/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; + }; + }; +} diff --git a/fourmolu.yaml b/fourmolu.yaml new file mode 100644 index 0000000..ef5582d --- /dev/null +++ b/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 \ No newline at end of file diff --git a/hie.yaml b/hie.yaml new file mode 100644 index 0000000..effdfbf --- /dev/null +++ b/hie.yaml @@ -0,0 +1,4 @@ +cradle: + cabal: + - path: "src" + component: "exe:lambda" diff --git a/lambda.cabal b/lambda.cabal new file mode 100644 index 0000000..4f8339b --- /dev/null +++ b/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 diff --git a/shell.nix b/shell.nix new file mode 100644 index 0000000..8745f50 --- /dev/null +++ b/shell.nix @@ -0,0 +1 @@ +(builtins.getFlake ("git+file://" + toString ./.)).devShells.${builtins.currentSystem}.default diff --git a/src/Lexer.hs b/src/Lexer.hs new file mode 100644 index 0000000..964d725 --- /dev/null +++ b/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" diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 index 0000000..fb35e1a --- /dev/null +++ b/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 diff --git a/src/Parser.hs b/src/Parser.hs new file mode 100644 index 0000000..4597174 --- /dev/null +++ b/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) diff --git a/src/Reduction.hs b/src/Reduction.hs new file mode 100644 index 0000000..5df6c3a --- /dev/null +++ b/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) diff --git a/src/Syntax.hs b/src/Syntax.hs new file mode 100644 index 0000000..273ac1a --- /dev/null +++ b/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