diff options
Diffstat (limited to 'std/List.bruijn')
| -rw-r--r-- | std/List.bruijn | 134 |
1 files changed, 72 insertions, 62 deletions
diff --git a/std/List.bruijn b/std/List.bruijn index 8683a43..b84f5d0 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -12,7 +12,7 @@ # empty list element empty false -# returns whether a list is empty +# returns true if a list is empty empty? [0 [[[false]]] true] <>?( empty? @@ -26,7 +26,6 @@ cons P.pair (:) cons :test ((+1) : ((+2) : empty)) (P.pair (+1) (P.pair (+2) empty)) -:test ('a' : ('b' : ('c' : empty))) ("abc") # returns the head of a list or empty head P.fst @@ -43,11 +42,10 @@ tail P.snd :test (~((+1) : ((+2) : empty))) ((+2) : empty) # returns the length of a list in balanced ternary -length Z [[[case-some]]] case-empty - case-some <>?0 case-end case-inc +length Z [[[rec]]] (+0) + rec <>?0 case-end case-inc case-inc 2 ++1 ~0 case-end 1 - case-empty (+0) #( length @@ -55,8 +53,8 @@ length Z [[[case-some]]] case-empty :test (#empty) ((+0)) # returns the element at index in list -index Z [[[case-some]]] - case-some <>?0 case-end case-index +index Z [[[rec]]] + rec <>?0 case-end case-index case-index =?1 ^0 (2 --1 ~0) case-end empty @@ -68,26 +66,25 @@ index Z [[[case-some]]] :test (((+1) : ((+2) : ((+3) : empty))) !! (+3)) (empty) # applies a left fold on a list -foldl Z [[[[case-some]]]] - case-some <>?0 case-end case-fold +foldl Z [[[[rec]]]] + rec <>?0 case-end case-fold case-fold 3 2 (2 1 ^0) ~0 case-end 1 -:test ((foldl add (+0) ((+1) : ((+2) : ((+3) : empty)))) =? (+6)) (true) -:test ((foldl sub (+6) ((+1) : ((+2) : ((+3) : empty)))) =? (+0)) (true) +:test ((foldl (+) (+0) ((+1) : ((+2) : ((+3) : empty)))) =? (+6)) (true) +:test ((foldl (-) (+6) ((+1) : ((+2) : ((+3) : empty)))) =? (+0)) (true) # foldl without starting value foldl1 [[foldl 1 ^0 ~0]] # applies a right fold on a list -foldr [[[Z [[case-some]] case-empty]]] - case-some <>?0 case-end case-fold +foldr [[[Z [[rec]] 0]]] + rec <>?0 case-end case-fold case-fold 4 ^0 (1 ~0) case-end 3 - case-empty 0 -:test ((foldr add (+0) ((+1) : ((+2) : ((+3) : empty)))) =? (+6)) (true) -:test ((foldr sub (+2) ((+1) : ((+2) : ((+3) : empty)))) =? (+0)) (true) +:test ((foldr (+) (+0) ((+1) : ((+2) : ((+3) : empty)))) =? (+6)) (true) +:test ((foldr (-) (+2) ((+1) : ((+2) : ((+3) : empty)))) =? (+0)) (true) # foldr without starting value foldr1 [[foldl 1 ^0 ~0]] @@ -118,7 +115,7 @@ product foldl mul (+1) :test (Π ((+1) : ((+2) : ((+3) : empty)))) ((+6)) # adds all values in list -sum foldl add (+0) +sum foldl (+) (+0) Σ sum @@ -146,8 +143,8 @@ reverse foldl \cons empty list [0 [[[2 (0 : 1)]]] reverse empty] # appends two lists -append Z [[[case-some]]] - case-some <>?1 case-end case-merge +append Z [[[rec]]] + rec <>?1 case-end case-merge case-merge ^1 : (2 ~1 0) case-end 0 @@ -164,8 +161,8 @@ snoc [[1 ++ (0 : empty)]] :test (((+1) : empty) ; (+2)) ((+1) : ((+2) : empty)) # maps each element to a function -map Z [[[case-some]]] - case-some <>?0 case-end case-map +map Z [[[rec]]] + rec <>?0 case-end case-map case-map (1 ^0) : (2 1 ~0) case-end empty @@ -174,8 +171,8 @@ map Z [[[case-some]]] :test (inc <$> ((+1) : ((+2) : ((+3) : empty)))) ((+2) : ((+3) : ((+4) : empty))) # filters a list based on a predicate -filter Z [[[case-some]]] - case-some <>?0 case-end case-filter +filter Z [[[rec]]] + rec <>?0 case-end case-filter case-filter 1 ^0 (cons ^0) I (2 1 ~0) case-end empty @@ -184,8 +181,8 @@ filter Z [[[case-some]]] :test (((+1) : ((+0) : ((+3) : empty))) <#> zero?) ((+0) : empty) # returns the last element of a list -last Z [[case-some]] - case-some <>?0 case-end case-last +last Z [[rec]] + rec <>?0 case-end case-last case-last <>?(~0) ^0 (1 ~0) case-end empty @@ -194,8 +191,8 @@ _( last :test (last ((+1) : ((+2) : ((+3) : empty)))) ((+3)) # returns everything but the last element of a list -init Z [[case-some]] - case-some <>?0 case-end case-init +init Z [[rec]] + rec <>?0 case-end case-init case-init <>?(~0) empty (^0 : (1 ~0)) case-end empty @@ -214,61 +211,75 @@ concat-map [foldr (append . 0) empty] :test (concat-map [-0 : (0 : empty)] ((+1) : ((+2) : empty))) ((-1) : ((+1) : ((-2) : ((+2) : empty)))) # zips two lists discarding excess elements -zip Z [[[case-some]]] - case-some <>?1 case-end case-zip +zip Z [[[rec]]] + rec <>?1 case-end case-zip case-zip <>?0 empty ((^1 : ^0) : (2 ~1 ~0)) case-end empty :test (zip ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) (((+1) : (+2)) : (((+2) : (+1)) : empty)) # applies pairs of the zipped list as arguments to a function -zip-with Z [[[[case-some]]]] - case-some <>?1 case-end case-zip +zip-with Z [[[[rec]]]] + rec <>?1 case-end case-zip case-zip <>?0 empty ((2 ^1 ^0) : (3 2 ~1 ~0)) case-end empty -:test (zip-with add ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) ((+3) : ((+3) : empty)) +:test (zip-with (+) ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) ((+3) : ((+3) : empty)) # returns first n elements of a list -take Z [[[case-some]]] - case-some <>?0 case-end case-take +take Z [[[rec]]] + rec <>?0 case-end case-take case-take =?1 empty (^0 : (2 --1 ~0)) case-end empty :test (take (+2) ((+1) : ((+2) : ((+3) : empty)))) ((+1) : ((+2) : empty)) # takes elements while a predicate is satisfied -take-while Z [[[case-some]]] - case-some <>?0 case-end case-take +take-while Z [[[rec]]] + rec <>?0 case-end case-take case-take 1 ^0 (^0 : (2 1 ~0)) empty case-end empty :test (take-while zero? ((+0) : ((+0) : ((+1) : empty)))) ((+0) : ((+0) : empty)) # removes first n elements of a list -drop Z [[[case-some]]] - case-some <>?0 case-end case-drop +drop Z [[[rec]]] + rec <>?0 case-end case-drop case-drop =?1 0 (2 --1 ~0) case-end empty :test (drop (+2) ((+1) : ((+2) : ((+3) : empty)))) ((+3) : empty) # removes elements from list while a predicate is satisfied -drop-while Z [[[case-some]]] - case-some <>?0 case-end case-drop +drop-while Z [[[rec]]] + rec <>?0 case-end case-drop case-drop 1 ^0 (2 1 ~0) 0 case-end empty :test (drop-while zero? ((+0) : ((+0) : ((+1) : empty)))) ((+1) : empty) +# returns pair of take-while and drop-while +span Z [[[rec]]] + rec <>?0 case-end case-drop + case-drop 1 ^0 ((^0 : ^recced) : ~recced) (empty : 0) + recced 2 1 ~0 + case-end empty : empty + +:test (span (\(<?) (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty))) + +# same as span but with inverted predicate +break [span (not! . 0)] + +:test (break (\(>?) (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty))) + # returns true if any element in a list matches a predicate -any? [lor? . (map 0)] +any? [||( . (map 0)] :test (any? (\gre? (+2)) ((+1) : ((+2) : ((+3) : empty)))) (true) :test (any? (\gre? (+2)) ((+1) : ((+2) : ((+2) : empty)))) (false) # returns true if all elements in a list match a predicate -all? [land? . (map 0)] +all? [&&( . (map 0)] :test (all? (\gre? (+2)) ((+3) : ((+4) : ((+5) : empty)))) (true) :test (all? (\gre? (+2)) ((+4) : ((+3) : ((+2) : empty)))) (false) @@ -276,37 +287,36 @@ all? [land? . (map 0)] # returns true if element is part of a list based on eq predicate in? [[any? (\1 0)]] -:test (in? eq? (+3) ((+1) : ((+2) : ((+3) : empty)))) (true) -:test (in? eq? (+0) ((+1) : ((+2) : ((+3) : empty)))) (false) +:test (in? (=?) (+3) ((+1) : ((+2) : ((+3) : empty)))) (true) +:test (in? (=?) (+0) ((+1) : ((+2) : ((+3) : empty)))) (false) # returns true if all elements of one list are equal to corresponding elements of other list -# TODO: Better name -leq? [[[land? (zip-with 2 1 0)]]] +eq? &&( ... zip-with -:test (leq? eq? ((+1) : ((+2) : empty)) ((+1) : ((+2) : empty))) (true) -:test (leq? eq? ((+1) : ((+2) : empty)) ((+2) : ((+2) : empty))) (false) -:test (leq? eq? empty empty) (true) +:test (eq? (=?) ((+1) : ((+2) : empty)) ((+1) : ((+2) : empty))) (true) +:test (eq? (=?) ((+1) : ((+2) : empty)) ((+2) : ((+2) : empty))) (false) +:test (eq? (=?) empty empty) (true) # removes first element that match an eq predicate -remove Z [[[[case-some]]]] - case-some <>?0 case-end case-remove +remove Z [[[[rec]]]] + rec <>?0 case-end case-remove case-remove (2 ^0 1) ~0 (^0 : (3 2 1 ~0)) case-end empty -:test (remove eq? (+2) ((+1) : ((+2) : ((+3) : ((+2) : empty))))) ((+1) : ((+3) : ((+2) : empty))) +:test (remove (=?) (+2) ((+1) : ((+2) : ((+3) : ((+2) : empty))))) ((+1) : ((+3) : ((+2) : empty))) # removes duplicates from list based on eq predicate (keeps first occurrence) -nub Z [[[case-some]]] - case-some <>?0 case-end case-nub +nub Z [[[rec]]] + rec <>?0 case-end case-nub case-nub ^0 : (2 1 (~0 <#> [!(2 0 ^1)])) case-end empty -:test (nub eq? ((+1) : ((+2) : ((+3) : empty)))) (((+1) : ((+2) : ((+3) : empty)))) -:test (nub eq? ((+1) : ((+2) : ((+1) : empty)))) (((+1) : ((+2) : empty))) +:test (nub (=?) ((+1) : ((+2) : ((+3) : empty)))) (((+1) : ((+2) : ((+3) : empty)))) +:test (nub (=?) ((+1) : ((+2) : ((+1) : empty)))) (((+1) : ((+2) : empty))) # returns a list with infinite-times a element -repeat Z [[case-some]] - case-some 0 : (1 0) +repeat Z [[rec]] + rec 0 : (1 0) :test (take (+3) (repeat (+4))) ((+4) : ((+4) : ((+4) : empty))) @@ -316,14 +326,14 @@ replicate [[take 1 (repeat 0)]] :test (replicate (+3) (+4)) ((+4) : ((+4) : ((+4) : empty))) # returns an infinite list repeating a finite list -cycle Z [[case-some]] - case-some 0 ++ (1 0) +cycle Z [[rec]] + rec 0 ++ (1 0) :test (take (+6) (cycle "ab")) ("ababab") # returns a list with infinite-times previous (or start) value applied to a function -iterate Z [[[case-some]]] - case-some 0 : (2 1 (1 0)) +iterate Z [[[rec]]] + rec 0 : (2 1 (1 0)) :test (take (+5) (iterate inc (+0))) (((+0) : ((+1) : ((+2) : ((+3) : ((+4) : empty)))))) :test (take (+2) (iterate dec (+5))) (((+5) : ((+4) : empty))) |