effects_tree.idr

module Main
 
import Effect.State
 
data BTree a = Leaf
             | Node (BTree a) a (BTree a)
 
instance Show a => Show (BTree a) where
  show Leaf = "[]"
  show (Node l x r) = "[" ++ show l ++ " "
                          ++ show x ++ " "
                          ++ show r ++ "]"
 
testTree : BTree String
testTree = Node (Node Leaf "Jim" Leaf)
  "Fred"
  (Node (Node Leaf "Alice" Leaf)
    "Sheila"
    (Node Leaf "Bob" Leaf))
 
treeTagAux : BTree a -> { [STATE (List a)] } Eff m (BTree ((List a), a))
treeTagAux Leaf = pure Leaf
treeTagAux (Node l x r)
  = do l' <- treeTagAux l 
       i <- get
       put (x::i)
       r' <- treeTagAux r
       pure (Node l' (i, x) r')
 
treeTag : (i : (List a)) -> BTree a -> BTree ((List a), a)
treeTag i x = runPure (do put i
                          treeTagAux x)
 
main : IO ()
main = print (treeTag [] testTree)