From fdf35536b66499884dd5b4e1740ac67e5cebb1a2 Mon Sep 17 00:00:00 2001 From: tzlil Date: Fri, 14 Apr 2023 23:46:53 +0300 Subject: add homework material --- .envrc | 1 + .gitignore | 5 + README.md | 66 ++++++++++++ Setup.hs | 2 + flake.lock | 83 ++++++++++++++ flake.nix | 33 ++++++ lambda.cabal | 49 +++++++++ package.yaml | 36 +++++++ plc/Main.hs | 8 ++ src/AST.hs | 28 +++++ src/HW.hs | 50 +++++++++ src/Parse.hs | 91 ++++++++++++++++ stack.yaml | 67 ++++++++++++ tests/examples/beta.lam | 3 + tests/examples/beta.out | 1 + tests/examples/beta1.lam | 3 + tests/examples/beta1.out | 1 + tests/examples/beta2.lam | 3 + tests/examples/beta2.out | 1 + tests/examples/beta3.lam | 3 + tests/examples/beta3.out | 1 + tests/examples/bools-and-t-f.lam | 16 +++ tests/examples/bools-and-t-f.out | 1 + tests/examples/bools-not-t.lam | 16 +++ tests/examples/bools-not-t.out | 1 + tests/examples/bools-or-f-t.lam | 16 +++ tests/examples/bools-or-f-t.out | 1 + tests/examples/currying.lam | 3 + tests/examples/currying.out | 1 + tests/examples/fac-three.lam | 31 ++++++ tests/examples/fac-three.out | 1 + tests/examples/head-normal-form.lam | 6 ++ tests/examples/head-normal-form.out | 1 + tests/examples/normal-form.lam | 6 ++ tests/examples/normal-form.out | 1 + tests/examples/nums-env.lam | 27 +++++ tests/examples/nums-env.out | 1 + tests/examples/nums-isZero-one.lam | 27 +++++ tests/examples/nums-isZero-one.out | 1 + tests/examples/nums-isZero-two.lam | 27 +++++ tests/examples/nums-isZero-two.out | 1 + tests/examples/nums-isZero-zero.lam | 27 +++++ tests/examples/nums-isZero-zero.out | 1 + tests/examples/nums-minus-one-two.lam | 27 +++++ tests/examples/nums-minus-one-two.out | 1 + tests/examples/nums-minus-three-two.lam | 27 +++++ tests/examples/nums-minus-three-two.out | 1 + tests/examples/nums-mult-two-three.lam | 27 +++++ tests/examples/nums-mult-two-three.out | 1 + tests/examples/nums-plus-three-two.lam | 27 +++++ tests/examples/nums-plus-three-two.out | 1 + tests/examples/nums-pred-four.lam | 27 +++++ tests/examples/nums-pred-four.out | 1 + tests/examples/nums-pred-one.lam | 27 +++++ tests/examples/nums-pred-one.out | 1 + tests/examples/nums-pred-two.lam | 27 +++++ tests/examples/nums-pred-two.out | 1 + tests/examples/nums-pred-zero.lam | 27 +++++ tests/examples/nums-pred-zero.out | 1 + tests/examples/nums-succ-two.lam | 27 +++++ tests/examples/nums-succ-two.out | 1 + tests/examples/nums-succ-zero.lam | 27 +++++ tests/examples/nums-succ-zero.out | 1 + tests/examples/omega-arg.lam | 1 + tests/examples/omega-arg.out | 1 + tests/examples/omega.lam | 6 ++ tests/examples/omega.out | 1 + tests/examples/pairs-fst-snd.lam | 15 +++ tests/examples/pairs-fst-snd.out | 1 + tests/examples/pairs-fst.lam | 15 +++ tests/examples/pairs-fst.out | 1 + tests/examples/pairs-snd.lam | 15 +++ tests/examples/pairs-snd.out | 1 + tests/examples/weak-head-normal-form.lam | 6 ++ tests/examples/weak-head-normal-form.out | 1 + tests/examples/weak-normal-form.lam | 6 ++ tests/examples/weak-normal-form.out | 1 + tests/examples/y.lam | 7 ++ tests/examples/y.out | 1 + tests/runtests.sh | 179 +++++++++++++++++++++++++++++++ 80 files changed, 1286 insertions(+) create mode 100644 .envrc create mode 100644 .gitignore create mode 100644 README.md create mode 100644 Setup.hs create mode 100644 flake.lock create mode 100644 flake.nix create mode 100644 lambda.cabal create mode 100644 package.yaml create mode 100644 plc/Main.hs create mode 100644 src/AST.hs create mode 100644 src/HW.hs create mode 100644 src/Parse.hs create mode 100644 stack.yaml create mode 100644 tests/examples/beta.lam create mode 100644 tests/examples/beta.out create mode 100644 tests/examples/beta1.lam create mode 100644 tests/examples/beta1.out create mode 100644 tests/examples/beta2.lam create mode 100644 tests/examples/beta2.out create mode 100644 tests/examples/beta3.lam create mode 100644 tests/examples/beta3.out create mode 100644 tests/examples/bools-and-t-f.lam create mode 100644 tests/examples/bools-and-t-f.out create mode 100644 tests/examples/bools-not-t.lam create mode 100644 tests/examples/bools-not-t.out create mode 100644 tests/examples/bools-or-f-t.lam create mode 100644 tests/examples/bools-or-f-t.out create mode 100644 tests/examples/currying.lam create mode 100644 tests/examples/currying.out create mode 100644 tests/examples/fac-three.lam create mode 100644 tests/examples/fac-three.out create mode 100644 tests/examples/head-normal-form.lam create mode 100644 tests/examples/head-normal-form.out create mode 100644 tests/examples/normal-form.lam create mode 100644 tests/examples/normal-form.out create mode 100644 tests/examples/nums-env.lam create mode 100644 tests/examples/nums-env.out create mode 100644 tests/examples/nums-isZero-one.lam create mode 100644 tests/examples/nums-isZero-one.out create mode 100644 tests/examples/nums-isZero-two.lam create mode 100644 tests/examples/nums-isZero-two.out create mode 100644 tests/examples/nums-isZero-zero.lam create mode 100644 tests/examples/nums-isZero-zero.out create mode 100644 tests/examples/nums-minus-one-two.lam create mode 100644 tests/examples/nums-minus-one-two.out create mode 100644 tests/examples/nums-minus-three-two.lam create mode 100644 tests/examples/nums-minus-three-two.out create mode 100644 tests/examples/nums-mult-two-three.lam create mode 100644 tests/examples/nums-mult-two-three.out create mode 100644 tests/examples/nums-plus-three-two.lam create mode 100644 tests/examples/nums-plus-three-two.out create mode 100644 tests/examples/nums-pred-four.lam create mode 100644 tests/examples/nums-pred-four.out create mode 100644 tests/examples/nums-pred-one.lam create mode 100644 tests/examples/nums-pred-one.out create mode 100644 tests/examples/nums-pred-two.lam create mode 100644 tests/examples/nums-pred-two.out create mode 100644 tests/examples/nums-pred-zero.lam create mode 100644 tests/examples/nums-pred-zero.out create mode 100644 tests/examples/nums-succ-two.lam create mode 100644 tests/examples/nums-succ-two.out create mode 100644 tests/examples/nums-succ-zero.lam create mode 100644 tests/examples/nums-succ-zero.out create mode 100644 tests/examples/omega-arg.lam create mode 100644 tests/examples/omega-arg.out create mode 100644 tests/examples/omega.lam create mode 100644 tests/examples/omega.out create mode 100644 tests/examples/pairs-fst-snd.lam create mode 100644 tests/examples/pairs-fst-snd.out create mode 100644 tests/examples/pairs-fst.lam create mode 100644 tests/examples/pairs-fst.out create mode 100644 tests/examples/pairs-snd.lam create mode 100644 tests/examples/pairs-snd.out create mode 100644 tests/examples/weak-head-normal-form.lam create mode 100644 tests/examples/weak-head-normal-form.out create mode 100644 tests/examples/weak-normal-form.lam create mode 100644 tests/examples/weak-normal-form.out create mode 100644 tests/examples/y.lam create mode 100644 tests/examples/y.out create mode 100755 tests/runtests.sh diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..3550a30 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..82d9aa7 --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +.direnv +result +*.pdf +tests/runtests.log +tests/out diff --git a/README.md b/README.md new file mode 100644 index 0000000..9195860 --- /dev/null +++ b/README.md @@ -0,0 +1,66 @@ +# Lambda Calculus Expressions + +## Building + +Use the Haskell Tool Stack [https://www.haskellstack.org] + +`stack build` + +## Testing + +``` +cd tests +./runtests.sh +beta1...OK +beta2...OK +beta3...OK +``` + +## Use + +``` +stack ghci +ghci> parse "x y z" +x y z +ghci> parse "(\\ n . pred n) 3" +(\n . pred n) 3 +ghci> parse "x (y z)" +x (y z) +ghci> parse "(x y) z" +x y z +ghci> parse "\\x.y z" +\x . y z +ghci> parse "\\x y z . x (y z)" +\x . \y . \z . x (y z) +ghci> parse "\\x.x (\\z . z)" +\x . x (\z . z) +ghci> parse "(\\x.x) (\\z . z)" +(\x . x) (\z . z) +ghci> :i Expr +type Expr :: * +data Expr = Var String | Lam String Expr | App Expr Expr +instance Show Expr +ghci> Lam "a" (App (Var "b") (Var "c")) +\a . b c +``` + +# Syntax + +``` + ::= -- variable + | `\' + `.' -- lambda abstraction + | -- application + | `(' `)' -- grouping +``` + +Variable identifiers are any sequence of characters excluding +`\`, `.`, `(`, `)`, `-`, and whitespace + +Lambda abstractions are at the lowest precedence; +application binds left-to-right + +Space is needed to separate identifiers but is optional elsewhere + +Single-line comments start with `--` + +Multi-line comments are between `{-` and `-}' and may nest diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..fe99fdd --- /dev/null +++ b/flake.lock @@ -0,0 +1,83 @@ +{ + "nodes": { + "flake-parts": { + "inputs": { + "nixpkgs-lib": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1680392223, + "narHash": "sha256-n3g7QFr85lDODKt250rkZj2IFS3i4/8HBU2yKHO3tqw=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "dcc36e45d054d7bb554c9cdab69093debd91a0b5", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1681358109, + "narHash": "sha256-eKyxW4OohHQx9Urxi7TQlFBTDWII+F+x2hklDOQPB50=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "96ba1c52e54e74c3197f4d43026b3f3d92e83ff9", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1680945546, + "narHash": "sha256-8FuaH5t/aVi/pR1XxnF0qi4WwMYC+YxlfdsA0V+TEuQ=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "d9f759f2ea8d265d974a6e1259bd510ac5844c5d", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-parts": "flake-parts", + "nixpkgs": "nixpkgs", + "treefmt-nix": "treefmt-nix" + } + }, + "treefmt-nix": { + "inputs": { + "nixpkgs": "nixpkgs_2" + }, + "locked": { + "lastModified": 1681115235, + "narHash": "sha256-VCETW6vOzNlByc0A5gTJoFE9L/ikP91rX6XynBUgIno=", + "owner": "numtide", + "repo": "treefmt-nix", + "rev": "f3dd071be31528261034022020fc7e4c010f7179", + "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..b32c2ca --- /dev/null +++ b/flake.nix @@ -0,0 +1,33 @@ +{ + inputs = { + nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable"; + flake-parts = { url = "github:hercules-ci/flake-parts"; inputs.nixpkgs-lib.follows = "nixpkgs"; }; + treefmt-nix.url = "github:numtide/treefmt-nix"; + }; + + outputs = inputs: + inputs.flake-parts.lib.mkFlake { inherit inputs; } { + systems = [ "x86_64-linux" ]; + imports = [ + inputs.treefmt-nix.flakeModule + ]; + + perSystem = { pkgs, ... }: { + packages.default = pkgs.haskellPackages.callCabal2nix "example" ./. { }; + + devShells.default = pkgs.haskellPackages.shellFor { + packages = ps: [ ]; + buildInputs = with pkgs.haskellPackages; [ + cabal-install + haskell-language-server + megaparsec + ]; + }; + treefmt = { + projectRootFile = "flake.nix"; + programs.nixpkgs-fmt.enable = true; + programs.cabal-fmt.enable = true; + }; + }; + }; +} diff --git a/lambda.cabal b/lambda.cabal new file mode 100644 index 0000000..68d5068 --- /dev/null +++ b/lambda.cabal @@ -0,0 +1,49 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.35.1. +-- +-- see: https://github.com/sol/hpack + +name: lambda +version: 0.1.0.0 +author: John Hui, Stephen Edwards +maintainer: sedwards@cs.columbia.edu +copyright: 2023 John Hui and Stephen Edwards +license: BSD3 +build-type: Simple +extra-source-files: README.md + +library + exposed-modules: + AST + HW + Parse + + other-modules: Paths_lambda + hs-source-dirs: src + ghc-options: + -Wall -Wcompat -Widentities -Wincomplete-record-updates + -Wincomplete-uni-patterns -Wmissing-export-lists + -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints + + build-depends: + base >=4.7 && <5 + , containers + , megaparsec + + default-language: Haskell2010 + +executable plc + main-is: Main.hs + other-modules: Paths_lambda + hs-source-dirs: plc + ghc-options: + -Wall -Wcompat -Widentities -Wincomplete-record-updates + -Wincomplete-uni-patterns -Wmissing-export-lists + -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints + + build-depends: + base >=4.7 && <5 + , lambda + + default-language: Haskell2010 diff --git a/package.yaml b/package.yaml new file mode 100644 index 0000000..deb4306 --- /dev/null +++ b/package.yaml @@ -0,0 +1,36 @@ +name: lambda +version: 0.1.0.0 +license: BSD3 +author: "John Hui, Stephen Edwards" +maintainer: "sedwards@cs.columbia.edu" +copyright: "2023 John Hui and Stephen Edwards" + +extra-source-files: +- README.md + +dependencies: +- base >= 4.7 && < 5 + +ghc-options: +- -Wall +- -Wcompat +- -Widentities +- -Wincomplete-record-updates +- -Wincomplete-uni-patterns +- -Wmissing-export-lists +- -Wmissing-home-modules +- -Wpartial-fields +- -Wredundant-constraints + +library: + source-dirs: src + dependencies: + - megaparsec + - containers + +executables: + plc: + main: Main.hs + source-dirs: plc + dependencies: + - lambda diff --git a/plc/Main.hs b/plc/Main.hs new file mode 100644 index 0000000..9e8a7b8 --- /dev/null +++ b/plc/Main.hs @@ -0,0 +1,8 @@ +module Main (main) where + +import Parse + +main :: IO () +main = do + s <- getContents + print $ parse s diff --git a/src/AST.hs b/src/AST.hs new file mode 100644 index 0000000..456338e --- /dev/null +++ b/src/AST.hs @@ -0,0 +1,28 @@ +-- | Abstract syntax tree for the untyped lambda calculus, plus some helpers. +module AST ( + Expr (..) +) where + +-- | Lambda Expressions +data Expr + = Var String + | Lam String Expr + | App Expr Expr + deriving (Eq, Ord) + + +-- https://www.haskellforall.com/2020/11/pretty-print-syntax-trees-with-this-one.html +showLam, showApp, showVar :: Expr -> String +showLam (Lam i e) = "\\" ++ i ++ " . " ++ showLam e +showLam e = showApp e + +showApp (App e1 e2) = showApp e1 ++ " " ++ showVar e2 +showApp e = showVar e + +showVar (Var i) = i +showVar e = "(" ++ showLam e ++ ")" + +instance Show Expr where + show e = showLam e + + diff --git a/src/HW.hs b/src/HW.hs new file mode 100644 index 0000000..88fb1c2 --- /dev/null +++ b/src/HW.hs @@ -0,0 +1,50 @@ +module HW + ( fv + , subst + , normalstep + , pickFresh + , repeatedly + , printnormal + ) where + +import AST +import qualified Data.Set as Set +import Parse (parse) + +-- | Return the free variables in an expression +fv :: Expr -> Set.Set String +fv _ = Set.singleton "UNIMPLEMENTED" -- Replace with your solution to problem 1 + + + +-- | Substitute n for x in e, avoiding name capture +-- subst n x e e[x := n] +subst :: Expr -> String -> Expr -> Expr +subst _ _ _ = Var "UNIMPLEMENTED" -- Replace with your solution to problem 2 + + + +-- | Take a single step in normal order reduction or return Nothing +normalstep :: Expr -> Maybe Expr +normalstep _ = Just (Var "UNIMPLEMENTED") -- Replace with your solution to problem 3 + + + + +-- | Return a "fresh" name not already in the set. +-- Tries x' then x'', etc. +pickFresh :: Set.Set String -> String -> String +pickFresh s = pickFresh' + where pickFresh' n | n `Set.notMember` s = n + pickFresh' n = pickFresh' $ n ++ "'" + +-- | Repeatedly apply a function to transform a value, returning the list +-- of steps it took. The result list starts with the given initial value +repeatedly :: (a -> Maybe a) -> a -> [a] +repeatedly f = repeatedly' + where repeatedly' x = x : case f x of Nothing -> [] + Just y -> repeatedly' y + +-- | Print out the series of normal order reduction steps +printnormal :: String -> IO () +printnormal = mapM_ print . repeatedly normalstep . parse diff --git a/src/Parse.hs b/src/Parse.hs new file mode 100644 index 0000000..748bd98 --- /dev/null +++ b/src/Parse.hs @@ -0,0 +1,91 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -Wno-unused-top-binds #-} + +-- | Parser for the untyped lambda calculus, whose AST is defined in "AST". +module Parse (parse, tryParse) where + +import qualified AST as A + +import Text.Megaparsec ( + MonadParsec (..), + Parsec, + errorBundlePretty, + noneOf, + runParser, + some, + (), + (<|>), + between + ) +import Text.Megaparsec.Char( space1 ) +import qualified Text.Megaparsec.Char.Lexer as L + +import Control.Monad (void) +import Data.Bifunctor (Bifunctor (..)) +import Data.Void (Void) + +-- * Exposed functions + +-- | Parse a Lambda expression; throw an exception over an error +parse :: String -> A.Expr +parse = either error id . tryParse + +-- | Parse some code 'String' into an 'L.Expr' or an error message. +tryParse :: String -> Either String A.Expr +tryParse = first errorBundlePretty . + runParser (pSpace >> pExpr <* eof) "" + +{- * Expression parser + +Note that Megaparsec allows us to label tokens with 'label' or '()', which +helps it produce human-readable error messages. +-} + +-- | Entry point for parser. +pExpr :: Parser A.Expr +pExpr = pBody "expression" + +-- | Parse expressions at the lowest level of precedence, i.e., lambdas. +pBody :: Parser A.Expr +pBody = pLam <|> pApp + where + pLam = do + pToken "\\" + bs <- some pIdent "lambda binders" + pToken "." + body <- pBody "lambda body" + return $ foldr A.Lam body bs + +-- | Parse juxtaposition as application. +pApp :: Parser A.Expr +pApp = foldl1 A.App <$> some pAtom "term application" + +-- | Parse expressions at the highest precedence, including parenthesized terms +pAtom :: Parser A.Expr +pAtom = A.Var <$> pVar <|> pParens pExpr + where + pVar = pIdent "variable" + +-- * Megaparsec boilerplate and helpers + +-- | Parsing monad. +type Parser = Parsec Void String + +-- | Parse an identifier, possible surrounded by spaces +pIdent :: Parser String +pIdent = L.lexeme pSpace (some $ noneOf ['\\','.','(',')',' ','\n','\r','\t','-']) + +-- | Consume a token defined by a string, possibly surrounded by spaces +pToken :: String -> Parser () +pToken = void . L.symbol pSpace + +-- | Parse some element surrounded by parentheses. +pParens :: Parser a -> Parser a +pParens = between (pToken "(") (pToken ")") + +-- | Consumes whitespace and comments. +pSpace :: Parser () +pSpace = label "whitespace" $ L.space + space1 + (L.skipLineComment "--") + (L.skipBlockCommentNested "{-" "-}") diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 0000000..47f8c24 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,67 @@ +# This file was automatically generated by 'stack init' +# +# Some commonly used options have been documented as comments in this file. +# For advanced use and comprehensive documentation of the format, please see: +# https://docs.haskellstack.org/en/stable/yaml_configuration/ + +# Resolver to choose a 'specific' stackage snapshot or a compiler version. +# A snapshot resolver dictates the compiler version and the set of packages +# to be used for project dependencies. For example: +# +# resolver: lts-3.5 +# resolver: nightly-2015-09-21 +# resolver: ghc-7.10.2 +# +# The location of a snapshot can be provided as a file or url. Stack assumes +# a snapshot provided as a file might change, whereas a url resource does not. +# +# resolver: ./custom-snapshot.yaml +# resolver: https://example.com/snapshots/2018-01-01.yaml +resolver: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/20/13.yaml + +# User packages to be built. +# Various formats can be used as shown in the example below. +# +# packages: +# - some-directory +# - https://example.com/foo/bar/baz-0.0.2.tar.gz +# subdirs: +# - auto-update +# - wai +packages: +- . +# Dependency packages to be pulled from upstream that are not in the resolver. +# These entries can reference officially published versions as well as +# forks / in-progress versions pinned to a git hash. For example: +# +# extra-deps: +# - acme-missiles-0.3 +# - git: https://github.com/commercialhaskell/stack.git +# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a +# +# extra-deps: [] + +# Override default flag values for local packages and extra-deps +# flags: {} + +# Extra package databases containing global packages +# extra-package-dbs: [] + +# Control whether we use the GHC we find on the path +# system-ghc: true +# +# Require a specific version of Stack, using version ranges +# require-stack-version: -any # Default +# require-stack-version: ">=2.9" +# +# Override the architecture used by Stack, especially useful on Windows +# arch: i386 +# arch: x86_64 +# +# Extra directories used by Stack for building +# extra-include-dirs: [/path/to/dir] +# extra-lib-dirs: [/path/to/dir] +# +# Allow a newer minor version of GHC than the snapshot specifies +# compiler-check: newer-minor diff --git a/tests/examples/beta.lam b/tests/examples/beta.lam new file mode 100644 index 0000000..9d53b08 --- /dev/null +++ b/tests/examples/beta.lam @@ -0,0 +1,3 @@ +(\ x . (\ z . z z) x three) ((\ y . y y) (\ w . w)) + +-- Should reduce to three diff --git a/tests/examples/beta.out b/tests/examples/beta.out new file mode 100644 index 0000000..ac8f0f0 --- /dev/null +++ b/tests/examples/beta.out @@ -0,0 +1 @@ +(\x . (\z . z z) x three) ((\y . y y) (\w . w)) diff --git a/tests/examples/beta1.lam b/tests/examples/beta1.lam new file mode 100644 index 0000000..3ffc446 --- /dev/null +++ b/tests/examples/beta1.lam @@ -0,0 +1,3 @@ +(\x . x three) (\y . plus y y) + +-- Should reduce to plus three three diff --git a/tests/examples/beta1.out b/tests/examples/beta1.out new file mode 100644 index 0000000..6ceecd5 --- /dev/null +++ b/tests/examples/beta1.out @@ -0,0 +1 @@ +(\x . x three) (\y . plus y y) diff --git a/tests/examples/beta2.lam b/tests/examples/beta2.lam new file mode 100644 index 0000000..02ae576 --- /dev/null +++ b/tests/examples/beta2.lam @@ -0,0 +1,3 @@ +(\x . (\x . x) x) one + +-- should reduce to one diff --git a/tests/examples/beta2.out b/tests/examples/beta2.out new file mode 100644 index 0000000..3434328 --- /dev/null +++ b/tests/examples/beta2.out @@ -0,0 +1 @@ +(\x . (\x . x) x) one diff --git a/tests/examples/beta3.lam b/tests/examples/beta3.lam new file mode 100644 index 0000000..e112b5c --- /dev/null +++ b/tests/examples/beta3.lam @@ -0,0 +1,3 @@ +(\ x . \ y . x y ) y + +-- Should reduce to \z . y z (for some fresh z) diff --git a/tests/examples/beta3.out b/tests/examples/beta3.out new file mode 100644 index 0000000..322346c --- /dev/null +++ b/tests/examples/beta3.out @@ -0,0 +1 @@ +(\x . \y . x y) y diff --git a/tests/examples/bools-and-t-f.lam b/tests/examples/bools-and-t-f.lam new file mode 100644 index 0000000..fd9a29c --- /dev/null +++ b/tests/examples/bools-and-t-f.lam @@ -0,0 +1,16 @@ +(\ true false and or not . + + and true false + + -- Should reduce to false, i.e., \ x y . y +) +-- true +(\ x y . x) +-- false +(\ x y . y) +-- and +(\ p q . p q p) +-- or +(\ p q . p p q) +-- not +(\ p x y . p y x) diff --git a/tests/examples/bools-and-t-f.out b/tests/examples/bools-and-t-f.out new file mode 100644 index 0000000..e422fcc --- /dev/null +++ b/tests/examples/bools-and-t-f.out @@ -0,0 +1 @@ +(\true . \false . \and . \or . \not . and true false) (\x . \y . x) (\x . \y . y) (\p . \q . p q p) (\p . \q . p p q) (\p . \x . \y . p y x) diff --git a/tests/examples/bools-not-t.lam b/tests/examples/bools-not-t.lam new file mode 100644 index 0000000..9afcc48 --- /dev/null +++ b/tests/examples/bools-not-t.lam @@ -0,0 +1,16 @@ +(\ true false and or not . + + not true + + -- Should reduce to false, i.e., \ x y . y +) +-- true +(\ x y . x) +-- false +(\ x y . y) +-- and +(\ p q . p q p) +-- or +(\ p q . p p q) +-- not +(\ p x y . p y x) diff --git a/tests/examples/bools-not-t.out b/tests/examples/bools-not-t.out new file mode 100644 index 0000000..2a6a257 --- /dev/null +++ b/tests/examples/bools-not-t.out @@ -0,0 +1 @@ +(\true . \false . \and . \or . \not . not true) (\x . \y . x) (\x . \y . y) (\p . \q . p q p) (\p . \q . p p q) (\p . \x . \y . p y x) diff --git a/tests/examples/bools-or-f-t.lam b/tests/examples/bools-or-f-t.lam new file mode 100644 index 0000000..5c39cd8 --- /dev/null +++ b/tests/examples/bools-or-f-t.lam @@ -0,0 +1,16 @@ +(\ true false and or not . + + or false true + + -- Should reduce to true, i.e., \ x y . x +) +-- true +(\ x y . x) +-- false +(\ x y . y) +-- and +(\ p q . p q p) +-- or +(\ p q . p p q) +-- not +(\ p x y . p y x) diff --git a/tests/examples/bools-or-f-t.out b/tests/examples/bools-or-f-t.out new file mode 100644 index 0000000..78a2057 --- /dev/null +++ b/tests/examples/bools-or-f-t.out @@ -0,0 +1 @@ +(\true . \false . \and . \or . \not . or false true) (\x . \y . x) (\x . \y . y) (\p . \q . p q p) (\p . \q . p p q) (\p . \x . \y . p y x) diff --git a/tests/examples/currying.lam b/tests/examples/currying.lam new file mode 100644 index 0000000..5463ce7 --- /dev/null +++ b/tests/examples/currying.lam @@ -0,0 +1,3 @@ +(\x y. plus (plus x y) x) one two + +-- Should reduce to plus (plus one two) one diff --git a/tests/examples/currying.out b/tests/examples/currying.out new file mode 100644 index 0000000..5660f00 --- /dev/null +++ b/tests/examples/currying.out @@ -0,0 +1 @@ +(\x . \y . plus (plus x y) x) one two diff --git a/tests/examples/fac-three.lam b/tests/examples/fac-three.lam new file mode 100644 index 0000000..613c933 --- /dev/null +++ b/tests/examples/fac-three.lam @@ -0,0 +1,31 @@ +(\ zero one two three succ plus mult pred minus isZero yComb . + (\ fac . + fac three + -- NOTE: the y-combinator does not have a normal form + ) (yComb (\ f n . (isZero n) one (mult n (f (pred n))))) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) + +-- yComb +(\ f . (\ x . f (x x)) (\ x . f (x x))) diff --git a/tests/examples/fac-three.out b/tests/examples/fac-three.out new file mode 100644 index 0000000..5430f7f --- /dev/null +++ b/tests/examples/fac-three.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . \yComb . (\fac . fac three) (yComb (\f . \n . isZero n one (mult n (f (pred n)))))) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) (\f . (\x . f (x x)) (\x . f (x x))) diff --git a/tests/examples/head-normal-form.lam b/tests/examples/head-normal-form.lam new file mode 100644 index 0000000..bf859a0 --- /dev/null +++ b/tests/examples/head-normal-form.lam @@ -0,0 +1,6 @@ +-- normal form N +-- weak normal form N +-- head normal form Y +-- weak head normal form Y + +f ((\x . x x) (\x . x x)) diff --git a/tests/examples/head-normal-form.out b/tests/examples/head-normal-form.out new file mode 100644 index 0000000..574706c --- /dev/null +++ b/tests/examples/head-normal-form.out @@ -0,0 +1 @@ +f ((\x . x x) (\x . x x)) diff --git a/tests/examples/normal-form.lam b/tests/examples/normal-form.lam new file mode 100644 index 0000000..36afd00 --- /dev/null +++ b/tests/examples/normal-form.lam @@ -0,0 +1,6 @@ +-- normal form Y +-- weak normal form Y +-- head normal form Y +-- weak head normal form Y + +f (\x . x x) (\x . x x) diff --git a/tests/examples/normal-form.out b/tests/examples/normal-form.out new file mode 100644 index 0000000..07dc4b3 --- /dev/null +++ b/tests/examples/normal-form.out @@ -0,0 +1 @@ +f (\x . x x) (\x . x x) diff --git a/tests/examples/nums-env.lam b/tests/examples/nums-env.lam new file mode 100644 index 0000000..c8e8a7e --- /dev/null +++ b/tests/examples/nums-env.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + insert_your_expression_here + +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-env.out b/tests/examples/nums-env.out new file mode 100644 index 0000000..41b34f0 --- /dev/null +++ b/tests/examples/nums-env.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . insert_your_expression_here) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-isZero-one.lam b/tests/examples/nums-isZero-one.lam new file mode 100644 index 0000000..67e54dd --- /dev/null +++ b/tests/examples/nums-isZero-one.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + isZero one + -- Should evaluate to false, i.e., \ x y . y +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-isZero-one.out b/tests/examples/nums-isZero-one.out new file mode 100644 index 0000000..4d24c9e --- /dev/null +++ b/tests/examples/nums-isZero-one.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . isZero one) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-isZero-two.lam b/tests/examples/nums-isZero-two.lam new file mode 100644 index 0000000..086bdc0 --- /dev/null +++ b/tests/examples/nums-isZero-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + isZero two + -- Should evaluate to false, i.e., \ x y . y +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-isZero-two.out b/tests/examples/nums-isZero-two.out new file mode 100644 index 0000000..b897fd1 --- /dev/null +++ b/tests/examples/nums-isZero-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . isZero two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-isZero-zero.lam b/tests/examples/nums-isZero-zero.lam new file mode 100644 index 0000000..4cf9dd3 --- /dev/null +++ b/tests/examples/nums-isZero-zero.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + isZero zero + -- Should evaluate to true, i.e., \ x y . x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-isZero-zero.out b/tests/examples/nums-isZero-zero.out new file mode 100644 index 0000000..88be213 --- /dev/null +++ b/tests/examples/nums-isZero-zero.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . isZero zero) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-minus-one-two.lam b/tests/examples/nums-minus-one-two.lam new file mode 100644 index 0000000..cd54d34 --- /dev/null +++ b/tests/examples/nums-minus-one-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + minus one two + -- Should evaluate to zero, i.e., \ f x . x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-minus-one-two.out b/tests/examples/nums-minus-one-two.out new file mode 100644 index 0000000..04b0c6a --- /dev/null +++ b/tests/examples/nums-minus-one-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . minus one two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-minus-three-two.lam b/tests/examples/nums-minus-three-two.lam new file mode 100644 index 0000000..e2fe489 --- /dev/null +++ b/tests/examples/nums-minus-three-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + minus three two + -- Should evaluate to one, i.e., \ f x . f x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-minus-three-two.out b/tests/examples/nums-minus-three-two.out new file mode 100644 index 0000000..e924284 --- /dev/null +++ b/tests/examples/nums-minus-three-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . minus three two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-mult-two-three.lam b/tests/examples/nums-mult-two-three.lam new file mode 100644 index 0000000..f8ea7ed --- /dev/null +++ b/tests/examples/nums-mult-two-three.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + mult two three + -- Should evaluate to six, i.e., \ f x . f (f (f (f (f (f x))))) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-mult-two-three.out b/tests/examples/nums-mult-two-three.out new file mode 100644 index 0000000..1390573 --- /dev/null +++ b/tests/examples/nums-mult-two-three.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . mult two three) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-plus-three-two.lam b/tests/examples/nums-plus-three-two.lam new file mode 100644 index 0000000..70839a5 --- /dev/null +++ b/tests/examples/nums-plus-three-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + plus three two + -- Should evaluate to five, i.e., (\ f x . f (f (f (f (f x))))) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-plus-three-two.out b/tests/examples/nums-plus-three-two.out new file mode 100644 index 0000000..67ccb01 --- /dev/null +++ b/tests/examples/nums-plus-three-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . plus three two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-pred-four.lam b/tests/examples/nums-pred-four.lam new file mode 100644 index 0000000..02602c0 --- /dev/null +++ b/tests/examples/nums-pred-four.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + pred four + -- Should evaluate to three, i.e., \ f x . f (f (f x)) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-pred-four.out b/tests/examples/nums-pred-four.out new file mode 100644 index 0000000..f57d3e0 --- /dev/null +++ b/tests/examples/nums-pred-four.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred four) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-pred-one.lam b/tests/examples/nums-pred-one.lam new file mode 100644 index 0000000..413046d --- /dev/null +++ b/tests/examples/nums-pred-one.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + pred one + -- Should evaluate to zero, i.e., \ f x . x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-pred-one.out b/tests/examples/nums-pred-one.out new file mode 100644 index 0000000..5e72285 --- /dev/null +++ b/tests/examples/nums-pred-one.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred one) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-pred-two.lam b/tests/examples/nums-pred-two.lam new file mode 100644 index 0000000..d003d33 --- /dev/null +++ b/tests/examples/nums-pred-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + pred two + -- Should evaluate to zero, i.e., \ f x . f x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-pred-two.out b/tests/examples/nums-pred-two.out new file mode 100644 index 0000000..7c032fd --- /dev/null +++ b/tests/examples/nums-pred-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-pred-zero.lam b/tests/examples/nums-pred-zero.lam new file mode 100644 index 0000000..dd0a17b --- /dev/null +++ b/tests/examples/nums-pred-zero.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + pred zero + -- Should evaluate to zero, i.e., \ f x . x +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-pred-zero.out b/tests/examples/nums-pred-zero.out new file mode 100644 index 0000000..7f3455b --- /dev/null +++ b/tests/examples/nums-pred-zero.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . pred zero) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-succ-two.lam b/tests/examples/nums-succ-two.lam new file mode 100644 index 0000000..89f5761 --- /dev/null +++ b/tests/examples/nums-succ-two.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + succ two + -- Should evaluate to three, i.e., \ f x . f (f (f x)) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-succ-two.out b/tests/examples/nums-succ-two.out new file mode 100644 index 0000000..3973621 --- /dev/null +++ b/tests/examples/nums-succ-two.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . succ two) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/nums-succ-zero.lam b/tests/examples/nums-succ-zero.lam new file mode 100644 index 0000000..28b0d8c --- /dev/null +++ b/tests/examples/nums-succ-zero.lam @@ -0,0 +1,27 @@ +(\ zero one two three succ plus mult pred minus isZero . + + succ zero + -- Should evaluate to one, i.e., (\ f x . f x) +) + +-- zero +(\ f x . x) +-- one +(\ f x . f x) +-- two +(\ f x . f (f x)) +-- three +(\ f x . f (f (f x))) + +-- succ +(\n f x . f (n f x)) +-- plus +(\m n f x . m f (n f x)) +-- mult +(\m n f . m (n f)) +-- pred +(\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) +-- minus +(\ m n . n (\n f x . n (\ g h . h (g f)) (\ u . x) (\ u . u)) m) +-- isZero +(\ n . n (\ x . (\ x y . y)) (\ x y . x)) diff --git a/tests/examples/nums-succ-zero.out b/tests/examples/nums-succ-zero.out new file mode 100644 index 0000000..716960a --- /dev/null +++ b/tests/examples/nums-succ-zero.out @@ -0,0 +1 @@ +(\zero . \one . \two . \three . \succ . \plus . \mult . \pred . \minus . \isZero . succ zero) (\f . \x . x) (\f . \x . f x) (\f . \x . f (f x)) (\f . \x . f (f (f x))) (\n . \f . \x . f (n f x)) (\m . \n . \f . \x . m f (n f x)) (\m . \n . \f . m (n f)) (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) (\m . \n . n (\n . \f . \x . n (\g . \h . h (g f)) (\u . x) (\u . u)) m) (\n . n (\x . \x . \y . y) (\x . \y . x)) diff --git a/tests/examples/omega-arg.lam b/tests/examples/omega-arg.lam new file mode 100644 index 0000000..8a7138a --- /dev/null +++ b/tests/examples/omega-arg.lam @@ -0,0 +1 @@ +(\a x . x) ((\z . z z) (\z . z z)) diff --git a/tests/examples/omega-arg.out b/tests/examples/omega-arg.out new file mode 100644 index 0000000..33d80d7 --- /dev/null +++ b/tests/examples/omega-arg.out @@ -0,0 +1 @@ +(\a . \x . x) ((\z . z z) (\z . z z)) diff --git a/tests/examples/omega.lam b/tests/examples/omega.lam new file mode 100644 index 0000000..29ed0ff --- /dev/null +++ b/tests/examples/omega.lam @@ -0,0 +1,6 @@ +-- normal form N +-- weak normal form N +-- head normal form N +-- weak head normal form N + +(\x . x x) (\x . x x) diff --git a/tests/examples/omega.out b/tests/examples/omega.out new file mode 100644 index 0000000..f7f18c2 --- /dev/null +++ b/tests/examples/omega.out @@ -0,0 +1 @@ +(\x . x x) (\x . x x) diff --git a/tests/examples/pairs-fst-snd.lam b/tests/examples/pairs-fst-snd.lam new file mode 100644 index 0000000..19791ad --- /dev/null +++ b/tests/examples/pairs-fst-snd.lam @@ -0,0 +1,15 @@ +(\ pair fst snd . + + fst (snd (pair (pair a b) (pair c d))) + + -- Should reduce to c +) + +-- pair +(\ x y f . f x y) + +-- fst +(\ p . p (\ x y . x)) + +-- snd +(\ p . p (\ x y . y)) diff --git a/tests/examples/pairs-fst-snd.out b/tests/examples/pairs-fst-snd.out new file mode 100644 index 0000000..cb53fb8 --- /dev/null +++ b/tests/examples/pairs-fst-snd.out @@ -0,0 +1 @@ +(\pair . \fst . \snd . fst (snd (pair (pair a b) (pair c d)))) (\x . \y . \f . f x y) (\p . p (\x . \y . x)) (\p . p (\x . \y . y)) diff --git a/tests/examples/pairs-fst.lam b/tests/examples/pairs-fst.lam new file mode 100644 index 0000000..5ee215a --- /dev/null +++ b/tests/examples/pairs-fst.lam @@ -0,0 +1,15 @@ +(\ pair fst snd . + + fst (pair a b) + + -- Should reduce to a +) + +-- pair +(\ x y f . f x y) + +-- fst +(\ p . p (\ x y . x)) + +-- snd +(\ p . p (\ x y . y)) diff --git a/tests/examples/pairs-fst.out b/tests/examples/pairs-fst.out new file mode 100644 index 0000000..c11f799 --- /dev/null +++ b/tests/examples/pairs-fst.out @@ -0,0 +1 @@ +(\pair . \fst . \snd . fst (pair a b)) (\x . \y . \f . f x y) (\p . p (\x . \y . x)) (\p . p (\x . \y . y)) diff --git a/tests/examples/pairs-snd.lam b/tests/examples/pairs-snd.lam new file mode 100644 index 0000000..b2f0a75 --- /dev/null +++ b/tests/examples/pairs-snd.lam @@ -0,0 +1,15 @@ +(\ pair fst snd . + + snd (pair a b) + + -- Should reduce to b +) + +-- pair +(\ x y f . f x y) + +-- fst +(\ p . p (\ x y . x)) + +-- snd +(\ p . p (\ x y . y)) diff --git a/tests/examples/pairs-snd.out b/tests/examples/pairs-snd.out new file mode 100644 index 0000000..ebfb43b --- /dev/null +++ b/tests/examples/pairs-snd.out @@ -0,0 +1 @@ +(\pair . \fst . \snd . snd (pair a b)) (\x . \y . \f . f x y) (\p . p (\x . \y . x)) (\p . p (\x . \y . y)) diff --git a/tests/examples/weak-head-normal-form.lam b/tests/examples/weak-head-normal-form.lam new file mode 100644 index 0000000..6b8c0e0 --- /dev/null +++ b/tests/examples/weak-head-normal-form.lam @@ -0,0 +1,6 @@ +-- normal form N +-- weak normal form Y +-- head normal form Y +-- weak head normal form Y + +\f . f ((\x . x x) (\x . x x)) diff --git a/tests/examples/weak-head-normal-form.out b/tests/examples/weak-head-normal-form.out new file mode 100644 index 0000000..6b4a7fc --- /dev/null +++ b/tests/examples/weak-head-normal-form.out @@ -0,0 +1 @@ +\f . f ((\x . x x) (\x . x x)) diff --git a/tests/examples/weak-normal-form.lam b/tests/examples/weak-normal-form.lam new file mode 100644 index 0000000..8d80a75 --- /dev/null +++ b/tests/examples/weak-normal-form.lam @@ -0,0 +1,6 @@ +-- normal form N +-- weak normal form Y +-- head normal form N +-- weak head normal form Y + +\f . (\x . x x) (\x . x x) diff --git a/tests/examples/weak-normal-form.out b/tests/examples/weak-normal-form.out new file mode 100644 index 0000000..54963a1 --- /dev/null +++ b/tests/examples/weak-normal-form.out @@ -0,0 +1 @@ +\f . (\x . x x) (\x . x x) diff --git a/tests/examples/y.lam b/tests/examples/y.lam new file mode 100644 index 0000000..996802d --- /dev/null +++ b/tests/examples/y.lam @@ -0,0 +1,7 @@ +-- normal form N +-- weak normal form Y +-- head normal form N +-- weak head normal form Y + +-- Y combinator +\ f . (\ x . f (x x)) (\ x . f (x x)) diff --git a/tests/examples/y.out b/tests/examples/y.out new file mode 100644 index 0000000..afe09a5 --- /dev/null +++ b/tests/examples/y.out @@ -0,0 +1 @@ +\f . (\x . f (x x)) (\x . f (x x)) diff --git a/tests/runtests.sh b/tests/runtests.sh new file mode 100755 index 0000000..75f1f3c --- /dev/null +++ b/tests/runtests.sh @@ -0,0 +1,179 @@ +#!/usr/bin/env bash + +PLC="nix run" + +globallog=runtests.log +rm -f $globallog +error= +keep= + +# Destination directory for generated files (log excepted) +mkdir -p out + +# Set time limit +ulimit -t 5 + +Usage() { + echo "Usage: runtests.sh [options] [files]" + echo "-k Keep intermediate files" + echo "-h Print this help" + exit 1 +} + +# NoteGen +# Remember that the given filename was generated so we can clean up +NoteGen() { + generatedfiles="$generatedfiles $1" +} + +SignalError() { + if [ -z "$error" ] ; then + echo "FAILED" + error=1 + fi + echo " $1" +} + +# Compare +# Compares the outfile with reffile. Differences, if any, written to difffile +Compare() { + NoteGen "$3" + if ! [ -f "$2" ] ; then + SignalError "$2 not found" + echo "$2 not found" 1>&2 + else + echo diff -b $1 $2 ">" $3 1>&2 + diff -b "$1" "$2" > "$3" 2>&1 || { + SignalError "$1 differs" + echo "FAILED $1 differs from $2" 1>&2 + cat $3 >&2 + } + fi +} + +# Run +# Report the command, run it, and report any errors +Run() { + echo $* 1>&2 + eval $* || { + SignalError "failed: $*" + return 1 + } +} + +# RunFail +# Report the command, run it, and expect an error +RunFail() { + echo $* 1>&2 + eval $* && { + SignalError "failed: $* did not report an error" + return 1 + } + return 0 +} + +# Run the parser on the given file +Check() { + error= + basename=`basename $1 | sed 's/[.][^.]*$//'` + reffile=`echo $1 | sed 's/[.][^.]*$//'` + basedir=`dirname $1` + + echo -n "$basename..." + + echo 1>&2 + echo "###### Testing $basename" 1>&2 + + generatedfiles= + + # Run the parser + result="out/${basename}.out" + reference="${reffile}.out" + diff="out/${basename}.diff" + NoteGen "${result} ${diff}" + + Run $PLC "<" "$1" ">" "${result}" && + Compare "${result}" "${reference}" "${diff}" + + if [ -z "$error" ] ; then + if [ -z "$keep" ] ; then + rm -f $generatedfiles + fi + echo "OK" + echo "###### SUCCESS" 1>&2 + else + echo "###### FAILED" 1>&2 + globalerror=$error + fi +} + +# Run the compiler and expect an error +CheckFail() { + error= + basename=`basename $1 | sed 's/[.][^.]*$//'` + reffile=`echo $1 | sed 's/[.][^.]*$//'` + basedir=`dirname $1` + + echo -n "$basename..." + + echo 1>&2 + echo "###### Testing failure $basename" 1>&2 + + generatedfiles= + + # Run the parser + + parsed="out/${basename}.lam" + difffile="out/${basename}.diff" + NoteGen "${parsed} ${difffile}" + RunFail $PLC "<" "$1" ">" "${parsed}" "2>" "${errfile}" && + Compare "${errfile}" "${reffile}.err" "${difffile}" + + # Report the status and clean up the generated files + + if [ -z "$error" ] ; then + if [ -z "$keep" ] ; then + rm -f $generatedfiles + fi + echo "OK" + echo "###### SUCCESS" 1>&2 + else + echo "###### FAILED" 1>&2 + globalerror=$error + fi +} + +while getopts kh c; do + case $c in + k) # Keep intermediate files + keep=1 + ;; + h) # Help + Usage + ;; + esac +done + +shift `expr $OPTIND - 1` + +if [ $# -ge 1 ] +then + files=$@ +else + files="examples/*.lam" +fi + +for file in $files +do + case "$file" in + *-fail.lam) + CheckFail "$file" 2>> $globallog + ;; + *) + Check "$file" 2>> $globallog + ;; + esac +done + +exit $globalerror + -- cgit 1.4.1