open import Level
open import Data.Maybe
open import Data.Sum
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Relation.Nullary
open import Relation.Nullary.Decidable
private
isJust' : ∀ {ℓ} {t : Set ℓ} → (x : t) → (Maybe.just x) ≡ nothing → ⊥
isJust' x ()
isJust : ∀ {ℓ} {t : Set ℓ} → (y : Maybe t) → Dec (∃ λ x → just x ≡ y)
isJust (just x) = yes (x , refl)
isJust nothing = no λ k → isJust' _ (proj₂ k)
record Search {ℓ₁ ℓ₂} (t₁ : Set ℓ₁) (t₂ : t₁ → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
field
try : (x : t₁) → Maybe (t₂ x)
# : ∀ x → {p : True (isJust (try x))} → (t₂ x)
# x {p} = proj₁ (toWitness p)
open Search {{...}} using (#) public
record Projection {ℓ₁ ℓ₂ ℓ'} {t : Set ℓ₁} {f : t → Set ℓ₂} (_●_ : ∀ (x : t) → f x → Set ℓ') (x : t) (x' : f x) : Set ℓ' where
field
proj : x ● x'
open Projection
infix 0 _⟫>_
_⟫>_ : ∀ {ℓ₁ ℓ₂} → _
_⟫>_ {ℓ₁} {ℓ₂} = Projection λ (a : Set ℓ₁) (b : a → Set ℓ₂) → (x : _) → b x
instance
×-Left : ∀ {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : t₁ → Set ℓ₂} → ∃ t₂ ⟫> t₂ ∘ proj₁
×-Left = record { proj = proj₂ }
×-Right : ∀ {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : t₁ → Set ℓ₂} → ∃ t₂ ⟫> const t₁
×-Right = record { proj = proj₁ }
×-RLeft : ∀ {ℓ₁ ℓ₂ ℓ₃} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} {t : t₁ → Set ℓ₃} → t₁ ⟫> t → t₁ × t₂ ⟫> t ∘ proj₁
×-RLeft i = record { proj = proj i ∘ proj₁ }
×-RRight : ∀ {ℓ₁ ℓ₂ ℓ₃} {t₁ : Set ℓ₁} {t₂ : t₁ → Set ℓ₂} {t : ∀ {x} → t₂ x → Set ℓ₃} → (∀ {x} → t₂ x ⟫> t) → ∃ t₂ ⟫> t ∘ proj₂
×-RRight i = record { proj = proj i ∘ proj₂ }
×-build : ∀ {ℓ₁ ℓ₂ ℓ} {t : Set ℓ} {t₁ : t → Set ℓ₁} {t₂ : t → Set ℓ₂} → t ⟫> t₁ → t ⟫> t₂ → t ⟫> λ x → t₁ x × t₂ x
×-build i j = record { proj = λ x → proj i x , proj j x }
⊎-Left : ∀ {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} → t₁ ⟫> const (t₁ ⊎ t₂)
⊎-Left = record { proj = inj₁ }
⊎-Right : ∀ {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} → t₂ ⟫> const (t₁ ⊎ t₂)
⊎-Right = record { proj = inj₂ }
⊎-RRight : ∀ {ℓ₁ ℓ₂ ℓ} {t : Set ℓ} {t₁ : t → Set ℓ₁} {t₂ : Set ℓ₂} → t ⟫> t₁ → t ⟫> λ x → t₁ x ⊎ t₂
⊎-RRight i = record { proj = inj₁ ∘ proj i }
⊎-RLeft : ∀ {ℓ₁ ℓ₂ ℓ} {t : Set ℓ} {t₁ : Set ℓ₁} {t₂ : t → Set ℓ₂} → t ⟫> t₂ → t ⟫> λ x → t₁ ⊎ t₂ x
⊎-RLeft i = record { proj = inj₂ ∘ proj i }
⊎-build : ∀ {ℓ₁ ℓ₂ ℓ} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} {t : t₁ ⊎ t₂ → Set ℓ} → t₁ ⟫> t ∘ inj₁ → t₂ ⟫> t ∘ inj₂ → t₁ ⊎ t₂ ⟫> t
⊎-build {t = t} i j = record { proj = λ where
(inj₁ x) → proj i x
(inj₂ x) → proj j x
}
projectionSearch : ∀ {ℓ₁ ℓ₂} {t : Set ℓ₁} {t₂ : t → Set ℓ₂} → t ⟫> t₂ → Search t t₂
projectionSearch i = record { try = just ∘ proj i }
private
_ : ∀ {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} → t₁ → t₁ ⊎ t₂
_ = λ x → # x
_ : ∀ {a b : Set} → a → b ⊎ a
_ = λ x → # x
_ : ∀ {a b c d e f g : Set} → a → ((c ⊎ b) ⊎ f) ⊎ (g ⊎ a ⊎ d) ⊎ e
_ = λ x → # x
_ : ∀ {a b : Set} → a × b → a
_ = λ x → # x
_ : ∀ {a b : Set} → a × b → b
_ = λ x → # x
_ : ∀ {a b c d e f g : Set} → ((c × b) × f) × (g × a × d) × e → a
_ = λ x → # x
_ : ∀ {a b c : Set} → a × c ⊎ c × b → c
_ = λ x → # x
_ : ∀ {a b c d e f g : Set} → e × a × (d × f) ⊎ g × d × b → d
_ = λ x → # x
_ : ∀ {a b c d : Set} → (a × b) × (c × d) → b × c
_ = λ x → # x
_ : ∀ {a b c d : Set} → a × b ⊎ c × d → a ⊎ c
_ = λ x → # x
instance
equality : ∀ {ℓ} {t : Set ℓ} → t ⟫> λ x → x ≡ x
equality = record { proj = λ _ → refl }
_ : ∀ {t : Set} → (x : t) → x ≡ x
_ = λ x → # x