path: root/std/Number.bruijn

# MIT License, Copyright (c) 2022 Marvin Borner
# According to works of T.Æ. Mogensen

:import std/Combinator .

:import std/Pair .

:import std/List

:import std/Logic .

# negative trit indicating coeffecient of -1
trit-neg [[[2]]]

# returns whether a trit is negative
trit-neg? [0 T F F]

# positive trit indicating coeffecient of +1
trit-pos [[[1]]]

# returns whether a trit is positive
trit-pos? [0 F T F]

# zero trit indicating coeffecient of 0
trit-zero [[[0]]]

# returns whether a trit is zero
trit-zero? [0 F F T]

:test trit-neg? trit-neg = T
:test trit-neg? trit-pos = F
:test trit-neg? trit-zero = F
:test trit-pos? trit-neg = F
:test trit-pos? trit-pos = T
:test trit-pos? trit-zero = F
:test trit-zero? trit-neg = F
:test trit-zero? trit-pos = F
:test trit-zero? trit-zero = T

# shifts a negative trit into a balanced ternary number
up-neg [[[[[2 (4 3 2 1 0)]]]]]

:test up-neg +0 = -1
:test up-neg -1 = -4
:test up-neg +42 = +125

# shifts a positive trit into a balanced ternary number
up-pos [[[[[1 (4 3 2 1 0)]]]]]

:test up-pos +0 = +1
:test up-pos -1 = -2
:test up-pos +42 = +127

# shifts a zero trit into a balanced ternary number
up-zero [[[[[0 (4 3 2 1 0)]]]]]

:test up-zero +0 = [[[[0 3]]]]
:test up-zero +1 = +3
:test up-zero +42 = +126

# shifts a specified trit into a balanced ternary number
up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]

:test up trit-neg +42 = up-neg +42
:test up trit-pos +42 = up-pos +42
:test up trit-zero +42 = up-zero +42

# shifts the least significant trit out - basically div by 3
down [snd (0 z neg pos zero)]
	z pair +0 +0
	neg [0 [[pair (up-neg 1) 1]]]
	pos [0 [[pair (up-pos 1) 1]]]
	zero [0 [[pair (up-zero 1) 1]]]

# extracts least significant trit from balanced ternary numbers
lst [0 trit-zero [trit-neg] [trit-pos] [trit-zero]]

:test lst +0 = trit-zero
:test lst -1 = trit-neg
:test lst +1 = trit-pos
:test lst +42 = trit-zero

# negates a balanced ternary number
negate [[[[[4 3 1 2 0]]]]]

:test negate +0 = +0
:test negate -1 = +1
:test negate +42 = -42

# converts a balanced ternary number to a list of trits
list! [0 z neg pos zero]
	z List.empty
	neg [[pair trit-neg 1]]
	pos [[pair trit-pos 1]]
	zero [[pair trit-zero 1]]

# TODO: Tests!

# strips leading 0s from balanced ternary number
strip [fst (0 z neg pos zero)]
	z pair +0 T
	neg [0 [[pair (up-neg 1) F]]]
	pos [0 [[pair (up-pos 1) F]]]
	zero [0 [[pair (0 +0 (up-zero 1)) 0]]]

:test strip [[[[0 3]]]] = +0
:test strip [[[[2 (0 (0 (0 (0 3))))]]]] = -1
:test strip +42 = +42

# extracts most significant trit from balanced ternary numbers
# TODO: Find a more elegant way to do this
mst [fix (List.last (list! (strip 0)))]
	fix [if (or (trit-neg? 0) (or (trit-pos? 0) (trit-zero? 0))) 0 [[0]]]

:test mst +0 = trit-zero
:test mst -1 = trit-neg
:test mst +1 = trit-pos
:test mst +42 = trit-pos

# returns whether balanced ternary number is negative
negative? [trit-neg? (mst 0)]

:test negative? +0 = F
:test negative? -1 = T
:test negative? +1 = F
:test negative? +42 = F

# returns whether balanced ternary number is positive
positive? [trit-pos? (mst 0)]

:test positive? +0 = F
:test positive? -1 = F
:test positive? +1 = T
:test positive? +42 = T

# checks whether balanced ternary number is zero
zero? [0 T [F] [F] I]

:test zero? +0 = T
:test zero? -1 = F
:test zero? +1 = F
:test zero? +42 = F

# converts the normal balanced ternary representation into abstract
# -> the abstract representation is used in add/sub/mul
abstract! [0 z neg pos zero]
	z +0
	neg [[[[[2 4]]]]]
	pos [[[[[1 4]]]]]
	zero [[[[[0 4]]]]]

:test abstract! -3 = [[[[0 [[[[2 [[[[3]]]]]]]]]]]]
:test abstract! +0 = [[[[3]]]]
:test abstract! +3 = [[[[0 [[[[1 [[[[3]]]]]]]]]]]]

# converts the abstracted balanced ternary representation back to normal
# using ω to solve recursion
normal! ω rec
	rec [[0 +0 [up-neg ([3 3 0] 0)] [up-pos ([3 3 0] 0)] [up-zero ([3 3 0] 0)]]]

:test normal! [[[[3]]]] = +0
:test normal! (abstract! +42) = +42
:test normal! (abstract! -42) = -42

# checks whether two balanced ternary numbers are equal
# -> removes leading 0s!
eq? [[abs 1 (abstract! 0)]]
	z [zero? (normal! 0)]
	neg [[0 F [2 0] [F] [F]]]
	pos [[0 F [F] [2 0] [F]]]
	zero [[0 (1 0) [F] [F] [2 0]]]
	abs [0 z neg pos zero]

:test eq? -42 -42 = T
:test eq? -1 -1 = T
:test eq? -1 +0 = F
:test eq? +0 +0 = T
:test eq? +1 +0 = F
:test eq? +1 +1 = T
:test eq? +42 +42 = T
:test eq? [[[[(1 (0 (0 (0 (0 3)))))]]]] +1 = T

# 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
# +/0 in comparison to their implementation, yet the order of neg/pos/zero is
# the same. Something's weird.

# adds +1 to a balanced ternary number (can introduce leading 0s)
inc [snd (0 z neg pos zero)]
	z pair +0 +1
	neg [0 [[pair (up-neg 1) (up-zero 1)]]]
	zero [0 [[pair (up-zero 1) (up-pos 1)]]]
	pos [0 [[pair (up-pos 1) (up-neg 0)]]]

sinc [strip (inc 0)]

:test eq? (inc -42) -41 = T
:test eq? (inc -1) +0 = T
:test eq? (inc +0) +1 = T
:test eq? (inc (inc (inc (inc (inc +0))))) +5 = T
:test eq? (inc +42) +43 = T

# subs +1 from a balanced ternary number (can introduce leading 0s)
dec [snd (0 dec-z dec-neg dec-pos dec-zero)]
	dec-z pair +0 -1
	dec-neg [0 [[pair (up-neg 1) (up-pos 0)]]]
	dec-zero [0 [[pair (up-zero 1) (up-neg 1)]]]
	dec-pos [0 [[pair (up-pos 1) (up-zero 1)]]]

sdec [strip (dec 0)]

:test eq? (dec -42) -43 = T
:test eq? (dec +0) -1 = T
:test eq? (dec (dec (dec (dec (dec +5))))) +0 = T
:test eq? (dec +1) +0 = T
:test eq? (dec +42) +41 = T

# adds two balanced ternary numbers (can introduce leading 0s)
add [[abs 1 (abstract! 0)]]
	c [[1 0 trit-zero]]
	b-neg2 [1 (up-zero (3 0 trit-neg)) (up-neg (3 0 trit-zero)) (up-pos (3 0 trit-neg))]
	b-neg [1 (up-pos (3 0 trit-neg)) (up-zero (3 0 trit-zero)) (up-neg (3 0 trit-zero))]
	b-zero [up 1 (3 0 trit-zero)]
	b-pos [1 (up-zero (3 0 trit-zero)) (up-neg (3 0 trit-pos)) (up-pos (3 0 trit-zero))]
	b-pos2 [1 (up-pos (3 0 trit-zero)) (up-zero (3 0 trit-pos)) (up-neg (3 0 trit-pos))]
	a-neg [[[1 (b-neg 1) b-neg2 b-zero b-neg]]]
	a-pos [[[1 (b-pos 1) b-zero b-pos2 b-pos]]]
	a-zero [[[1 (b-zero 1) b-neg b-pos b-zero]]]
	z [[0 (dec (normal! 1)) (inc (normal! 1)) (normal! 1)]]
	abs [c (0 z a-neg a-pos a-zero)]

sadd [[strip (add 1 0)]]

:test eq? (add -42 -1) -43 = T
:test eq? (add -5 +6) +1 = T
:test eq? (add -1 +0) -1 = T
:test eq? (add +0 +0) +0 = T
:test eq? (add +1 +2) +3 = T
:test eq? (add +42 +1) +43 = T

# subs two balanced ternary numbers (can introduce leading 0s)
sub [[add 1 (negate 0)]]

ssub [[strip (sub 1 0)]]

:test eq? (sub -42 -1) -41 = T
:test eq? (sub -5 +6) -11 = T
:test eq? (sub -1 +0) -1 = T
:test eq? (sub +0 +0) +0 = T
:test eq? (sub +1 +2) -1 = T
:test eq? (sub +42 +1) +41 = T

# returns whether number is greater than other number
gre? [[negative? (sub 0 1)]]

# returns whether number is less than or equal to other number
leq? [[not (gre? 1 0)]]

:test List.sort leq? gre? (List.append +1 (List.append +4 (List.append +3 (List.append +0 List.empty)))) = List.append +0 (List.append +1 (List.append +3 (List.append +4 List.empty)))

# muls two balanced ternary numbers (can introduce leading 0s)
mul [[1 +0 neg pos zero]]
	neg [sub (up-zero 0) 1]
	pos [add (up-zero 0) 1]
	zero [up-zero 0]

smul [[strip (mul 1 0)]]

:test eq? (mul +42 +0) +0 = T
:test eq? (mul -1 +42) -42 = T
:test eq? (mul +3 +11) +33 = T
:test eq? (mul +42 -4) -168 = T