0 | module Pack.Database.Tree
  1 |
  2 | import Control.Monad.State
  3 | import Data.Maybe
  4 | import Data.List
  5 | import Data.Nat
  6 | import Data.SortedMap
  7 | import Idris.Package.Types
  8 | import Pack.Core.Types
  9 | import Pack.Database.Types
 10 |
 11 | %default covering
 12 |
 13 | --------------------------------------------------------------------------------
 14 | --         Graphs
 15 | --------------------------------------------------------------------------------
 16 |
 17 | ||| A dependency graph
 18 | public export
 19 | 0 Graph : Type -> Type
 20 | Graph a = SortedMap a (List a)
 21 |
 22 | ||| Returns the graph with all edges inverted
 23 | export
 24 | invertGraph : Ord a => Graph a -> Graph a
 25 | invertGraph = foldl add empty . SortedMap.toList
 26 |
 27 |   where
 28 |     ins : a -> Graph a -> a -> Graph a
 29 |     ins v g k = case lookup k g of
 30 |       Nothing => insert k [v] g
 31 |       Just vs => insert k (v::vs) g
 32 |
 33 |     add : Graph a -> (a,List a) -> Graph a
 34 |     add g (k,vs) = foldl (ins k) g vs
 35 |
 36 | export
 37 | dependencyGraph : SortedMap PkgName (ResolvedLib t) -> Graph PkgName
 38 | dependencyGraph = map dependencies
 39 |
 40 | --------------------------------------------------------------------------------
 41 | --         Trees
 42 | --------------------------------------------------------------------------------
 43 |
 44 | public export
 45 | record Tree a where
 46 |   constructor T
 47 |   label : a
 48 |   deps  : List (Tree a)
 49 |
 50 | export
 51 | Functor Tree where
 52 |   map f (T l ds) = T (f l) (map f <$> ds)
 53 |
 54 | export
 55 | filter : (a -> Bool) -> Tree a -> Maybe (Tree a)
 56 | filter f (T l ds) =
 57 |    if f l then Just $ T l (mapMaybe (filter f) ds) else Nothing
 58 |
 59 | public export
 60 | 0 TreeMap : Type -> Type
 61 | TreeMap a = SortedMap a (Tree a)
 62 |
 63 | 0 TreeST : Type -> Type -> Type
 64 | TreeST a t = State (TreeMap a) t
 65 |
 66 | tree : Ord a => Graph a -> a -> TreeST a (Tree a)
 67 | tree g k = do
 68 |   Nothing <- lookup k <$> get | Just t => pure t
 69 |   ts      <- traverse (tree g) (maybe [] id $ lookup k g)
 70 |   modify (insert k $ T k ts)
 71 |   pure $ T k ts
 72 |
 73 | export
 74 | treeMap : Ord a => Graph a -> TreeMap a
 75 | treeMap g = execState empty $ traverse_ (ignore . tree g) (keys g)
 76 |
 77 | export %inline
 78 | childMap : SortedMap PkgName (ResolvedLib t) -> TreeMap PkgName
 79 | childMap = treeMap . dependencyGraph
 80 |
 81 | export %inline
 82 | parentMap : SortedMap PkgName (ResolvedLib t) -> TreeMap PkgName
 83 | parentMap = treeMap . invertGraph . dependencyGraph
 84 |
 85 | export
 86 | treeLookup : Ord a => a -> TreeMap a -> Tree a
 87 | treeLookup v = fromMaybe (T v []) . lookup v
 88 |
 89 | --------------------------------------------------------------------------------
 90 | --          Pretty-printing Tree
 91 | --------------------------------------------------------------------------------
 92 |
 93 | parameters {0 a     : Type}
 94 |            {auto ip : Interpolation a}
 95 |            (rev     : Bool)
 96 |
 97 |   0 PrettyST : Type -> Type
 98 |   PrettyST t = State (SnocList String) t
 99 |
100 |   lst : String
101 |   lst = if rev then "┌─" else "└─"
102 |
103 |   append : String -> PrettyST ()
104 |   append s = modify (:< s)
105 |
106 |   children : String -> List (Tree a) -> PrettyST ()
107 |   children _   []       = pure ()
108 |   children pre [T l cs] = do
109 |     append (pre ++ lst ++ "\{l}")
110 |     children (pre ++ "  ") cs
111 |
112 |   children pre (T l cs :: xs) = do
113 |     append (pre ++ "├─\{l}")
114 |     children (pre ++ "│ ") cs
115 |     children pre xs
116 |
117 |   export %inline
118 |   prettyTree : Tree a -> String
119 |   prettyTree (T l cs) =
120 |     let ss := execState [<"\{l}"] (children "" cs) <>> []
121 |      in if rev then unlines (reverse ss) else unlines ss
122 |