# MIT License, Copyright (c) 2024 Marvin Borner
# see "on the representation of data in lambda-calculus" (Parigot 1989)
# has a "one-step" predecessor *and* addition function

# Compared to unary/church, they're also faster in many reducers

:import std/Combinator .
:import std/Logic .

# zero Parigot number
zero i ⧗ Parigot

# returns true if Parigot number is zero
zero? [0 [true] [false]] ⧗ Parigot → Boolean

=?‣ zero?

:test (=?zero) (true)
:test (=?[[0 1]]) (false)
:test (=?[[0 [0 2]]]) (false)

# increments Parigot number
inc q''' ⧗ Parigot → Parigot

++‣ inc

:test (++zero) ([[0 1]])
:test (++[[0 1]]) ([[0 [0 2]]])

# decrements Parigot number
dec r i ⧗ Parigot → Parigot

--‣ dec

:test (--(++zero)) (zero)
:test (--[[0 [0 2]]]) ([[0 1]])

# decrements Parigot number with `dec 0 = 0`
dec' [0 [[[0]]] [[0]] [1 0 [0]]] ⧗ Parigot → Parigot

# adds two Parigot numbers
add b ⧗ Parigot → Parigot → Parigot

…+… add

:test (add (inc (zero)) (inc (inc zero))) (inc (inc (inc zero)))

# multiplies two Parigot numbers
# [[iter zero (add 1) 0]]
mul [[[1 [[[0]]] 0 0] [[[4 (2 1 1 0)]]]]] ⧗ Parigot → Parigot → Parigot

…⋅… mul

:test ((inc zero) ⋅ zero) (zero)
:test ((inc zero) ⋅ (inc (inc zero))) (inc (inc zero))
:test ((inc (inc (inc zero))) ⋅ (inc (inc zero))) (inc (inc (inc (inc (inc (inc zero))))))

# subtracts two Parigot numbers
# will not give correct results when b>a in a-b (use sub' then)
# [[iter 1 dec 0]]
sub [[[1 [[4]] 0 0] [[[2 1 1 0 [0]]]]]] ⧗ Parigot → Parigot → Parigot

…-… sub

:test ((inc zero) - zero) (inc zero)
:test ((inc (inc (inc zero))) - (inc zero)) (inc (inc zero))

# subtracts two Parigot numbers such that a-b=0 if b>a
sub' [[[0 [[3]] 2 2]]] [[dec' (1 0 0)]] ⧗ Parigot → Parigot → Parigot

…-*… sub'

:test ((inc zero) -* zero) (inc zero)
:test ((inc (inc (inc zero))) -* (inc zero)) (inc (inc zero))
:test ((inc zero) -* (inc (inc zero))) (zero)

# returns true if Parigot number is greater than other Parigot number
gt? not! ∘∘ (zero? ∘∘ sub') ⧗ Parigot → Parigot → Parigot

iter [[[0 ι ρ ρ]]] ⧗ a → (a → a) → Parigot → a
	ρ [[3 (1 0 0)]]
	ι [[4]]

:test (iter zero inc (inc (inc (inc zero)))) (inc (inc (inc zero)))

rec [[[0 ι ρ ρ --0]]] ⧗ Parigot → (Parigot → Boolean) → Parigot → Parigot
	ρ [[[4 0 (2 1 1)]]]
	ι [[[5]]]