More examples

4 files changed, 185 insertions, 124 deletions

diff --git a/README.md b/README.md
index 5f348d6..edfd3d6 100644
--- a/README.md
+++ b/README.md
@@ -3,6 +3,8 @@
 A purely academic programming language based on lambda calculus and De
 Bruijn indices written in Haskell.
 
+[Jump to examples](#Examples)
+
 ## Features
 
 -   De Bruijn indices\[0\] eliminate the complexity of α-equivalence and
@@ -34,19 +36,19 @@ You can read more about De Bruijn indices on
 
 ### Syntax
 
-In general the syntax is pretty similar to the previously presented
-normal lambda calculus syntax with De Bruijn indices.
+In general the syntax of bruijn is pretty similar to the previously
+presented normal lambda calculus syntax with De Bruijn indices.
 
 You can use any function that you’ve previously defined. You can also
 overwrite previously defined functions. The environment gets interpreted
-from bottom to top.
+from bottom to top (starting at `main`).
 
 The following are the main syntax specifications in the (minorly
 extended) [Backus-Naur
 form](https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form).
 Additional spaces are optional but allowed.
 
-    <identifier>  ::= [a-ω,A-Ω,_][a-ω,A-Ω,0-9,?,!,',_]*
+    <identifier>  ::= [a-ω,A-Ω,_][a-ω,A-Ω,0-9,?,!,',-]*
     <abstraction> ::= "[" <expression> "]"
     <numeral>     ::= ("+" | "-")[0-9]+
     <bruijn>      ::= [0-9]
@@ -73,6 +75,19 @@ mandatory.
     <definition> ::= <identifier> = <expression>
     <line>       ::= <definition> | <expression> | <comment> | <import> | <test> | "\n"
 
+### Numerals
+
+Numbers in bruijn always have a sign in front of them or else they will
+be mistaken for De Bruijn indices. Generally the decimal representation
+is only syntactic sugar for its internal balanced ternary
+representation. We use balanced ternary because it’s a great compromise
+between performance and size (according to \[1\]).
+
+You don’t have to care about the internal side too much though, if you
+use the included operations from the standard library. The REPL even
+tries its best at displaying expressions that look like ternary numbers
+as decimal numbers in paranthesis next to it.
+
 ### Standard library
 
 You may want to use the included standard library to reach your
@@ -83,7 +98,19 @@ You can import it from `std.bruijn` using `:import std`.
 
 ### Examples
 
-Plain execution
+You can try these by experimenting in the REPL or by running them as a
+file. Note, however, that you need an equal sign between the function
+name and its definition if you’re using the REPL.
+
+Plain execution:
+
+    # this is a comment
+    # we now define a function returning a ternary 1
+    get-one +1
+
+    # we can use the function in all functions below its definition
+    get-one2 get-one
+    :test get-one2 = +1
 
     # equivalent of λx.x
     id [0]
@@ -91,30 +118,43 @@ Plain execution
     # equivalent of (λx.x) (λx.λy.x) = λx.λy.x
     :test id [[1]] = [[1]]
 
+    # multiple arguments
+    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
+
     # endless loop using omega combinator
     om [0 0]
     nom om
     main om nom
 
-Using standard library
+    # you may have realized you can't easily operate with numbers
+    # or anything else really without writing crazy functions
+    # -> luckily the standard library defines many standard operations!
 
-    :import std
+Using standard library:
 
-    # equivalent of (λx.x) (λx.λy.x) = λx.λy.x
-    outer id [[1]]
-    :test outer = [[1]]
+    :import std
 
-    # pairs
+    # pairs with some values
     me [[[1]]]
     you [[[2]]]
     love pair me you
     :test fst love = me
     :test snd love = you
 
+    # numerical operations
+    five pred (sub (add +8 -4) -2)
+    not-five? [if (eq? 0 +5) false true]
+    :test not-five? five = false
+
     # boolean
     main not (or (and false true) true)
     :test main = [0]
 
+    # read the std.bruijn file for an overview of all functions
+
 ### Compilation to BLC
 
 You can compile bruijn to John Tromp’s BLC\[2\]\[3\]. Only the used
diff --git a/src/Parser.hs b/src/Parser.hs
index 29f40b9..dc6951a 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -24,7 +24,7 @@ symbol = L.symbol sc
 
 identifier :: Parser String
 identifier = lexeme
-  ((:) <$> (letterChar <|> char '_') <*> many (alphaNumChar <|> oneOf "?!'_"))
+  ((:) <$> (letterChar <|> char '_') <*> many (alphaNumChar <|> oneOf "?!'_-"))
 
 parens :: Parser a -> Parser a
 parens = between (symbol "(") (symbol ")")
diff --git a/std.bruijn b/std.bruijn
index 377ba8c..22f7fae 100644
--- a/std.bruijn
+++ b/std.bruijn
@@ -48,20 +48,20 @@ zero? [0 T [F] [F] I]
 :test zero? +1 = F
 :test zero? +42 = F
 
-upNeg [[[[[2 (4 3 2 1 0)]]]]]
-:test upNeg +0 = -1
-:test upNeg -1 = -4
-:test upNeg +42 = +125
+up-neg [[[[[2 (4 3 2 1 0)]]]]]
+:test up-neg +0 = -1
+:test up-neg -1 = -4
+:test up-neg +42 = +125
 
-upPos [[[[[1 (4 3 2 1 0)]]]]]
-:test upPos +0 = +1
-:test upPos -1 = -2
-:test upPos +42 = +127
+up-pos [[[[[1 (4 3 2 1 0)]]]]]
+:test up-pos +0 = +1
+:test up-pos -1 = -2
+:test up-pos +42 = +127
 
-upZero [[[[[0 (4 3 2 1 0)]]]]]
-:test upZero +0 = [[[[0 3]]]]
-:test upZero +1 = +3
-:test upZero +42 = +126
+up-zero [[[[[0 (4 3 2 1 0)]]]]]
+:test up-zero +0 = [[[[0 3]]]]
+:test up-zero +1 = +3
+:test up-zero +42 = +126
 
 up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
 # TODO: up is incorrect
@@ -71,20 +71,20 @@ negate [[[[[4 3 1 2 0]]]]]
 :test negate -1 = +1
 :test negate +42 = -42
 
-tritNeg [[[2]]]
-tritPos [[[1]]]
-tritZero [[[0]]]
-lst [0 tritZero [tritNeg] [tritPos] [tritZero]]
-:test lst +0 = tritZero
-:test lst -1 = tritNeg
-:test lst +1 = tritPos
-:test lst +42 = tritZero
-
-_stripZ pair +0 T
-_stripANeg [0 [[pair (upNeg 1) F]]]
-_stripAPos [0 [[pair (upPos 1) F]]]
-_stripAZero [0 [[pair (0 +0 (upZero 1)) 0]]]
-strip [fst (0 _stripZ _stripANeg _stripAPos _stripAZero)]
+trit-neg [[[2]]]
+trit-pos [[[1]]]
+trit-zero [[[0]]]
+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
+
+_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
@@ -94,11 +94,11 @@ strip [fst (0 _stripZ _stripANeg _stripAPos _stripAZero)]
 # in comparison to their implementation, yet the order of neg/pos/zero is
 # the same. Something's weird.
 
-_succZ pair +0 +1
-_succNeg [0 [[pair (upNeg 1) (upZero 1)]]]
-_succZero [0 [[pair (upZero 1) (upPos 1)]]]
-_succPos [0 [[pair (upPos 1) (upNeg 0)]]]
-succ [snd (0 _succZ _succNeg _succPos _succZero)]
+_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
@@ -106,11 +106,11 @@ ssucc [strip (succ 0)]
 :test succ (succ (succ (succ (succ +0)))) = +5
 :test succ +42 = +43
 
-_predZ pair +0 -1
-_predNeg [0 [[pair (upNeg 1) (upPos 0)]]]
-_predZero [0 [[pair (upZero 1) (upNeg 1)]]]
-_predPos [0 [[pair (upPos 1) (upZero 1)]]]
-pred [snd (0 _predZ _predNeg _predPos _predZero)]
+_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
@@ -118,50 +118,62 @@ spred [strip (pred 0)]
 :test spred +1 = +0
 :test pred +42 = +41
 
-_absNeg [[[[[2 4]]]]]
-_absPos [[[[[1 4]]]]]
-_absZero [[[[[0 4]]]]]
-abstractify [0 [[[[3]]]] _absNeg _absPos _absZero]
+_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 [upNeg ([3 3 0] 0)] [upPos ([3 3 0] 0)] [upZero ([3 3 0] 0)]]]
+_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
 
-_eqZ [zero? (normalize 0)]
-_eqNeg [[0 F [2 0] [F] [F]]]
-_eqPos [[0 F [F] [2 0] [F]]]
-_eqZero [[0 (1 0) [F] [F] [2 0]]]
-_eqAbs [0 _eqZ _eqNeg _eqPos _eqZero]
-eq [[_eqAbs 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
+_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
-_addZ [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]]
-_addC [[1 0 tritZero]]
-_addBNeg2 [1 (upZero (3 0 tritNeg)) (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero))]
-_addBNeg [1 (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero)) (upZero (3 0 tritZero))]
-_addBZero [up 1 (3 0 tritZero)]
-_addBPos [1 (upZero (3 0 tritZero)) (upPos (3 0 tritZero)) (upNeg (3 0 tritPos))]
-_addBPos2 [1 (upPos (3 0 tritZero)) (upNeg (3 0 tritPos)) (upZero (3 0 tritPos))]
-_addANeg [[[1 (_addBNeg 1) _addBNeg2 _addBNeg _addBZero]]]
-_addAZero [[[1 (_addBZero 1) _addBNeg _addBZero _addBPos]]]
-_addAPos [[[1 (_addBPos 1) _addBZero _addBPos _addBPos2]]]
-_addAbs [_addC (0 _addZ _addANeg _addAZero _addAPos)]
-add [[_addAbs 1 (abstractify 0)]]
+_add-z [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]]
+_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-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 [[_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
 
 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
 
 # ===============
 # Boolean algebra
@@ -177,10 +189,10 @@ if [[[2 1 0]]]
 # Church numerals
 # ===============
 
-churchZero [[0]]
-churchSucc [[[1 (2 1 0)]]]
-churchAdd [[[[3 1 (2 1 0)]]]]
-churchMul [[[2 (1 0)]]]
-churchExp [[0 1]]
+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]]]
diff --git a/test.bruijn b/test.bruijn
index a846bd4..24a0083 100644
--- a/test.bruijn
+++ b/test.bruijn
@@ -12,6 +12,15 @@ atom4 [[[[[0]]]]]
 :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
 # ===========
@@ -30,55 +39,55 @@ i [0 S K]
 # Church numerals
 # ===============
 
-chrch_n0 [[0]]
-chrch_n1 [[1 0]]
-chrch_n2 [[1 (1 0)]]
-chrch_n3 [[1 (1 (1 0))]]
-chrch_n4 [[1 (1 (1 (1 0)))]]
-chrch_n5 [[1 (1 (1 (1 (1 0))))]]
-chrch_n6 [[1 (1 (1 (1 (1 (1 0)))))]]
-chrch_n7 [[1 (1 (1 (1 (1 (1 (1 0))))))]]
-chrch_n8 [[1 (1 (1 (1 (1 (1 (1 (1 0)))))))]]
-chrch_n9 [[1 (1 (1 (1 (1 (1 (1 (1 (1 0))))))))]]
-chrch_add [[[[3 1 (2 1 0)]]]]
-chrch_mul [[[2 (1 0)]]]
-chrch_pow [[0 1]]
+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 chrch_add chrch_n2 chrch_n3 = chrch_n5
-:test chrch_mul chrch_n2 chrch_n3 = chrch_n6
-:test chrch_pow chrch_n2 chrch_n3 = chrch_n8
+: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
+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
+:test lnnrt-eqnat lnnrt-n720 (lnnrt-add lnnrt-n703 lnnrt-n17) = lnnrt-true
 
 main [[1]]