module 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

-- Without machine arithmetic we have to 
-- 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)

-- An example of how to compute by reduction:
--   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

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

{-# BUILTIN NATURAL Nat #-}

-- Binary machine arithmetic for + and *:

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

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

-- the primitive recursion combinator (look at LambdaNotation.agda first)
-- 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!

_+‘_ : 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.

-- 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. No termination checker could:
-- as Turing proved the halting problem is not computable!