diff options
| -rw-r--r-- | readme.md | 6 | ||||
| -rw-r--r-- | samples/rosetta/empty_program.bruijn | 1 | ||||
| -rw-r--r-- | samples/rosetta/universal_lambda_machine.bruijn | 19 | ||||
| -rw-r--r-- | src/Helper.hs | 32 | ||||
| -rw-r--r-- | std/Combinator.bruijn | 2 | ||||
| -rw-r--r-- | std/Meta.bruijn | 38 | ||||
| -rw-r--r-- | std/Number/Conversion.bruijn | 4 |
7 files changed, 83 insertions, 19 deletions
@@ -6,14 +6,13 @@ > De Bruijn indices written in Haskell. Wiki, docs, articles, examples and more: -[website](https://bruijn.marvinborner.de). +[website](https://bruijn.marvinborner.de). Also: [Rosetta +Code](https://rosettacode.org/wiki/Category:Bruijn). ## Features - **De Bruijn indices** eliminate the complexity of α-equivalence and α-conversion -- Unique **bracket-style representation** for lambda abstractions - enables improved human-readability and faster syntactic perception - **Call-by-need** reduction with great time/memory complexity by using the RKNL abstract machine (similar to [calm](https://github.com/marvinborner/calm/)) @@ -23,7 +22,6 @@ Wiki, docs, articles, examples and more: itself - Highly space-efficient compilation to **binary lambda calculus (BLC)** additionally to normal interpretation and REPL -- Strongly **opinionated parser** with strict syntax rules - **Recursion** can be implemented using combinators such as Y, Z or ω - Substantial **standard library** featuring many useful functions (see `std/`) diff --git a/samples/rosetta/empty_program.bruijn b/samples/rosetta/empty_program.bruijn new file mode 100644 index 0000000..42e2f47 --- /dev/null +++ b/samples/rosetta/empty_program.bruijn @@ -0,0 +1 @@ +main [0] diff --git a/samples/rosetta/universal_lambda_machine.bruijn b/samples/rosetta/universal_lambda_machine.bruijn new file mode 100644 index 0000000..2f003ce --- /dev/null +++ b/samples/rosetta/universal_lambda_machine.bruijn @@ -0,0 +1,19 @@ +:import std/Combinator . +:import std/Number/Binary . +:import std/Meta . +:import std/List . + +# converts string to list of bits +str→blc map (c ∘ lsb) + +:test (str→blc "0010") ([[1]] : ([[1]] : ([[0]] : {}[[1]]))) + +# converts list of bits to string +blc→str map [0 '0' '1'] + +:test (blc→str ([[1]] : ([[1]] : ([[0]] : {}[[1]])))) ("0010") + +# reduces BLC string to BLC string +main str→blc → blc→meta → β* → meta→blc → blc→str + +:test (main "0010") ("0010") diff --git a/src/Helper.hs b/src/Helper.hs index 4500de6..50d8b95 100644 --- a/src/Helper.hs +++ b/src/Helper.hs @@ -13,6 +13,7 @@ import Data.Array import qualified Data.BitString as Bit import qualified Data.ByteString.Lazy as Byte import qualified Data.ByteString.Lazy.Char8 as C +import Data.Char import Data.List import qualified Data.Map as M import Data.Maybe ( fromMaybe @@ -313,8 +314,10 @@ matchingFunctions e (Environment env) = maybeHumanifyExpression :: Expression -> Maybe String maybeHumanifyExpression e = unaryToDecimal e + <|> binaryToChar e <|> binaryToDecimal e <|> ternaryToDecimal e + <|> humanifyString e <|> humanifyList e <|> humanifyPair e <|> humanifyMeta e @@ -330,7 +333,7 @@ humanifyMeta e = ("`" <>) <$> go e go (Abstraction (Abstraction (Abstraction (Application (Application (Bruijn 1) a) b)))) = go a >>= \l -> go b >>= \r -> pure $ "(" <> l <> " " <> r <> ")" go (Abstraction (Abstraction (Abstraction (Application (Bruijn 2) n)))) = - unaryToDecimal' n + fmap show (unaryToDecimal' n) go _ = Nothing humanifyList :: Expression -> Maybe String @@ -340,6 +343,12 @@ humanifyList e = do m = map conv es pure $ "{" <> intercalate ", " m <> "}" +humanifyString :: Expression -> Maybe String +humanifyString e = do + es <- unlistify e + str <- mapM binaryToChar' es + pure $ show str + humanifyPair :: Expression -> Maybe String humanifyPair e = do es <- unpairify e @@ -384,12 +393,12 @@ decimalToDeBruijn n | n < 0 = decimalToDeBruijn 0 gen n' = Abstraction $ gen (n' - 1) unaryToDecimal :: Expression -> Maybe String -unaryToDecimal e = (<> "u") <$> unaryToDecimal' e +unaryToDecimal e = (<> "u") . show <$> unaryToDecimal' e -unaryToDecimal' :: Expression -> Maybe String +unaryToDecimal' :: Expression -> Maybe Integer unaryToDecimal' e = do res <- resolve e - return $ show (sum res :: Integer) + return (sum res :: Integer) where multiplier (Bruijn 1) = Just 1 multiplier _ = Nothing @@ -403,9 +412,20 @@ unaryToDecimal' e = do resolve _ = Nothing binaryToDecimal :: Expression -> Maybe String -binaryToDecimal e = do +binaryToDecimal e = (<> "b") . show <$> binaryToDecimal' e + +binaryToChar :: Expression -> Maybe String +binaryToChar e = show <$> binaryToChar' e + +binaryToChar' :: Expression -> Maybe Char +binaryToChar' e = do + n <- binaryToDecimal' e + if n < 255 then Just $ chr $ fromIntegral n else Nothing + +binaryToDecimal' :: Expression -> Maybe Integer +binaryToDecimal' e = do res <- resolve e - return $ show (sum $ zipWith (*) res (iterate (* 2) 1) :: Integer) <> "b" + return (sum $ zipWith (*) res (iterate (* 2) 1) :: Integer) where multiplier (Bruijn 0) = Just 0 multiplier (Bruijn 1) = Just 1 diff --git a/std/Combinator.bruijn b/std/Combinator.bruijn index 71ad078..81db105 100644 --- a/std/Combinator.bruijn +++ b/std/Combinator.bruijn @@ -126,6 +126,8 @@ o [[0 (1 0)]] ⧗ ((a → b) → a) → (a → b) → b # queer bird combinator: reverse function composition q [[[1 (2 0)]]] ⧗ (a → b) → (b → c) → a → c +…→… q + # quixotic bird combinator q' [[[2 (0 1)]]] ⧗ (b → c) → a → (a → b) → c diff --git a/std/Meta.bruijn b/std/Meta.bruijn index 3b67c35..5f8da84 100644 --- a/std/Meta.bruijn +++ b/std/Meta.bruijn @@ -93,14 +93,38 @@ blc1 [[0]] ⧗ LcBit # false bit blc0 [[1]] ⧗ LcBit +# converts blc index to meta index + rest +blc→unary y [[[rec]]] (+0u) ⧗ (List LcBit) → (Pair Meta (List LcBit)) + rec 0 [[1 case-end case-rec]] + case-rec 4 ++3 0 + case-end (idx --3) : 0 + +:test (blc→unary (blc1 : {}blc0)) (`0 : [[0]]) +:test (blc→unary (blc1 : (blc1 : {}blc0))) (`1 : [[0]]) +:test (blc→unary (blc1 : (blc1 : (blc1 : {}blc0)))) (`2 : [[0]]) +:test (blc→unary (blc1 : (blc1 : (blc1 : (blc0 : {}blc1))))) (`2 : {}blc1) + +# converts blc list to meta term +# TODO: use CSP instead? +blc→meta head ∘ (y [[rec]]) ⧗ (List LcBit) → Meta + rec 0 [[1 case-0 case-1]] + case-0 ^0 case-00 case-01 + case-00 3 ~0 [[(abs 1) : 0]] + case-01 3 ~0 [[5 0 [[(app 3 1) : 0]]]] + case-1 blc→unary 2 + +:test (blc→meta (blc0 : (blc0 : (blc1 : {}blc0)))) (`[0]) +:test (blc→meta (blc0 : (blc0 : (blc0 : (blc0 : (blc0 : (blc1 : (blc1 : (blc1 : (blc0 : (blc1 : (blc1 : {}blc0)))))))))))) (`[[1 1]]) + # converts meta term to blc list -blc fold idx-cb app-cb abs-cb ⧗ Meta → (List LcBit) +meta→blc fold idx-cb app-cb abs-cb ⧗ Meta → (List LcBit) idx-cb [++0 (cons blc1) {}blc0] app-cb (cons blc0) ∘ (cons blc1) ∘∘ append abs-cb (cons blc0) ∘ (cons blc0) -:test (blc `[0]) (blc0 : (blc0 : (blc1 : {}blc0))) -:test (blc `[[1 1]]) (blc0 : (blc0 : (blc0 : (blc0 : (blc0 : (blc1 : (blc1 : (blc1 : (blc0 : (blc1 : (blc1 : {}blc0))))))))))) +:test (meta→blc `[0]) (blc0 : (blc0 : (blc1 : {}blc0))) +:test (meta→blc `[[1 1]]) (blc0 : (blc0 : (blc0 : (blc0 : (blc0 : (blc1 : (blc1 : (blc1 : (blc0 : (blc1 : (blc1 : {}blc0))))))))))) +:test (blc→meta (meta→blc `meta→blc)) (`meta→blc) α-eq? y [[[rec]]] ⧗ Meta → Meta → Bool rec 1 case-idx case-app case-abs @@ -128,7 +152,7 @@ eval-blc y [[[rec]]] [0 Ω] ⧗ (List LcBit) → a case-10 4 head case-11 [6 [6 [1 ~0]] 2] -eval* eval-blc ∘ blc ⧗ Meta → Meta +eval* eval-blc ∘ meta→blc ⧗ Meta → a # self interpreter for meta encoding eval y [[[rec]]] [0 Ω] ⧗ Meta → a @@ -226,7 +250,7 @@ map [[0 case-idx case-app case-abs]] ⧗ (Meta → Meta) → Meta → Meta :test (map inc `0) (`1) :test (map (map inc) `[0]) (`[1]) -# ternary encoding of meta terms +# encodes meta terms as ternary number # inspired by Helmut Brandl's and Steve Goguen's work # uses ternary for lower space complexity encode fold idx-cb app-cb abs-cb ⧗ Meta → Number @@ -240,9 +264,9 @@ encode fold idx-cb app-cb abs-cb ⧗ Meta → Number :test (ternary-to-unary (encode `[1])) ((+7u)) :test (ternary-to-unary (encode `[0])) ((+8u)) -# decode ternary encoding back to meta term +# decodes ternary encoding back to meta term # TODO: improve performance (maybe with different unpairing function or better sqrt) -decode z [[unpair-ternary 0 go]] ⧗ Number → Meta +decode y [[unpair-ternary 0 go]] ⧗ Number → Meta go [[(case-idx : (case-app : {}case-abs)) !! 1 0]] case-idx idx ∘ ternary-to-unary case-app [unpair-ternary 0 (ψ app 4)] diff --git a/std/Number/Conversion.bruijn b/std/Number/Conversion.bruijn index c9a568f..fe7e63c 100644 --- a/std/Number/Conversion.bruijn +++ b/std/Number/Conversion.bruijn @@ -4,13 +4,13 @@ :import std/Number/Unary U :import std/Number/Ternary T -# convert unary numbers to ternary +# converts unary numbers to ternary unary-to-ternary [0 T.inc (+0)] ⧗ Unary → Ternary :test (unary-to-ternary (+0u)) ((+0)) :test (unary-to-ternary (+2u)) ((+2)) -# convert ternary numbers to unary +# converts ternary numbers to unary ternary-to-unary [T.apply 0 U.inc (+0u)] ⧗ Ternary → Unary :test (ternary-to-unary (+0)) ((+0u)) |