More examples

1 files changed, 83 insertions, 71 deletions

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]]]