-- 2. Natural numbers

module IType.Nat where

-- Unary natural numbers, you can get access
-- to decimal notation 
-- and machine arithmetic 
-- by using "builtin" numbers (below)

data Nat : Set where
  zero : Nat
  succ : Nat → Nat

one = succ zero
two = succ one

pred : Nat → Nat
pred zero = zero
pred (succ n) = n

-- We define + and * by primitive recursion:

_+_ : Nat → Nat → Nat
m + zero     = m
m + (succ n) = succ (m + n)

_*_ : Nat → Nat → Nat
m * zero   = zero
m * succ n = m + (m * n)

-- ^C^C in the hole to refine a pattern

_-_ : Nat → Nat → Nat
zero - n = zero
succ m - zero = succ m
succ m - succ n = m - n

-- Decimal notation by "built in" natural numbers: 

{-# BUILTIN NATURAL Nat #-}

ten : Nat
ten = 10

-- Binary machine arithmetic for + and *:

{-# BUILTIN NATPLUS _+_ #-}

-- ^C^N 3 + 7

-- {-# BUILTIN NATTIMES _*_ #-}

-- There are many other built-in types:
-- (integers, floats, strings, characters) 

-- An example of how to compute by reduction: ^C-^N
--   one * one 
-- = one * succ zero
-- = one + one * zero
-- = one + zero
-- = one 

-- We can declare precedences and associations in Agda.
-- + and * are both infix operations which associate to the left
-- * binds harder than +:

infixl 60 _+_
infixl 70 _*_

-- Thus x + y + z parses as (x + y) + z

f : Nat → Nat → Nat → Nat
f x y z = x + y + z


-- the primitive recursion combinator
-- is a polymorphic higher order function:

natrec : {X : Set} -> X -> (Nat -> X -> X) -> Nat -> X
natrec base step zero     = base
natrec base step (succ n) = step n (natrec base step n)

-- Given a base case base : X and a step function step : Nat -> X -> X, 
-- we can define a function from
-- n : Nat to X by induction (primitive recursion) on the number n!

_+‘_ : Nat → Nat → Nat
m +‘ n = natrec m (λ _ x → succ x) n

-- Gödel system T is simply typed lambda calculus with Nat, zero, succ, and natrec
-- a programming language where all programs terminate. 
-- Agda is a more expressive language where all programs 
-- terminate

-- If we try to write a non-terminating program:

-- loop : Nat → Nat
-- loop x = loop x

-- Then Agda's termination checker will protest and colour the culprit in light salmon.
-- Note that Agda's termination checker will reject some terminating programs.

-- Exercises. Define exponential, factorial, ackerman-peter function (wikipedia)
-- http://en.wikipedia.org/wiki/Primitive_recursive_function gives a number of primitive recursive functions

-- what does the termination checker do to see that ack terminates? lexicographic ordering

iter : {X : Set} → (X → X) → X → Nat → X
iter f a zero = a
iter f a (succ n) = f (iter f a n)

h : (Nat → Nat) → Nat → Nat
-- h f zero = f 1
-- h f (succ n) = f (h f n)
-- h f = natrec (f 1) (λ x y → f y)
h f = iter f (f one)

ack : Nat → Nat → Nat
-- ack zero = succ 
-- ack (succ m) = h (ack m)
-- ack = natrec succ (λ x y → h y)
ack = iter h succ

-- In Gödel's T we can write primitive recursive functions, and functionals. A challenge is division