Obviously trivial

7 files changed, 215 insertions, 74 deletions

diff --git a/README.md b/README.md
index fad19b4..bafc272 100644
--- a/README.md
+++ b/README.md
@@ -147,7 +147,7 @@ Plain execution without any predefined functions:
 
 Using standard library:
 
-    :import std/Boolean .
+    :import std/Logic .
     :import std/Combinator .
     :import std/Number .
     :import std/Option .
diff --git a/bruijn.cabal b/bruijn.cabal
index 85f648a..6979a61 100644
--- a/bruijn.cabal
+++ b/bruijn.cabal
@@ -19,9 +19,10 @@ extra-source-files:
     README.md
 data-files:
     config
-    std/Boolean.bruijn
     std/Church.bruijn
     std/Combinator.bruijn
+    std/List.bruijn
+    std/Logic.bruijn
     std/Number.bruijn
     std/Option.bruijn
     std/Pair.bruijn
diff --git a/src/Eval.hs b/src/Eval.hs
index 0eb6c9e..0e4f1f3 100644
--- a/src/Eval.hs
+++ b/src/Eval.hs
@@ -125,7 +125,7 @@ evalInstruction instr s@(EnvState env) rec isRepl = case instr of
                | otherwise        = namespace ++ "."
     env'' <- pure $ Environment $ map (\((n, e), o) -> ((prefix ++ n, e), o))
                                      ((\(Environment e) -> e) env') -- TODO: Improve
-    rec (EnvState $ env <> env'') False -- import => isRepl = False
+    rec (EnvState $ env'' <> env) False -- import => isRepl = False
   Evaluate e ->
     let (res, _) = evalExp e (Environment []) `runState` env
     in  putStrLn
diff --git a/std/Combinator.bruijn b/std/Combinator.bruijn
index bedc1e9..2a6bb29 100644
--- a/std/Combinator.bruijn
+++ b/std/Combinator.bruijn
@@ -22,6 +22,8 @@ F [[0]]
 
 Y [[1 (0 0)] [1 (0 0)]]
 
+Z [[1 [1 1 0]] [1 [1 1 0]]]
+
 Θ [[0 (1 1 0)]] [[0 (1 1 0)]]
 
 i [0 S K]
diff --git a/std/List.bruijn b/std/List.bruijn
new file mode 100644
index 0000000..a4fa40a
--- /dev/null
+++ b/std/List.bruijn
@@ -0,0 +1,54 @@
+# MIT License, Copyright (c) 2022 Marvin Borner
+#              Copyright (c) 2017-2019 Sandro Lovnički
+# TODO: Tests.
+
+:import std/Combinator .
+
+:import std/Logic .
+
+# empty list element
+empty [[1]]
+
+# appends an element to a list
+append [[[[0 3 2]]]]
+
+# returns the head of a list or empty
+head [0 F T]
+
+# returns the tail of a list or empty
+tail [0 F F]
+
+# returns whether a list is empty
+empty? [0 T [[F]]]
+
+# returns the last element of a list or empty
+last Z [[empty? 0 [empty] [empty? (tail 1) (head 1) (2 (tail 1))] I]]
+
+# swaps both sides of a list
+swap [[[2 0 1]]]
+
+# TODO: Fix ternary inc
+# finds index of number in list or empty
+# find [[Y rec 1 0 +0]]
+# 	rec [[[[(empty? 1) empty ((eq? 2 (head 1)) 0 (3 2 (tail 1) (S 0)))]]]]
+
+# TODO: Fix ternary inc
+# gets element of list by index or empty
+# get [[Y rec 1 0 +0]]
+# 	rec [[[[(empty? 1) empty ((eq? 2 0) (head 1) (3 2 (tail 1) (S 0)))]]]]
+
+# merges two lists to one
+merge Y rec
+	rec [[[1 0 [[append 1 (4 0 2)]]]]]
+
+# reverses a list
+reverse [Y rec 0 empty]
+	rec [[[(empty? 1) 0 (2 (tail 1) (append (head 1) 0))]]]
+
+# removes elements of a list that satisfy a condition
+remove Y rec
+	rec [[[0 empty [[((3 1) I (append 1)) (4 3 0)]]]]]
+
+# sorts a list using quick sort (leq? and gre? as argument)
+sort [[Y (rec 1 0)]]
+	rec [[[[0 empty [[merge (3 (remove (swap 4 1) 0)) (append 1 (3 (remove (swap 5 1) 0)))]]]]]]
diff --git a/std/Boolean.bruijn b/std/Logic.bruijn
index 36d11bd..2e1e654 100644
--- a/std/Boolean.bruijn
+++ b/std/Logic.bruijn
@@ -3,56 +3,66 @@
 :import std/Combinator .
 
 not [0 F T]
+
 :test not T = F
 :test not F = T
 
 and [[1 0 F]]
+
 :test and T T = T
 :test and T F = F
 :test and F T = F
 :test and F F = F
 
 nand [[1 0 1 F T]]
+
 :test nand T T = F
 :test nand T F = T
 :test nand F T = T
 :test nand F F = T
 
 or [[1 T 0]]
+
 :test or T T = T
 :test or T F = T
 :test or F T = T
 :test or F F = F
 
 nor [[1 1 0 F T]]
+
 :test nor T T = F
 :test nor T F = F
 :test nor F T = F
 :test nor F F = T
 
 xor [[1 (not 0) 0]]
+
 :test xor T T = F
 :test xor T F = T
 :test xor F T = T
 :test xor F F = F
 
 xnor [[1 0 (not 0)]]
+
 :test xnor T T = T
 :test xnor T F = F
 :test xnor F T = F
 :test xnor F F = T
 
 if [[[2 1 0]]]
+
 :test if T T F = T
 :test if F T F = F
 
 implies [[or (not 1) 0]]
+
 :test implies T T = T
 :test implies T F = F
 :test implies F T = T
 :test implies F F = T
 
 iff [[and (implies 1 0) (implies 0 1)]]
+
 :test iff T T = T
 :test iff T F = F
 :test iff F T = F
diff --git a/std/Number.bruijn b/std/Number.bruijn
index fa97989..51db7e7 100644
--- a/std/Number.bruijn
+++ b/std/Number.bruijn
@@ -5,23 +5,38 @@
 
 :import std/Pair .
 
-# checks whether balanced ternary number is zero
-zero? [0 T [F] [F] I]
+:import std/List
 
-:test zero? +0 = T
-:test zero? -1 = F
-:test zero? +1 = F
-:test zero? +42 = F
+: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)]]]]]
 
@@ -50,12 +65,12 @@ up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
 :test up trit-pos +42 = up-pos +42
 :test up trit-zero +42 = up-zero +42
 
-# negates a balanced ternary number
-negate [[[[[4 3 1 2 0]]]]]
-
-:test negate +0 = +0
-:test negate -1 = +1
-:test negate +42 = -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]]
@@ -65,34 +80,96 @@ lst [0 trit-zero [trit-neg] [trit-pos] [trit-zero]]
 :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
-abstractify [0 [[[[3]]]] abs-neg abs-pos abs-zero]
-	abs-neg [[[[[2 4]]]]]
-	abs-pos [[[[[1 4]]]]]
-	abs-zero [[[[[0 4]]]]]
+abstract! [0 z neg pos zero]
+	z +0
+	neg [[[[[2 4]]]]]
+	pos [[[[[1 4]]]]]
+	zero [[[[[0 4]]]]]
 
-:test abstractify -3 = [[[[0 [[[[2 [[[[3]]]]]]]]]]]]
-:test abstractify +0 = [[[[3]]]]
-:test abstractify +3 = [[[[0 [[[[1 [[[[3]]]]]]]]]]]]
+: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 Y/ω to solve recursion
-normalize ω normalize'
-	normalize' [[0 +0 [up-neg ([3 3 0] 0)] [up-pos ([3 3 0] 0)] [up-zero ([3 3 0] 0)]]]
+# 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 normalize [[[[3]]]] = +0
-:test normalize (abstractify +42) = +42
-:test normalize (abstractify -42) = -42
+: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? [[eq-abs 1 (abstractify 0)]]
-	eq-z [zero? (normalize 0)]
-	eq-neg [[0 F [2 0] [F] [F]]]
-	eq-pos [[0 F [F] [2 0] [F]]]
-	eq-zero [[0 (1 0) [F] [F] [2 0]]]
-	eq-abs [0 eq-z eq-neg eq-pos eq-zero]
+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
@@ -103,28 +180,17 @@ eq? [[eq-abs 1 (abstractify 0)]]
 :test eq? +42 +42 = T
 :test eq? [[[[(1 (0 (0 (0 (0 3)))))]]]] +1 = T
 
-# strips leading 0s from balanced ternary number
-strip [fst (0 strip-z strip-neg strip-pos strip-zero)]
-	strip-z pair +0 T
-	strip-neg [0 [[pair (up-neg 1) F]]]
-	strip-pos [0 [[pair (up-pos 1) F]]]
-	strip-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
-
-# I believe Mogensen's Paper has an error in its inc/dec definitions.
-# They use 3 abstractions in the inc* functions, also we use switched +/0
-# in comparison to their implementation, yet the order of neg/pos/zero is
+# 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 inc-z inc-neg inc-pos inc-zero)]
-	inc-z pair +0 +1
-	inc-neg [0 [[pair (up-neg 1) (up-zero 1)]]]
-	inc-zero [0 [[pair (up-zero 1) (up-pos 1)]]]
-	inc-pos [0 [[pair (up-pos 1) (up-neg 0)]]]
+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)]
 
@@ -143,25 +209,25 @@ dec [snd (0 dec-z dec-neg dec-pos dec-zero)]
 
 sdec [strip (dec 0)]
 
-:test dec -42 = -43
-:test dec +0 = -1
-:test sdec (dec (dec (dec (dec +5)))) = +0
-:test sdec +1 = +0
-:test dec +42 = +41
+: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 [[add-abs 1 (abstractify 0)]]
-	add-c [[1 0 trit-zero]]
-	add-b-neg2 [1 (up-zero (3 0 trit-neg)) (up-neg (3 0 trit-zero)) (up-pos (3 0 trit-neg))]
-	add-b-neg [1 (up-pos (3 0 trit-neg)) (up-zero (3 0 trit-zero)) (up-neg (3 0 trit-zero))]
-	add-b-zero [up 1 (3 0 trit-zero)]
-	add-b-pos [1 (up-zero (3 0 trit-zero)) (up-neg (3 0 trit-pos)) (up-pos (3 0 trit-zero))]
-	add-b-pos2 [1 (up-pos (3 0 trit-zero)) (up-zero (3 0 trit-pos)) (up-neg (3 0 trit-pos))]
-	add-a-neg [[[1 (add-b-neg 1) add-b-neg2 add-b-zero add-b-neg]]]
-	add-a-pos [[[1 (add-b-pos 1) add-b-zero add-b-pos2 add-b-pos]]]
-	add-a-zero [[[1 (add-b-zero 1) add-b-neg add-b-pos add-b-zero]]]
-	add-z [[0 (dec (normalize 1)) (inc (normalize 1)) (normalize 1)]]
-	add-abs [add-c (0 add-z add-a-neg add-a-pos add-a-zero)]
+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)]]
 
@@ -184,11 +250,19 @@ ssub [[strip (sub 1 0)]]
 :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 mul-neg mul-pos mul-zero]]
-	mul-neg [sub (up-zero 0) 1]
-	mul-pos [add (up-zero 0) 1]
-	mul-zero [up-zero 0]
+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)]]