{-# OPTIONS --allow-unsolved-metas #-}
open import Padova2024.EquationalReasoning
data _×_ (X Y : Set) : Set where
_,_ : X → Y → X × Y
data ⊤ : Set where
tt : ⊤
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
_+_ : ℕ → ℕ → ℕ
zero + b = b
succ a + b = succ (a + b)
module _ where private
tick : {X : Set} → X → ℕ → ℕ × X
tick x s = (succ s , x)
State : Set → Set → Set
State S X = S → S × X
_>>=_ : {S X Y : Set} → State S X → (X → State S Y) → State S Y
(f >>= h) s with f s
... | s' , y = h y s'
_>>_ : {S X Y : Set} → State S X → State S Y → State S Y
f >> g = f >>= λ _ → g
return : {S X : Set} → X → State S X
return x s = s , x
get : {S : Set} → State S S
get s = s , s
put : {S : Set} → S → State S ⊤
put s' s = s' , tt
modify : {S : Set} → (S → S) → State S ⊤
modify f s = f s , tt
module _ where private
postulate
X Y Z : Set
S : Set
f : X → State S Y
g : Y → State S Z
h : X → State S Z
h x = f x >>= g
h' : X → State S Z
h' x = do
y ← f x
z ← g y
{!!}
data Tree (X : Set) : Set where
leaf : X → Tree X
fork : Tree X → Tree X → Tree X
tick : State ℕ ⊤
tick = do
count ← get
put (succ count)
sum : Tree ℕ → State ℕ ℕ
sum (leaf x) = do
tick
return x
sum (fork left right) = do
leftSum ← sum left
rightSum ← sum right
return (leftSum + rightSum)
exampleTree : Tree ℕ
exampleTree = fork (fork (leaf 4) (leaf 5)) (leaf 6)
_ : sum exampleTree 0 ≡ (3 , 15)
_ = refl