------------------------------------------------------------------------
-- The Agda standard library
--
-- The free monad construction on indexed containers
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Container.Indexed.FreeMonad where
open import Level using (Level; _⊔_; lower)
open import Function.Base hiding (const)
open import Effect.Monad.Predicate using (RawPMonad)
open import Data.Container.Indexed using (Container; Command; Response; next; ⟦_⟧; μ)
open import Data.Container.Indexed.Combinator hiding (id; _∘_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sum.Base using (inj₁; inj₂)
open import Data.Product.Base using (_,_)
open import Data.W.Indexed using (sup)
open import Relation.Unary using (Pred; _⊆_; ⋃; _∈_; ｛_｝)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Binary.PropositionalEquality.Core using (refl)
------------------------------------------------------------------------
infixl 9 _⋆C_
infix 9 _⋆_
_⋆C_ : ∀ {i o c r} {I : Set i} {O : Set o} →
Container I O c r → Pred O c → Container I O _ _
C ⋆C X = const X ⊎′ C
_⋆_ : ∀ {ℓ} {O : Set ℓ} → Container O O ℓ ℓ → Pt O ℓ
C ⋆ X = μ (C ⋆C X)
pattern returnP x = (inj₁ x , _)
pattern doP c k = (inj₂ c , k)
inn : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {X} →
⟦ C ⟧ (C ⋆ X) ⊆ C ⋆ X
inn (c , k) = sup (doP c k)
rawPMonad : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} →
RawPMonad {ℓ = ℓ} (_⋆_ C)
rawPMonad {C = C} = record
{ return? = return
; _=<?_ = _=<<_
}
where
return : ∀ {X} → X ⊆ C ⋆ X
return x = sup (inj₁ x , ⊥-elim ∘ lower)
_=<<_ : ∀ {X Y} → X ⊆ C ⋆ Y → C ⋆ X ⊆ C ⋆ Y
f =<< sup (returnP x) = f x
f =<< sup (doP c k) = inn (c , λ r → f =<< k r)
leaf : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {X : Pred O ℓ} →
⟦ C ⟧ X ⊆ C ⋆ X
leaf (c , k) = inn (c , return? ∘ k)
where
open RawPMonad rawPMonad
generic : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {o}
(c : Command C o) →
o ∈ C ⋆ (⋃[ r ∶ Response C c ] ｛ next C c r ｝)
generic c = inn (c , λ r → return? (r , refl))
where
open RawPMonad rawPMonad
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4