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

# =================
# Alternative names
# =================

true T
false F
id I

# =====
# Pairs
# =====

pair [[[0 2 1]]]
fst [0 T]
snd [0 F]

:test fst (pair [[0]] [[1]]) = [[0]]
:test snd (pair [[0]] [[1]]) = [[1]]

# TODO: contract-like type-checking
#       like: `+ ... : [[[[# 3]]]]`

# ===================================
# Ternary
# According to works of T.Æ. Mogensen
# ===================================

zero? [0 T [F] [F] I]
:test zero? +0 = T
:test zero? -1 = F
: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

upPos [[[[[1 (4 3 2 1 0)]]]]]
:test upPos +0 = +1
:test upPos -1 = -2
:test upPos +42 = +127

upZero [[[[[0 (4 3 2 1 0)]]]]]
:test upZero +0 = [[[[0 3]]]]
:test upZero +1 = +3
:test upZero +42 = +126

up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
# TODO: up is incorrect

negate [[[[[4 3 1 2 0]]]]]
:test negate +0 = +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)]
: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.

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

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

_absNeg [[[[[2 4]]]]]
_absPos [[[[[1 4]]]]]
_absZero [[[[[0 4]]]]]
abstractify [0 [[[[3]]]] _absNeg _absPos _absZero]
: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 ω _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

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

sub [[add 1 (negate 0)]]

# ===============
# Boolean algebra
# ===============

not [0 F T]
and [[1 0 F]]
or [[1 T 0]]
xor [[1 (not 0) 0]]
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]]

main [[[0 2 1]]]