From c5dc5c2d811c66b47733b98a304c0f0b6cc6c947 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Tue, 21 Feb 2023 05:42:41 +0100
Subject: Standard library sync
---
std/Byte.bruijn | 2 +-
std/Church.bruijn | 8 ++-
std/Combinator.bruijn | 1 +
std/List.bruijn | 70 +++++++++++++-----------
std/Math.bruijn | 35 +++++++++++-
std/Number.bruijn | 143 +++++++++++++++++++++++++++-----------------------
std/Pair.bruijn | 16 +++---
std/String.bruijn | 8 +--
8 files changed, 169 insertions(+), 114 deletions(-)
diff --git a/std/Byte.bruijn b/std/Byte.bruijn
index 36aaf58..8dcbb7b 100644
--- a/std/Byte.bruijn
+++ b/std/Byte.bruijn
@@ -11,7 +11,7 @@ b0 false
b1 true
# returns true if two bytes are equal
-eq? &&‣ .. (zip-with xnor?)
+eq? ⋀?‣ ∘∘ (zip-with xnor?)
…=?… eq?
diff --git a/std/Church.bruijn b/std/Church.bruijn
index 6277dcc..9e567b0 100644
--- a/std/Church.bruijn
+++ b/std/Church.bruijn
@@ -2,6 +2,12 @@
zero [[0]]
+zero? [0 [[[0]]] [[1]]]
+
+dec [[[2 [[0 (1 3)]] [1] [0]]]]
+
+--‣ dec
+
inc [[[1 (2 1 0)]]]
++‣ inc
@@ -12,7 +18,7 @@ add [[[[3 1 (2 1 0)]]]]
mul [[[2 (1 0)]]]
-…*… mul
+…⋅… mul
exp [[0 1]]
diff --git a/std/Combinator.bruijn b/std/Combinator.bruijn
index 34f9631..37fa504 100644
--- a/std/Combinator.bruijn
+++ b/std/Combinator.bruijn
@@ -180,6 +180,7 @@ w' [[0 1 1]]
y [[1 (0 0)] [1 (0 0)]]
# z fixed point combinator
+# y and z are almost always interchangeable
z [[1 [1 1 0]] [1 [1 1 0]]]
# theta combinator
diff --git a/std/List.bruijn b/std/List.bruijn
index f0cbc47..bce9463 100644
--- a/std/List.bruijn
+++ b/std/List.bruijn
@@ -12,9 +12,9 @@ empty false
# returns true if a list is empty
empty? [0 [[[false]]] true]
-<>?‣ empty?
+∅?‣ empty?
-:test (<>?empty) (true)
+:test (∅?empty) (true)
# prepends an element to a list
cons P.pair
@@ -22,7 +22,7 @@ cons P.pair
…:… cons
:test ((+1) : ((+2) : empty)) (P.pair (+1) (P.pair (+2) empty))
-:test (<>?((+2) : empty)) (false)
+:test (∅?((+2) : empty)) (false)
# returns the head of a list or empty
head P.fst
@@ -40,18 +40,18 @@ tail P.snd
# returns the length of a list in balanced ternary
length z [[[rec]]] (+0)
- rec <>?0 case-end case-inc
+ rec ∅?0 case-end case-inc
case-inc 2 ++1 ~0
case-end 1
-#‣ length
+∀‣ length
-:test (#((+1) : ((+2) : empty))) ((+2))
-:test (#empty) ((+0))
+:test (∀((+1) : ((+2) : empty))) ((+2))
+:test (∀empty) ((+0))
# returns the element at index in list
index z [[[rec]]]
- rec <>?0 case-end case-index
+ rec ∅?0 case-end case-index
case-index =?1 ^0 (2 --1 ~0)
case-end empty
@@ -64,7 +64,7 @@ index z [[[rec]]]
# applies a left fold on a list
foldl z [[[[rec]]]]
- rec <>?0 case-end case-fold
+ rec ∅?0 case-end case-fold
case-fold 3 2 (2 1 ^0) ~0
case-end 1
@@ -76,7 +76,7 @@ foldl1 [[foldl 1 ^0 ~0]]
# applies a right fold on a list
foldr [[[z [[rec]] 0]]]
- rec <>?0 case-end case-fold
+ rec ∅?0 case-end case-fold
case-fold 4 ^0 (1 ~0)
case-end 3
@@ -124,7 +124,7 @@ singleton [0 : empty]
# appends two lists
append z [[[rec]]]
- rec <>?1 case-end case-append
+ rec ∅?1 case-end case-append
case-append ^1 : (2 ~1 0)
case-end 0
@@ -142,7 +142,7 @@ snoc [[1 ++ ({ 0 })]]
# maps each element to a function
map z [[[rec]]]
- rec <>?0 case-end case-map
+ rec ∅?0 case-end case-map
case-map (1 ^0) : (2 1 ~0)
case-end empty
@@ -152,7 +152,7 @@ map z [[[rec]]]
# filters a list based on a predicate
filter z [[[rec]]]
- rec <>?0 case-end case-filter
+ rec ∅?0 case-end case-filter
case-filter 1 ^0 (cons ^0) i (2 1 ~0)
case-end empty
@@ -163,20 +163,20 @@ filter z [[[rec]]]
# returns the last element of a list
# - slow algorithm:
# last z [[rec]]
-# rec <>?0 case-end case-last
-# case-last <>?(~0) ^0 (1 ~0)
+# rec ∅?0 case-end case-last
+# case-last ∅?(~0) ^0 (1 ~0)
# case-end empty
# - taking the first element of the reversed list is actually way faster because laziness
last ^‣ ∘ <~>‣
_‣ last
-:test (last ((+1) : ((+2) : ((+3) : empty)))) ((+3))
+:test (_((+1) : ((+2) : ((+3) : empty)))) ((+3))
# returns everything but the last element of a list
init z [[rec]]
- rec <>?0 case-end case-init
- case-init <>?(~0) empty (^0 : (1 ~0))
+ rec ∅?0 case-end case-init
+ case-init ∅?(~0) empty (^0 : (1 ~0))
case-end empty
:test (init ((+1) : ((+2) : ((+3) : empty)))) ((+1) : ((+2) : empty))
@@ -196,16 +196,16 @@ concat-map concat ∘∘ map
# zips two lists discarding excess elements
zip z [[[rec]]]
- rec <>?1 case-end case-zip
- case-zip <>?0 empty ((^1 : ^0) : (2 ~1 ~0))
+ rec ∅?1 case-end case-zip
+ case-zip ∅?0 empty ((^1 : ^0) : (2 ~1 ~0))
case-end empty
:test (zip ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) (((+1) : (+2)) : (((+2) : (+1)) : empty))
# applies pairs of the zipped list as arguments to a function
zip-with z [[[[rec]]]]
- rec <>?1 case-end case-zip
- case-zip <>?0 empty ((2 ^1 ^0) : (3 2 ~1 ~0))
+ rec ∅?1 case-end case-zip
+ case-zip ∅?0 empty ((2 ^1 ^0) : (3 2 ~1 ~0))
case-end empty
:test (zip-with …+… ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) ((+3) : ((+3) : empty))
@@ -222,7 +222,7 @@ zip-with z [[[[rec]]]]
# returns first n elements of a list
take z [[[rec]]]
- rec <>?0 case-end case-take
+ rec ∅?0 case-end case-take
case-take =?1 empty (^0 : (2 --1 ~0))
case-end empty
@@ -230,7 +230,7 @@ take z [[[rec]]]
# takes elements while a predicate is satisfied
take-while z [[[rec]]]
- rec <>?0 case-end case-take
+ rec ∅?0 case-end case-take
case-take 1 ^0 (^0 : (2 1 ~0)) empty
case-end empty
@@ -238,7 +238,7 @@ take-while z [[[rec]]]
# removes first n elements of a list
drop z [[[rec]]]
- rec <>?0 case-end case-drop
+ rec ∅?0 case-end case-drop
case-drop =?1 0 (2 --1 ~0)
case-end empty
@@ -246,7 +246,7 @@ drop z [[[rec]]]
# removes elements from list while a predicate is satisfied
drop-while z [[[rec]]]
- rec <>?0 case-end case-drop
+ rec ∅?0 case-end case-drop
case-drop 1 ^0 (2 1 ~0) 0
case-end empty
@@ -254,7 +254,7 @@ drop-while z [[[rec]]]
# returns pair of take-while and drop-while
span z [[[rec]]]
- rec <>?0 case-end case-drop
+ rec ∅?0 case-end case-drop
case-drop 1 ^0 ((^0 : ^recced) : ~recced) (empty : 0)
recced 2 1 ~0
case-end empty : empty
@@ -266,6 +266,16 @@ break span ∘ (…∘… ¬‣)
:test (break (\gre? (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty)))
+# splits a list into two lists based on predicate
+split-at z [[[rec]]]
+ rec ∅?dropped case-end case-split
+ dropped drop-while 1 0
+ case-split ^broken : (2 1 ~broken)
+ broken break 1 dropped
+ case-end empty
+
+:test (split-at (…=?… (+1)) ((+2) : ((+1) : ((+3) : ((+2) : empty))))) ((((+2) : empty) : (((+3) : ((+2) : empty)) : empty)))
+
# returns true if any element in a list matches a predicate
any? ⋁?‣ ∘∘ map
@@ -293,7 +303,7 @@ eq? ⋀?‣ ∘∘∘ zip-with
# removes first element that match an eq predicate
remove z [[[[rec]]]]
- rec <>?0 case-end case-remove
+ rec ∅?0 case-end case-remove
case-remove (2 ^0 1) ~0 (^0 : (3 2 1 ~0))
case-end empty
@@ -301,7 +311,7 @@ remove z [[[[rec]]]]
# removes duplicates from list based on eq predicate (keeps first occurrence)
nub z [[[rec]]]
- rec <>?0 case-end case-nub
+ rec ∅?0 case-end case-nub
case-nub ^0 : (2 1 (~0 <#> [¬(2 0 ^1)]))
case-end empty
@@ -330,6 +340,6 @@ iterate z [[[rec]]]
rec 0 : (2 1 (1 0))
:test (take (+5) (iterate ++‣ (+0))) (((+0) : ((+1) : ((+2) : ((+3) : ((+4) : empty))))))
-:test (take (+2) (iterate sdec (+5))) (((+5) : ((+4) : empty)))
+:test (take (+2) (iterate (%‣ ∘ dec) (+5))) (((+5) : ((+4) : empty)))
:test (take (+5) (iterate i (+4))) (take (+5) (repeat (+4)))
:test (take (+0) (iterate ++‣ (+0))) (empty)
diff --git a/std/Math.bruijn b/std/Math.bruijn
index 9d3dff2..7cf0af0 100644
--- a/std/Math.bruijn
+++ b/std/Math.bruijn
@@ -1,7 +1,6 @@
# MIT License, Copyright (c) 2022 Marvin Borner
:import std/List .
-
:input std/Number .
# adds all values in list
@@ -69,6 +68,23 @@ pow […!!… (iterate (…*… 0) (+1))]
:test (((+2) ** (+3)) =? ((+8))) (true)
+# power function using ternary exponentiation
+# a 1 → b 0
+# pow' z [[[rec]]]
+# rec =?0 case-end case-pow
+# case-pow =?(lst 0) (mult ⊩r) ((mult ⊩r) ⋅ 1)
+# mult [0 ⋅ 0 ⋅ 0]
+# r 2 1 /³0
+# case-end (+1)
+pow' z [[[rec]]]
+ rec =?0 case-end case-pow
+ case-pow =?(lst 0) (r ⋅ r ⋅ r) (r ⋅ r ⋅ r ⋅ 1)
+ r 2 1 /³0
+ case-end (+1)
+
+# prime number sequence
+primes nub ((…≠?… (+1)) ∘∘ gcd) (iterate ++‣ (+2))
+
# factorial function
# TODO: faster fac?
fac [∏ (+1) → 0 | i]
@@ -82,3 +98,20 @@ fibs fst <$> (iterate [~0 : (^0 + ~0)] ((+0) : (+1)))
fib [fibs !! ++0]
:test (fib (+5)) ((+8))
+
+# pascal triangle
+# TODO: this generally works, BUT lists in lists get reduced and mess up indexing
+pascal iterate [zip-with …+… ({ (+0) } ++ 0) (0 ; (+0))] ({ (+1) })
+
+# π
+# q 3, r 2, t 1, i 0
+# translation of unbounded spigot algorithm by Jeremy Gibbons
+π g (+1) (+180) (+60) (+2)
+ g y [[[[[calc]]]]]
+ calc b : (4 q r t i)
+ a ↑⁰(↑⁺0 ⋅ (↑⁰0 + (+2)))
+ b (3 ⋅ ↑⁰(↑⁻(↑⁻0)) + ((+5) ⋅ 2)) /! ((+5) ⋅ 1)
+ q (+10) ⋅ 3 ⋅ 0 ⋅ --((+2) ⋅ 0)
+ r (+10) ⋅ a ⋅ (3 ⋅ ((+5) ⋅ 0 - (+2)) + 2 - (b ⋅ 1)
+ t 1 ⋅ a
+ i ++0
diff --git a/std/Number.bruijn b/std/Number.bruijn
index ae4a3ac..3a2efe9 100644
--- a/std/Number.bruijn
+++ b/std/Number.bruijn
@@ -8,22 +8,22 @@
:import std/Logic .
# negative trit indicating coeffecient of (-1)
-t⁻ [[[2]]]
+t⁻ [[[2]]] ⧗ Trit
# returns true if a trit is negative
-t⁻? [0 true false false]
+t⁻? [0 true false false] ⧗ Trit → Boolean
# positive trit indicating coeffecient of (+1)
-t⁺ [[[1]]]
+t⁺ [[[1]]] ⧗ Trit
# returns true if a trit is positive
-t⁺? [0 false true false]
+t⁺? [0 false true false] ⧗ Trit → Boolean
# zero trit indicating coeffecient of 0
-t⁰ [[[0]]]
+t⁰ [[[0]]] ⧗ Trit
# returns true if a trit is zero
-t⁰? [0 false false true]
+t⁰? [0 false false true] ⧗ Trit → Boolean
:test (t⁻? t⁻) (true)
:test (t⁻? t⁺) (false)
@@ -36,28 +36,28 @@ t⁰? [0 false false true]
:test (t⁰? t⁰) (true)
# shifts a negative trit into a balanced ternary number
-↑⁻‣ [[[[[2 (4 3 2 1 0)]]]]]
+↑⁻‣ [[[[[2 (4 3 2 1 0)]]]]] ⧗ Number → Number
:test (↑⁻(+0)) ((-1))
:test (↑⁻(-1)) ((-4))
:test (↑⁻(+42)) ((+125))
# shifts a positive trit into a balanced ternary number
-↑⁺‣ [[[[[1 (4 3 2 1 0)]]]]]
+↑⁺‣ [[[[[1 (4 3 2 1 0)]]]]] ⧗ Number → Number
:test (↑⁺(+0)) ((+1))
:test (↑⁺(-1)) ((-2))
:test (↑⁺(+42)) ((+127))
# shifts a zero trit into a balanced ternary number
-↑⁰‣ [[[[[0 (4 3 2 1 0)]]]]]
+↑⁰‣ [[[[[0 (4 3 2 1 0)]]]]] ⧗ Number → Number
:test (↑⁰(+0)) ([[[[0 3]]]])
:test (↑⁰(+1)) ((+3))
:test (↑⁰(+42)) ((+126))
# shifts a specified trit into a balanced ternary number
-up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
+up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]] ⧗ Trit → Number → Number
:test (up t⁻ (+42)) (↑⁻(+42))
:test (up t⁺ (+42)) (↑⁺(+42))
@@ -65,10 +65,10 @@ up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
# infinity
# WARNING: using this mostly results in undefined behavior! (TODO?)
-infty z [[[[[1 (4 1)]]]]]
+infty z [[[[[1 (4 1)]]]]] ⧗ Number
# negates a balanced ternary number
-negate [[[[[4 3 1 2 0]]]]]
+negate [[[[[4 3 1 2 0]]]]] ⧗ Number → Number
-‣ negate
@@ -77,7 +77,7 @@ negate [[[[[4 3 1 2 0]]]]]
:test (-(+42)) ((-42))
# converts a balanced ternary number to a list of trits
-list! [0 z a⁻ a⁺ a⁰]
+list! [0 z a⁻ a⁺ a⁰] ⧗ Number → List
z [[0]]
a⁻ [t⁻ : 0]
a⁺ [t⁺ : 0]
@@ -86,7 +86,7 @@ list! [0 z a⁻ a⁺ a⁰]
# TODO: Tests!
# strips leading 0s from balanced ternary number
-strip [^(0 z a⁻ a⁺ a⁰)]
+strip [^(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number
z (+0) : true
a⁻ [0 [[↑⁻1 : false]]]
a⁺ [0 [[↑⁺1 : false]]]
@@ -99,15 +99,15 @@ strip [^(0 z a⁻ a⁺ a⁰)]
:test (%(+42)) ((+42))
# extracts least significant trit from balanced ternary numbers
-lst [0 t⁰ [t⁻] [t⁺] [t⁰]]
+lst [0 t⁰ [t⁻] [t⁺] [t⁰]] ⧗ Number → Trit
:test (lst (-1)) (t⁻)
:test (lst (+0)) (t⁰)
:test (lst (+1)) (t⁺)
:test (lst (+42)) (t⁰)
-# checks true if balanced ternary number is zero
-zero? [0 true [false] [false] i]
+# returns true if balanced ternary number is zero
+zero? [0 true [false] [false] i] ⧗ Number → Boolean
=?‣ zero?
@@ -116,11 +116,21 @@ zero? [0 true [false] [false] i]
:test (=?(+1)) (false)
:test (=?(+42)) (false)
+# returns true if balanced ternary number is not
+not-zero? [0 false [true] [true] i] ⧗ Number → Boolean
+
+≠?‣ not-zero?
+
+:test (≠?(+0)) (false)
+:test (≠?(-1)) (true)
+:test (≠?(+1)) (true)
+:test (≠?(+42)) (true)
+
# extracts most significant trit from balanced ternary numbers
# <~>/<>? are hardcoded because list import would be recursive (TODO?)
# while this looks incredibly inefficient it's actually fairly fast because laziness
# TODO: find way of removing requirement of stripping first
-mst [=?0 t⁰ ^(<~>(list! %0))]
+mst [=?0 t⁰ ^(<~>(list! %0))] ⧗ Number → Trit
<~>‣ z [[[[<>?0 1 (3 2 (2 1 ^0) ~0)]]]] f false
<>?‣ [0 [[[false]]] true]
@@ -130,7 +140,7 @@ mst [=?0 t⁰ ^(<~>(list! %0))]
:test (mst (+42)) (t⁺)
# returns true if balanced ternary number is negative
-negative? [t⁻? (mst 0)]
+negative? [t⁻? (mst 0)] ⧗ Number → Boolean
<?‣ negative?
@@ -140,7 +150,7 @@ negative? [t⁻? (mst 0)]
:test (<?(+42)) (false)
# returns true if balanced ternary number is positive
-positive? [t⁺? (mst 0)]
+positive? [t⁺? (mst 0)] ⧗ Number → Boolean
>?‣ positive?
@@ -152,7 +162,7 @@ positive? [t⁺? (mst 0)]
# converts the normal balanced ternary representation into abstract
# infinity can't be abstracted in finite time
# → the abstract representation is used in eq?/add/sub/mul
-abstract! [0 z a⁻ a⁺ a⁰]
+abstract! [0 z a⁻ a⁺ a⁰] ⧗ Number → AbstractNumber
z (+0)
a⁻ [[[[[2 4]]]]]
a⁺ [[[[[1 4]]]]]
@@ -165,7 +175,7 @@ abstract! [0 z a⁻ a⁺ a⁰]
:test (→^(+3)) ([[[[0 [[[[1 [[[[3]]]]]]]]]]]])
# converts the abstracted balanced ternary representation back to normal
-normal! ω [[0 z a⁻ a⁺ a⁰]]
+normal! ω [[0 z a⁻ a⁺ a⁰]] ⧗ AbstractNumber → Number
z (+0)
a⁻ [↑⁻([3 3 0] 0)]
a⁺ [↑⁺([3 3 0] 0)]
@@ -177,10 +187,10 @@ normal! ω [[0 z a⁻ a⁺ a⁰]]
:test (→_(→^(+42))) ((+42))
:test (→_(→^(-42))) ((-42))
-# checks whether two balanced ternary numbers are equal
+# returns true if two balanced ternary numbers are equal
# larger numbers should be second argument (performance)
# → ignores leading 0s!
-eq? [[abs 1 →^0]]
+eq? [[abs 1 →^0]] ⧗ Number → Number → Boolean
abs [0 z a⁻ a⁺ a⁰]
z [=?(→_0)]
a⁻ [[0 false [2 0] [false] [false]]]
@@ -189,9 +199,9 @@ eq? [[abs 1 →^0]]
…=?… eq?
-neq? not! ∘∘ eq?
+not-eq? not! ∘∘ eq? ⧗ Number → Number → Boolean
-…/=?… neq?
+…≠?… not-eq?
:test ((-42) =? (-42)) (true)
:test ((-1) =? (-1)) (true)
@@ -201,8 +211,8 @@ neq? not! ∘∘ eq?
:test ((+1) =? (+1)) (true)
:test ((+42) =? (+42)) (true)
:test ([[[[(1 (0 (0 (0 (0 3)))))]]]] =? (+1)) (true)
-:test ((+1) /=? (+0)) (true)
-:test ((-42) /=? (+42)) (true)
+:test ((+1) ≠? (+0)) (true)
+:test ((-42) ≠? (+42)) (true)
# I believe Mogensen's Paper has an error in its inc/dec/add/mul/eq definitions.
# They use 3 instead of 2 abstractions in the functions, also we use switched
@@ -210,7 +220,7 @@ neq? not! ∘∘ eq?
# the same. Something's weird.
# adds (+1) to a balanced ternary number (can introduce leading 0s)
-inc [~(0 z a⁻ a⁺ a⁰)]
+inc [~(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number
z (+0) : (+1)
a⁻ [0 [[↑⁻1 : ↑⁰1]]]
a⁺ [0 [[↑⁺1 : ↑⁻0]]]
@@ -218,9 +228,6 @@ inc [~(0 z a⁻ a⁺ a⁰)]
++‣ inc
-# adds (+1) to a balanced ternary number and strips leading 0s
-ssinc strip ∘ inc
-
:test ((++(-42)) =? (-41)) (true)
:test ((++(-1)) =? (+0)) (true)
:test ((++(+0)) =? (+1)) (true)
@@ -228,7 +235,7 @@ ssinc strip ∘ inc
:test ((++(+42)) =? (+43)) (true)
# subs (+1) from a balanced ternary number (can introduce leading 0s)
-dec [~(0 z a⁻ a⁺ a⁰)]
+dec [~(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number
z (+0) : (-1)
a⁻ [0 [[↑⁻1 : ↑⁺0]]]
a⁺ [0 [[↑⁺1 : ↑⁰1]]]
@@ -236,9 +243,6 @@ dec [~(0 z a⁻ a⁺ a⁰)]
--‣ dec
-# subs (+1) from a balanced ternary number and strips leading 0s
-sdec strip ∘ dec
-
:test ((--(-42)) =? (-43)) (true)
:test ((--(+0)) =? (-1)) (true)
:test ((--(--(--(--(--(+5)))))) =? (+0)) (true)
@@ -247,7 +251,7 @@ sdec strip ∘ dec
# adds two balanced ternary numbers (can introduce leading 0s)
# second argument gets abstracted (performance)
-add [[abs 1 →^0]]
+add [[abs 1 →^0]] ⧗ Number → Number → Number
abs [c (0 z a⁻ a⁺ a⁰)]
b⁻ [1 ↑⁺(3 0 t⁻) ↑⁰(3 0 t⁰) ↑⁻(3 0 t⁰)]
b⁰ [up 1 (3 0 t⁰)]
@@ -262,9 +266,6 @@ add [[abs 1 →^0]]
…+… add
-# adds two balanced ternary numbers and strips leading 0s
-sadd strip ∘∘ add
-
:test (((-42) + (-1)) =? (-43)) (true)
:test (((-5) + (+6)) =? (+1)) (true)
:test (((-1) + (+0)) =? (-1)) (true)
@@ -274,13 +275,10 @@ sadd strip ∘∘ add
# subs two balanced ternary numbers (can introduce leading 0s)
# second argument gets abstracted (performance)
-sub [[1 + -0]]
+sub [[1 + -0]] ⧗ Number → Number → Number
…-… sub
-# subs two balanced ternary numbers and strips leading 0s
-ssub strip ∘∘ sub
-
:test (((-42) - (-1)) =? (-41)) (true)
:test (((-5) - (+6)) =? (-11)) (true)
:test (((-1) - (+0)) =? (-1)) (true)
@@ -290,7 +288,7 @@ ssub strip ∘∘ sub
# returns true if number is greater than other number
# larger numbers should be second argument (performance)
-gre? [[>?(1 - 0)]]
+gre? [[>?(1 - 0)]] ⧗ Number → Number → Boolean
…>?… gre?
@@ -300,7 +298,7 @@ gre? [[>?(1 - 0)]]
# returns true if number is less than other number
# smaller numbers should be second argument (performance)
-les? \gre?
+les? \gre? ⧗ Number → Number → Boolean
…<?… les?
@@ -310,7 +308,7 @@ les? \gre?
# returns true if number is less than or equal to other number
# smaller numbers should be second argument (performance)
-leq? [[¬(1 >? 0)]]
+leq? [[¬(1 >? 0)]] ⧗ Number → Number → Boolean
…≤?… leq?
@@ -320,7 +318,7 @@ leq? [[¬(1 >? 0)]]
# returns true if number is greater than or equal to other number
# smaller numbers should be second argument (performance)
-geq? \leq?
+geq? \leq? ⧗ Number → Number → Boolean
…≥?… geq?
@@ -329,7 +327,7 @@ geq? \leq?
:test ((+3) ≥? (+2)) (true)
# negates a balanced ternary number if <0
-abs [<?0 -0 0]
+abs [<?0 -0 0] ⧗ Number → Number
|‣ abs
@@ -337,24 +335,31 @@ abs [<?0 -0 0]
:test (|(-1)) ((+1))
:test (|(+42)) ((+42))
+# apply a function n times to a value
+# ~> substitute church numbers
+apply z [[[rec]]] ⧗ Number → (a → a) → a → a
+ rec =?1 case-end case-apply
+ case-apply 0 ∘ (2 --1 0)
+ case-end i
+
+:test (apply (+5) ++‣ (+3)) ((+8))
+
# muls two balanced ternary numbers (can introduce leading 0s)
-mul [[1 z a⁻ a⁺ a⁰]]
+mul [[1 z a⁻ a⁺ a⁰]] ⧗ Number → Number → Number
z (+0)
a⁻ [↑⁰0 - 1]
a⁺ [↑⁰0 + 1]
a⁰ [↑⁰0]
-…*… mul
-
-smul strip ∘∘ mul
+…⋅… mul
-:test (((+42) * (+0)) =? (+0)) (true)
-:test (((-1) * (+42)) =? (-42)) (true)
-:test (((+3) * (+11)) =? (+33)) (true)
-:test (((+42) * (-4)) =? (-168)) (true)
+:test (((+42) ⋅ (+0)) =? (+0)) (true)
+:test (((-1) ⋅ (+42)) =? (-42)) (true)
+:test (((+3) ⋅ (+11)) =? (+33)) (true)
+:test (((+42) ⋅ (-4)) =? (-168)) (true)
# divs a balanced ternary number by three (rshifts least significant trit)
-div³ [~(0 z a⁻ a⁺ a⁰)]
+div³ [~(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number
z (+0) : (+0)
a⁻ [0 [[↑⁻1 : 1]]]
a⁺ [0 [[↑⁺1 : 1]]]
@@ -367,7 +372,7 @@ div³ [~(0 z a⁻ a⁺ a⁰)]
:test (/³(+5)) ((+2))
# divs a balanced ternary number by two (essentially binary >>1)
-div² [z [[[[rec]]]] (+0) 0 0]
+div² [z [[[[rec]]]] (+0) 0 0] ⧗ Number → Number
rec =?1 case-end case-div
case-div 3 /³(2 + 0) /³1 0
case-end 2
@@ -381,7 +386,7 @@ div² [z [[[[rec]]]] (+0) 0 0]
# manually counts how many times a balanced ternary number fits into another one
# TODO: quadratic approximation?
# TODO: fix for negative numbers
-brute-div \[z [[[[[rec]]]]] (+0) 0 0]
+brute-div \[z [[[[[rec]]]]] (+0) 0 0] ⧗ Number → Number → Number
rec (2 >? 0) case-end case-count
case-count 4 ++3 (2 + 1) 1 0
case-end 3
@@ -393,16 +398,20 @@ brute-div \[z [[[[[rec]]]]] (+0) 0 0]
:test ((+4) /! (+5)) ((+0))
# TODO: fix for negative numbers
-brute-mod \[z [[[[[rec]]]]] (+0) 0 0]
+brute-mod \[z [[[[[rec]]]]] (+0) 0 0] ⧗ Number → Number → Number
rec (2 >? 0) case-end case-count
case-count 4 ++3 (2 + 1) 1 0
- case-end 0 - (3 * 1)
+ case-end 0 - (3 ⋅ 1)
…%!… brute-mod
# finds quotient and remainder using long division
# WARNING: don't use; incorrect and slow
-quot-rem [[z [[[[rec]]]] ((+1) : (+0)) 1 0]]
+# TODO: faster algorithm
+# dividend -> divisor -> (quot, rem)
+# 0 divisor, 1 dividend, 2 (quot, rem)
+# align: (quot, divisor)
+quot-rem [[z [[[[rec]]]] ((+1) : (+0)) 1 0]] ⧗ Number → Number → (Pair Number Number)
rec (1 =? 0) case-eq ((1 <? 0) case-les case-div)
case-div calc (z [[[align]]] ^2 0)
align (0 ≤? 4) (1 : 0) (2 ↑⁰1 ↑⁰0)
@@ -413,18 +422,18 @@ quot-rem [[z [[[[rec]]]] ((+1) : (+0)) 1 0]]
# divs two balanced ternary numbers
# WARNING: don't use; incorrect and slow
-div ^‣ ∘∘ quot-rem
+div ^‣ ∘∘ quot-rem ⧗ Number → Number
…/… div
# returns remainder of integer division
# WARNING: don't use; incorrect and slow
-mod ~‣ ∘∘ quot-rem
+mod ~‣ ∘∘ quot-rem ⧗ Number → Number
…%… mod
# returns max number of two
-max [[(1 ≤? 0) 0 1]]
+max [[(1 ≤? 0) 0 1]] ⧗ Number → Number → Number
# returns min number of two
-min [[(1 ≤? 0) 1 0]]
+min [[(1 ≤? 0) 1 0]] ⧗ Number → Number → Number
diff --git a/std/Pair.bruijn b/std/Pair.bruijn
index 7cc93fb..a955fe2 100644
--- a/std/Pair.bruijn
+++ b/std/Pair.bruijn
@@ -3,45 +3,45 @@
:import std/Combinator .
# pairs two expressions into one
-pair [[[0 2 1]]]
+pair [[[0 2 1]]] ⧗ a → b → (Pair a b)
…:… pair
# extracts first expression from pair
-fst [0 k]
+fst [0 k] ⧗ (Pair a b) → a
^‣ fst
:test (^([[0]] : [[1]])) ([[0]])
# extracts second expression from pair
-snd [0 ki]
+snd [0 ki] ⧗ (Pair a b) → b
~‣ snd
:test (~([[0]] : [[1]])) ([[1]])
# applies both elements of a pair to a function
-uncurry [[1 ^0 ~0]]
+uncurry [[1 ^0 ~0]] ⧗ (a → b → c) → (Pair a b) → c
:test (uncurry w ([[0]] : [[1]])) ([[1]])
# applies a function to the pair of two values
-curry [[[2 (1 : 0)]]]
+curry [[[2 (1 : 0)]]] ⧗ ((Pair a b) → c) → a → b → c
:test (curry fst [[0]] [[1]]) ([[0]])
# zips two pairs (basically rotating the elements)
-zip [[(^1 : ^0) : (~1 : ~0)]]
+zip [[(^1 : ^0) : (~1 : ~0)]] ⧗ (Pair a b) → (Pair c d) → (Pair (Pair a c) (Pair b d))
:test (zip ([[0]] : [[[0]]]) ([[1]] : [[[1]]])) (([[0]] : [[1]]) : ([[[0]]] : [[[1]]]))
# applies pairs of two pairs as arguments to a function
-zip-with [[[(2 ^1 ^0) : (2 ~1 ~0)]]]
+zip-with [[[(2 ^1 ^0) : (2 ~1 ~0)]]] ⧗ (a → b → c) → (Pair a b) → (Pair a b) → (Pair c c)
:test (zip-with w ([[0]] : [[[0]]]) ([[1]] : [[[1]]])) ([[1]] : [0])
# swaps the elements of a pair
-swap [~0 : ^0]
+swap [~0 : ^0] ⧗ (Pair a b) → (Pair b a)
:test (swap ([[0]] : [[1]])) ([[1]] : [[0]])
diff --git a/std/String.bruijn b/std/String.bruijn
index bc80840..a288bac 100644
--- a/std/String.bruijn
+++ b/std/String.bruijn
@@ -28,16 +28,12 @@ ni? \in?
# splits string by newline character
lines z [[rec]]
- rec <>?(~broken) (^broken : empty) (^broken : (1 ~(~broken)))
+ rec ∅?(~broken) (^broken : empty) (^broken : (1 ~(~broken)))
broken break (B.eq? '\n') 0
:test (lines "ab\ncd") ("ab" : ("cd" : empty))
-# :test (lines "ab\ncd\n") ("ab" : ("cd" : empty))
-
# concats list of strings with newline character
-unlines concat-map (\(;) '\n')
+unlines concat-map (\(…;…) '\n')
:test (unlines ("ab" : ("cd" : empty))) ("ab\ncd\n")
-
-main lines "ab\ncd"
--
cgit v1.2.3