module Records where

-- Recall the way a datatype definition works:
data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ -> ℕ -> ℕ
_+_ = {!!}

data Bool : Set where
  false : Bool
  true : Bool

postulate String : Set
{-# BUILTIN STRING String #-}

module Tuples-as-Datatypes where

  -- A special case arises when we have just one constructor.

  -- The type of triples of natural numbers.
  data Triple : Set where
    triple : ℕ -> ℕ -> ℕ -> Triple
  
  -- The type of quadruples of two natural numbers and two booleans.
  data Quadruple : Set where
    quad : ℕ -> ℕ -> Bool -> Bool -> Quadruple
  
  module Examples where
  
    my-triple : Triple
    my-triple = triple zero zero zero
  
    my-quad : Quadruple
    my-quad = quad zero zero true false

module Tuples-as-Records where

  -- A record is a better way to define these tuple types.
  record Triple : Set where
    field
      fst : ℕ
      snd : ℕ
      thd : ℕ
  
  my-triple : Triple
  my-triple = record { fst = zero; snd = zero; thd = zero }

  record Person : Set where
    field
      name : String
      age : ℕ
      has-drivers-license : Bool

  selinger : Person
  selinger = record { name = "Selinger"; age = 50; has-drivers-license = true }

  -- A record come with "accessor functions". In the case of the
  -- Person record, they are:
  --
  -- Person.name : Person -> String
  -- Person.age : Person -> ℕ
  -- Person.has-drivers-license : Person -> Bool
  --
  -- Every time we define a record in Agda, it will automatically
  -- create module for the record. This is called a "record module".

  module My-People where

    open Person
  
    my-name : String
    my-name = name selinger
  
    my-name2 : String
    my-name2 = selinger .name
  
  record Animal : Set where
    constructor animal
    field
      name : String
      age : ℕ
      species : String

  vanilla : Animal
  vanilla = record { name = "Vanilla"; age = 1; species = "Chicken" }

  module MyAnimals where

    -- Record modules can be opened, like any other module.
    open Animal
  
    -- Records can also be defined by "copatterns".
    rosie : Animal
    Animal.name rosie = "Rosie"
    Animal.age rosie = 1
    Animal.species rosie = "Chicken"
  
    honey : Animal
    name honey = "Honey"
    age honey = 1
    species honey = "Chicken"
  
    marley : Animal
    marley .name = "Marley"
    marley .age = 2
    marley .species = "Cat"
  
    macey : Animal
    macey .Animal.name = "Macey"
    macey .Animal.age = 2
    macey .Animal.species = "Cat"
  
    ellen : Animal
    ellen = animal "Ellen" 0 "Hamster"

  module Delta-module where
    name : String
    name = "Delta"

    age : ℕ
    age = 0

    species : String
    species = "Bettafish"

    memo : String
    memo = "Delta is red"

  -- A record can be initialized from a module
  delta : Animal
  delta = record { Delta-module }

  -- A record can be initialized from another record.
  gamma : Animal
  gamma = record delta { name = "Gamma" }

module Pair-old where

  data Pair (A B : Set) : Set where
    _,_ : A -> B -> Pair A B

  fst : ∀ {A B} -> Pair A B -> A
  fst (a , b) = a

  snd : ∀ {A B} -> Pair A B -> B
  snd (a , b) = b

  sum-pair : Pair ℕ ℕ -> ℕ
  sum-pair (a , b) = a + b

module Pair-new where

  record Pair (A B : Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B

  sum-pair : Pair ℕ ℕ -> ℕ
  sum-pair (a , b) = a + b