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
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₁
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 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
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
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 : ∀ {s} → Signature s → List Label
labels ∅ = []
labels (Sig , ℓ ∶ A) = ℓ ∷ labels Sig
labels (Sig , ℓ ≔ a) = ℓ ∷ labels Sig
infix 4 _∈_
_∈_ : ∀ {s} → Label → Signature s → Set
ℓ ∈ Sig =
foldr (λ ℓ′ → if ⌊ ℓ ≟ ℓ′ ⌋ then (λ _ → ⊤) else id) ⊥ (labels Sig)
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 ℓ {ℓ∈}
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) ℓ {ℓ∈}
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) ,)