diff options
| author | Marvin Borner | 2024-02-21 20:28:55 +0100 |
|---|---|---|
| committer | Marvin Borner | 2024-02-21 22:25:09 +0100 |
| commit | c9b30f99992c98745d52807f5e45a12f6aee2c5f (patch) | |
| tree | 68eaf084eaed2ae515e62fb9c55d52836a327b24 /std | |
| parent | 241315c452b1b06e4b9721cf336d9ab150f7234d (diff) | |
Additions for Rosetta Code
Diffstat (limited to 'std')
| -rw-r--r-- | std/Combinator.bruijn | 2 | ||||
| -rw-r--r-- | std/Meta.bruijn | 38 | ||||
| -rw-r--r-- | std/Number/Conversion.bruijn | 4 |
3 files changed, 35 insertions, 9 deletions
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)) |