6 | import Derive.Prelude
8 | %language ElabReflection
17 | record Tree (a : Type) where
20 | forest : List (Tree a)
24 | Forest : Type -> Type
25 | Forest = List . Tree
27 | %runElab derive "Tree" [Show,Eq]
34 | singleton : a -> Tree a
35 | singleton a = MkTree a []
38 | replicate : (width : Nat) -> (depth : Nat) -> a -> Tree a
39 | replicate _ 0 x = MkTree x []
40 | replicate width (S k) x = MkTree x $
replicate width (replicate width k x)
44 | unfold : (depth : Nat) -> (f : s -> (a,List s)) -> s -> Tree a
45 | unfold 0 f s = MkTree (fst $
f s) []
48 | in MkTree a (map (unfold k f) ss)
54 | zipWithKeep : (a -> a -> a) -> List a -> List a -> List a
55 | zipWithKeep f [] ys = ys
56 | zipWithKeep f xs [] = xs
57 | zipWithKeep f (x :: xs) (y :: ys) = f x y :: zipWithKeep f xs ys
60 | flatten : Tree a -> List a
61 | flatten (MkTree v vs) = v :: flattenF vs
64 | flattenF : Forest a -> List a
66 | flattenF (x :: xs) = flatten x ++ flattenF xs
69 | layers : Tree a -> List (List a)
70 | layers (MkTree v vs) = [v] :: layersF vs
73 | layersF : Forest a -> List (List a)
75 | layersF (x :: xs) = zipWithKeep (++) (layers x) (layersF xs)
82 | index : List Nat -> Tree a -> Maybe a
83 | index [] x = Just x.value
84 | index (y :: ys) x = ix y x.forest >>= index ys
87 | ix : Nat -> List b -> Maybe b
89 | ix 0 (z :: _) = Just z
90 | ix (S k) (_ :: zs) = ix k zs
97 | foldlTree : (a -> e -> a) -> a -> Tree e -> a
98 | foldlTree f acc (MkTree v vs) = foldlF (f acc v) vs
101 | foldlF : a -> Forest e -> a
103 | foldlF y (x :: xs) = foldlF (foldlTree f y x) xs
105 | foldrTree : (e -> a -> a) -> a -> Tree e -> a
106 | foldrTree f acc (MkTree v vs) = f v (foldrF acc vs)
109 | foldrF : a -> Forest e -> a
111 | foldrF y (x :: xs) = foldrTree f (foldrF y xs) x
113 | traverseTree : Applicative f => (a -> f b) -> Tree a -> f (Tree b)
114 | traverseTree fun (MkTree v vs) = [| MkTree (fun v) (traverseF vs) |]
117 | traverseF : Forest a -> f (Forest b)
118 | traverseF [] = pure []
119 | traverseF (x :: xs) = [| traverseTree fun x :: traverseF xs |]
121 | mapTree : (a -> b) -> Tree a -> Tree b
122 | mapTree f (MkTree v vs) = MkTree (f v) (mapF vs)
125 | mapF : Forest a -> Forest b
127 | mapF (h :: t) = mapTree f h :: mapF t
129 | bindTree : Tree a -> (a -> Tree b) -> Tree b
130 | bindTree (MkTree va tas) f =
131 | let MkTree vb tbs := f va
132 | in MkTree vb (tbs ++ bindF tas)
135 | bindF : Forest a -> Forest b
137 | bindF (x :: xs) = bindTree x f :: bindF xs
139 | apTree : Tree (a -> b) -> Tree a -> Tree b
140 | apTree tf ta = bindTree tf $
\f => mapTree (apply f) ta
142 | joinTree : Tree (Tree a) -> Tree a
143 | joinTree (MkTree (MkTree va tas) ftas) =
144 | MkTree va $
tas ++ joinF ftas
147 | joinF : Forest (Tree a) -> Forest a
149 | joinF (x :: xs) = joinTree x :: joinF xs
156 | drawTree : Tree String -> String
157 | drawTree = unlines . draw
160 | drawForest : Forest String -> String
161 | drawForest = unlines . map drawTree
163 | draw : Tree String -> List String
164 | draw (MkTree x ts0) = lines x ++ subTrees ts0
167 | shift : String -> String -> List String -> List String
168 | shift first other tails =
169 | zipWith (++) (first :: replicate (length tails) other) tails
171 | subTrees : Forest String -> List String
173 | subTrees [t] = "│" :: shift "└╼" " " (draw t)
174 | subTrees (t::ts) = "│" :: shift "├╼" "│ " (draw t) ++ subTrees ts
180 | public export %inline
181 | Foldable Tree where
186 | public export %inline
190 | public export %inline
191 | Applicative Tree where
192 | pure a = MkTree a Nil
195 | public export %inline
200 | public export %inline
201 | Traversable Tree where
202 | traverse = traverseTree