git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/ST/TreeTag.idr
29 lines 871 B history raw
1import Control.ST
3data BTree a = Leaf
4 | Node (BTree a) a (BTree a)
6testTree : BTree String
7testTree = Node (Node Leaf "Jim" Leaf)
8 "Fred"
9 (Node (Node Leaf "Alice" Leaf)
10 "Sheila"
11 (Node Leaf "Bob" Leaf))
14treeTagAux : (tag : Var) -> BTree a -> ST m (BTree (Int, a)) [tag ::: State Int]
15treeTagAux tag Leaf = pure Leaf
16treeTagAux tag (Node left val right)
17 = do left' <- treeTagAux tag left
18 thisTag <- read tag
19 write tag (thisTag + 1)
20 right' <- treeTagAux tag right
21 pure (Node left' (thisTag, val) right')
23treeTag : (i : Int) -> BTree a -> BTree (Int, a)
24treeTag i tree = runPure (do tag <- new i
25 t <- treeTagAux tag tree
26 delete tag
27 pure t)