git.iko.soy/Idris-dev
on bd2fa8d help sign in
Idris-dev/samples/effects/TreeTagCount.idr
29 lines 910 B history raw
1import Effects
2import Effect.State
3import Effect.StdIO
5data BTree a = Leaf
6 | Node (BTree a) a (BTree a)
8testTree : BTree String
9testTree = Node (Node Leaf "Jim" Leaf)
10 "Fred"
11 (Node (Node Leaf "Alice" Leaf)
12 "Sheila"
13 (Node Leaf "Bob" Leaf))
15treeTagAux : BTree a -> { ['Tag ::: STATE Int,
16 'Leaves ::: STATE Int] } Eff (BTree (Int, a))
17treeTagAux Leaf = do 'Leaves :- update (+1)
18 pure Leaf
19treeTagAux (Node l x r)
20 = do l' <- treeTagAux l
21 i <- 'Tag :- get
22 'Tag :- put (i + 1)
23 r' <- treeTagAux r
24 pure (Node l' (i, x) r')
26treeTag : (i : Int) -> BTree a -> (BTree (Int, a), Int)
27treeTag i x = runPureInit ['Tag := i, 'Leaves := 0]
28 (do x' <- treeTagAux x
29 pure (x', !('Leaves :- get)))