diff options
| -rw-r--r-- | std/Box.bruijn | 22 | ||||
| -rw-r--r-- | std/List.bruijn | 32 |
2 files changed, 37 insertions, 17 deletions
diff --git a/std/Box.bruijn b/std/Box.bruijn index 1bdac0a..acb2413 100644 --- a/std/Box.bruijn +++ b/std/Box.bruijn @@ -11,31 +11,35 @@ empty true ⧗ (Box a) # returns true if the box is empty empty? [0 true [false]] ⧗ (Box a) → Boolean -:test (empty? empty) (true) +∅?‣ empty? + +:test (∅?empty) (true) # builds a box out of a value box [[[0 2]]] ⧗ a → (Box a) +<>‣ box + # returns true if the box is set set? [0 false [true]] ⧗ (Box a) → Boolean -:test (set? (box [0])) (true) +:test (set? <>[0]) (true) :test (set? empty) (false) # sets the value of a empty box, ignores argument if already set -store! [[empty? 1 (box 0) 1]] ⧗ (Box a) → a → (Box a) +store! [[∅?1 <>0 1]] ⧗ (Box a) → a → (Box a) -:test (store! (box [[0]]) [[1]]) (box [[0]]) -:test (store! empty [[1]]) (box [[1]]) +:test (store! <>[[0]] [[1]]) (<>[[0]]) +:test (store! empty [[1]]) (<>[[1]]) # sets/overrides the value of a box -set! [[box 0]] ⧗ (Box a) → a → (Box a) +set! [[<>0]] ⧗ (Box a) → a → (Box a) -:test (set! (box [[0]]) [[1]]) (box [[1]]) -:test (set! empty [[1]]) (box [[1]]) +:test (set! <>[[0]] [[1]]) (<>[[1]]) +:test (set! empty [[1]]) (<>[[1]]) # extracts value from a box or returns first argument if none get [[0 1 i]] ⧗ a → (Box b) → c -:test (get [[0]] (box [[1]])) ([[1]]) +:test (get [[0]] <>[[1]]) ([[1]]) :test (get [[0]] empty) ([[0]]) diff --git a/std/List.bruijn b/std/List.bruijn index f35ec6f..4291a0e 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -7,6 +7,7 @@ :import std/Pair P :import std/Logic . :import std/Number/Ternary . +:import std/Box B # empty list element empty false ⧗ (List a) @@ -63,12 +64,16 @@ apply z [[[rec]]] ⧗ (a → b) → (List a) → b case-app 2 (1 ^0) ~0 case-end 1 -:test (apply …+… ((+1) : {}(+2))) ((+3)) +…<!… apply + +:test (…+… <! ((+1) : {}(+2))) ((+3)) # applies each element of the tail to the head -eval [apply ^0 ~0] ⧗ (Pair (a → b) (List a)) → b +eval [^0 <! ~0] ⧗ (Pair (a → b) (List a)) → b + +!‣ eval -:test (eval (…+… : ((+1) : {}(+2)))) ((+3)) +:test (!(…+… : ((+1) : {}(+2)))) ((+3)) # returns the element at index in list index z [[[rec]]] ⧗ (List a) → Number → a @@ -140,11 +145,6 @@ reverse foldl \cons empty ⧗ (List a) → (List a) :test (<~>((+1) : ((+2) : {}(+3)))) ((+3) : ((+2) : {}(+1))) -# creates list out of n terms -# TODO: use balanced ternary -# TODO: fix/remove incorrect type? -list [0 [[[2 (0 : 1)]]] reverse empty] ⧗ (List a) → Unary → b → (List b) - # appends two lists append z [[[rec]]] ⧗ (List a) → (List a) → (List a) rec ∅?1 case-end case-append @@ -166,6 +166,21 @@ snoc [[1 ++ {}0]] ⧗ (List a) → a → (List a) :test (empty ; (+1)) ({}(+1)) :test ({}(+1) ; (+2)) ((+1) : {}(+2)) +# generates a variadic variation of a list-based function +# TODO: Fix variadicity in signature +# TODO: Find a solution that does not require boxed terms +variadic [[y [[[[rec]]]] 1 0 [[0]]]] ⧗ ((List a) → b) → ((Box a) → (Box c) → b) + rec B.∅?1 (2 0) [4 3 0 (1 ; (B.get i 2))] + +:test (variadic reverse B.<>(+1) B.<>(+2) B.<>(+3) B.empty) ((+3) : ((+2) : {}(+1))) + +# constructs list out of boxed terms, ended with an empty box +# TODO: Fix variadicity in signature +list variadic i ⧗ a → (List a) + +:test (list B.<>(+2) B.<>(+3) B.empty) ((+2) : {}(+3)) +:test (^(list B.<>(+2) B.<>(+3))) ((+2) : {}(+3)) + # maps each element to a function map z [[[rec]]] ⧗ (a → b) → (List a) → (List b) rec ∅?0 case-end case-map @@ -448,3 +463,4 @@ iterate z [[[rec]]] ⧗ (a → a) → a → (List a) :test (take (+2) (iterate (%‣ ∘ dec) (+5))) (((+5) : {}(+4))) :test (take (+5) (iterate i (+4))) (take (+5) (repeat (+4))) :test (take (+0) (iterate ++‣ (+0))) (empty) + |