diff options
80 files changed, 1286 insertions, 0 deletions
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 + +``` +<expr> ::= <id> -- variable + | `\' <id>+ `.' <expr> -- lambda abstraction + | <expr> <expr> -- application + | `(' <expr> `)' -- 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) "<input>" + +{- * 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 <filename> +# 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 <outfile> <reffile> <difffile> +# 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 <args> +# Report the command, run it, and report any errors +Run() { + echo $* 1>&2 + eval $* || { + SignalError "failed: $*" + return 1 + } +} + +# RunFail <args> +# 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 + |