Features

very descriptive

5 files changed, 140 insertions, 167 deletions

diff --git a/README.md b/README.md
index edfd3d6..99a5bfc 100644
--- a/README.md
+++ b/README.md
@@ -151,7 +151,7 @@ Using standard library:
 
     # boolean
     main not (or (and false true) true)
-    :test main = [0]
+    :test main = false
 
     # read the std.bruijn file for an overview of all functions
 
diff --git a/benchmark.bruijn b/benchmark.bruijn
new file mode 100644
index 0000000..e11668f
--- /dev/null
+++ b/benchmark.bruijn
@@ -0,0 +1,31 @@
+# ==================
+# Lennart
+# From Lambda-n-ways
+# ==================
+
+true [[0]]
+false [[1]]
+if [[[2 0 1]]]
+zero [[1]]
+succ [[[0 2]]]
+one succ zero
+two succ one
+three succ two
+const [[1]]
+pair [[[0 2 1]]]
+fst [[1 0 [[1]]]]
+snd [[1 0 [[0]]]]
+fix [[1 (0 0)] [1 (0 0)]]
+add fix [[[1 0 [succ (3 0 1)]]]]
+mul fix [[[1 zero [add 1 (3 0 1)]]]]
+fac fix [[0 one [mul 1 (2 0)]]]
+eqnat fix [[[1 (0 true (const false)) [1 false [4 1 0]]]]]
+sumto fix [[0 zero [add 1 (2 0)]]]
+n5 add two three
+n6 add three three
+n17 add n6 (add n6 n5)
+n37 succ (mul n6 n6)
+n703 sumto n37
+n720 fac n6
+
+main eqnat n720 (add n703 n17) = true
diff --git a/src/Eval.hs b/src/Eval.hs
index 1c33fa2..77e5990 100644
--- a/src/Eval.hs
+++ b/src/Eval.hs
@@ -93,7 +93,7 @@ eval (line : ls) state@(EnvState env) isRepl =
                     else eval ls (EnvState env') isRepl
           Import path -> do
             lib    <- getDataFileName path -- TODO: Use actual lib directory
-            exists <- pure False -- doesFileExist lib
+            exists <- doesFileExist lib
             loadFile $ if exists then lib else path
           Evaluate exp ->
             let (res, env') = evalExp exp `runState` env
diff --git a/std.bruijn b/std.bruijn
index 22f7fae..9a05cdf 100644
--- a/std.bruijn
+++ b/std.bruijn
@@ -15,71 +15,118 @@ Y [[1 (0 0)] [1 (0 0)]]
 Θ [[0 (1 1 0)]] [[0 (1 1 0)]]
 i [0 S K]
 
-# =================
-# Alternative names
-# =================
-
-true T
-false F
-id I
+: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]]]
-fst [0 T]
-snd [0 F]
 
+# 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: contract-like type-checking
-#       like: `+ ... : [[[[# 3]]]]`
+# 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)]]]]]]
-# TODO: up is incorrect
+: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
 
-trit-neg [[[2]]]
-trit-pos [[[1]]]
-trit-zero [[[0]]]
+# 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]]]
@@ -94,18 +141,20 @@ strip [fst (0 _strip-z _strip-neg _strip-pos _strip-zero)]
 # 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 succ -42 = -41
-:test ssucc -1 = +0
-:test succ +0 = +1
-:test succ (succ (succ (succ (succ +0)))) = +5
-:test succ +42 = +43
+: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)]]]
@@ -118,62 +167,47 @@ spred [strip (pred 0)]
 :test spred +1 = +0
 :test pred +42 = +41
 
-_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]]]]]]]]]]]]
-
-# solving recursion using Y/ω
-_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
-
-_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
-
-# TODO: Much zero/one switching needed
-_add-z [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]]
+# 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-pos (3 0 trit-neg)) (up-neg (3 0 trit-zero))]
-_add-b-neg [1 (up-pos (3 0 trit-neg)) (up-neg (3 0 trit-zero)) (up-zero (3 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-pos (3 0 trit-zero)) (up-neg (3 0 trit-pos))]
-_add-b-pos2 [1 (up-pos (3 0 trit-zero)) (up-neg (3 0 trit-pos)) (up-zero (3 0 trit-pos))]
-_add-a-neg [[[1 (_add-b-neg 1) _add-b-neg2 _add-b-neg _add-b-zero]]]
-_add-a-zero [[[1 (_add-b-zero 1) _add-b-neg _add-b-zero _add-b-pos]]]
-_add-a-pos [[[1 (_add-b-pos 1) _add-b-zero _add-b-pos _add-b-pos2]]]
-_add-abs [_add-c (0 _add-z _add-a-neg _add-a-pos _add-a-neg)]
+_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)]]
-:test add -42 -1 = -43
-:test add -5 +6 = +1
-:test add -1 +0 = -1
-:test add +0 +0 = +0
-:test add +1 +2 = +3
-:test add +42 +1 = +43
-
+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)]]
-:test sub -42 -1 = -41
-:test sub -5 +6 = -11
-:test sub -1 +0 = -1
-:test sub +0 +0 = +0
-:test sub +1 +2 = -1
-:test sub +42 +1 = +41
+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
@@ -184,6 +218,7 @@ 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
diff --git a/test.bruijn b/test.bruijn
deleted file mode 100644
index 24a0083..0000000
--- a/test.bruijn
+++ /dev/null
@@ -1,93 +0,0 @@
-atom0 [[[[[4]]]]]
-atom1 [[[[[3]]]]]
-atom2 [[[[[2]]]]]
-atom3 [[[[[1]]]]]
-atom4 [[[[[0]]]]]
-
-# =========
-# Reduction
-# =========
-
-:test [0] atom0 = atom0
-:test [[0 1 0]] atom0 atom1 = atom1 atom0 atom1
-:test [[[[3 2 1 0]]]] atom0 atom1 atom2 atom3 = atom0 atom1 atom2 atom3
-
-# ===============
-# Random examples
-# ===============
-
-set-of-three [[[[0 1 2 3]]]]
-number-set set-of-three +1 +2 +3
-access-first [0 [[[0]]]]
-:test access-first number-set = +1
-
-# ===========
-# Combinators
-# ===========
-
-S [[[2 0 (1 0)]]]
-K [[1]]
-I [0]
-
-i [0 S K]
-
-:test I = i i
-:test K = i (i (i i))
-:test S = i (i (i (i i)))
-
-# ===============
-# Church numerals
-# ===============
-
-church-n0 [[0]]
-church-n1 [[1 0]]
-church-n2 [[1 (1 0)]]
-church-n3 [[1 (1 (1 0))]]
-church-n4 [[1 (1 (1 (1 0)))]]
-church-n5 [[1 (1 (1 (1 (1 0))))]]
-church-n6 [[1 (1 (1 (1 (1 (1 0)))))]]
-church-n7 [[1 (1 (1 (1 (1 (1 (1 0))))))]]
-church-n8 [[1 (1 (1 (1 (1 (1 (1 (1 0)))))))]]
-church-n9 [[1 (1 (1 (1 (1 (1 (1 (1 (1 0))))))))]]
-church-add [[[[3 1 (2 1 0)]]]]
-church-mul [[[2 (1 0)]]]
-church-pow [[0 1]]
-
-:test church-add church-n2 church-n3 = church-n5
-:test church-mul church-n2 church-n3 = church-n6
-:test church-pow church-n2 church-n3 = church-n8
-
-# ==================
-# Lennart
-# From Lambda-n-ways
-# ==================
-
-lnnrt-true [[0]]
-lnnrt-false [[1]]
-lnnrt-if [[[2 0 1]]]
-lnnrt-zero [[1]]
-lnnrt-succ [[[0 2]]]
-lnnrt-one lnnrt-succ lnnrt-zero
-lnnrt-two lnnrt-succ lnnrt-one
-lnnrt-three lnnrt-succ lnnrt-two
-lnnrt-const [[1]]
-lnnrt-pair [[[0 2 1]]]
-lnnrt-fst [[1 0 [[1]]]]
-lnnrt-snd [[1 0 [[0]]]]
-lnnrt-fix [[1 (0 0)] [1 (0 0)]]
-lnnrt-add lnnrt-fix [[[1 0 [lnnrt-succ (3 0 1)]]]]
-lnnrt-mul lnnrt-fix [[[1 lnnrt-zero [lnnrt-add 1 (3 0 1)]]]]
-lnnrt-fac lnnrt-fix [[0 lnnrt-one [lnnrt-mul 1 (2 0)]]]
-lnnrt-eqnat lnnrt-fix [[[1 (0 lnnrt-true (lnnrt-const lnnrt-false)) [1 lnnrt-false [4 1 0]]]]]
-lnnrt-sumto lnnrt-fix [[0 lnnrt-zero [lnnrt-add 1 (2 0)]]]
-lnnrt-n5 lnnrt-add lnnrt-two lnnrt-three
-lnnrt-n6 lnnrt-add lnnrt-three lnnrt-three
-lnnrt-n17 lnnrt-add lnnrt-n6 (lnnrt-add lnnrt-n6 lnnrt-n5)
-lnnrt-n37 lnnrt-succ (lnnrt-mul lnnrt-n6 lnnrt-n6)
-lnnrt-n703 lnnrt-sumto lnnrt-n37
-lnnrt-n720 lnnrt-fac lnnrt-n6
-
-# this test can take a minute, comment it if you're in a hurry
-:test lnnrt-eqnat lnnrt-n720 (lnnrt-add lnnrt-n703 lnnrt-n17) = lnnrt-true
-
-main [[1]]