From 692d839c34fb3f2097200504ecbdda3b6260a9f7 Mon Sep 17 00:00:00 2001 From: reijix Date: Mon, 17 Apr 2023 08:55:09 +0200 Subject: [PATCH] redacted prelude solutions --- .envrc | 2 + .gitattributes | 1 + .github/workflows/ci.yaml | 38 +++++++ .github/workflows/update-flake-lock.yaml | 24 ++++ .gitignore | 12 ++ .vscode/extensions.json | 9 ++ .vscode/settings.json | 8 ++ .vscode/tasks.json | 27 +++++ LICENSE | 19 ++++ flake.lock | 133 +++++++++++++++++++++++ flake.nix | 97 +++++++++++++++++ fourmolu.yaml | 8 ++ hie.yaml | 4 + lambda.cabal | 34 ++++++ shell.nix | 1 + src/Lexer.hs | 50 +++++++++ src/Main.hs | 75 +++++++++++++ src/Parser.hs | 79 ++++++++++++++ src/Reduction.hs | 120 ++++++++++++++++++++ src/Syntax.hs | 33 ++++++ 20 files changed, 774 insertions(+) create mode 100644 .envrc create mode 100644 .gitattributes create mode 100644 .github/workflows/ci.yaml create mode 100644 .github/workflows/update-flake-lock.yaml create mode 100644 .gitignore create mode 100644 .vscode/extensions.json create mode 100644 .vscode/settings.json create mode 100644 .vscode/tasks.json create mode 100644 LICENSE create mode 100644 flake.lock create mode 100644 flake.nix create mode 100644 fourmolu.yaml create mode 100644 hie.yaml create mode 100644 lambda.cabal create mode 100644 shell.nix create mode 100644 src/Lexer.hs create mode 100644 src/Main.hs create mode 100644 src/Parser.hs create mode 100644 src/Reduction.hs create mode 100644 src/Syntax.hs 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