-
Notifications
You must be signed in to change notification settings - Fork 3
/
Sec212.hs
36 lines (30 loc) · 1002 Bytes
/
Sec212.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
-- Adapted from Brady's ICFP '13 paper.
{-# LANGUAGE TypeInType, RebindableSyntax, TypeOperators,
TemplateHaskell, ScopedTypeVariables, TypeFamilies,
GADTs #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors
-Wno-name-shadowing #-}
module Sec212 where
import Sec211
import Effects
import Effect.State
import Data.Nat
import Data.Singletons.TH
$(singletons [d| data Vars = Count | Tag |])
tagCount :: Tree a -> Eff m '[ Tag ::: STATE Nat
, Count ::: STATE Nat ] (Tree (Nat, a))
tagCount Leaf
= do SCount |- update_ (+1)
return Leaf
tagCount (Node l x r)
= do l' <- tagCount l
lbl <- STag |- get_
STag |- put_ (lbl + 1)
r' <- tagCount r
return (Node l' (lbl, x) r')
tagCountFrom :: Nat -> Tree a -> (Nat, Tree (Nat, a))
tagCountFrom x t
= let (_ :> SCount := leaves :> Empty, tree) =
runPureEnv (STag := x :> SCount := 0 :> Empty) (tagCount t)
in
(leaves, tree)