diff options
| -rw-r--r-- | bruijn.cabal | 18 | ||||
| -rw-r--r-- | package.yaml | 12 | ||||
| -rw-r--r-- | src/Binary.hs | 26 | ||||
| -rw-r--r-- | src/Eval.hs | 57 | ||||
| -rw-r--r-- | src/Helper.hs | 24 | ||||
| -rw-r--r-- | src/Parser.hs | 31 | ||||
| -rw-r--r-- | src/Reducer.hs | 3 | ||||
| -rw-r--r-- | stack.yaml | 2 | ||||
| -rw-r--r-- | stack.yaml.lock | 13 | ||||
| -rw-r--r-- | std.bruijn | 153 |
10 files changed, 227 insertions, 112 deletions
diff --git a/bruijn.cabal b/bruijn.cabal index 22628ab..999d6ab 100644 --- a/bruijn.cabal +++ b/bruijn.cabal @@ -9,11 +9,10 @@ version: 0.1.0.0 description: Please see the README on GitHub at <https://github.com/githubuser/bruijn#readme> homepage: https://github.com/githubuser/bruijn#readme bug-reports: https://github.com/githubuser/bruijn/issues -author: Author name here -maintainer: example@example.com -copyright: 2022 Author name here -license: BSD3 -license-file: LICENSE +author: Marvin Borner +maintainer: develop@marvinborner.de +copyright: 2022 Marvin Borner +license: MIT build-type: Simple extra-source-files: README.md @@ -25,6 +24,7 @@ source-repository head library exposed-modules: + Binary Eval Helper Parser @@ -37,13 +37,15 @@ library LambdaCase build-depends: base >=4.7 && <5 + , bitstring + , bytestring , containers , haskeline , mtl , parsec default-language: Haskell2010 -executable bruijn-exe +executable bruijn main-is: Main.hs other-modules: Paths_bruijn @@ -54,7 +56,9 @@ executable bruijn-exe ghc-options: -threaded -rtsopts -with-rtsopts=-N build-depends: base >=4.7 && <5 + , bitstring , bruijn + , bytestring , containers , haskeline , mtl @@ -73,7 +77,9 @@ test-suite bruijn-test ghc-options: -threaded -rtsopts -with-rtsopts=-N build-depends: base >=4.7 && <5 + , bitstring , bruijn + , bytestring , containers , haskeline , mtl diff --git a/package.yaml b/package.yaml index 9fdee03..c864ddf 100644 --- a/package.yaml +++ b/package.yaml @@ -1,10 +1,10 @@ name: bruijn version: 0.1.0.0 github: "githubuser/bruijn" -license: BSD3 -author: "Author name here" -maintainer: "example@example.com" -copyright: "2022 Author name here" +license: MIT +author: "Marvin Borner" +maintainer: "develop@marvinborner.de" +copyright: "2022 Marvin Borner" extra-source-files: - README.md @@ -28,12 +28,14 @@ dependencies: - haskeline - parsec - containers +- bytestring +- bitstring library: source-dirs: src executables: - bruijn-exe: + bruijn: main: Main.hs source-dirs: app ghc-options: diff --git a/src/Binary.hs b/src/Binary.hs index 4575c49..fbf0a07 100644 --- a/src/Binary.hs +++ b/src/Binary.hs @@ -1,14 +1,17 @@ module Binary ( toBinary , fromBinary + , toBitString + , fromBitString ) where import Control.Applicative +import qualified Data.BitString as Bit import Data.Char import Helper toBinary :: Expression -> String -toBinary (Bruijn x ) = (replicate x '1') ++ "0" +toBinary (Bruijn x ) = (replicate (x + 1) '1') ++ "0" toBinary (Abstraction exp ) = "00" ++ toBinary exp toBinary (Application exp1 exp2) = "01" ++ (toBinary exp1) ++ (toBinary exp2) @@ -25,3 +28,24 @@ fromBinary = foldr showsBin n x = if n == 0 then id else let (x', b) = divMod x 2 in showsBin (n - 1) x' . (intToDigit b :) + +-- TODO: Fix weird endianess things +padBitList :: [Bool] -> [Bool] +padBitList lst | length lst `mod` 8 == 0 = lst + | otherwise = padBitList ([False] ++ lst) + +toBitString :: String -> Bit.BitString +toBitString = Bit.fromList . padBitList . map + (\case + '0' -> False + '1' -> True + ) + +fromBitString :: Bit.BitString -> String +fromBitString = + map + (\case + False -> '0' + True -> '1' + ) + . Bit.toList diff --git a/src/Eval.hs b/src/Eval.hs index a5941c1..a5c29bf 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -5,6 +5,8 @@ module Eval import Binary import Control.Exception import Control.Monad.State +import qualified Data.BitString as Bit +import qualified Data.ByteString as Byte import Debug.Trace import Helper import Parser @@ -66,6 +68,29 @@ eval (line : ls) env = case parse parseLine "FILE" line of in case res of Left err -> print err >> eval ls env' Right _ -> eval ls env' + Import path -> + liftIO + $ (try $ readFile path :: IO (Either IOError String)) + >>= (\case -- TODO: Make this more abstract and reusable + Left exception -> print (exception :: IOError) >> pure env + Right file -> eval (filter (not . null) $ lines file) [] >>= pure + ) + Evaluate exp -> + let (res, env') = evalExp exp `runState` env + in putStrLn + (case res of + Left err -> show err + Right exp -> + "<> " + <> (show exp) + <> "\n*> " + <> (show reduced) + <> "\t(" + <> (show $ binaryToDecimal reduced) + <> ")" + where reduced = reduce exp + ) + >> eval ls env Test exp1 exp2 -> let (res, _) = evalTest exp1 exp2 `runState` env in case res of @@ -114,7 +139,7 @@ evalRepl line env = case parse parseReplLine "REPL" line of where reduced = reduce exp ) >> pure env - Load path -> + Import path -> liftIO $ (try $ readFile path :: IO (Either IOError String)) >>= (\case -- TODO: Make this more abstract and reusable @@ -145,26 +170,26 @@ evalFile path = do Right file -> do env <- eval (filter (not . null) $ lines file) [] case evalFunc "main" env of - Nothing -> putStrLn $ "main function not found" + Nothing -> putStrLn $ "ERROR: main function not found" Just exp -> print exp -compile :: String -> IO () -compile path = do +compile :: String -> (a -> IO ()) -> (String -> a) -> IO () +compile path write conv = do file <- try $ readFile path :: IO (Either IOError String) case file of Left exception -> print (exception :: IOError) Right file -> do env <- eval (filter (not . null) $ lines file) [] case lookup "main" env of - Nothing -> putStrLn $ "main function not found" - Just exp -> putStrLn $ toBinary exp + Nothing -> putStrLn $ "ERROR: main function not found" + Just exp -> write $ conv $ toBinary exp -exec :: String -> IO () -exec path = do - file <- try $ readFile path :: IO (Either IOError String) +exec :: String -> (String -> IO (Either IOError a)) -> (a -> String) -> IO () +exec path read conv = do + file <- read path case file of Left exception -> print (exception :: IOError) - Right file -> print $ reduce $ fromBinary file + Right file -> print $ reduce $ fromBinary $ conv file repl :: Environment -> InputT IO () repl env = @@ -183,7 +208,11 @@ evalMain = do case args of [] -> runInputT defaultSettings { historyFile = Just ".bruijn-history" } $ repl [] - ["-c", path] -> compile path -- TODO: -C: raw binary - ["-e", path] -> exec path -- TODO: -E: raw binary - [path] -> evalFile path - _ -> usage + ["-c", path] -> + compile path (Byte.putStr . Bit.realizeBitStringStrict) toBitString + ["-C", path] -> compile path putStrLn id + ["-e", path] -> + exec path (try . Byte.readFile) (fromBitString . Bit.bitString) + ["-E", path] -> exec path (try . readFile) id + ['-' : _] -> usage + [path ] -> evalFile path diff --git a/src/Helper.hs b/src/Helper.hs index 57fb9f4..60941be 100644 --- a/src/Helper.hs +++ b/src/Helper.hs @@ -3,9 +3,8 @@ module Helper where import Control.Monad.State import Text.Parsec hiding ( State ) -data Error = SyntaxError ParseError | UndeclaredFunction String | DuplicateFunction String | InvalidIndex Int | FatalError String +data Error = UndeclaredFunction String | DuplicateFunction String | InvalidIndex Int | FatalError String instance Show Error where - show (SyntaxError err) = show err show (UndeclaredFunction err) = "ERROR: undeclared function " <> show err show (DuplicateFunction err) = "ERROR: duplicate function " <> show err show (InvalidIndex err) = "ERROR: invalid index " <> show err @@ -14,7 +13,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 | Load String | Test Expression Expression +data Instruction = Define String Expression | Evaluate Expression | Comment String | Import String | Test Expression Expression deriving (Show) instance Show Expression where show (Bruijn x ) = show x @@ -25,24 +24,23 @@ instance Show Expression where type Environment = [(String, Expression)] type Program = State Environment --- Dec to Bal3 in Bruijn encoding: reversed application with 1=>0; 0=>1; T=>2; end=>3 --- e.g. 0=0=[[[[3]]]]; 2=1T=[[[[2 (0 3)]]]] -5=T11=[[[[0 (0 (2 3))]]]] -decimalToTernary :: Integer -> Expression -decimalToTernary n = - Abstraction $ Abstraction $ Abstraction $ Abstraction $ gen n +decimalToBinary :: Integer -> Expression +decimalToBinary n = Abstraction $ Abstraction $ Abstraction $ Abstraction $ gen + n where -- TODO: Consider switching 0 and 1 for better readability fix 0 = 1 fix 1 = 0 - fix 2 = 2 gen 0 = Bruijn 3 - gen n = Application (Bruijn $ fix $ mod n 3) (gen $ div (n + 1) 3) + gen 1 = Application (Bruijn 0) (gen 0) + gen n | n < 0 = Application (Bruijn 2) (gen (-n)) + | otherwise = Application (Bruijn $ fix $ mod n 2) (gen $ div n 2) -ternaryToDecimal :: Expression -> Integer -ternaryToDecimal exp = sum $ zipWith (*) (resolve exp) (iterate (* 3) 1) +binaryToDecimal :: Expression -> Integer +binaryToDecimal exp = sum $ zipWith (*) (resolve exp) (iterate (* 2) 1) where multiplier (Bruijn 0) = 1 multiplier (Bruijn 1) = 0 - multiplier (Bruijn 2) = (-1) + multiplier (Bruijn 2) = -1 -- TODO resolve' (Application x@(Bruijn _) (Bruijn 3)) = [multiplier x] resolve' (Application fst@(Bruijn _) rst@(Application _ _)) = (multiplier fst) : (resolve' rst) diff --git a/src/Parser.hs b/src/Parser.hs index 33b3c44..6df479d 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -35,6 +35,9 @@ almostAnything :: Parser String almostAnything = many1 $ oneOf ".`#~@$%^&*_+-=|;',/?[]<>(){} " <|> letter <|> digit +importPath :: Parser String +importPath = many1 $ oneOf "./_+-" <|> letter <|> digit + parseAbstraction :: Parser Expression parseAbstraction = do reservedOp "[" @@ -57,7 +60,7 @@ parseNumeral :: Parser Expression parseNumeral = do num <- number spaces - pure $ decimalToTernary num + pure $ decimalToBinary num where sign = (char '-' >> return negate) <|> (char '+' >> return id) nat = read <$> many1 digit @@ -104,8 +107,21 @@ parseReplDefine = do parseComment :: Parser Instruction parseComment = string "#" >> Comment <$> almostAnything -parseLoad :: Parser Instruction -parseLoad = string ":load " >> Load <$> almostAnything +parseImport :: Parser Instruction +parseImport = do + string ":import " + spaces + path <- importPath + spaces + pure $ Import $ path ++ ".bruijn" + +parsePrint :: Parser Instruction +parsePrint = do + string ":print " + spaces + exp <- parseExpression + spaces + pure $ Evaluate exp parseTest :: Parser Instruction parseTest = do @@ -118,12 +134,17 @@ parseTest = do pure $ Test exp1 exp2 parseLine :: Parser Instruction -parseLine = try parseDefine <|> try parseComment <|> try parseTest +parseLine = + try parseDefine + <|> try parseComment + <|> try parsePrint + <|> try parseImport + <|> try parseTest parseReplLine :: Parser Instruction parseReplLine = try parseReplDefine <|> try parseComment <|> try parseEvaluate - <|> try parseLoad + <|> try parseImport <|> try parseTest diff --git a/src/Reducer.hs b/src/Reducer.hs index a7c544a..2de307d 100644 --- a/src/Reducer.hs +++ b/src/Reducer.hs @@ -6,6 +6,9 @@ import Helper -- TODO: Research interaction nets and optimal reduction +-- TODO: Eta-reduction: [f 0] => f +-- (Abstraction f@_ (Bruijn 0)) = f + (<+>) :: Expression -> Int -> Expression (<+>) (Bruijn x ) n = if x > n then Bruijn (pred x) else Bruijn x (<+>) (Application exp1 exp2) n = Application (exp1 <+> n) (exp2 <+> n) @@ -41,6 +41,8 @@ packages: # commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a # # extra-deps: [] +extra-deps: +- bitstring-0.0.0@sha256:7638c1c515d728a84507e33c830854cfd141a5bcabec6963e68f52baf27979e9,1248 # Override default flag values for local packages and extra-deps # flags: {} diff --git a/stack.yaml.lock b/stack.yaml.lock deleted file mode 100644 index 6c8ac8e..0000000 --- a/stack.yaml.lock +++ /dev/null @@ -1,13 +0,0 @@ -# This file was autogenerated by Stack. -# You should not edit this file by hand. -# For more information, please see the documentation at: -# https://docs.haskellstack.org/en/stable/lock_files - -packages: [] -snapshots: -- completed: - size: 617368 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/3.yaml - sha256: a209d3455279ee76eb45f01f73bbb960ceaaa8dfad8891435384689df4dcb653 - original: - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/19/3.yaml @@ -15,6 +15,14 @@ Y [[1 (0 0)] [1 (0 0)]] Θ [[0 (1 1 0)]] [[0 (1 1 0)]] i [0 S K] +# ================= +# Alternative names +# ================= + +true T +false F +id I + # ===== # Pairs # ===== @@ -24,64 +32,99 @@ fst [0 T] snd [0 F] # =================================== +# Binary +# According to works of T.Æ. Mogensen +# =================================== + +# TODO: contract-like type-checking +# like: `+ ... : [[[[# 3]]]]` + +# TODO: Fix for negative 4x abstraction + +upZero [[[[1 (3 2 1 0)]]]] +upOne [[[[0 (3 2 1 0)]]]] +up [[[[[4 1 0 (3 2 1 0)]]]]] + +zero? [0 T I [F]] + +binZero [[[2]]] +binOne [[[0 2]]] + +_succZ (pair binZero binOne) +_succA [0 [[pair (upZero 1) (upOne 1)]]] +_succB [0 [[pair (upOne 1) (upZero 0)]]] +succ [snd (0 _succZ _succA _succB)] + +_predZ (pair binZero binZero) +_predA [0 [[pair (upZero 1) (upOne 0)]]] +_predB [0 [[pair (upOne 1) (upZero 1)]]] +pred [snd (0 _predZ _predA _predB)] + +# =================================== # Ternary # According to works of T.Æ. Mogensen # =================================== -zero? [0 T [F] I [F]] -upNeg [[[[[2 (4 3 2 1 0)]]]]] -upZero [[[[[1 (4 3 2 1 0)]]]]] -upPos [[[[[0 (4 3 2 1 0)]]]]] -up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]] - -negate [[[[[4 3 0 1 2]]]]] - -tritNeg [[[2]]] -tritZero [[[1]]] -tritPos [[[0]]] -lst [0 tritZero [tritNeg] [tritZero] [tritPos]] - -_succZ (pair +0 +1) -_succANeg [0 [[[pair (upNeg 2) (upZero 2)]]]] -_succAZero [0 [[[pair (upZero 2) (upPos 2)]]]] -_succAPos [0 [[[pair (upPos 2) (upNeg 1)]]]] -succ [snd (0 _succZ _succANeg _succAZero _succAPos)] - -_predZ (pair +0 -1) -_predANeg [0 [[[pair (upNeg 2) (upPos 1)]]]] -_predAZero [0 [[[pair (upZero 2) (upNeg 2)]]]] -_predAPos [0 [[[pair (upPos 2) (upZero 2)]]]] -pred [snd (0 _predZ _predANeg _predAZero _predAPos)] - -_absNeg [[[[[2 4]]]]] -_absZero [[[[[1 4]]]]] -_absPos [[[[[0 4]]]]] -abstractify [0 [[[[3]]]] _absNeg _absZero _absPos] - -_normalize [[0 [ +0 ] [[upNeg (1 1 0)]] [[upZero (1 1 0)]] [[upPos (1 1 0)]] 1]] -normalize ω _normalize - -_eqZero? [zero? (normalize 0)] -_eqNeg [[0 F [2 0] [F] [F]]] -_eqZero [[0 (1 0) [F] [2 0] [F]]] -_eqPos [[0 F [F] [F] [2 0]]] -_eqAbs [0 _eqZero? _eqNeg _eqZero _eqPos] -eq [[_eqAbs 1 (abstractify 0)]] - -_addZ [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]] -_addC [[1 0 tritZero]] -_addBNeg2 [1 (upZero (3 0 tritNeg)) (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero))] -_addBNeg [1 (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero)) (upZero (3 0 tritZero))] -_addBZero [up 1 (3 0 tritZero)] -_addBPos [1 (upZero (3 0 tritZero)) (upPos (3 0 tritZero)) (upNeg (3 0 tritPos))] -_addBPos2 [1 (upPos (3 0 tritZero)) (upNeg (3 0 tritPos)) (upZero (3 0 tritPos))] -_addANeg [[[1 (_addBNeg 1) _addBNeg2 _addBNeg _addBZero]]] -_addAZero [[[1 (_addBZero 1) _addBNeg _addBZero _addBPos]]] -_addAPos [[[1 (_addBPos 1) _addBZero _addBPos _addBPos2]]] -_addAbs [_addC (0 _addZ _addANeg _addAZero _addAPos)] -add [[_addAbs 1 (abstractify 0)]] - -sub [[add 1 (negate 0)]] +# zero? [0 T [F] I [F]] +# upNeg [[[[[2 (4 3 2 1 0)]]]]] +# upZero [[[[[1 (4 3 2 1 0)]]]]] +# upPos [[[[[0 (4 3 2 1 0)]]]]] +# up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]] +# +# negate [[[[[4 3 0 1 2]]]]] +# +# tritNeg [[[2]]] +# tritZero [[[1]]] +# tritPos [[[0]]] +# lst [0 tritZero [tritNeg] [tritZero] [tritPos]] +# +# _stripZ pair +0 T +# _stripANeg [0 [[pair (0 +0 (upNeg 1)) 0]]] +# _stripAZero [0 [[pair (upZero 1) F]]] +# _stripAPos [0 [[pair (upPos 1) F]]] +# strip [fst (0 _stripZ _stripANeg _stripAZero _stripAPos)] +# +# _succZ pair +0 +1 +# _succANeg [0 [[[pair (upNeg 2) (upZero 2)]]]] +# _succAZero [0 [[[pair (upZero 2) (upPos 2)]]]] +# _succAPos [0 [[[pair (upPos 2) (upNeg 1)]]]] +# succ [snd (0 _succZ _succANeg _succAZero _succAPos)] +# +# _predZ pair +0 -1 +# _predANeg [0 [[[pair (upNeg 2) (upPos 1)]]]] +# _predAZero [0 [[[pair (upZero 2) (upNeg 2)]]]] +# _predAPos [0 [[[pair (upPos 2) (upZero 2)]]]] +# pred [snd (0 _predZ _predANeg _predAZero _predAPos)] +# +# _absNeg [[[[[2 4]]]]] +# _absZero [[[[[1 4]]]]] +# _absPos [[[[[0 4]]]]] +# abstractify [0 [[[[3]]]] _absNeg _absZero _absPos] +# +# _normalize [[0 [ +0 ] [[upNeg (1 1 0)]] [[upZero (1 1 0)]] [[upPos (1 1 0)]] 1]] +# normalize ω _normalize +# +# _eqZero? [zero? (normalize 0)] +# _eqNeg [[0 F [2 0] [F] [F]]] +# _eqZero [[0 (1 0) [F] [2 0] [F]]] +# _eqPos [[0 F [F] [F] [2 0]]] +# _eqAbs [0 _eqZero? _eqNeg _eqZero _eqPos] +# eq [[_eqAbs 1 (abstractify 0)]] +# +# _addZ [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]] +# _addC [[1 0 tritZero]] +# _addBNeg2 [1 (upZero (3 0 tritNeg)) (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero))] +# _addBNeg [1 (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero)) (upZero (3 0 tritZero))] +# _addBZero [up 1 (3 0 tritZero)] +# _addBPos [1 (upZero (3 0 tritZero)) (upPos (3 0 tritZero)) (upNeg (3 0 tritPos))] +# _addBPos2 [1 (upPos (3 0 tritZero)) (upNeg (3 0 tritPos)) (upZero (3 0 tritPos))] +# _addANeg [[[1 (_addBNeg 1) _addBNeg2 _addBNeg _addBZero]]] +# _addAZero [[[1 (_addBZero 1) _addBNeg _addBZero _addBPos]]] +# _addAPos [[[1 (_addBPos 1) _addBZero _addBPos _addBPos2]]] +# _addAbs [_addC (0 _addZ _addANeg _addAZero _addAPos)] +# add [[_addAbs 1 (abstractify 0)]] +# +# sub [[add 1 (negate 0)]] # =============== # Boolean algebra @@ -103,4 +146,4 @@ churchAdd [[[[3 1 (2 1 0)]]]] churchMul [[[2 (1 0)]]] churchExp [[0 1]] -main I F +main [[[0 2 1]]] |