Tree erasure

tree.idr

data Tree : Nat -> Type -> Type where
     Leaf : Tree Z a
     Node : Tree ln a -> a -> Tree rn a -> Tree (ln + (S rn)) a

insert : Ord a => a -> Tree n a -> Tree (S n) a
insert val Leaf = Node Leaf val Leaf
insert val (Node l x r) with (val <= x)
  insert val (Node l x r) | True = Node (insert val l) x r
  insert val (Node l x r) | False ?= {tree_right} Node l x (insert val r)

tree_right a constrarg val ln rn l x r value = 
   rewrite plusSuccRightSucc ln (S rn) in value

flatten : Tree n a -> Vect n a
flatten Leaf = []
flatten (Node l x r) = flatten l ++ x :: flatten r

insertThings : Tree n String -> IO (Exists (\n' => Tree n' String))
insertThings x = do putStr ": "
                    val_in <- getLine 
                    let val = trim val_in
                    if val == "" then return (evidence _ x)
                                 else insertThings (insert val x)

main : IO ()
main = do evidence _ t <- insertThings Leaf
          print (flatten t)