0 | module Data.Container.Base.RoseTree.Instances
  1 |
  2 | import Data.Fin
  3 | import Data.Vect
  4 | import Data.List.Quantifiers
  5 |
  6 | import Data.Container.Base.Object.Definition
  7 | import Data.Container.Base.Morphism.Definition
  8 | import Data.Container.Base.Extension.Definition
  9 | import Data.Container.Base.Properties.Definition
 10 | import Data.Container.Base.Product.Definition
 11 | import Data.Container.Base.Object.Instances
 12 | import Data.Container.Base.Morphism.Instances
 13 | import Data.Container.Base.Extension.Instances
 14 | import Data.Container.Base.Properties.Instances
 15 | import Data.Container.Base.Monoid.Definition
 16 | import Data.Container.Base.Monoid.Instances
 17 | import Data.Container.Base.RoseTree.Definition
 18 |
 19 | import Data.Trees
 20 |
 21 | ||| Generalisation of Rose trees with a container of subtrees instead of
 22 | ||| a list of subtrees. It's required that the container is a TensorMonoid
 23 | public export
 24 | ApplicativeRoseTree : TensorMonoid c => Cont
 25 | ApplicativeRoseTree = (t : RoseTreeShape c) !> RoseTreePos c t
 26 |
 27 | ||| Same as above, but with data stored at nodes
 28 | public export
 29 | ApplicativeRoseTreeNode : TensorMonoid c => Cont
 30 | ApplicativeRoseTreeNode = (t : RoseTreeShape c) !> RoseTreePosNode c t
 31 |
 32 | ||| Same as above, but with data stored at leaf
 33 | public export
 34 | ApplicativeRoseTreeLeaf : TensorMonoid c => Cont
 35 | ApplicativeRoseTreeLeaf = (t : RoseTreeShape c) !> RoseTreePosLeaf c t
 36 |
 37 | ||| Rose trees with data stored at both nodes and leaves
 38 | public export
 39 | RoseTree : Cont
 40 | RoseTree = ApplicativeRoseTree {c=List}
 41 |   
 42 | ||| Rose trees with data stored at nodes
 43 | public export
 44 | RoseTreeNode : Cont
 45 | RoseTreeNode = ApplicativeRoseTreeNode {c=List}
 46 |   
 47 | ||| Rose trees with data stored at leaves
 48 | public export
 49 | RoseTreeLeaf : Cont
 50 | RoseTreeLeaf = ApplicativeRoseTreeLeaf {c=List}
 51 |
 52 |
 53 | {-
 54 | old rose tree implementation
 55 | namespace RoseTrees
 56 |   ||| Rose tree, a tree with a variable number of children.
 57 |   ||| This can likely be generalised to other Applicatives than List
 58 |   public export
 59 |   data RoseTreeShape : Type where
 60 |     LeafS : RoseTreeShape
 61 |     NodeS : List RoseTreeShape -> RoseTreeShape
 62 |
 63 |   %runElab derive "RoseTreeShape" [Eq, Show]
 64 |   %name RoseTreeShape t, t1, t2, t3
 65 |
 66 |   public export
 67 |   numLeaves : RoseTreeShape -> Nat
 68 |   numLeaves LeafS = 1
 69 |   numLeaves (NodeS ts) = sum (numLeaves <$> ts)
 70 |   
 71 |   public export
 72 |   numNodes : RoseTreeShape -> Nat
 73 |   numNodes LeafS = 0
 74 |   numNodes (NodeS ts) = 1 + sum (numNodes <$> ts)
 75 |
 76 |   namespace NodesAndLeaves
 77 |     ||| Positions corresponding to both nodes and leaves within a RoseTreeShape
 78 |     public export
 79 |     data RoseTreePos : (t : RoseTreeShape) -> Type where
 80 |       AtLeaf : RoseTreePos LeafS
 81 |       AtNode : {ts : List RoseTreeShape} -> RoseTreePos (NodeS ts)
 82 |       SubTree : {ts : List RoseTreeShape} ->
 83 |         (i : Fin (length ts)) -> -- which subtree
 84 |         RoseTreePos (index' ts i) -> -- position in that subtree
 85 |         RoseTreePos (NodeS ts)
 86 |
 87 |     -- For some reason the line below breaks?
 88 |     -- %runElab deriveIndexed "RoseTreePos" [Eq, Show]
 89 |
 90 |   namespace Nodes
 91 |     ||| Positions corresponding to internal nodes within a RoseTreeNode shape.
 92 |     public export
 93 |     data RoseTreePosNode : (t : RoseTreeShape) -> Type where
 94 |       Done : {ts : List RoseTreeShape} -> RoseTreePosNode (NodeS ts)
 95 |       SubTree : {ts : List RoseTreeShape} ->
 96 |         (i : Fin (length ts)) -> -- which subtree
 97 |         RoseTreePosNode (index' ts i) -> -- position in that subtree
 98 |         RoseTreePosNode (NodeS ts)
 99 |
100 |     -- %runElab deriveIndexed "RoseTreePosNode" [Eq, Show]
101 |   
102 |   namespace Leaves
103 |     ||| Positions corresponding to leaves within a RoseTreeLeaf shape.
104 |     public export
105 |     data RoseTreePosLeaf : (t : RoseTreeShape) -> Type where
106 |       Done : RoseTreePosLeaf LeafS
107 |       SubTree : {ts : List RoseTreeShape} ->
108 |         (i : Fin (length ts)) -> -- which subtree
109 |         RoseTreePosLeaf (index' ts i) -> -- position in that subtree
110 |         RoseTreePosLeaf (NodeS ts)
111 |   
112 |     -- %runElab deriveIndexed "RoseTreePosLeaf" [Eq, Show]
113 |  -}
114 |
115 |
116 | ||| Isomorphic to Data.Tree.ApplicativeRoseTree (TODO)
117 | public export
118 | ApplicativeRoseTree' : TensorMonoid c => Type -> Type
119 | ApplicativeRoseTree' = Ext (ApplicativeRoseTree {c=c})
120 |
121 | public export
122 | ApplicativeRoseTreeNode' : TensorMonoid c => Type -> Type
123 | ApplicativeRoseTreeNode' = Ext (ApplicativeRoseTreeNode {c=c})
124 |
125 | public export
126 | ApplicativeRoseTreeLeaf' : TensorMonoid c => Type -> Type
127 | ApplicativeRoseTreeLeaf' = Ext (ApplicativeRoseTreeLeaf {c=c})
128 |
129 |
130 | ||| Isomorphic to Data.Tree.RoseTree
131 | public export
132 | RoseTree' : Type -> Type
133 | RoseTree' = Ext RoseTree
134 |
135 | ||| Isomorphic to Data.Tree.RoseTreeNode (TODO)
136 | public export
137 | RoseTreeNode' : Type -> Type
138 | RoseTreeNode' = Ext RoseTreeNode
139 |
140 | ||| Isomorphic to Data.Tree.RoseTreeLeaf (TODO)
141 | public export
142 | RoseTreeLeaf' : Type -> Type
143 | RoseTreeLeaf' = Ext RoseTreeLeaf
144 |
145 |
146 |
147 | public export covering
148 | fromRoseTreeSame : RoseTreeSame a -> RoseTree' a
149 | fromRoseTreeSame (Leaf a) = LeafS <| \_ => a
150 | fromRoseTreeSame (Node a rts) =
151 |   let t = fromRoseTreeSame <$> fromList rts
152 |   in NodeS (shapeExt <$> t) <| \case
153 |     AtNode => a
154 |     SubTree ps posSt =>
155 |       let rw1 : (shapeExt t = shapeExt (shapeExt <$> t)) := sym (mapShapeExt t)
156 |           rw2 : (shapeExt (index t (rewrite sym (mapShapeExt {f=shapeExt} t) in ps)) = index (shapeExt <$> t) ps) := mapIndexCont {c=List} {f=shapeExt} t ps
157 |       in index
158 |       (index t (rewrite rw1 in ps))
159 |       (rewrite rw2 in posSt)
160 |       -- for some reason all the explicit type annotations above are needed
161 |       -- to convince the typechecker
162 |
163 | public export covering
164 | toRoseTreeSame : RoseTree' a -> RoseTreeSame a
165 | toRoseTreeSame (LeafS <| contentAt) = Leaf (contentAt AtLeaf)
166 | toRoseTreeSame (NodeS (len <| content) <| contentAt)
167 |   = Node (contentAt AtNode)
168 |          (toList $ toRoseTreeSame 
169 |                 <$> (\i => content i <| contentAt . SubTree i)
170 |                 <$> positionsCont)
171 |
172 | public export covering
173 | IsConcrete RoseTree where
174 |   func = RoseTreeSame
175 |   functorInstance = %search
176 |   fromConcreteTy = fromRoseTreeSame
177 |   toConcreteTy = toRoseTreeSame
178 |
179 |
180 | ||| In `Data.Tree` we have analogos maps that need to be translated here
181 | public export
182 | TensorMonoid c => TensorMonoid (ApplicativeRoseTree {c=c}) where
183 |   tensorN = !% \() => (LeafS ** \_ => ())
184 |   tensorM = !% \(lt, rt) => ?applicativeRoseTree_tensorM
185 |
186 | public export
187 | TensorMonoid c => TensorMonoid (ApplicativeRoseTreeLeaf {c=c}) where
188 |   tensorN = ?applicativeRoseTreeLeaf_tensorN
189 |   tensorM = ?applicativeRoseTreeLeaf_tensorM
190 |
191 | -- Node version likely does not exist?
192 | public export
193 | TensorMonoid c => TensorMonoid (ApplicativeRoseTreeNode {c=c}) where
194 |   tensorN = ?applicativeRoseTreeNode_tensorN
195 |   tensorM = ?applicativeRoseTreeNode_tensorM
196 |
197 |   -- public export
198 |   -- ApplicativeRoseTree : ContA -> ContA
199 |   -- ApplicativeRoseTree c = (#) (ApplicativeRoseTree c)
200 |
201 |
202 | -- namespace RoseTreeInstances
203 | --   -- TODO this should be superseeded by the general applicative instance above?
204 | --   public export
205 | --   liftA2RoseTree' : RoseTree' a -> RoseTree' b -> RoseTree' (a, b)
206 | --   liftA2RoseTree' t1 t2 = fromRoseTreeSame $
207 | --     liftA2RoseTreeSame (toRoseTreeSame t1) (toRoseTreeSame t2)
208 | -- 
209 | --   public export
210 | --   Applicative RoseTree' where
211 | --     pure a = LeafS <| \_ => a
212 | --     fs <*> vs = uncurry ($) <$> liftA2RoseTree' fs vs
213 |