Implementations

2 files changed, 125 insertions, 47 deletions

diff --git a/std/List.bruijn b/std/List.bruijn
index a4fa40a..5bc49e1 100644
--- a/std/List.bruijn
+++ b/std/List.bruijn
@@ -1,54 +1,129 @@
 # MIT License, Copyright (c) 2022 Marvin Borner
-#              Copyright (c) 2017-2019 Sandro Lovnički
-# TODO: Tests.
 
 :import std/Combinator .
 
+:import std/Pair P
+
 :import std/Logic .
 
+:import std/Number N
+
 # empty list element
-empty [[1]]
+empty F
+
+# returns whether a list is empty
+empty? [0 [[[F]]] T]
+
+:test empty? empty = T
+:test empty? (cons +2 empty) = F
 
 # appends an element to a list
-append [[[[0 3 2]]]]
+cons P.pair
+
+:test cons +1 (cons +2 empty) = P.pair +1 (P.pair +2 empty)
 
 # returns the head of a list or empty
-head [0 F T]
+head P.fst
+
+:test head (cons +1 (cons +2 empty)) = +1
 
 # returns the tail of a list or empty
-tail [0 F F]
+tail P.snd
 
-# returns whether a list is empty
-empty? [0 T [[F]]]
+:test tail (cons +1 (cons +2 empty)) = cons +2 empty
+
+# returns the length of a list in balanced ternary
+length Z [[[empty? 0 [2] [3 (N.inc 2) (tail 1)] I]]] +0
+
+:test length (cons +1 (cons +2 empty)) = +2
+:test length empty = +0
+
+# returns the element at index in list
+# TODO: fix for balanced ternary
+index [[head (1 tail 0)]]
+
+# reverses a list
+reverse Z [[[empty? 0 [2] [3 (cons (head 1) 2) (tail 1)] I]]] empty
+
+:test reverse (cons +1 (cons +2 (cons +3 empty))) = cons +3 (cons +2 (cons +1 empty))
+
+# creates list out of n terms
+# TODO: fix for balanced ternary
+list [0 [[[2 (cons 0 1)]]] reverse empty]
+
+# merges two lists
+merge Z [[[empty? 1 [1] [cons (head 2) (3 (tail 2) 1)] I]]]
+
+:test merge (cons +1 (cons +2 (cons +3 empty))) (cons +4 empty) = cons +1 (cons +2 (cons +3 (cons +4 empty)))
+
+# maps each element to a function
+map Z [[[empty? 0 [empty] [cons (2 (head 1)) (3 2 (tail 1))] I]]]
+
+:test map N.inc (cons +1 (cons +2 (cons +3 empty))) = cons +2 (cons +3 (cons +4 empty))
 
-# returns the last element of a list or empty
+# applies a left fold on a list
+foldl Z [[[[empty? 0 [2] [4 3 (3 2 (head 1)) (tail 1)] I]]]]
+
+:test N.eq? (foldl N.add +0 (cons +1 (cons +2 (cons +3 empty)))) +6 = T
+:test N.eq? (foldl N.sub +6 (cons +1 (cons +2 (cons +3 empty)))) +0 = T
+
+# applies a right fold on a list
+foldr [[[Z [[empty? 0 [4] [5 (head 1) (2 (tail 1))] I]] 0]]]
+
+:test N.eq? (foldr N.add +0 (cons +1 (cons +2 (cons +3 empty)))) +6 = T
+:test N.eq? (foldr N.sub +2 (cons +1 (cons +2 (cons +3 empty)))) +0 = T
+
+# filters a list based on a predicate
+filter Z [[[empty? 0 [empty] [2 (head 1) (cons (head 1)) I (3 2 (tail 1))] I]]]
+
+:test filter N.zero? (cons +1 (cons +0 (cons +3 empty))) = cons +0 empty
+
+# checks whether an element is part of a list
+elem [[foldr [or (N.eq? 1 0)] F 2]]
+
+# returns the last element of a list
 last Z [[empty? 0 [empty] [empty? (tail 1) (head 1) (2 (tail 1))] I]]
 
-# swaps both sides of a list
-swap [[[2 0 1]]]
+:test last (cons +1 (cons +2 (cons +3 empty))) = +3
 
-# 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)))]]]]
+# returns everything but the last element of a list
+init Z [[empty? 0 [empty] [empty? (tail 1) empty (cons (head 1) (2 (tail 1)))] I]]
 
-# 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)))]]]]
+:test init (cons +1 (cons +2 (cons +3 empty))) = cons +1 (cons +2 empty)
 
-# merges two lists to one
-merge Y rec
-	rec [[[1 0 [[append 1 (4 0 2)]]]]]
+# zips two lists discarding excess elements
+zip Z [[[empty? 1 [empty] [empty? 1 empty (cons (cons (head 2) (head 1)) (3 (tail 2) (tail 1)))] I]]]
 
-# reverses a list
-reverse [Y rec 0 empty]
-	rec [[[(empty? 1) 0 (2 (tail 1) (append (head 1) 0))]]]
+:test zip (cons +1 (cons +2 empty)) (cons +2 (cons +1 empty)) = cons (P.pair +1 +2) (cons (P.pair +2 +1) empty)
+
+# applies pairs of the zipped list as arguments to a function
+zip-with Z [[[[empty? 1 [empty] [empty? 1 empty (cons (3 (head 2) (head 1)) (4 3 (tail 2) (tail 1)))] I]]]]
+
+:test zip-with N.add (cons +1 (cons +2 empty)) (cons +2 (cons +1 empty)) = cons +3 (cons +3 empty)
+
+# returns first n elements of a list
+take Z [[[empty? 0 [empty] [N.zero? 2 empty (cons (head 1) (3 (N.dec 2) (tail 1)))] I]]]
+
+:test take +2 (cons +1 (cons +2 (cons +3 empty))) = cons +1 (cons +2 empty)
+
+# takes elements while a predicate is satisfied
+take-while Z [[[empty? 0 [empty] [2 (head 1) (cons (head 1) (3 2 (tail 1))) empty] I]]]
+
+:test take-while N.zero? (cons +0 (cons +0 (cons +1 empty))) = cons +0 (cons +0 empty)
+
+# removes first n elements of a list
+drop Z [[[empty? 0 [empty] [N.zero? 2 1 (3 (N.dec 2) (tail 1))] I]]]
+
+:test drop +2 (cons +1 (cons +2 (cons +3 empty))) = cons +3 empty
+
+# removes elements while a predicate is satisfied
+drop-while Z [[[empty? 0 [empty] [2 (head 1) (3 2 (tail 1)) 1] I]]]
+
+:test drop-while N.zero? (cons +0 (cons +0 (cons +1 empty))) = cons +1 empty
 
-# removes elements of a list that satisfy a condition
-remove Y rec
-	rec [[[0 empty [[((3 1) I (append 1)) (4 3 0)]]]]]
+# returns a list with n-times a element
+repeat Z [[[N.zero? 1 [empty] [P.pair 1 (3 (N.dec 2) 1)] I]]]
 
-# 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)))]]]]]]
+:test repeat +5 +4 = (cons +4 (cons +4 (cons +4 (cons +4 (cons +4 empty)))))
+:test repeat +1 +4 = (cons +4 empty)
+:test repeat +0 +4 = empty
diff --git a/std/Number.bruijn b/std/Number.bruijn
index 51db7e7..2a4ca25 100644
--- a/std/Number.bruijn
+++ b/std/Number.bruijn
@@ -5,8 +5,6 @@
 
 :import std/Pair .
 
-:import std/List
-
 :import std/Logic .
 
 # negative trit indicating coeffecient of -1
@@ -72,14 +70,6 @@ down [snd (0 z neg pos zero)]
 	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]]]]]
 
@@ -89,7 +79,7 @@ negate [[[[[4 3 1 2 0]]]]]
 
 # converts a balanced ternary number to a list of trits
 list! [0 z neg pos zero]
-	z List.empty
+	z F
 	neg [[pair trit-neg 1]]
 	pos [[pair trit-pos 1]]
 	zero [[pair trit-zero 1]]
@@ -107,10 +97,21 @@ strip [fst (0 z neg pos zero)]
 :test strip [[[[2 (0 (0 (0 (0 3))))]]]] = -1
 :test strip +42 = +42
 
+# 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
+
 # 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]]]
+# mst [fix (List.last (list! (strip 0)))]
+# fix [if (or (trit-neg? 0) (or (trit-pos? 0) (trit-zero? 0))) 0 [[0]]]
+
+# TODO: Fix list import loop
+mst [trit-zero]
 
 :test mst +0 = trit-zero
 :test mst -1 = trit-neg
@@ -163,7 +164,7 @@ normal! ω rec
 :test normal! (abstract! -42) = -42
 
 # checks whether two balanced ternary numbers are equal
-# -> removes leading 0s!
+# -> ignores leading 0s!
 eq? [[abs 1 (abstract! 0)]]
 	z [zero? (normal! 0)]
 	neg [[0 F [2 0] [F] [F]]]
@@ -192,6 +193,7 @@ inc [snd (0 z neg pos zero)]
 	zero [0 [[pair (up-zero 1) (up-pos 1)]]]
 	pos [0 [[pair (up-pos 1) (up-neg 0)]]]
 
+# adds +1 to a balanced ternary number and strips leading 0s
 sinc [strip (inc 0)]
 
 :test eq? (inc -42) -41 = T
@@ -207,6 +209,7 @@ dec [snd (0 dec-z dec-neg dec-pos dec-zero)]
 	dec-zero [0 [[pair (up-zero 1) (up-neg 1)]]]
 	dec-pos [0 [[pair (up-pos 1) (up-zero 1)]]]
 
+# subs +1 from a balanced ternary number and strips leading 0s
 sdec [strip (dec 0)]
 
 :test eq? (dec -42) -43 = T
@@ -229,6 +232,7 @@ add [[abs 1 (abstract! 0)]]
 	z [[0 (dec (normal! 1)) (inc (normal! 1)) (normal! 1)]]
 	abs [c (0 z a-neg a-pos a-zero)]
 
+# adds two balanced ternary numbers and strips leading 0s
 sadd [[strip (add 1 0)]]
 
 :test eq? (add -42 -1) -43 = T
@@ -241,6 +245,7 @@ sadd [[strip (add 1 0)]]
 # subs two balanced ternary numbers (can introduce leading 0s)
 sub [[add 1 (negate 0)]]
 
+# subs two balanced ternary numbers and strips leading 0s
 ssub [[strip (sub 1 0)]]
 
 :test eq? (sub -42 -1) -41 = T
@@ -256,8 +261,6 @@ 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]