Moved/improved standard library

and other things

1 files changed, 0 insertions, 233 deletions

diff --git a/std.bruijn b/std.bruijn
deleted file mode 100644
index 9a05cdf..0000000
--- a/std.bruijn
+++ /dev/null
@@ -1,233 +0,0 @@
-# ==================
-# Common combinators
-# ==================
-
-S [[[2 0 (1 0)]]]
-K [[1]]
-I [0]
-B [[[2 (1 0)]]]
-C [[[2 0 1]]]
-T [[1]]
-F [[0]]
-ω [0 0]
-Ω ω ω
-Y [[1 (0 0)] [1 (0 0)]]
-Θ [[0 (1 1 0)]] [[0 (1 1 0)]]
-i [0 S K]
-
-:test I = i i
-:test K = i (i (i i))
-:test S = i (i (i (i i)))
-
-# =====
-# Pairs
-# =====
-
-# pairs two expressions into one
-pair [[[0 2 1]]]
-
-# extracts first expression from pair
-fst [0 T]
-:test fst (pair [[0]] [[1]]) = [[0]]
-
-# extracts second expression from pair
-snd [0 F]
-:test snd (pair [[0]] [[1]]) = [[1]]
-
-# TODO: investigate currying and chaining functions
-#       -> WHNF things?
-# chain [[[2 (1 0)]]]
-
-# ===================================
-# Ternary
-# According to works of T.Æ. Mogensen
-# ===================================
-
-# checks whether balanced ternary number is zero
-zero? [0 T [F] [F] I]
-:test zero? +0 = T
-:test zero? -1 = F
-:test zero? +1 = F
-:test zero? +42 = F
-
-trit-neg [[[2]]]
-trit-pos [[[1]]]
-trit-zero [[[0]]]
-
-# shifts a negative trit into a balanced ternary number
-up-neg [[[[[2 (4 3 2 1 0)]]]]]
-:test up-neg +0 = -1
-:test up-neg -1 = -4
-:test up-neg +42 = +125
-
-# shifts a positive trit into a balanced ternary number
-up-pos [[[[[1 (4 3 2 1 0)]]]]]
-:test up-pos +0 = +1
-:test up-pos -1 = -2
-:test up-pos +42 = +127
-
-# shifts a zero trit into a balanced ternary number
-up-zero [[[[[0 (4 3 2 1 0)]]]]]
-:test up-zero +0 = [[[[0 3]]]]
-:test up-zero +1 = +3
-:test up-zero +42 = +126
-
-# shifts a specified trit into a balanced ternary number
-up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
-:test up trit-neg +42 = up-neg +42
-:test up trit-pos +42 = up-pos +42
-:test up trit-zero +42 = up-zero +42
-
-# negates a balanced ternary number
-negate [[[[[4 3 1 2 0]]]]]
-:test negate +0 = +0
-:test negate -1 = +1
-:test negate +42 = -42
-
-# extracts least significant trit from balanced ternary numbers
-lst [0 trit-zero [trit-neg] [trit-pos] [trit-zero]]
-:test lst +0 = trit-zero
-:test lst -1 = trit-neg
-:test lst +1 = trit-pos
-:test lst +42 = trit-zero
-
-# converts the normal balanced ternary representation into abstract
-# -> the abstract representation is used in add/sub/mul
-_abs-neg [[[[[2 4]]]]]
-_abs-pos [[[[[1 4]]]]]
-_abs-zero [[[[[0 4]]]]]
-abstractify [0 [[[[3]]]] _abs-neg _abs-pos _abs-zero]
-:test abstractify -3 = [[[[0 [[[[2 [[[[3]]]]]]]]]]]]
-:test abstractify +0 = [[[[3]]]]
-:test abstractify +3 = [[[[0 [[[[1 [[[[3]]]]]]]]]]]]
-
-# converts the abstracted balanced ternary representation back to normal
-# using Y/ω to solve recursion
-_normalize [[0 +0 [up-neg ([3 3 0] 0)] [up-pos ([3 3 0] 0)] [up-zero ([3 3 0] 0)]]]
-normalize ω _normalize
-:test normalize [[[[3]]]] = +0
-:test normalize (abstractify +42) = +42
-:test normalize (abstractify -42) = -42
-
-# checks whether two balanced ternary numbers are equal
-# -> removes leading 0s!
-_eq-z [zero? (normalize 0)]
-_eq-neg [[0 F [2 0] [F] [F]]]
-_eq-pos [[0 F [F] [2 0] [F]]]
-_eq-zero [[0 (1 0) [F] [F] [2 0]]]
-_eq-abs [0 _eq-z _eq-neg _eq-pos _eq-zero]
-eq? [[_eq-abs 1 (abstractify 0)]]
-:test eq? -42 -42 = T
-:test eq? -1 -1 = T
-:test eq? -1 +0 = F
-:test eq? +0 +0 = T
-:test eq? +1 +0 = F
-:test eq? +1 +1 = T
-:test eq? +42 +42 = T
-:test eq? [[[[(1 (0 (0 (0 (0 3)))))]]]] +1 = T
-
-# strips leading 0s from balanced ternary number
-_strip-z pair +0 T
-_strip-neg [0 [[pair (up-neg 1) F]]]
-_strip-pos [0 [[pair (up-pos 1) F]]]
-_strip-zero [0 [[pair (0 +0 (up-zero 1)) 0]]]
-strip [fst (0 _strip-z _strip-neg _strip-pos _strip-zero)]
-:test strip [[[[0 3]]]] = +0
-:test strip [[[[2 (0 (0 (0 (0 3))))]]]] = -1
-:test strip +42 = +42
-
-# I believe Mogensen's Paper has an error in its succ/pred definitions.
-# They use 3 abstractions in the _succ* functions, also we use switched +/0
-# in comparison to their implementation, yet the order of neg/pos/zero is
-# the same. Something's weird.
-
-# adds +1 to a balanced ternary number (can introduce leading 0s)
-_succ-z pair +0 +1
-_succ-neg [0 [[pair (up-neg 1) (up-zero 1)]]]
-_succ-zero [0 [[pair (up-zero 1) (up-pos 1)]]]
-_succ-pos [0 [[pair (up-pos 1) (up-neg 0)]]]
-succ [snd (0 _succ-z _succ-neg _succ-pos _succ-zero)]
-ssucc [strip (succ 0)]
-:test eq? (succ -42) -41 = T
-:test eq? (succ -1) +0 = T
-:test eq? (succ +0) +1 = T
-:test eq? (succ (succ (succ (succ (succ +0))))) +5 = T
-:test eq? (succ +42) +43 = T
-
-# subs +1 from a balanced ternary number (can introduce leading 0s)
-_pred-z pair +0 -1
-_pred-neg [0 [[pair (up-neg 1) (up-pos 0)]]]
-_pred-zero [0 [[pair (up-zero 1) (up-neg 1)]]]
-_pred-pos [0 [[pair (up-pos 1) (up-zero 1)]]]
-pred [snd (0 _pred-z _pred-neg _pred-pos _pred-zero)]
-spred [strip (pred 0)]
-:test pred -42 = -43
-:test pred +0 = -1
-:test spred (pred (pred (pred (pred +5)))) = +0
-:test spred +1 = +0
-:test pred +42 = +41
-
-# adds two balanced ternary numbers (can introduce leading 0s)
-_add-c [[1 0 trit-zero]]
-_add-b-neg2 [1 (up-zero (3 0 trit-neg)) (up-neg (3 0 trit-zero)) (up-pos (3 0 trit-neg))]
-_add-b-neg [1 (up-pos (3 0 trit-neg)) (up-zero (3 0 trit-zero)) (up-neg (3 0 trit-zero))]
-_add-b-zero [up 1 (3 0 trit-zero)]
-_add-b-pos [1 (up-zero (3 0 trit-zero)) (up-neg (3 0 trit-pos)) (up-pos (3 0 trit-zero))]
-_add-b-pos2 [1 (up-pos (3 0 trit-zero)) (up-zero (3 0 trit-pos)) (up-neg (3 0 trit-pos))]
-_add-a-neg [[[1 (_add-b-neg 1) _add-b-neg2 _add-b-zero _add-b-neg]]]
-_add-a-pos [[[1 (_add-b-pos 1) _add-b-zero _add-b-pos2 _add-b-pos]]]
-_add-a-zero [[[1 (_add-b-zero 1) _add-b-neg _add-b-pos _add-b-zero]]]
-_add-z [[0 (pred (normalize 1)) (succ (normalize 1)) (normalize 1)]]
-_add-abs [_add-c (0 _add-z _add-a-neg _add-a-pos _add-a-zero)]
-add [[_add-abs 1 (abstractify 0)]]
-sadd [[strip (add 1 0)]]
-:test eq? (add -42 -1) -43 = T
-:test eq? (add -5 +6) +1 = T
-:test eq? (add -1 +0) -1 = T
-:test eq? (add +0 +0) +0 = T
-:test eq? (add +1 +2) +3 = T
-:test eq? (add +42 +1) +43 = T
-
-# subs two balanced ternary numbers (can introduce leading 0s)
-sub [[add 1 (negate 0)]]
-ssub [[strip (sub 1 0)]]
-:test eq? (sub -42 -1) -41 = T
-:test eq? (sub -5 +6) -11 = T
-:test eq? (sub -1 +0) -1 = T
-:test eq? (sub +0 +0) +0 = T
-:test eq? (sub +1 +2) -1 = T
-:test eq? (sub +42 +1) +41 = T
-
-# muls two balanced ternary numbers (can introduce leading 0s)
-_mul-neg [sub (up-zero 0) 1]
-_mul-pos [add (up-zero 0) 1]
-_mul-zero [up-zero 0]
-mul [[1 +0 _mul-neg _mul-pos _mul-zero]]
-smul [[strip (mul 1 0)]]
-:test eq? (mul +42 +0) +0 = T
-:test eq? (mul -1 +42) -42 = T
-:test eq? (mul +3 +11) +33 = T
-:test eq? (mul +42 -4) -168 = T
-
-# ===============
-# Boolean algebra
-# ===============
-
-not [0 F T]
-and [[1 0 F]]
-or [[1 T 0]]
-xor [[1 (not 0) 0]]
-if [[[2 1 0]]]
-:test not (or (and false true) true) = false
-
-# ===============
-# Church numerals
-# ===============
-
-church-zero [[0]]
-church-succ [[[1 (2 1 0)]]]
-church-add [[[[3 1 (2 1 0)]]]]
-church-mul [[[2 (1 0)]]]
-church-exp [[0 1]]
-
-main [[[0 2 1]]]