------------------------------------------------------------------------
-- 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.

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

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

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

open import Data.Bool
open import Data.Empty
open import Data.List
open import Data.Product hiding (proj₁; proj₂)
open import Data.Unit
open import Function
open import Level
open import Relation.Nullary
open import Relation.Nullary.Decidable

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

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

infix 4 _,

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 5 _,_∶_ _,_≔_

  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
    constructor rec
    field fun : Record-fun Sig

  Record-fun :  {s}  Signature s  Set s
  Record-fun              = Lift 
  Record-fun (Sig ,   A) =          Σ (Record Sig) A
  Record-fun (Sig ,   a) = Manifest-Σ (Record Sig) a

------------------------------------------------------------------------
-- Variants of Signature and Record

-- It may be easier to define values of type Record′ (Sig⇒Sig′ Sig)
-- than of type Record Sig.

mutual

  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′ :  {s}  Signature′ s  Set s
  Record′              = Lift 
  Record′ (Sig ,   A) =          Σ (Record′ Sig) A
  Record′ (Sig ,   a) = Manifest-Σ (Record′ Sig) a

-- We can convert between the two kinds of signatures/records.

mutual

  Sig′⇒Sig :  {s}  Signature′ s  Signature s
  Sig′⇒Sig              = 
  Sig′⇒Sig (Sig ,   A) = Sig′⇒Sig Sig ,   (A  Rec⇒Rec′ _)
  Sig′⇒Sig (Sig ,   a) = Sig′⇒Sig Sig ,   (a  Rec⇒Rec′ _)

  Rec⇒Rec′ :  {s} (Sig : Signature′ s) 
             Record (Sig′⇒Sig Sig)  Record′ Sig
  Rec⇒Rec′              (rec r) = r
  Rec⇒Rec′ (Sig ,   A) (rec r) = (Rec⇒Rec′ _ (Σ.proj₁ r) , Σ.proj₂ r)
  Rec⇒Rec′ (Sig ,   a) (rec r) = (Rec⇒Rec′ _ (Manifest-Σ.proj₁ r) ,)

mutual

  Sig⇒Sig′ :  {s}  Signature s  Signature′ s
  Sig⇒Sig′              = 
  Sig⇒Sig′ (Sig ,   A) = Sig⇒Sig′ Sig ,   (A  Rec′⇒Rec _)
  Sig⇒Sig′ (Sig ,   a) = Sig⇒Sig′ Sig ,   (a  Rec′⇒Rec _)

  Rec′⇒Rec :  {s} (Sig : Signature s) 
             Record′ (Sig⇒Sig′ Sig)  Record Sig
  Rec′⇒Rec              r = rec r
  Rec′⇒Rec (Sig ,   A) r = rec (Rec′⇒Rec _ (Σ.proj₁ r) , Σ.proj₂ r)
  Rec′⇒Rec (Sig ,   a) r = rec (Rec′⇒Rec _ (Manifest-Σ.proj₁ r) ,)

------------------------------------------------------------------------
-- 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 4 _∈_

_∈_ :  {s}  Label  Signature s  Set
  Sig =
  foldr  ℓ′  if    ℓ′  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   ℓ′
... | yes _ = Sig
... | no  _ = Restrict Sig  ℓ∈
Restrict (Sig , ℓ′  a)  ℓ∈ with   ℓ′
... | yes _ = Sig
... | no  _ = 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   ℓ′
... | yes _ = A
... | no  _ = Proj Sig  {ℓ∈}
Proj (_,_≔_ Sig ℓ′ {A = A} a)  {ℓ∈} with   ℓ′
... | yes _ = A
... | no  _ = Proj Sig  {ℓ∈}

-- Record restriction and projection.

infixl 5 _∣_

_∣_ :  {s} {Sig : Signature s}  Record Sig 
      ( : Label) {ℓ∈ :   Sig}  Restricted Sig  ℓ∈
_∣_ {Sig = }            r        {}
_∣_ {Sig = Sig , ℓ′  A} (rec r)  {ℓ∈} with   ℓ′
... | yes _ = Σ.proj₁ r
... | no  _ = _∣_ (Σ.proj₁ r)  {ℓ∈}
_∣_ {Sig = Sig , ℓ′  a} (rec r)  {ℓ∈} with   ℓ′
... | yes _ = Manifest-Σ.proj₁ r
... | no  _ = _∣_ (Manifest-Σ.proj₁ r)  {ℓ∈}

infixl 5 _·_

_·_ :  {s} {Sig : Signature s} (r : Record Sig)
      ( : Label) {ℓ∈ :   Sig} 
      Proj Sig  {ℓ∈} (r  )
_·_ {Sig = }            r        {}
_·_ {Sig = Sig , ℓ′  A} (rec r)  {ℓ∈} with   ℓ′
... | yes _ = Σ.proj₂ r
... | no  _ = _·_ (Σ.proj₁ r)  {ℓ∈}
_·_ {Sig = Sig , ℓ′  a} (rec r)  {ℓ∈} with   ℓ′
... | yes _ = Manifest-Σ.proj₂ r
... | no  _ = _·_ (Manifest-Σ.proj₁ r)  {ℓ∈}

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

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

mutual

  infixl 5 _With_≔_

  _With_≔_ :  {s} (Sig : Signature s) ( : Label) {ℓ∈ :   Sig} 
             ((r : Restricted Sig  ℓ∈)  Proj Sig  r)  Signature s
  _With_≔_   {} a
  _With_≔_ (Sig , ℓ′  A)    {ℓ∈} a with   ℓ′
  ... | yes _ = Sig                   , ℓ′  a
  ... | no  _ = _With_≔_ Sig  {ℓ∈} a , ℓ′  A  drop-With
  _With_≔_  (Sig , ℓ′  a′)  {ℓ∈} a with   ℓ′
  ... | yes _ = Sig                   , ℓ′  a
  ... | no  _ = _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   ℓ′
  ... | yes _ = rec (Manifest-Σ.proj₁ r , Manifest-Σ.proj₂ r)
  ... | no  _ = rec (drop-With (Σ.proj₁ r) , Σ.proj₂ r)
  drop-With {Sig = Sig , ℓ′  a} {} (rec r) with   ℓ′
  ... | yes _ = rec (Manifest-Σ.proj₁ r ,)
  ... | no  _ = rec (drop-With (Manifest-Σ.proj₁ r) ,)