------------------------------------------------------------------------
-- The Agda standard library
--
-- Record types with manifest fields and "with", based on Randy
-- Pollack's "Dependently Typed Records in Type Theory"
------------------------------------------------------------------------

-- For an example of how this module can be used, see README.Record.

{-# OPTIONS --cubical-compatible --safe #-}

open import Data.Bool.Base using (true; false; if_then_else_)
open import Data.Empty
open import Data.List.Base
open import Data.Product.Base hiding (proj₁; proj₂)
open import Data.Unit.Polymorphic
open import Function.Base using (id; _∘_)
open import Level
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Decidable

-- The module is parametrised by the type of labels, which should come
-- with decidable equality.

module Data.Record {ℓ} (Label : Set ℓ) (_≟_ : Decidable {A = Label} _≡_) where

------------------------------------------------------------------------
-- A Σ-type with a manifest field

-- A variant of Σ where the value of the second field is "manifest"
-- (given by the first).

infix  _,

record Manifest-Σ {a b} (A : Set a) {B : A → Set b}
                  (f : (x : A) → B x) : Set a where
  constructor _,
  field proj₁ : A

  proj₂ : B proj₁
  proj₂ = f proj₁

------------------------------------------------------------------------
-- Signatures and records

mutual

  infixl  _,_∶_ _,_≔_

  data Signature s : Set (suc s ⊔ ℓ) where
    ∅     : Signature s
    _,_∶_ : (Sig : Signature s)
            (ℓ : Label)
            (A : Record Sig → Set s) →
            Signature s
    _,_≔_ : (Sig : Signature s)
            (ℓ : Label)
            {A : Record Sig → Set s}
            (a : (r : Record Sig) → A r) →
            Signature s

  -- Record is a record type to ensure that the signature can be
  -- inferred from a value of type Record Sig.

  record Record {s} (Sig : Signature s) : Set s where
    eta-equality
    inductive
    constructor rec
    field fun : Record-fun Sig

  Record-fun : ∀ {s} → Signature s → Set s
  Record-fun ∅             = ⊤
  Record-fun (Sig , ℓ ∶ A) =          Σ (Record Sig) A
  Record-fun (Sig , ℓ ≔ a) = Manifest-Σ (Record Sig) a

------------------------------------------------------------------------
-- Labels

-- A signature's labels, starting with the last one.

labels : ∀ {s} → Signature s → List Label
labels ∅             = []
labels (Sig , ℓ ∶ A) = ℓ ∷ labels Sig
labels (Sig , ℓ ≔ a) = ℓ ∷ labels Sig

-- Inhabited if the label is part of the signature.

infix  _∈_

_∈_ : ∀ {s} → Label → Signature s → Set
ℓ ∈ Sig =
  foldr (λ ℓ′ → if does (ℓ ≟ ℓ′) then (λ _ → ⊤) else id) ⊥ (labels Sig)

------------------------------------------------------------------------
-- Projections

-- Signature restriction and projection. (Restriction means removal of
-- a given field and all subsequent fields.)

Restrict : ∀ {s} (Sig : Signature s) (ℓ : Label) → ℓ ∈ Sig →
           Signature s
Restrict ∅              ℓ ()
Restrict (Sig , ℓ′ ∶ A) ℓ ℓ∈ with does (ℓ ≟ ℓ′)
... | true  = Sig
... | false = Restrict Sig ℓ ℓ∈
Restrict (Sig , ℓ′ ≔ a) ℓ ℓ∈ with does (ℓ ≟ ℓ′)
... | true  = Sig
... | false = Restrict Sig ℓ ℓ∈

Restricted : ∀ {s} (Sig : Signature s) (ℓ : Label) → ℓ ∈ Sig → Set s
Restricted Sig ℓ ℓ∈ = Record (Restrict Sig ℓ ℓ∈)

Proj : ∀ {s} (Sig : Signature s) (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
       Restricted Sig ℓ ℓ∈ → Set s
Proj ∅              ℓ {}
Proj (Sig , ℓ′ ∶ A) ℓ {ℓ∈} with does (ℓ ≟ ℓ′)
... | true  = A
... | false = Proj Sig ℓ {ℓ∈}
Proj (_,_≔_ Sig ℓ′ {A = A} a) ℓ {ℓ∈} with does (ℓ ≟ ℓ′)
... | true  = A
... | false = Proj Sig ℓ {ℓ∈}

-- Record restriction and projection.

infixl  _∣_

_∣_ : ∀ {s} {Sig : Signature s} → Record Sig →
      (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} → Restricted Sig ℓ ℓ∈
_∣_ {Sig = ∅}            r       ℓ {}
_∣_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with does (ℓ ≟ ℓ′)
... | true  = Σ.proj₁ r
... | false = _∣_ (Σ.proj₁ r) ℓ {ℓ∈}
_∣_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ {ℓ∈} with does (ℓ ≟ ℓ′)
... | true  = Manifest-Σ.proj₁ r
... | false = _∣_ (Manifest-Σ.proj₁ r) ℓ {ℓ∈}

infixl  _·_

_·_ : ∀ {s} {Sig : Signature s} (r : Record Sig)
      (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
      Proj Sig ℓ {ℓ∈} (r ∣ ℓ)
_·_ {Sig = ∅}            r       ℓ {}
_·_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with does (ℓ ≟ ℓ′)
... | true  = Σ.proj₂ r
... | false = _·_ (Σ.proj₁ r) ℓ {ℓ∈}
_·_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ {ℓ∈} with does (ℓ ≟ ℓ′)
... | true  = Manifest-Σ.proj₂ r
... | false = _·_ (Manifest-Σ.proj₁ r) ℓ {ℓ∈}

------------------------------------------------------------------------
-- With

-- Sig With ℓ ≔ a is the signature Sig, but with the ℓ field set to a.

mutual

  infixl  _With_≔_

  _With_≔_ : ∀ {s} (Sig : Signature s) (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
             ((r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ r) → Signature s
  _With_≔_ ∅ ℓ {} a
  _With_≔_ (Sig , ℓ′ ∶ A)   ℓ {ℓ∈} a with does (ℓ ≟ ℓ′)
  ... | true  = Sig                   , ℓ′ ≔ a
  ... | false = _With_≔_ Sig ℓ {ℓ∈} a , ℓ′ ∶ A ∘ drop-With
  _With_≔_  (Sig , ℓ′ ≔ a′) ℓ {ℓ∈} a with does (ℓ ≟ ℓ′)
  ... | true  = Sig                   , ℓ′ ≔ a
  ... | false = _With_≔_ Sig ℓ {ℓ∈} a , ℓ′ ≔ a′ ∘ drop-With

  drop-With : ∀ {s} {Sig : Signature s} {ℓ : Label} {ℓ∈ : ℓ ∈ Sig}
              {a : (r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ r} →
              Record (_With_≔_ Sig ℓ {ℓ∈} a) → Record Sig
  drop-With {Sig = ∅} {ℓ∈ = ()}      r
  drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} (rec r) with does (ℓ ≟ ℓ′)
  ... | true  = rec (Manifest-Σ.proj₁ r , Manifest-Σ.proj₂ r)
  ... | false = rec (drop-With (Σ.proj₁ r) , Σ.proj₂ r)
  drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} (rec r) with does (ℓ ≟ ℓ′)
  ... | true  = rec (Manifest-Σ.proj₁ r ,)
  ... | false = rec (drop-With (Manifest-Σ.proj₁ r) ,)