diff options
| -rw-r--r-- | README.md | 35 | ||||
| -rw-r--r-- | bruijn.cabal | 12 | ||||
| -rw-r--r-- | package.yaml | 15 | ||||
| -rw-r--r-- | src/Eval.hs | 21 | ||||
| -rw-r--r-- | src/Helper.hs | 2 | ||||
| -rw-r--r-- | src/Parser.hs | 22 | ||||
| -rw-r--r-- | std/Boolean.bruijn | 60 | ||||
| -rw-r--r-- | std/Church.bruijn | 7 | ||||
| -rw-r--r-- | std/Combinator.bruijn | 22 | ||||
| -rw-r--r-- | std/Number.bruijn (renamed from std.bruijn) | 68 | ||||
| -rw-r--r-- | std/Option.bruijn | 39 | ||||
| -rw-r--r-- | std/Pair.bruijn | 26 | ||||
| -rw-r--r-- | std/Result.bruijn | 21 |
13 files changed, 256 insertions, 94 deletions
@@ -17,8 +17,8 @@ Bruijn indices written in Haskell. - Highly space-efficient compilation to binary lambda calculus (BLC)\[2\]\[3\] additionally to normal interpretation and REPL - Recursion can be implemented using combinators such as Y or ω -- Included standard library featuring many useful functions - (`std.bruijn`) +- Included standard library featuring many useful functions (see + `std/`) ## Basics @@ -49,14 +49,15 @@ form](https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form). Additional spaces are optional but allowed. <identifier> ::= [a-ω,A-Ω,_][a-ω,A-Ω,0-9,?,!,',-]* + <namespace> ::= [A-Ω][a-ω,A-Ω]+ <abstraction> ::= "[" <expression> "]" <numeral> ::= ("+" | "-")[0-9]+ <bruijn> ::= [0-9] - <singleton> ::= <bruijn> | <numeral> | <abstraction> | "(" <application> ")" | <identifier> + <singleton> ::= <bruijn> | <numeral> | <abstraction> | "(" <application> ")" | [namespace.]<identifier> <application> ::= <singleton> <singleton> <expression> ::= <application> | <singleton> <test> ::= ":test " <expression> = <expression> - <import> ::= ":import " <path> + <import> ::= ":import " <path> [namespace] <comment> ::= "# " <letter>* The following are the differences in syntax between REPL and file: @@ -94,7 +95,9 @@ You may want to use the included standard library to reach your program’s full potential. It includes many common combinators as well as functions for numerical, boolean and IO operations and much more. -You can import it from `std.bruijn` using `:import std`. +For example, you can import the standard library for numbers using +`:import std/Number`. You can find all available libraries in the `std/` +directory. ### Examples @@ -135,7 +138,11 @@ Plain execution: Using standard library: - :import std + :import std/Boolean . + :import std/Combinator . + :import std/Number . + :import std/Option . + :import std/Pair . # pairs with some values me [[[1]]] @@ -144,16 +151,22 @@ Using standard library: :test fst love = me :test snd love = you + # options + :test map succ (some +1) = some +2 + :test apply (some +1) [some (succ 0)] = some +2 + # numerical operations five pred (sub (add +8 -4) -2) - not-five? [if (eq? 0 +5) false true] - :test not-five? five = false + not-five? [if (eq? 0 +5) F T] + :test not-five? five = F + + :test eq? (uncurry mul (pair +3 +2)) = +6 # boolean - main not (or (and false true) true) - :test main = false + main not (or (and F T) T) + :test main = F - # read the std.bruijn file for an overview of all functions + # read the files in std/ for an overview of all functions/libraries ### Compilation to BLC diff --git a/bruijn.cabal b/bruijn.cabal index 139f41e..c7eafe5 100644 --- a/bruijn.cabal +++ b/bruijn.cabal @@ -13,12 +13,19 @@ author: Marvin Borner maintainer: develop@marvinborner.de copyright: 2022 Marvin Borner license: MIT +license-file: LICENSE build-type: Simple extra-source-files: README.md data-files: config - std.bruijn + std/Boolean.bruijn + std/Church.bruijn + std/Combinator.bruijn + std/Number.bruijn + std/Option.bruijn + std/Pair.bruijn + std/Result.bruijn source-repository head type: git @@ -44,6 +51,7 @@ library , bytestring , containers , directory + , filepath , haskeline , megaparsec , mtl @@ -66,6 +74,7 @@ executable bruijn , bytestring , containers , directory + , filepath , haskeline , megaparsec , mtl @@ -89,6 +98,7 @@ test-suite bruijn-test , bytestring , containers , directory + , filepath , haskeline , megaparsec , mtl diff --git a/package.yaml b/package.yaml index 9f83342..03b080e 100644 --- a/package.yaml +++ b/package.yaml @@ -11,7 +11,7 @@ extra-source-files: data-files: - config -- std.bruijn +- std/* # Metadata used when publishing your package # synopsis: Short description of your package @@ -27,14 +27,15 @@ default-extensions: dependencies: - base >= 4.7 && < 5 -- mtl -- haskeline -- megaparsec +- binary +- bitstring +- bytestring - containers - directory -- bytestring -- bitstring -- binary +- filepath +- haskeline +- megaparsec +- mtl library: source-dirs: src diff --git a/src/Eval.hs b/src/Eval.hs index 77e5990..5494ee7 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -19,6 +19,7 @@ import System.Console.Haskeline.Completion import System.Directory import System.Environment import System.Exit +import System.FilePath.Posix ( takeBaseName ) import System.IO import Text.Megaparsec hiding ( State , try @@ -29,6 +30,7 @@ data EnvState = EnvState } type M = StrictState.StateT EnvState IO +-- TODO: Force naming convention for namespaces/files loadFile :: String -> IO EnvState loadFile path = do file <- try $ readFile path :: IO (Either IOError String) @@ -75,8 +77,8 @@ evalTest exp1 exp2 = ) eval :: [String] -> EnvState -> Bool -> IO EnvState -eval [] state@(EnvState env) _ = return state -eval [""] state@(EnvState env) _ = return state +eval [] state _ = return state +eval [""] state _ = return state eval (line : ls) state@(EnvState env) isRepl = handleInterrupt (putStrLn "<aborted>" >> return state) $ case parse lineParser "" line of @@ -91,10 +93,17 @@ eval (line : ls) state@(EnvState env) isRepl = then (putStrLn $ name <> " = " <> show exp) >> return (EnvState env') else eval ls (EnvState env') isRepl - Import path -> do - lib <- getDataFileName path -- TODO: Use actual lib directory - exists <- doesFileExist lib - loadFile $ if exists then lib else path + -- TODO: Import loop detection + -- TODO: Don't import subimports into main env + Import path namespace -> do + lib <- getDataFileName path -- TODO: Use actual lib directory + exists <- doesFileExist lib + EnvState env' <- loadFile $ if exists then lib else path + let prefix | null namespace = takeBaseName path ++ "." + | namespace == "." = "" + | otherwise = namespace ++ "." + env' <- pure $ map (\(n, e) -> (prefix ++ n, e)) env' + eval ls (EnvState $ env <> env') isRepl Evaluate exp -> let (res, env') = evalExp exp `runState` env in diff --git a/src/Helper.hs b/src/Helper.hs index 76a1f83..5c31aba 100644 --- a/src/Helper.hs +++ b/src/Helper.hs @@ -12,7 +12,7 @@ type Failable = Either Error data Expression = Bruijn Int | Variable String | Abstraction Expression | Application Expression Expression deriving (Ord, Eq) -data Instruction = Define String Expression | Evaluate Expression | Comment String | Import String | Test Expression Expression +data Instruction = Define String Expression | Evaluate Expression | Comment String | Import String String | Test Expression Expression deriving (Show) instance Show Expression where show (Bruijn x ) = "\ESC[31m" <> show x <> "\ESC[0m" diff --git a/src/Parser.hs b/src/Parser.hs index dc6951a..f4afb69 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -22,9 +22,21 @@ lexeme = L.lexeme sc symbol :: String -> Parser String symbol = L.symbol sc +-- def identifier disallows the import prefix dots +defIdentifier :: Parser String +defIdentifier = lexeme + ((:) <$> (letterChar <|> char '_') <*> many (alphaNumChar <|> oneOf "?!'_-")) + +-- TODO: write as extension to defIdentifier identifier :: Parser String identifier = lexeme - ((:) <$> (letterChar <|> char '_') <*> many (alphaNumChar <|> oneOf "?!'_-")) + ((:) <$> (letterChar <|> char '_') <*> many (alphaNumChar <|> oneOf "?!'_-.")) + +namespace :: Parser String +namespace = + lexeme ((:) <$> upperChar <*> many letterChar) + <|> string "." + <|> (space >> return "") parens :: Parser a -> Parser a parens = between (symbol "(") (symbol ")") @@ -93,13 +105,13 @@ parseEvaluate = Evaluate <$> parseExpression parseDefine :: Parser Instruction parseDefine = do - var <- identifier + var <- defIdentifier space Define var <$> parseExpression parseReplDefine :: Parser Instruction parseReplDefine = do - var <- identifier + var <- defIdentifier space symbol "=" space @@ -114,7 +126,9 @@ parseImport = do space path <- importPath space - pure $ Import $ path ++ ".bruijn" + ns <- namespace + space + pure $ Import (path ++ ".bruijn") ns parsePrint :: Parser Instruction parsePrint = do diff --git a/std/Boolean.bruijn b/std/Boolean.bruijn new file mode 100644 index 0000000..36d11bd --- /dev/null +++ b/std/Boolean.bruijn @@ -0,0 +1,60 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +:import std/Combinator . + +not [0 F T] +:test not T = F +:test not F = T + +and [[1 0 F]] +:test and T T = T +:test and T F = F +:test and F T = F +:test and F F = F + +nand [[1 0 1 F T]] +:test nand T T = F +:test nand T F = T +:test nand F T = T +:test nand F F = T + +or [[1 T 0]] +:test or T T = T +:test or T F = T +:test or F T = T +:test or F F = F + +nor [[1 1 0 F T]] +:test nor T T = F +:test nor T F = F +:test nor F T = F +:test nor F F = T + +xor [[1 (not 0) 0]] +:test xor T T = F +:test xor T F = T +:test xor F T = T +:test xor F F = F + +xnor [[1 0 (not 0)]] +:test xnor T T = T +:test xnor T F = F +:test xnor F T = F +:test xnor F F = T + +if [[[2 1 0]]] +:test if T T F = T +:test if F T F = F + +implies [[or (not 1) 0]] +:test implies T T = T +:test implies T F = F +:test implies F T = T +:test implies F F = T + +iff [[and (implies 1 0) (implies 0 1)]] +:test iff T T = T +:test iff T F = F +:test iff F T = F +:test iff F F = T + diff --git a/std/Church.bruijn b/std/Church.bruijn new file mode 100644 index 0000000..40807dd --- /dev/null +++ b/std/Church.bruijn @@ -0,0 +1,7 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +church-zero [[0]] +church-succ [[[1 (2 1 0)]]] +church-add [[[[3 1 (2 1 0)]]]] +church-mul [[[2 (1 0)]]] +church-exp [[0 1]] diff --git a/std/Combinator.bruijn b/std/Combinator.bruijn new file mode 100644 index 0000000..95338a6 --- /dev/null +++ b/std/Combinator.bruijn @@ -0,0 +1,22 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +S [[[2 0 (1 0)]]] +K [[1]] +I [0] +B [[[2 (1 0)]]] +C [[[2 0 1]]] +W [[1 0 0]] +T [[1]] +F [[0]] +ω [0 0] +Ω ω ω +Y [[1 (0 0)] [1 (0 0)]] +Θ [[0 (1 1 0)]] [[0 (1 1 0)]] +i [0 S K] + +:test I = i i +:test K = i (i (i i)) +:test S = i (i (i (i i))) +:test B = S (K S) K +:test C = S (S (K (S (K S) K)) S) (K K) +:test W = S S (S K) diff --git a/std.bruijn b/std/Number.bruijn index 9a05cdf..5bc95a1 100644 --- a/std.bruijn +++ b/std/Number.bruijn @@ -1,47 +1,8 @@ -# ================== -# Common combinators -# ================== - -S [[[2 0 (1 0)]]] -K [[1]] -I [0] -B [[[2 (1 0)]]] -C [[[2 0 1]]] -T [[1]] -F [[0]] -ω [0 0] -Ω ω ω -Y [[1 (0 0)] [1 (0 0)]] -Θ [[0 (1 1 0)]] [[0 (1 1 0)]] -i [0 S K] - -:test I = i i -:test K = i (i (i i)) -:test S = i (i (i (i i))) - -# ===== -# Pairs -# ===== - -# pairs two expressions into one -pair [[[0 2 1]]] - -# extracts first expression from pair -fst [0 T] -:test fst (pair [[0]] [[1]]) = [[0]] - -# extracts second expression from pair -snd [0 F] -:test snd (pair [[0]] [[1]]) = [[1]] - -# TODO: investigate currying and chaining functions -# -> WHNF things? -# chain [[[2 (1 0)]]] - -# =================================== -# Ternary +# MIT License, Copyright (c) 2022 Marvin Borner # According to works of T.Æ. Mogensen -# =================================== + +:import std/Combinator . +:import std/Pair . # checks whether balanced ternary number is zero zero? [0 T [F] [F] I] @@ -209,25 +170,4 @@ smul [[strip (mul 1 0)]] :test eq? (mul +3 +11) +33 = T :test eq? (mul +42 -4) -168 = T -# =============== -# Boolean algebra -# =============== - -not [0 F T] -and [[1 0 F]] -or [[1 T 0]] -xor [[1 (not 0) 0]] -if [[[2 1 0]]] -:test not (or (and false true) true) = false - -# =============== -# Church numerals -# =============== - -church-zero [[0]] -church-succ [[[1 (2 1 0)]]] -church-add [[[[3 1 (2 1 0)]]]] -church-mul [[[2 (1 0)]]] -church-exp [[0 1]] -main [[[0 2 1]]] diff --git a/std/Option.bruijn b/std/Option.bruijn new file mode 100644 index 0000000..e33cbb5 --- /dev/null +++ b/std/Option.bruijn @@ -0,0 +1,39 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +:import std/Combinator . + +# empty option +none T + +# encapsulates value in option +some [[[0 2]]] + +# checks whether option is none +none? [0 T [F]] +:test none? none = T +:test none? (some [[0]]) = F + +# checks whether option is some +some? [0 F [T]] +:test some? none = F +:test some? (some [[0]]) = T + +# applies a function to the value in a option +map [[0 none [some (2 0)]]] +:test map [[1]] (some [[0]]) = some [[[0]]] +:test map [[1]] none = none + +# applies a function to the value in a option or returns first arg if none +map-or [[[0 2 1]]] +:test map-or [[[2]]] [[1]] (some [[0]]) = [[[0]]] +:test map-or [[[2]]] [[1]] none = [[[2]]] + +# extracts value from option or returns first argument if none +unwrap-or [[0 1 I]] +:test unwrap-or F (some T) = T +:test unwrap-or F none = F + +# applies encapsulated value to given function +apply [[1 none 0]] +:test apply none [some ([[1]] 0)] = none +:test apply (some [[0]]) [some ([[1]] 0)] = some [[[0]]] diff --git a/std/Pair.bruijn b/std/Pair.bruijn new file mode 100644 index 0000000..75d8680 --- /dev/null +++ b/std/Pair.bruijn @@ -0,0 +1,26 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +:import std/Combinator . + +# pairs two expressions into one +pair [[[0 2 1]]] + +# extracts first expression from pair +fst [0 T] +:test fst (pair [[0]] [[1]]) = [[0]] + +# extracts second expression from pair +snd [0 F] +:test snd (pair [[0]] [[1]]) = [[1]] + +# applies both elements of a pair to a function +uncurry [[1 (fst 0) (snd 0)]] +:test uncurry W (pair [[0]] [[1]]) = [[1]] + +# applies a function to the pair of two values +curry [[[2 (pair 1 0)]]] +:test curry fst [[0]] [[1]] = [[0]] + +# swaps the values of a pair +swap [pair (snd 0) (fst 0)] +:test swap (pair [[0]] [[1]]) = pair [[1]] [[0]] diff --git a/std/Result.bruijn b/std/Result.bruijn new file mode 100644 index 0000000..28b8181 --- /dev/null +++ b/std/Result.bruijn @@ -0,0 +1,21 @@ +# MIT License, Copyright (c) 2022 Marvin Borner + +:import std/Combinator . + +# encapsulates a value in ok +ok [[[1 2]]] +:test ok [[0]] = [[1 [[0]]]] + +# encapsulates a value in err +err [[[0 2]]] +:test err [[0]] = [[0 [[0]]]] + +# checks whether result is ok +ok? [0 [T] [F]] +:test ok? (ok [[0]]) = T +:test ok? (err [[0]]) = F + +# checks whether result is not ok +err? [0 [F] [T]] +:test err? (ok [[0]]) = F +:test err? (err [[0]]) = T |