Tests

1 files changed, 31 insertions, 32 deletions

diff --git a/std.bruijn b/std.bruijn
index 16d851a..a27dabb 100644
--- a/std.bruijn
+++ b/std.bruijn
@@ -15,9 +15,18 @@ Y [[1 (0 0)] [1 (0 0)]]
 Θ [[0 (1 1 0)]] [[0 (1 1 0)]]
 i [0 S K]
 
-# =======
+# =====
+# Pairs
+# =====
+
+pair [[[0 2 1]]]
+fst [0 T]
+snd [0 F]
+
+# ===================================
 # Ternary
-# =======
+# According to works of T.Æ. Mogensen
+# ===================================
 
 zero? [0 T [F] I [F]]
 upNeg [[[[[2 (4 3 2 1 0)]]]]]
@@ -30,13 +39,26 @@ negate [[[[[4 3 0 1 2]]]]]
 tritNeg [[[2]]]
 tritZero [[[1]]]
 tritPos [[[0]]]
+lst [0 tritZero [tritNeg] [tritZero] [tritPos]]
+
+_succZ (pair +0 +1)
+_succANeg [0 [[[pair (upNeg 2) (upZero 2)]]]]
+_succAZero [0 [[[pair (upZero 2) (upPos 2)]]]]
+_succAPos [0 [[[pair (upPos 2) (upNeg 1)]]]]
+succ [snd (0 _succZ _succANeg _succAZero _succAPos)]
+
+_predZ (pair +0 -1)
+_predANeg [0 [[[pair (upNeg 2) (upPos 1)]]]]
+_predAZero [0 [[[pair (upZero 2) (upNeg 2)]]]]
+_predAPos [0 [[[pair (upPos 2) (upZero 2)]]]]
+pred [snd (0 _predZ _predANeg _predAZero _predAPos)]
 
 _absNeg [[[[[2 4]]]]]
 _absZero [[[[[1 4]]]]]
 _absPos [[[[[0 4]]]]]
 abstractify [0 [[[[3]]]] _absNeg _absZero _absPos]
 
-_normalize [[0 [ +0 ] [[upNeg (1 1 0)]] [[upZero (1 1 0)]] [[upPos (1 1 0)]] 0]]
+_normalize [[0 [ +0 ] [[upNeg (1 1 0)]] [[upZero (1 1 0)]] [[upPos (1 1 0)]] 1]]
 normalize ω _normalize
 
 _eqZero? [zero? (normalize 0)]
@@ -46,24 +68,9 @@ _eqPos [[0 F [F] [F] [2 0]]]
 _eqAbs [0 _eqZero? _eqNeg _eqZero _eqPos]
 eq [[_eqAbs 1 (abstractify 0)]]
 
-proj22 [0 [[0]]]
-tuple [[[0 1 2]]]
-
-_succZ (tuple +0 +1)
-_succANeg [0 [[[tuple (upNeg 2) (upZero 2)]]]]
-_succAZero [0 [[[tuple (upZero 2) (upPos 2)]]]]
-_succAPos [0 [[[tuple (upPos 2) (upNeg 1)]]]]
-succ [proj22 (0 _succZ _succANeg _succAZero _succAPos)]
-
-_predZ (tuple +0 -1)
-_predANeg [0 [[[tuple (upNeg 2) (upPos 1)]]]]
-_predAZero [0 [[[tuple (upZero 2) (upNeg 2)]]]]
-_predAPos [0 [[[tuple (upPos 2) (upZero 2)]]]]
-pred [proj22 (0 _predZ _predANeg _predAZero _predAPos)]
-
 _addZ [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]]
 _addC [[1 0 tritZero]]
-_addBNeg2 [1 (upZero (3 0 tritNeg)) (upPos (3 0 tritZero)) (upNeg (3 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))]
@@ -76,14 +83,6 @@ add [[_addAbs 1 (abstractify 0)]]
 
 sub [[add 1 (negate 0)]]
 
-# =====
-# Pairs
-# =====
-
-pair [[[0 2 1]]]
-fst [0 T]
-snd [0 F]
-
 # ===============
 # Boolean algebra
 # ===============
@@ -98,10 +97,10 @@ if [[[2 1 0]]]
 # Church numerals
 # ===============
 
-zero [[0]]
-succ [[[1 (2 1 0)]]]
-add [[[[3 1 (2 1 0)]]]]
-mul [[[2 (1 0)]]]
-exp [[0 1]]
+churchZero [[0]]
+churchSucc [[[1 (2 1 0)]]]
+churchAdd [[[[3 1 (2 1 0)]]]]
+churchMul [[[2 (1 0)]]]
+churchExp [[0 1]]
 
 main I F