{-

  Now records.

-}

module Records where

open import Data.Unit using (⊤; tt)
open import Data.Bool

-- Records are just Σ-types. So here's Σ:

record Σ (A : Set)(B : A → Set) : Set where
  field
    fst : A
    snd : B fst

-- Building record values
ex : Σ Bool T
ex = record { fst = true; snd = tt }

{-

  What about accessing the fields?

  There are two ways one might want to do this:

    • Projection, for instance using projection functions

        fst : ∀ {A B} → Σ A B → A
        snd : ∀ {A B}(p : Σ A B) → B (fst p)

    • Opening, given p : Σ A B we might want to open p to get

        fst : A
        snd : B fst

  Using the module system we can get both!

  For each record you get a parameterized module
  containing projection functions:

  record R : Set where
    field
      x₁ : A₁
      x₂ : A₂ [x₁]
      ...
      xn : An [x₁..xn-1]

  module R (r : R) where
    x₁ : A₁
    x₂ : A₂ [x₁]
    ...
    xn : An [x₁..xn-1]

-}

-- Doing C-c C-o Σ to see the contents of the Σ module gives us:
-- Modules
-- Names
--   fst : {A : Set} {B : A → Set} → Σ A B → A
--   snd : {A : Set} {B : A → Set} (r : Σ A B) → B (Σ.fst r)

-- We can also instantiate it to a particular record value:
open Σ ex renaming (fst to x; snd to y)
-- now  x = true : Bool  and
--      y = tt   : ⊤

-- Let's return to the sort example.

-- We can pack up a set and a comparison function
-- in a Poset record.

record Poset : Set₁ where
  field
    A   : Set
    _≤_ : A → A → Bool

  -- Definitions inside a record go in the record module.
  _≥_ : A → A → Bool
  x ≥ y = y ≤ x

  op : Poset
  op = record { _≤_ = _≥_ }

-- C-c C-o Poset gives us
-- Modules
-- Names
--   _≤_ : (r : Poset) → Poset.A r → Poset.A r → Bool
--   _≥_ : (r : Poset) → Poset.A r → Poset.A r → Bool
--   A   : Poset → Set
--   op  : (r : Poset) → Poset

open import Data.List

-- Our sort module is now parameterized on a Poset record (not the module).
module Sort (P : Poset) where

  -- This is a good example of where opening a record is really nice.
  open Poset P

  insert : A → List A → List A
  insert y [] = y ∷ []
  insert y (x ∷ xs) =
    if y ≤ x then y ∷ x ∷ xs
             else x ∷ insert y xs

  sort : List A → List A
  sort []       = []
  sort (x ∷ xs) = insert x (sort xs)

open import Nat

NAT : Poset
NAT = record { _≤_ = _≤_ } -- the A field can be inferred from _≤_

-- We now instantiate with the NAT poset.
open Sort NAT

-- Now sort : List ℕ → List ℕ

xs =  ∷  ∷  ∷  ∷  ∷ []

test₁ = sort xs