-- tries to implement integers using fold and a generalized notion of 'reduction' instead of
-- utilizing recursion explicitly in all operations./
-- maximum (reasonable) code reuse, information hiding and conciseness is emphasized through
-- generalized mechanisms, particularly hiding the internal representation and avoiding excessive
-- pattern matchings.
-- integers are interpreted as distances from 0 on the negative or positive sides of the
-- axis. 'reducing' (`fold` and `loop`) tries to (recursively) reach `Zero` which means
-- either `suc` or `pred` depending on the sign (`bck`).
module Z

-- an integer has a sign (P or N) and a distance from 0 (the Nat part with a little quirk*)
-- *the little quirk:
-- if `P n` == +n and `N n` == -n then both `P O` (+0) and `N O` (-0) would represent 0 which is terrible
-- since this should be taken care of throughout the module so I got smart, heeded the elders
-- advice and decided to interpret n to mean n+1 in `P n` and `N n`. this way `P 0` means +1 and `N 2` means -3.
-- so far only `Cast Z Int instance`, `pred` and `suc` had to pay. other parts of the module are
-- totally agnostic to this quirk which probably means it is the right approach.
data Z = P Nat | N Nat | Zero
data Sign = pos | neg | zro

-- picks an operation and performs it on `n` according to its sign and distance from 0
-- this is a powerful abstraction since many functions could be defined over it
total match : (n : Z) -> (zero : a) -> (positive : Nat->a) -> (negative : Nat->a) -> a
match Zero zero _ _ = zero
match (P n) _ positive _ = positive n
match (N n) _ _ negative = negative n

-- same as `match` but works on Nats
-- pay attention that input (`n`) comes last here
-- because `nmatch` is used in situations that is more
-- convenient with this arrangement
total nmatch : (zero : a) -> (nonzero : Nat->a) -> (n:Nat) -> a
nmatch zero _ O = zero
nmatch  _ nonzero (S k) = nonzero k

-- move left
total pred : Z -> Z
pred n = match n (N O) (nmatch Zero P) (N . S)

-- move right
total suc : Z -> Z
suc n = match n (P O) (P . S) (nmatch Zero N)

-- converts a constant of type `a` to a function that accepts a `b` and returns an `a`
-- useful in places that expect a function but a simple value would suffice.
-- parameters `a` and `b` make this mechanism very flexible.
instance Cast a (b->a) where
    cast c = (x=>c)

-- sign of an integer
total sgn : Z -> Sign
sgn n = match n zro (cast pos) (cast neg) -- employs the above Cast to prevent writing (n=> ...)

-- distance from Zero as a positive `Z`. contrast with `match` arguments that receives the same thing as a `Nat`
total abs : Z -> Z
abs n = match n Zero P P

-- negation
total ngt : Z -> Z
ngt n = match n Zero N P

-- transforms `n` depending on its sign
-- basically `match` but passes the whole `n` instead of it's distance, effectively
-- removing duplication in such functions as `fwd` and `bck`
total caseOnSgn : (n:Z) -> (zero:a) -> (positive : Z->a) -> (negative : Z->a) -> a
caseOnSgn n zero positive negative = match n zero (positive . P) (negative . N)

-- move one number away from Zero
total fwd : Z -> Z
fwd n = caseOnSgn n Zero suc pred

-- move one number towards Zero
-- since Zero is the base case for almost all functions operating on integers, this
-- effectively defines the reducing mechanism for the whole Z as demonstrated in `fold`
total bck : Z -> Z
bck n = caseOnSgn n Zero pred suc

-- folding from Zero towards `n`
-- uses `bck` instead of explicit pattern matching on `n` thus eliminating
-- duplication , resulting in a more point-free style implementation
%assert_total
total fold : (i : Z) -> (f: Z->Z->Z) -> (n:Z) -> Z
fold i _ Zero = i
fold i f n = let acc = fold i f (bck n) in f acc n -- `acc` introduced for clarity

-- like fold but ignores the index
-- useful in situations where the intermediate indices are irrelevant (`add`)
loop : (i:Z) -> (f:Z->Z) -> (n:Z) -> Z
loop i f n = fold i (acc,index=>f acc) n -- just discards the `index`

-- addition
-- very simple and expressive interpretation of addition
-- m+n means :
-- moving `n` units to the right from `m` if `n` is positive
-- moving `n` units to the left from `m` if `n` is negative
-- or just `m` if `n` is Zero
add : Z -> Z -> Z
add n m = caseOnSgn m n (loop n suc) (loop n pred) -- `suc` : move to the right, `pred` : move to the left

-- subtraction
-- n-m = n + (-m)
sub : Z -> Z -> Z
sub n m = add n (ngt m)

instance Cast Z Int where
    cast Zero = 0
    cast (P k) = cast {to=Int} (S k) -- (S k) => the little quirk, see definition of `Z`
    cast (N k) = -1 * cast {to=Int} (S k)

instance Show Z where
    show n = show $ cast {to=Int} n

instance Show Sign where
    show zro = "0"
    show pos = "+"
    show neg = "-"