← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Data/Container/Indexed/FreeMonad.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Container/Indexed/FreeMonad.agda
 
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
 
4
-- The free monad construction on indexed containers
 
5
------------------------------------------------------------------------
 
6
 
 
7
module Data.Container.Indexed.FreeMonad where
 
8
 
 
9
open import Level
 
10
open import Function hiding (const)
 
11
open import Category.Monad.Predicate
 
12
open import Data.Container.Indexed hiding (_∈_)
 
13
open import Data.Container.Indexed.Combinator hiding (id; _∘_)
 
14
open import Data.Empty
 
15
open import Data.Sum using (inj₁; inj₂)
 
16
open import Data.Product
 
17
open import Data.W.Indexed
 
18
open import Relation.Unary
 
19
open import Relation.Unary.PredicateTransformer
 
20
 
 
21
------------------------------------------------------------------------
 
22
 
 
23
infixl 9 _⋆C_
 
24
infix  9 _⋆_
 
25
 
 
26
_⋆C_ : ∀ {i o c r} {I : Set i} {O : Set o} →
 
27
       Container I O c r → Pred O c → Container I O _ _
 
28
C ⋆C X = const X ⊎ C
 
29
 
 
30
_⋆_ : ∀ {ℓ} {O : Set ℓ} → Container O O ℓ ℓ → Pt O ℓ
 
31
C ⋆ X = μ (C ⋆C X)
 
32
 
 
33
pattern returnP x = (inj₁ x , _)
 
34
pattern doP c k   = (inj₂ c , k)
 
35
 
 
36
do : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {X} →
 
37
     ⟦ C ⟧ (C ⋆ X) ⊆ C ⋆ X
 
38
do (c , k) = sup (doP c k)
 
39
 
 
40
rawPMonad : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} →
 
41
            RawPMonad {ℓ = ℓ} (_⋆_ C)
 
42
rawPMonad {C = C} = record
 
43
  { return? = return
 
44
  ; _=<?_  = _=<<_
 
45
  }
 
46
  where
 
47
  return : ∀ {X} → X ⊆ C ⋆ X
 
48
  return x = sup (inj₁ x , ⊥-elim ∘ lower)
 
49
 
 
50
  _=<<_ : ∀ {X Y} → X ⊆ C ⋆ Y → C ⋆ X ⊆ C ⋆ Y
 
51
  f =<< sup (returnP x) = f x
 
52
  f =<< sup (doP c k)   = do (c , λ r → f =<< k r)
 
53
 
 
54
leaf : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {X : Pred O ℓ} →
 
55
       ⟦ C ⟧ X ⊆ C ⋆ X
 
56
leaf (c , k) = do (c , return? ∘ k)
 
57
  where
 
58
  open RawPMonad rawPMonad