diff options
| -rw-r--r-- | std/List.bruijn | 4 | ||||
| -rw-r--r-- | std/Meta.bruijn | 6 | ||||
| -rw-r--r-- | std/Number/Binary.bruijn | 16 | ||||
| -rw-r--r-- | std/Number/Ternary.bruijn | 24 | ||||
| -rw-r--r-- | std/Number/Unary.bruijn | 22 | ||||
| -rw-r--r-- | std/Option.bruijn | 2 | ||||
| -rw-r--r-- | std/Pair.bruijn | 4 |
7 files changed, 39 insertions, 39 deletions
diff --git a/std/List.bruijn b/std/List.bruijn index bb8bed3..0d0a038 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -68,7 +68,7 @@ apply z [[[rec]]] ⧗ (a* → b) → (List a) → b :test (…+… <! ((+1) : {}(+2))) ((+3)) # applies each element of the tail to the head (left-associative) -eval [0 apply] ⧗ (Pair (a → b) (List a)) → b +eval &apply ⧗ (Pair (a → b) (List a)) → b !‣ eval @@ -472,4 +472,4 @@ iterate z [[[rec]]] ⧗ (a → a) → a → (List a) y* [[[0 1] <$> 0] xs] ⧗ a → (List b) xs [[1 <! ([[1 2 0]] <$> 0)]] <$> 0 -:test ([0 (+5)] <$> (y* ([[[=?0 true (1 --0)]]] : {}[[[=?0 false (2 --0)]]]))) (false : {}true) +:test (&(+5) <$> (y* ([[[=?0 true (1 --0)]]] : {}[[[=?0 false (2 --0)]]]))) (false : {}true) diff --git a/std/Meta.bruijn b/std/Meta.bruijn index 3b4ccbd..77027e9 100644 --- a/std/Meta.bruijn +++ b/std/Meta.bruijn @@ -145,7 +145,7 @@ meta→blc fold idx-cb app-cb abs-cb ⧗ Meta → (List LcBit) :test (α-eq? `α-eq? `α-eq?) (true) # modified Tromp 232 bit universal machine -eval-blc y [[[rec]]] [0 Ω] ⧗ (List LcBit) → a +eval-blc y [[[rec]]] &Ω ⧗ (List LcBit) → a rec 0 [[0 [2 case-0 case-1]]] case-0 5 [1 case-00 case-01] case-00 5 [[2 (0 : 1)]] @@ -157,9 +157,9 @@ eval-blc y [[[rec]]] [0 Ω] ⧗ (List LcBit) → a eval* eval-blc ∘ meta→blc ⧗ Meta → a # self interpreter for meta encoding -eval y [[[rec]]] [0 Ω] ⧗ Meta → a +eval y [[[rec]]] &Ω ⧗ Meta → a rec 0 case-idx case-app case-abs - case-idx [2 [1 [0 [[0]]] 0 [[1]]]] + case-idx [2 [1 &[[0]] 0 [[1]]]] case-app 2 [3 [3 [2 0 (1 0)]]] case-abs 2 [2 [[2 [0 1 2]]]] diff --git a/std/Number/Binary.bruijn b/std/Number/Binary.bruijn index 6445d9f..fac9ba1 100644 --- a/std/Number/Binary.bruijn +++ b/std/Number/Binary.bruijn @@ -59,8 +59,8 @@ binary! foldr up (+0b) ⧗ (List Bit) → Binary # strips leading 0s from a binary number strip [^(0 z a¹ a⁰)] ⧗ Binary → Binary z (+0b) : true - a¹ [0 [[↑¹1 : false]]] - a⁰ [0 [[(0 (+0b) ↑⁰1) : 0]]] + a¹ &[[↑¹1 : false]] + a⁰ &[[(0 (+0b) ↑⁰1) : 0]] %‣ strip @@ -162,8 +162,8 @@ not-eq? not! ∘∘ eq? ⧗ Binary → Binary → Boolean # adds 1 to a binary number (can introduce leading 0s) inc [~(0 z a¹ a⁰)] ⧗ Binary → Binary z (+0b) : (+1b) - a¹ [0 [[↑¹1 : ↑⁰0]]] - a⁰ [0 [[↑⁰1 : ↑¹1]]] + a¹ &[[↑¹1 : ↑⁰0]] + a⁰ &[[↑⁰1 : ↑¹1]] ++‣ inc @@ -173,8 +173,8 @@ inc [~(0 z a¹ a⁰)] ⧗ Binary → Binary # subs 1 from a binary number (can introduce leading 0s) dec [~(0 z a¹ a⁰)] ⧗ Binary → Binary z (+0b) : (+0b) - a¹ [0 [[↑¹1 : ↑⁰1]]] - a⁰ [0 [[↑⁰1 : ↑¹0]]] + a¹ &[[↑¹1 : ↑⁰1]] + a⁰ &[[↑⁰1 : ↑¹0]] --‣ dec @@ -268,8 +268,8 @@ sub [[(0 =? 1) (+0b) -((pad 1 0) + -(pad 0 1))]] ⧗ Binary → Binary → Binar # rshifts least significant bit of a binary number div² [~(0 z a¹ a⁰)] ⧗ Binary → Binary z (+0b) : (+0b) - a¹ [0 [[↑¹1 : 1]]] - a⁰ [0 [[↑⁰1 : 1]]] + a¹ &[[↑¹1 : 1]] + a⁰ &[[↑⁰1 : 1]] /²‣ div² diff --git a/std/Number/Ternary.bruijn b/std/Number/Ternary.bruijn index e1b3893..f63d9ac 100644 --- a/std/Number/Ternary.bruijn +++ b/std/Number/Ternary.bruijn @@ -90,9 +90,9 @@ list! [0 z a⁻ a⁺ a⁰] ⧗ Number → List # strips leading 0s from a balanced ternary number strip [^(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number z (+0) : true - a⁻ [0 [[↑⁻1 : false]]] - a⁺ [0 [[↑⁺1 : false]]] - a⁰ [0 [[(0 (+0) ↑⁰1) : 0]]] + a⁻ &[[↑⁻1 : false]] + a⁺ &[[↑⁺1 : false]] + a⁰ &[[(0 (+0) ↑⁰1) : 0]] %‣ strip @@ -218,9 +218,9 @@ not-eq? not! ∘∘ eq? ⧗ Number → Number → Boolean # adds (+1) to a balanced ternary number (can introduce leading 0s) inc [~(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number z (+0) : (+1) - a⁻ [0 [[↑⁻1 : ↑⁰1]]] - a⁺ [0 [[↑⁺1 : ↑⁻0]]] - a⁰ [0 [[↑⁰1 : ↑⁺1]]] + a⁻ &[[↑⁻1 : ↑⁰1]] + a⁺ &[[↑⁺1 : ↑⁻0]] + a⁰ &[[↑⁰1 : ↑⁺1]] ++‣ inc @@ -233,9 +233,9 @@ inc [~(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number # subs (+1) from a balanced ternary number (can introduce leading 0s) dec [~(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number z (+0) : (-1) - a⁻ [0 [[↑⁻1 : ↑⁺0]]] - a⁺ [0 [[↑⁺1 : ↑⁰1]]] - a⁰ [0 [[↑⁰1 : ↑⁻1]]] + a⁻ &[[↑⁻1 : ↑⁺0]] + a⁺ &[[↑⁺1 : ↑⁰1]] + a⁰ &[[↑⁰1 : ↑⁻1]] --‣ dec @@ -366,9 +366,9 @@ mul [[1 z a⁻ a⁺ a⁰]] ⧗ Number → Number → Number # WARNING: Not necessarily equivalent to (/ (+3)): e.g. /³(+5) == (+2)! div³ [~(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number z (+0) : (+0) - a⁻ [0 [[↑⁻1 : 1]]] - a⁺ [0 [[↑⁺1 : 1]]] - a⁰ [0 [[↑⁰1 : 1]]] + a⁻ &[[↑⁻1 : 1]] + a⁺ &[[↑⁺1 : 1]] + a⁰ &[[↑⁰1 : 1]] /³‣ div³ diff --git a/std/Number/Unary.bruijn b/std/Number/Unary.bruijn index 6ace440..0c65c41 100644 --- a/std/Number/Unary.bruijn +++ b/std/Number/Unary.bruijn @@ -9,9 +9,9 @@ # id for church numerals # generic base for dec/fib/fac/etc. uid [[[extract (2 inc init)]]] ⧗ Unary → Unary - extract [0 [0]] - inc [[0 (1 3)]] - init [0 1] + extract &i + inc [&(0 2)] + init &0 :test (uid (+0u)) ((+0u)) :test (uid (+1u)) ((+1u)) @@ -36,8 +36,8 @@ inc [[[1 (2 1 0)]]] ⧗ Unary → Unary # subs 1 from a unary number dec [[[extract (2 inc const)]]] ⧗ Unary → Unary - extract [0 [0]] - inc [[0 (1 3)]] + extract &i + inc [&(0 2)] const [1] --‣ dec @@ -142,7 +142,7 @@ mul …∘… ⧗ Unary → Unary → Unary :test ((+2u) ⋅ (+3u)) ((+6u)) # divs two unary numbers -div [[[[3 [[0 1]] [1] (3 [3 [[0 1]] [3 (0 1)] [0]] 0)]]]] ⧗ Unary → Unary → Unary +div [[[[3 t [1] (3 [3 t [3 (0 1)] i] 0)]]]] ⧗ Unary → Unary → Unary …/… div @@ -156,7 +156,7 @@ div* [z rec ++0] ⧗ Unary → Unary → Unary rec [[[[[[=?0 ((+0u) 2 1) (2 (5 0 3 2 1))] (3 - 2)]]]]] # returns remainder of integer division -mod [[[[3 [0 [[1]]] (3 [3 [[[0 (2 (5 1)) 1]]] [1] 1] [1]) [[0]]]]]] ⧗ Unary → Unary → Unary +mod [[[[3 &k (3 [3 [[[0 (2 (5 1)) 1]]] [1] 1] [1]) ki]]]] ⧗ Unary → Unary → Unary …%… mod @@ -164,7 +164,7 @@ mod [[[[3 [0 [[1]]] (3 [3 [[[0 (2 (5 1)) 1]]] [1] 1] [1]) [[0]]]]]] ⧗ Unary :test ((+3u) % (+5u)) ((+3u)) # slower mod (more obvious impl) -mod* [[1 [0 [[(0 ⋀? (3 ≤? 1)) case-rec case-end]]] (1 : true) [[1]]]] ⧗ Unary → Unary → Unary +mod* [[1 &[[(0 ⋀? (2 ≤? 1)) case-rec case-end]] (1 : true) k]] ⧗ Unary → Unary → Unary case-rec (1 - 3) : true case-end 1 : false @@ -173,7 +173,7 @@ mod* [[1 [0 [[(0 ⋀? (3 ≤? 1)) case-rec case-end]]] (1 : true) [[1]]]] ⧗ Un pow* [[1 0]] ⧗ Unary → Unary → Unary # exponentiates two unary numbers -pow [[0 [[3 (1 0)]] [[1 0]]]] ⧗ Unary → Unary → Unary +pow [[0 [[3 (1 0)]] pow*]] ⧗ Unary → Unary → Unary …^… pow @@ -187,11 +187,11 @@ fib [0 [[[2 0 [2 (1 0)]]]] [[1]] [0]] ⧗ Unary → Unary :test (fib (+6u)) ((+8u)) # factorial function -fac [[1 [[0 (1 [[2 1 (1 0)]])]] [1] [0]]] ⧗ Unary → Unary +fac [[1 [[0 (1 [[2 1 (1 0)]])]] [1] i]] ⧗ Unary → Unary :test (fac (+3u)) ((+6u)) # hyperfactorial function -hyperfac [[1 [[(0 0) (1 [[2 1 (1 0)]])]] [1] [0]]] ⧗ Unary → Unary +hyperfac [[1 [[(0 0) (1 [[2 1 (1 0)]])]] [1] i]] ⧗ Unary → Unary :test (hyperfac (+3u)) ((+108u)) diff --git a/std/Option.bruijn b/std/Option.bruijn index fafe173..20e4a19 100644 --- a/std/Option.bruijn +++ b/std/Option.bruijn @@ -28,7 +28,7 @@ map [[0 none [some (2 0)]]] ⧗ (a → b) → (Option a) → (Option b) :test (map [[1]] none) (none) # applies a function to the value in option or returns first arg if none -map-or [[[0 2 1]]] ⧗ (a → b) → (Option a) → (Option c) +map-or v ⧗ (a → b) → (Option a) → (Option c) :test (map-or [[[2]]] [[1]] (some [[0]])) ([[[0]]]) :test (map-or [[[2]]] [[1]] none) ([[[2]]]) diff --git a/std/Pair.bruijn b/std/Pair.bruijn index 95995ee..7cf30bf 100644 --- a/std/Pair.bruijn +++ b/std/Pair.bruijn @@ -8,14 +8,14 @@ pair [[[0 2 1]]] ⧗ a → b → (Pair a b) …:… pair # extracts first expression from pair -fst [0 k] ⧗ (Pair a b) → a +fst &k ⧗ (Pair a b) → a ^‣ fst :test (^([[0]] : [[1]])) ([[0]]) # extracts second expression from pair -snd [0 ki] ⧗ (Pair a b) → b +snd &ki ⧗ (Pair a b) → b ~‣ snd |