git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/effects/TreeTag.idr
40 lines 1.1 kB history raw
1module Main
3import Effects
4import Effect.State
6data BTree a = Leaf
7 | Node (BTree a) a (BTree a)
9implementation Show a => Show (BTree a) where
10 show Leaf = "[]"
11 show (Node l x r) = "[" ++ show l ++ " "
12 ++ show x ++ " "
13 ++ show r ++ "]"
15testTree : BTree String
16testTree = Node (Node Leaf "Jim" Leaf)
17 "Fred"
18 (Node (Node Leaf "Alice" Leaf)
19 "Sheila"
20 (Node Leaf "Bob" Leaf))
22treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))
23treeTagAux Leaf = pure Leaf
24treeTagAux (Node l x r)
25 = do l' <- treeTagAux l
26 i <- get
27 put (i + 1)
28 r' <- treeTagAux r
29 pure (Node l' (i, x) r')
31treeTag : (i : Int) -> BTree a -> BTree (Int, a)
32treeTag i x = runPure (do put i
33 treeTagAux x)
35treeTagIO : (i : Int) -> BTree a -> IO (BTree (Int, a))
36treeTagIO i x = run (do put i
37 treeTagAux x)
39main : IO ()
40main = print (treeTag 1 testTree)