diff options
Diffstat (limited to 'std/List.bruijn')
| -rw-r--r-- | std/List.bruijn | 70 |
1 files changed, 40 insertions, 30 deletions
diff --git a/std/List.bruijn b/std/List.bruijn index f0cbc47..bce9463 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -12,9 +12,9 @@ empty false # returns true if a list is empty empty? [0 [[[false]]] true] -<>?‣ empty? +∅?‣ empty? -:test (<>?empty) (true) +:test (∅?empty) (true) # prepends an element to a list cons P.pair @@ -22,7 +22,7 @@ cons P.pair …:… cons :test ((+1) : ((+2) : empty)) (P.pair (+1) (P.pair (+2) empty)) -:test (<>?((+2) : empty)) (false) +:test (∅?((+2) : empty)) (false) # returns the head of a list or empty head P.fst @@ -40,18 +40,18 @@ tail P.snd # returns the length of a list in balanced ternary length z [[[rec]]] (+0) - rec <>?0 case-end case-inc + rec ∅?0 case-end case-inc case-inc 2 ++1 ~0 case-end 1 -#‣ length +∀‣ length -:test (#((+1) : ((+2) : empty))) ((+2)) -:test (#empty) ((+0)) +:test (∀((+1) : ((+2) : empty))) ((+2)) +:test (∀empty) ((+0)) # returns the element at index in list index z [[[rec]]] - rec <>?0 case-end case-index + rec ∅?0 case-end case-index case-index =?1 ^0 (2 --1 ~0) case-end empty @@ -64,7 +64,7 @@ index z [[[rec]]] # applies a left fold on a list foldl z [[[[rec]]]] - rec <>?0 case-end case-fold + rec ∅?0 case-end case-fold case-fold 3 2 (2 1 ^0) ~0 case-end 1 @@ -76,7 +76,7 @@ foldl1 [[foldl 1 ^0 ~0]] # applies a right fold on a list foldr [[[z [[rec]] 0]]] - rec <>?0 case-end case-fold + rec ∅?0 case-end case-fold case-fold 4 ^0 (1 ~0) case-end 3 @@ -124,7 +124,7 @@ singleton [0 : empty] # appends two lists append z [[[rec]]] - rec <>?1 case-end case-append + rec ∅?1 case-end case-append case-append ^1 : (2 ~1 0) case-end 0 @@ -142,7 +142,7 @@ snoc [[1 ++ ({ 0 })]] # maps each element to a function map z [[[rec]]] - rec <>?0 case-end case-map + rec ∅?0 case-end case-map case-map (1 ^0) : (2 1 ~0) case-end empty @@ -152,7 +152,7 @@ map z [[[rec]]] # filters a list based on a predicate filter z [[[rec]]] - rec <>?0 case-end case-filter + rec ∅?0 case-end case-filter case-filter 1 ^0 (cons ^0) i (2 1 ~0) case-end empty @@ -163,20 +163,20 @@ filter z [[[rec]]] # returns the last element of a list # - slow algorithm: # last z [[rec]] -# rec <>?0 case-end case-last -# case-last <>?(~0) ^0 (1 ~0) +# rec ∅?0 case-end case-last +# case-last ∅?(~0) ^0 (1 ~0) # case-end empty # - taking the first element of the reversed list is actually way faster because laziness last ^‣ ∘ <~>‣ _‣ last -:test (last ((+1) : ((+2) : ((+3) : empty)))) ((+3)) +:test (_((+1) : ((+2) : ((+3) : empty)))) ((+3)) # returns everything but the last element of a list init z [[rec]] - rec <>?0 case-end case-init - case-init <>?(~0) empty (^0 : (1 ~0)) + rec ∅?0 case-end case-init + case-init ∅?(~0) empty (^0 : (1 ~0)) case-end empty :test (init ((+1) : ((+2) : ((+3) : empty)))) ((+1) : ((+2) : empty)) @@ -196,16 +196,16 @@ concat-map concat ∘∘ map # zips two lists discarding excess elements zip z [[[rec]]] - rec <>?1 case-end case-zip - case-zip <>?0 empty ((^1 : ^0) : (2 ~1 ~0)) + 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 [[[[rec]]]] - rec <>?1 case-end case-zip - case-zip <>?0 empty ((2 ^1 ^0) : (3 2 ~1 ~0)) + rec ∅?1 case-end case-zip + case-zip ∅?0 empty ((2 ^1 ^0) : (3 2 ~1 ~0)) case-end empty :test (zip-with …+… ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) ((+3) : ((+3) : empty)) @@ -222,7 +222,7 @@ zip-with z [[[[rec]]]] # returns first n elements of a list take z [[[rec]]] - rec <>?0 case-end case-take + rec ∅?0 case-end case-take case-take =?1 empty (^0 : (2 --1 ~0)) case-end empty @@ -230,7 +230,7 @@ take z [[[rec]]] # takes elements while a predicate is satisfied take-while z [[[rec]]] - rec <>?0 case-end case-take + rec ∅?0 case-end case-take case-take 1 ^0 (^0 : (2 1 ~0)) empty case-end empty @@ -238,7 +238,7 @@ take-while z [[[rec]]] # removes first n elements of a list drop z [[[rec]]] - rec <>?0 case-end case-drop + rec ∅?0 case-end case-drop case-drop =?1 0 (2 --1 ~0) case-end empty @@ -246,7 +246,7 @@ drop z [[[rec]]] # removes elements from list while a predicate is satisfied drop-while z [[[rec]]] - rec <>?0 case-end case-drop + rec ∅?0 case-end case-drop case-drop 1 ^0 (2 1 ~0) 0 case-end empty @@ -254,7 +254,7 @@ drop-while z [[[rec]]] # returns pair of take-while and drop-while span z [[[rec]]] - rec <>?0 case-end case-drop + rec ∅?0 case-end case-drop case-drop 1 ^0 ((^0 : ^recced) : ~recced) (empty : 0) recced 2 1 ~0 case-end empty : empty @@ -266,6 +266,16 @@ break span ∘ (…∘… ¬‣) :test (break (\gre? (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty))) +# splits a list into two lists based on predicate +split-at z [[[rec]]] + rec ∅?dropped case-end case-split + dropped drop-while 1 0 + case-split ^broken : (2 1 ~broken) + broken break 1 dropped + case-end empty + +:test (split-at (…=?… (+1)) ((+2) : ((+1) : ((+3) : ((+2) : empty))))) ((((+2) : empty) : (((+3) : ((+2) : empty)) : empty))) + # returns true if any element in a list matches a predicate any? ⋁?‣ ∘∘ map @@ -293,7 +303,7 @@ eq? ⋀?‣ ∘∘∘ zip-with # removes first element that match an eq predicate remove z [[[[rec]]]] - rec <>?0 case-end case-remove + rec ∅?0 case-end case-remove case-remove (2 ^0 1) ~0 (^0 : (3 2 1 ~0)) case-end empty @@ -301,7 +311,7 @@ remove z [[[[rec]]]] # removes duplicates from list based on eq predicate (keeps first occurrence) nub z [[[rec]]] - rec <>?0 case-end case-nub + rec ∅?0 case-end case-nub case-nub ^0 : (2 1 (~0 <#> [¬(2 0 ^1)])) case-end empty @@ -330,6 +340,6 @@ iterate z [[[rec]]] rec 0 : (2 1 (1 0)) :test (take (+5) (iterate ++‣ (+0))) (((+0) : ((+1) : ((+2) : ((+3) : ((+4) : empty)))))) -:test (take (+2) (iterate sdec (+5))) (((+5) : ((+4) : empty))) +:test (take (+2) (iterate (%‣ ∘ dec) (+5))) (((+5) : ((+4) : empty))) :test (take (+5) (iterate i (+4))) (take (+5) (repeat (+4))) :test (take (+0) (iterate ++‣ (+0))) (empty) |