{- 
  Computer Aided Formal Reasoning (G53CFR, G54CFR)
  Thorsten Altenkirch

  Lecture 2: A first taste of Agda

  In this lecture we start to explore the Agda system, a functional
  programming language based on Type Theory. We start with some
  ordinary examples which we could have developed in Haskell as well. 
-}

module l02 where

module myNat where

  {- Agda has no automatically loaded prelude. Hence we can start from
     scratch and define the natural numbers. Later we will use the
     standard libray. -}
  
  data ℕ : Set where -- to type ℕ we type \bn 
    zero : ℕ
    suc : (m : ℕ) → ℕ -- \-> or \to

  {- To process an Agda file we use C-c C-c from emacs. Once Agda has
     checked the file the type checker also colours the different
     symbols. -}

  {- We define addition. Note Agda's syntax for mixfix operations. The
     arguments are represented by _s -}

  _+_ : ℕ → ℕ → ℕ
  zero + n = n
  suc m + n = suc (m + n)

  {- Try to evaluate: (suc (suc zero)) + (suc (suc zero))
     by typing in C-c C-n -}

{- Better we import the library definition of ℕ
   This way we can type 2 instead of (suc (suc zero))
-}
  
open import Data.Nat

{- We define Lists :  -}

data List (A : Set) : Set where
  [] : List A
  _∷_ : (a : A) → (as : List A) → List A

{- In future we'll use 
     open import Data.List -}

{- declare the fixity of ∷ (type \::) -}

infixr  _∷_

{- Two example lists -}

l1 : List ℕ
l1 =  ∷  ∷  ∷ []

l2 : List ℕ
l2 =  ∷  ∷ []

{- implementing append (++) -}

_++_ : {A : Set} → List A → List A → List A
[] ++ bs = bs
(a ∷ as) ++ bs = a ∷ (as ++ bs)

{- Note that Agda checks wether a function is terminating.
   If we type
   (a ∷ as) ++ bs = (a ∷ as) ++ bs
   in the 2nd line Agda will complain by coloring the offending 
   function calls in red.
-}

{- What does the following variant of ++ do ? -}

_++'_ : {A : Set} → List A → List A → List A
as ++' [] = as
as ++' (b ∷ bs) = (b ∷ as) ++' bs

{- Indeed it can be used to define reverse.  This way to implement
   reverse is often called fast reverse because it is "tail recursive"
   which leads to a more efficient execution than the naive
   implementation. -}

rev : {A : Set} → List A → List A
rev as = [] ++' as

{- We tried to define a function which accesses the nth element of a list:

_!!_ : {A : Set} → List A → ℕ → A
[] !! n = {!!}
(a ∷ as) !! zero = a
(a ∷ as) !! suc n = as !! n

  but there is no way to complete the first line (consider what happens
  if A is the empty type!  
-}

{- To fix this we handle errors explicitely, using Maybe -}

open import Data.Maybe

{- This version of the function can either return an element of the list 
    (just a) or an error (nothing).
-}
_!!_ : {A : Set} → List A → ℕ → Maybe A
[] !! n = nothing
(a ∷ as) !! zero = just a
(a ∷ as) !! suc n = as !! n