std/List.bruijn


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127

# MIT License, Copyright (c) 2022 Marvin Borner

:import std/Combinator .

:import std/Pair P

:import std/Logic .

:import std/Number N

# empty list element
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
cons P.pair

:test cons +1 (cons +2 empty) = P.pair +1 (P.pair +2 empty)
:test cons 'a' (cons 'b' (cons 'c' empty)) = "abc"

# returns the head of a list or empty
head P.fst

:test head (cons +1 (cons +2 empty)) = +1

# returns the tail of a list or empty
tail P.snd

: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))

# 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

# returns the last element of a list
last Z [[empty? 0 [empty] [empty? (tail 1) (head 1) (2 (tail 1))] I]]

:test last (cons +1 (cons +2 (cons +3 empty))) = +3

# 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]]

:test init (cons +1 (cons +2 (cons +3 empty))) = cons +1 (cons +2 empty)

# 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]]]

: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

# returns a list with n-times a element
repeat Z [[[N.zero? 1 [empty] [P.pair 1 (3 (N.dec 2) 1)] I]]]

: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