Cleanup Type base.

1 files changed, 119 insertions, 55 deletions

diff --git a/src/Cfe/Type/Base.agda b/src/Cfe/Type/Base.agda
index 33af9f6..98f7691 100644
--- a/src/Cfe/Type/Base.agda
+++ b/src/Cfe/Type/Base.agda
@@ -1,93 +1,157 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary using (_Respects_; Setoid)
 
 module Cfe.Type.Base
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open Setoid over using () renaming (Carrier to C; _≈_ to _∼_)
+open Setoid over using (trans) renaming (Carrier to C; _≈_ to _∼_)
 
-open import Cfe.Language over hiding (_≤_; _≈_)
-open import Data.Bool as 𝔹 hiding (_∨_) renaming (_≤_ to _≤ᵇ_)
-open import Data.Empty.Polymorphic
-open import Level as L renaming (suc to lsuc)
-open import Relation.Unary as U
+open import Cfe.Language over hiding (_∙_; _≈_)
+open import Data.Bool renaming (_∨_ to _∨ᵇ_; _≤_ to _≤ᵇ_)
+open import Data.Empty.Polymorphic using (⊥)
+open import Data.Product using (_×_)
+open import Data.Sum using (_⊎_; map)
+open import Function using (const; flip)
+open import Level
 open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Nullary using (¬_)
 
-infix 7 _∙_
-infix 6 _∨_
-infix 4 _⊨_
+private
+  variable
+    a b fℓ lℓ fℓ₁ lℓ₁ fℓ₂ lℓ₂ : Level
 
-record Type fℓ lℓ : Set (c ⊔ lsuc (fℓ ⊔ lℓ)) where
-  field
-    Null : Bool
-    First : Pred C fℓ
-    Flast : Pred C lℓ
+  union : (C → Set a) → (C → Set b) → C → Set _
+  union A B c = A c ⊎ B c
 
-open Type public
+  union-cong :
+    ∀ {A : C → Set a} {B : C → Set b} →
+    A Respects _∼_ → B Respects _∼_ → union A B Respects _∼_
+  union-cong A-cong B-cong x∼y = map (A-cong x∼y) (B-cong x∼y)
 
-τ⊥ : Type 0ℓ 0ℓ
-τ⊥ = record { Null = false ; First = U.∅ ; Flast = U.∅ }
+  if-cong :
+    ∀ {A B : C → Set a} cond →
+    A Respects _∼_ → B Respects _∼_ → (if cond then A else B) Respects _∼_
+  if-cong false A-cong B-cong = B-cong
+  if-cong true  A-cong B-cong = A-cong
 
-τε : Type 0ℓ 0ℓ
-τε = record { Null = true ; First = U.∅ ; Flast = U.∅ }
+------------------------------------------------------------------------
+-- Definitions
 
-τ[_] : C → Type ℓ 0ℓ
-τ[ c ] = record { Null = false ; First = c ∼_ ; Flast = U.∅ }
+record Type fℓ lℓ : Set (c ⊔ ℓ ⊔ suc (fℓ ⊔ lℓ)) where
+  field
+    null       : Bool
+    first      : C → Set fℓ
+    flast      : C → Set lℓ
+    first-cong : first Respects _∼_
+    flast-cong : flast Respects _∼_
+
+------------------------------------------------------------------------
+-- Special Types
+
+τ⊥ : Type fℓ lℓ
+τ⊥ = record
+  { null       = false
+  ; first      = const ⊥
+  ; flast      = const ⊥
+  ; first-cong = λ _ ()
+  ; flast-cong = λ _ ()
+  }
 
-_∨_ : ∀ {fℓ₁ lℓ₁ fℓ₂ lℓ₂} → Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ₂) (lℓ₁ ⊔ lℓ₂)
-τ₁ ∨ τ₂ = record
-  { Null = Null τ₁ 𝔹.∨ Null τ₂
-  ; First = First τ₁ ∪ First τ₂
-  ; Flast = Flast τ₁ ∪ Flast τ₂
+τε : Type fℓ lℓ
+τε = record
+  { null       = true
+  ; first      = const ⊥
+  ; flast      = const ⊥
+  ; first-cong = λ _ ()
+  ; flast-cong = λ _ ()
   }
 
-_∙_ : ∀ {fℓ₁ lℓ₁ fℓ₂ lℓ₂} → Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ₂) (lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂)
-_∙_ {lℓ₁ = lℓ₁} {fℓ₂} {lℓ₂} τ₁ τ₂ = record
-  { Null = Null τ₁ ∧ Null τ₂
-  ; First = First τ₁ ∪ (if Null τ₁ then First τ₂ else λ x → ⊥)
-  ; Flast = Flast τ₂ ∪ (if Null τ₂ then First τ₂ ∪ Flast τ₁ else λ x → ⊥)
+τ[_] : C → Type ℓ ℓ
+τ[ c ] = record
+  { null       = false
+  ; first      = c ∼_
+  ; flast      = const ⊥
+  ; first-cong = flip trans
+  ; flast-cong = λ _ ()
   }
 
-record _⊨_ {a} {fℓ} {lℓ} (A : Language a) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where
-  field
-    n⇒n : null A → T (Null τ)
-    f⇒f : first A ⊆ First τ
-    l⇒l : flast A ⊆ Flast τ
+------------------------------------------------------------------------
+-- Type Operations
+
+infix 7 _∙_
+infix 6 _∨_
 
-record _⊛_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ lℓ₁ ⊔ fℓ₂) where
+_∙_ : Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ₂) (lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂)
+τ₁ ∙ τ₂ = record
+  { null       = τ₁.null ∧ τ₂.null
+  ; first      = union τ₁.first (if τ₁.null then τ₂.first else const ⊥)
+  ; flast      = union τ₂.flast (if τ₂.null then union τ₂.first τ₁.flast else const ⊥)
+  ; first-cong = union-cong τ₁.first-cong (if-cong τ₁.null τ₂.first-cong (λ _ ()))
+  ; flast-cong =
+      union-cong τ₂.flast-cong (if-cong τ₂.null (union-cong τ₂.first-cong τ₁.flast-cong) (λ _ ()))
+  }
+  where
   module τ₁ = Type τ₁
   module τ₂ = Type τ₂
 
-  field
-    ∄[l₁∩f₂] : Empty (τ₁.Flast ∩ τ₂.First)
-    ¬n₁ : T (not τ₁.Null)
-
-record _#_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ fℓ₂) where
+_∨_ : Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ₂) (lℓ₁ ⊔ lℓ₂)
+τ₁ ∨ τ₂ = record
+  { null       = τ₁.null ∨ᵇ τ₂.null
+  ; first      = union τ₁.first τ₂.first
+  ; flast      = union τ₁.flast τ₂.flast
+  ; first-cong = union-cong τ₁.first-cong τ₂.first-cong
+  ; flast-cong = union-cong τ₁.flast-cong τ₂.flast-cong
+  }
+  where
   module τ₁ = Type τ₁
   module τ₂ = Type τ₂
 
+------------------------------------------------------------------------
+-- Relations
+
+infix 4 _≈_
+infix 4 _≤_
+infix 4 _⊨_
+infix 4 _⊛_
+infix 4 _#_
+
+record _≈_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂) where
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
   field
-    ∄[f₁∩f₂] : Empty (τ₁.First ∩ τ₂.First)
-    ¬n₁∨¬n₂ : T (not (τ₁.Null 𝔹.∨ τ₂.Null))
+    n≡n   : τ₁.null ≡ τ₂.null
+    f₁⊆f₂ : ∀ {c} → τ₁.first c → τ₂.first c
+    f₁⊇f₂ : ∀ {c} → τ₁.first c → τ₂.first c
+    l₁⊆l₂ : ∀ {c} → τ₁.flast c → τ₂.flast c
+    l₁⊇l₂ : ∀ {c} → τ₁.flast c → τ₂.flast c
 
-record _≤_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂) where
+record _≤_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂) where
   module τ₁ = Type τ₁
   module τ₂ = Type τ₂
+  field
+    n≤n : τ₁.null ≤ᵇ τ₂.null
+    f⊆f : ∀ {c} → τ₁.first c → τ₂.first c
+    l⊆l : ∀ {c} → τ₁.flast c → τ₂.flast c
 
+record _⊨_ (A : Language a) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where
+  module τ = Type τ
   field
-    n≤n : τ₁.Null ≤ᵇ τ₂.Null
-    f⊆f : τ₁.First ⊆ τ₂.First
-    l⊆l : τ₁.Flast ⊆ τ₂.Flast
+    n⇒n : Null A → T (τ.null)
+    f⇒f : ∀ {c} → First A c → τ.first c
+    l⇒l : ∀ {c} → Flast A c → τ.flast c
 
-record _≈_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂) where
+record _⊛_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ lℓ₁ ⊔ fℓ₂) where
   module τ₁ = Type τ₁
   module τ₂ = Type τ₂
+  field
+    ∄[l₁∩f₂] : ∀ c → ¬ (τ₁.flast c × τ₂.first c)
+    ¬n₁      : ¬ T (τ₁.null)
 
+record _#_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ fℓ₂) where
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
   field
-    n≡n : τ₁.Null ≡ τ₂.Null
-    f₁⊆f₂ : τ₁.First ⊆ τ₂.First
-    f₁⊇f₂ : τ₁.First ⊇ τ₂.First
-    l₁⊆l₂ : τ₁.Flast ⊆ τ₂.Flast
-    l₁⊇l₂ : τ₁.Flast ⊇ τ₂.Flast
+    ∄[f₁∩f₂] : ∀ c → ¬ (τ₁.first c × τ₂.first c)
+    ¬n₁∨¬n₂  : ¬ (T τ₁.null × T τ₂.null)