aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorMarvin Borner2023-02-23 14:25:27 +0100
committerMarvin Borner2023-02-23 14:25:27 +0100
commite8456ff880c5aa72171183e0b0043ca731a086fa (patch)
tree114924bedf3f3e10a50467ac724cf55c817ca6d4
parentc11a39217ac9e0a166442a634692114343a484ee (diff)
Additions to standard library
Mainly new binary encoding and corresponding functions
-rw-r--r--std/Binary.bruijn238
-rw-r--r--std/Byte.bruijn24
-rw-r--r--std/Church.bruijn25
-rw-r--r--std/Combinator.bruijn2
-rw-r--r--std/Number.bruijn43
-rw-r--r--std/String.bruijn2
-rw-r--r--std/Unary.bruijn57
7 files changed, 321 insertions, 70 deletions
diff --git a/std/Binary.bruijn b/std/Binary.bruijn
new file mode 100644
index 0000000..9fd95da
--- /dev/null
+++ b/std/Binary.bruijn
@@ -0,0 +1,238 @@
+# MIT License, Copyright (c) 2023 Marvin Borner
+# TODO: Use abstract representation for logic instead of listifying
+
+:import std/Combinator .
+:import std/List .
+:import std/Logic .
+
+# bit indicating a one, compatible with std/Logic
+b¹ true ⧗ Bit
+
+# bit indicating a zero, compatible with std/Logic
+b⁰ false ⧗ Bit
+
+# returns true if a bit is set
+b¹? i ⧗ Bit → Boolean
+
+:test (b¹? b¹) (true)
+:test (b¹? b⁰) (false)
+
+# returns true if a bit is unset
+b⁰? not! ⧗ Bit → Boolean
+
+:test (b⁰? b⁰) (true)
+:test (b⁰? b¹) (false)
+
+# shifts a one into a binary number
+↑¹‣ [[[[1 (3 2 1 0)]]]] ⧗ Binary → Binary
+
+:test (↑¹[[[0 2]]]) ([[[1 (0 2)]]])
+
+# shifts a zero into a binary number
+↑⁰‣ [[[[0 (3 2 1 0)]]]] ⧗ Binary → Binary
+
+:test (↑⁰(+1b)) ((+2b))
+
+# shifts a specified bit into a binary number
+up [[[[[4 1 0 (3 2 1 0)]]]]] ⧗ Bit → Binary → Binary
+
+:test (up b¹ [[[0 2]]]) ([[[1 (0 2)]]])
+:test (up b⁰ (+1b)) ((+2b))
+
+# converts a binary number to a list of bits
+list! [0 z a¹ a⁰] ⧗ Binary → (List Bit)
+ z empty
+ a¹ [b¹ : 0]
+ a⁰ [b⁰ : 0]
+
+:test (list! (+0b)) (empty)
+:test (list! (+6b)) (b⁰ : (b¹ : (b¹ : empty)))
+
+# converts a list of bits to a binary number
+binary! foldr up (+0b) ⧗ (List Bit) → Binary
+
+:test (binary! (list! (+0b))) ((+0b))
+:test (binary! (list! (+42b))) ((+42b))
+
+# 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]]]
+
+%‣ strip
+
+:test (%[[[0 2]]]) ((+0b))
+:test (%[[[1 (0 (0 (0 (0 2))))]]]) ((+1b))
+:test (%(+2b)) ((+2b))
+
+# returns true if a binary number is zero
+zero? [0 true [false] i] ⧗ Binary → Boolean
+
+=?‣ zero?
+
+:test (=?(+0b)) (true)
+:test (=?[[[0 (0 2)]]]) (true)
+:test (=?(+1b)) (false)
+
+# extracts least significant bit from a binary number
+lst [0 b⁰ [b¹] [b⁰]] ⧗ Binary → Bit
+
+:test (lst (+0b)) (b⁰)
+:test (lst (+1b)) (b¹)
+:test (lst (+42b)) (b⁰)
+
+# extracts most significant bit from a binary number
+# not really useful for binary numbers, but part of interface
+mst [=?0 b⁰ ^(<~>(list! %0))] ⧗ Binary → Bit
+
+:test (mst (+0b)) (b⁰)
+:test (mst (+1b)) (b¹)
+:test (mst (+42b)) (b¹)
+
+# extracts nth bit from a binary number
+nth …!!… ∘ list! ⧗ Binary → Number → Bit
+
+# logical and on two binary numbers
+and! binary! ∘∘ (ψ* zip-with …⋀?… list!) ⧗ Binary → Binary → Binary
+
+…⋀!… and!
+
+:test (and! (+1b) (+0b)) ((+0b))
+:test (and! (+5b) (+4b)) ((+4b))
+:test (and! (+10b) (+12b)) ((+8b))
+
+# logical or on two binary numbers
+# TODO: Fix for numbers with different length (→ zero padding?)
+or! binary! ∘∘ (ψ* zip-with …⋁?… list!) ⧗ Binary → Binary → Binary
+
+…⋁!… or!
+
+:test (or! (+10b) (+12b)) ((+14b))
+
+# :test (or! (+1b) (+0b)) ((+1b))
+# :test (or! (+5b) (+3b)) ((+7b))
+
+# converts the normal binary representation into abstract
+abstract! [0 z a¹ a⁰] ⧗ Binary → AbstractBinary
+ z (+0b)
+ a¹ [[[[1 3]]]]
+ a⁰ [[[[0 3]]]]
+
+→^‣ abstract!
+
+# converts the abstracted binary representation back to normal
+normal! ω [[0 z a¹ a⁰]] ⧗ AbstractBinary → Binary
+ z (+0b)
+ a¹ [↑¹([3 3 0] 0)]
+ a⁰ [↑⁰([3 3 0] 0)]
+
+→_‣ normal!
+
+# returns true if two binary numbers are equal
+# → ignores leading 0s!
+# also: ⋀?‣ ∘∘ (ψ* zip-with xnor? list!)
+eq? [[abs 1 →^0]] ⧗ Binary → Binary → Boolean
+ abs [0 z a¹ a⁰]
+ z [=?(→_0)]
+ a¹ [[0 false [2 0] [false]]]
+ a⁰ [[0 (1 0) [false] [2 0]]]
+
+…=?… eq?
+
+:test ((+0b) =? (+0b)) (true)
+:test ([[[1 (0 2)]]] =? [[[1 (0 2)]]]) (true)
+:test ([[[1 (0 2)]]] =? (+2b)) (false)
+
+# returns true if two binary numbers are not equal
+not-eq? not! ∘∘ eq? ⧗ Binary → Binary → Boolean
+
+…≠?… not-eq?
+
+:test ((+0b) ≠? (+0b)) (false)
+:test ([[[1 (0 2)]]] ≠? [[[1 (0 2)]]]) (false)
+:test ([[[1 (0 2)]]] ≠? (+2b)) (true)
+
+# 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]]]
+
+++‣ inc
+
+:test (++(+0b)) ((+1b))
+:test (++(+2b)) ((+3b))
+
+# 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]]]
+
+--‣ dec
+
+:test (--(+0b)) ((+0b))
+:test (--(+1b)) ([[[0 2]]])
+:test (--(+3b)) ((+2b))
+
+# adds two binary numbers (can introduce leading 0s)
+# second argument gets abstracted (performance)
+add [[abs 1 →^0]] ⧗ Binary → Binary → Binary
+ abs [c (0 z a¹ a⁰)]
+ c¹ [1 ↑⁰(3 0 b¹) ↑¹(3 0 b⁰)]
+ a¹ [[[1 (c¹ 1) c¹' c¹]]]
+ c¹' [up 1 (3 0 b¹)]
+ a⁰ [[[1 (c⁰ 1) c¹ c⁰]]]
+ c⁰ [up 1 (3 0 b⁰)]
+ z [[0 ++(→_1) →_1]]
+ c [[1 0 b⁰]]
+
+…+… add
+
+:test (((+0b) + (+0b)) =? (+0b)) (true)
+:test (((+0b) + (+3b)) =? (+3b)) (true)
+:test (((+1b) + (+2b)) =? (+3b)) (true)
+:test (((+42b) + (+1b)) =? (+43b)) (true)
+
+# subs two binary numbers (can introduce leading 0s)
+# second argument gets abstracted (performance)
+sub [[abs 1 →^0]] ⧗ Binary → Binary → Binary
+ abs [c (0 z a¹ a⁰)]
+ a¹ [[[1 (c¹ 1) c¹' c¹]]]
+ c¹ [1 ↑⁰(3 0 b¹) ↑¹(3 0 b⁰)]
+ c¹' [1 ↑¹(3 0 b⁰) ↑¹(3 0 b⁰)]
+ a⁰ [[[1 (c⁰ 1) c⁰' c⁰]]]
+ c⁰ [1 ↑¹(3 0 b⁰) ↑⁰(3 0 b⁰)]
+ c⁰' [1 (3 0 b⁰) ↑¹(3 0 b¹)]
+ z [[0 --(→_1) →_1]]
+ c [[1 0 b⁰]]
+
+…-… sub
+
+:test ((+5b) - (+0b)) ((+5b))
+:test ((+8b) - (+3b)) ((+5b))
+:test ((+10b) - (+5b)) ((+5b))
+:test (((+20b) - (+1b))) ((+19b))
+
+# :test (%((+20b) - (+0b))) ((+20b))
+# :test (%((+20b) - (+1b))) ((+19b))
+# :test (%((+19b) - (+1b))) ((+18b))
+# :test (%((+19b) - (+2b))) ((+17b))
+# :test (%((+18b) - (+2b))) ((+16b))
+# :test (%((+18b) - (+3b))) ((+15b))
+# :test (%((+17b) - (+3b))) ((+14b))
+# :test (%((+17b) - (+4b))) ((+13b))
+# :test (%((+16b) - (+4b))) ((+12b))
+# :test (%((+16b) - (+5b))) ((+11b))
+# :test (%((+15b) - (+5b))) ((+10b))
+# :test (%((+15b) - (+6b))) ((+9b))
+# :test (%((+14b) - (+6b))) ((+8b))
+# :test (%((+14b) - (+7b))) ((+7b))
+# :test (%((+13b) - (+7b))) ((+6b))
+# :test (%((+13b) - (+8b))) ((+5b))
+# :test (%((+12b) - (+8b))) ((+4b))
+# :test (%((+12b) - (+9b))) ((+3b))
+# :test (%((+11b) - (+9b))) ((+2b))
+# :test (%((+11b) - (+10b))) ((+1b))
+# :test (%((+10b) - (+10b))) ((+0b))
diff --git a/std/Byte.bruijn b/std/Byte.bruijn
deleted file mode 100644
index 8dcbb7b..0000000
--- a/std/Byte.bruijn
+++ /dev/null
@@ -1,24 +0,0 @@
-# MIT License, Copyright (c) 2022 Marvin Borner
-
-:import std/Logic .
-:import std/Combinator .
-:import std/List .
-
-# bit 0
-b0 false
-
-# bit 1
-b1 true
-
-# returns true if two bytes are equal
-eq? ⋀?‣ ∘∘ (zip-with xnor?)
-
-…=?… eq?
-
-:test ('a' =? 'a') (true)
-:test ('a' =? 'b') (false)
-
-# generates a byte with correct endianness
-byte [[[[[[[[0 : (1 : (2 : (3 : (4 : (5 : (6 : (7 : empty)))))))]]]]]]]]
-
-:test (byte b0 b1 b1 b0 b0 b0 b0 b1) ('a')
diff --git a/std/Church.bruijn b/std/Church.bruijn
deleted file mode 100644
index 9e567b0..0000000
--- a/std/Church.bruijn
+++ /dev/null
@@ -1,25 +0,0 @@
-# MIT License, Copyright (c) 2022 Marvin Borner
-
-zero [[0]]
-
-zero? [0 [[[0]]] [[1]]]
-
-dec [[[2 [[0 (1 3)]] [1] [0]]]]
-
---‣ dec
-
-inc [[[1 (2 1 0)]]]
-
-++‣ inc
-
-add [[[[3 1 (2 1 0)]]]]
-
-…+… add
-
-mul [[[2 (1 0)]]]
-
-…⋅… mul
-
-exp [[0 1]]
-
-…^… exp
diff --git a/std/Combinator.bruijn b/std/Combinator.bruijn
index 4529853..9cafbce 100644
--- a/std/Combinator.bruijn
+++ b/std/Combinator.bruijn
@@ -115,6 +115,8 @@ o [[0 (1 0)]] ⧗ ((a → b) → a) → (a → b) → b
# psi combinator: on
ψ [[[[3 (2 1) (2 0)]]]] ⧗ (b → b → c) → (a → b) → a → a → c
+ψ* [[[[[4 3 (2 1) (2 0)]]]]] ⧗ (c → b → b → d) → c → (a → b) → a → a → d
+
# queer bird combinator: reverse function composition: (f , g) x = g (f x)
q [[[1 (2 0)]]] ⧗ (a → b) → (b → c) → a → c
diff --git a/std/Number.bruijn b/std/Number.bruijn
index 3a2efe9..f1f4432 100644
--- a/std/Number.bruijn
+++ b/std/Number.bruijn
@@ -4,33 +4,35 @@
# Heavily inspired by the works of T.Æ. Mogensen and Douglas W. Jones (see refs in README)
:import std/Combinator .
-:import std/Pair .
:import std/Logic .
+:import std/Pair .
# negative trit indicating coeffecient of (-1)
t⁻ [[[2]]] ⧗ Trit
-# returns true if a trit is negative
-t⁻? [0 true false false] ⧗ Trit → Boolean
-
# positive trit indicating coeffecient of (+1)
t⁺ [[[1]]] ⧗ Trit
-# returns true if a trit is positive
-t⁺? [0 false true false] ⧗ Trit → Boolean
-
# zero trit indicating coeffecient of 0
t⁰ [[[0]]] ⧗ Trit
-# returns true if a trit is zero
-t⁰? [0 false false true] ⧗ Trit → Boolean
+# returns true if a trit is negative
+t⁻? [0 true false false] ⧗ Trit → Boolean
:test (t⁻? t⁻) (true)
:test (t⁻? t⁺) (false)
:test (t⁻? t⁰) (false)
+
+# returns true if a trit is positive
+t⁺? [0 false true false] ⧗ Trit → Boolean
+
:test (t⁺? t⁻) (false)
:test (t⁺? t⁺) (true)
:test (t⁺? t⁰) (false)
+
+# returns true if a trit is zero
+t⁰? [0 false false true] ⧗ Trit → Boolean
+
:test (t⁰? t⁻) (false)
:test (t⁰? t⁺) (false)
:test (t⁰? t⁰) (true)
@@ -85,7 +87,7 @@ list! [0 z a⁻ a⁺ a⁰] ⧗ Number → List
# TODO: Tests!
-# strips leading 0s from balanced ternary number
+# strips leading 0s from a balanced ternary number
strip [^(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number
z (+0) : true
a⁻ [0 [[↑⁻1 : false]]]
@@ -98,14 +100,6 @@ strip [^(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number
:test (%[[[[2 (0 (0 (0 (0 3))))]]]]) ((-1))
:test (%(+42)) ((+42))
-# extracts least significant trit from balanced ternary numbers
-lst [0 t⁰ [t⁻] [t⁺] [t⁰]] ⧗ Number → Trit
-
-:test (lst (-1)) (t⁻)
-:test (lst (+0)) (t⁰)
-:test (lst (+1)) (t⁺)
-:test (lst (+42)) (t⁰)
-
# returns true if balanced ternary number is zero
zero? [0 true [false] [false] i] ⧗ Number → Boolean
@@ -126,10 +120,19 @@ not-zero? [0 false [true] [true] i] ⧗ Number → Boolean
:test (≠?(+1)) (true)
:test (≠?(+42)) (true)
-# extracts most significant trit from balanced ternary numbers
+# extracts least significant trit from a balanced ternary number
+lst [0 t⁰ [t⁻] [t⁺] [t⁰]] ⧗ Number → Trit
+
+:test (lst (-1)) (t⁻)
+:test (lst (+0)) (t⁰)
+:test (lst (+1)) (t⁺)
+:test (lst (+42)) (t⁰)
+
+# extracts most significant trit from a balanced ternary number
# <~>/<>? 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
+# (or better solution in general)
mst [=?0 t⁰ ^(<~>(list! %0))] ⧗ Number → Trit
<~>‣ z [[[[<>?0 1 (3 2 (2 1 ^0) ~0)]]]] f false
<>?‣ [0 [[[false]]] true]
@@ -188,7 +191,6 @@ normal! ω [[0 z a⁻ a⁺ a⁰]] ⧗ AbstractNumber → Number
:test (→_(→^(-42))) ((-42))
# returns true if two balanced ternary numbers are equal
-# larger numbers should be second argument (performance)
# → ignores leading 0s!
eq? [[abs 1 →^0]] ⧗ Number → Number → Boolean
abs [0 z a⁻ a⁺ a⁰]
@@ -199,6 +201,7 @@ eq? [[abs 1 →^0]] ⧗ Number → Number → Boolean
…=?… eq?
+# returns true if two balanced ternary numbers are not equal
not-eq? not! ∘∘ eq? ⧗ Number → Number → Boolean
…≠?… not-eq?
diff --git a/std/String.bruijn b/std/String.bruijn
index a288bac..d09dd26 100644
--- a/std/String.bruijn
+++ b/std/String.bruijn
@@ -1,6 +1,6 @@
# MIT License, Copyright (c) 2022 Marvin Borner
-:import std/Byte B
+:import std/Binary B
:input std/List
diff --git a/std/Unary.bruijn b/std/Unary.bruijn
new file mode 100644
index 0000000..cf72e3b
--- /dev/null
+++ b/std/Unary.bruijn
@@ -0,0 +1,57 @@
+# MIT License, Copyright (c) 2022 Marvin Borner
+# classic Church style numerals
+
+:import std/Logic .
+
+zero [[0]]
+
+# returns true if a unary number is zero
+zero? [0 [[[0]]] [[1]]] ⧗ Unary → Boolean
+
+=?‣ zero?
+
+:test (=?(+0u)) (true)
+:test (=?(+42u)) (false)
+
+# adds 1 to a unary number
+inc [[[1 (2 1 0)]]] ⧗ Unary → Unary
+
+++‣ inc
+
+:test (++(+0u)) ((+1u))
+:test (++(+1u)) ((+2u))
+:test (++(+42u)) ((+43u))
+
+# subs 1 from a unary number
+dec [[[2 [[0 (1 3)]] [1] [0]]]] ⧗ Unary → Unary
+
+--‣ dec
+
+:test (--(+0u)) ((+0u))
+:test (--(+1u)) ((+0u))
+:test (--(+42u)) ((+41u))
+
+# adds two unary numbers
+add [[[[3 1 (2 1 0)]]]] ⧗ Unary → Unary → Unary
+
+…+… add
+
+:test ((+0u) + (+2u)) ((+2u))
+:test ((+5u) + (+3u)) ((+8u))
+
+# muls two unary numbers
+mul [[[2 (1 0)]]] ⧗ Unary → Unary → Unary
+
+…⋅… mul
+
+:test ((+0u) ⋅ (+2u)) ((+0u))
+:test ((+2u) ⋅ (+3u)) ((+6u))
+
+# exponentiates two unary numbers
+# gives 1 if exponent is 0
+exp [[0 1]] ⧗ Unary → Unary → Unary
+
+…^… exp
+
+:test ((+1u) ^ (+0u)) ((+1u))
+:test ((+2u) ^ (+3u)) ((+8u))