aboutsummaryrefslogtreecommitdiffhomepage
path: root/std/List.bruijn
diff options
context:
space:
mode:
Diffstat (limited to 'std/List.bruijn')
-rw-r--r--std/List.bruijn137
1 files changed, 106 insertions, 31 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