aboutsummaryrefslogtreecommitdiffhomepage
path: root/std/Number
diff options
context:
space:
mode:
authorMarvin Borner2024-03-02 16:13:20 +0100
committerMarvin Borner2024-03-02 16:13:20 +0100
commit46cc8f5b0da07d8c7cb354c7b7a281b8d0f3d7bf (patch)
tree83bd64ca498117fddf94f9271f1327081b1e0018 /std/Number
parenteff903fc61b060b6333cb60bfced95e44da000ba (diff)
Several additions to std
Some weren't committed for a year!
Diffstat (limited to 'std/Number')
-rw-r--r--std/Number/Binary.bruijn83
-rw-r--r--std/Number/Bruijn.bruijn23
-rw-r--r--std/Number/Conversion.bruijn10
3 files changed, 116 insertions, 0 deletions
diff --git a/std/Number/Binary.bruijn b/std/Number/Binary.bruijn
index 648af29..fcbe264 100644
--- a/std/Number/Binary.bruijn
+++ b/std/Number/Binary.bruijn
@@ -6,6 +6,11 @@
:import std/List .
:import std/Logic .
+# TODO: remove ternary conversion shortcuts
+# TODO: then move functions to reflect order of std/Ternary
+
+:import std/Number/Ternary T
+
# bit indicating a one, compatible with std/Logic
b¹ true ⧗ Bit
@@ -252,6 +257,17 @@ sub [[(0 =? 1) (+0b) -((pad 1 0) + -(pad 0 1))]] ⧗ Binary → Binary → Binar
:test ((+3b) - (+0b) =? (+3b)) (true)
:test ((+3b) - (+2b) =? (+1b)) (true)
+# muls two binary numbers (can introduce leading 0s)
+mul [[1 z a¹ a⁰]] ⧗ Number → Number → Number
+ z (+0b)
+ a¹ [↑⁰0 + 1]
+ a⁰ [↑⁰0]
+
+…⋅… mul
+
+:test ((+42b) ⋅ (+0b) =? (+0b)) (true)
+:test ((+3b) ⋅ (+11b) =? (+33b)) (true)
+
# rshifts least significant bit of a binary number
div² [~(0 z a¹ a⁰)] ⧗ Binary → Binary
z (+0b) : (+0b)
@@ -282,3 +298,70 @@ odd? lsb ⧗ Binary → Boolean
:test (odd? (+1b)) (true)
:test (odd? (+41b)) (true)
:test (odd? (+42b)) (false)
+
+# TODO: Remove (duplicate of std/Conversion because of dep loop)
+binary→ternary [y [[[rec]]] [0] 0 (+0t)] ⧗ Binary → Ternary
+ rec zero? 0 case-end case-rec
+ case-rec odd? 0 (2 (1 ∘ T.inc) (dec 0)) (2 (1 ∘ (T.mul (+2t))) (div² 0))
+ case-end 1
+
+# returns true if number is greater than other number
+# TODO: remove ternary conversion
+gre? T.gre? ⋔ binary→ternary ⧗ Binary → Binary → Boolean
+
+…>?… gre?
+
+:test ((+1b) >? (+2b)) (false)
+:test ((+2b) >? (+2b)) (false)
+:test ((+3b) >? (+2b)) (true)
+
+# returns true if number is less than other number
+les? \gre? ⧗ Binary → Binary → Boolean
+
+…<?… les?
+
+:test ((+1b) <? (+2b)) (true)
+:test ((+2b) <? (+2b)) (false)
+:test ((+3b) <? (+2b)) (false)
+
+# returns true if number is less than or equal to other number
+leq? not! ∘∘ gre? ⧗ Binary → Binary → Boolean
+
+…≤?… leq?
+
+:test ((+1b) ≤? (+2b)) (true)
+:test ((+2b) ≤? (+2b)) (true)
+:test ((+3b) ≤? (+2b)) (false)
+
+# returns true if number is greater than or equal to other number
+geq? \leq? ⧗ Binary → Binary → Boolean
+
+…≥?… geq?
+
+:test ((+1b) ≥? (+2b)) (false)
+:test ((+2b) ≥? (+2b)) (true)
+:test ((+3b) ≥? (+2b)) (true)
+
+# returns eq, lt, gt depending on comparison of two numbers
+# TODO: remove ternary conversion
+compare-case [[[(T.compare-case 2 1 0) ⋔ binary→ternary]]] ⧗ a → b → c → Binary → Binary → d
+
+# returns 1 if a>b, -1 if a<b and 0 if a=b
+# also: spaceship operator
+compare compare-case (+0) (+1) (-1) ⧗ Binary → Binary → Binary
+
+:test (compare (+2b) (+2b)) ((+0))
+:test (compare (+2b) (+1b)) ((+1))
+:test (compare (+1b) (+2b)) ((-1))
+
+…<=>… compare
+
+# returns max number of two
+max [[(1 ≤? 0) 0 1]] ⧗ Binary → Binary → Binary
+
+:test (max (+5b) (+2b)) ((+5b))
+
+# returns min number of two
+min [[(1 ≤? 0) 1 0]] ⧗ Binary → Binary → Binary
+
+:test (min (+5b) (+2b)) ((+2b))
diff --git a/std/Number/Bruijn.bruijn b/std/Number/Bruijn.bruijn
new file mode 100644
index 0000000..744d9a1
--- /dev/null
+++ b/std/Number/Bruijn.bruijn
@@ -0,0 +1,23 @@
+# MIT License, Copyright (c) 2023 Marvin Borner
+# De Bruijn numeral system (named by me)
+# proof that this numeral system does not support zero/eq/sub/etc. is in
+# Wadsworth, Christopher. "Some unusual λ-calculus numeral systems."
+# very sad indeed
+
+:import std/Combinator .
+
+# increments De Bruijn numeral
+inc [[[2 1]]]
+
+++‣ inc
+
+:test (++(+0d)) ((+1d))
+:test (++(+5d)) ((+6d))
+
+# decrements De Bruijn numeral
+dec [[1 0 0]]
+
+--‣ dec
+
+:test (--(+1d)) ((+0d))
+:test (--(+5d)) ((+4d))
diff --git a/std/Number/Conversion.bruijn b/std/Number/Conversion.bruijn
index c79e53f..0057310 100644
--- a/std/Number/Conversion.bruijn
+++ b/std/Number/Conversion.bruijn
@@ -27,3 +27,13 @@ binary→ternary [y [[[rec]]] [0] 0 (+0t)] ⧗ Binary → Ternary
:test (T.eq? (binary→ternary (+0b)) (+0t)) ([[1]])
:test (T.eq? (binary→ternary (+42b)) (+42t)) ([[1]])
+
+# converts numbers to binary
+# constructs reversed path of composed functions and applies to ternary
+ternary→binary [y [[[rec]]] [0] 0 (+0b)] ⧗ Ternary → Binary
+ rec T.zero? 0 case-end case-rec
+ case-rec T.odd? 0 (2 (1 ∘ B.inc) (T.dec 0)) (2 (1 ∘ (B.mul (+2b))) (T.div² 0))
+ case-end 1
+
+:test (B.eq? (ternary→binary (+0t)) (+0b)) ([[1]])
+:test (B.eq? (ternary→binary (+42t)) (+42b)) ([[1]])