0 | module Data.Container.Base.RoseTree.Definition
 1 |
 2 | import Data.Container.Base.Object.Definition
 3 | import Data.Container.Base.Extension.Definition
 4 | import Data.Container.Base.Monoid.Definition
 5 |
 6 | -- will be refactored away too
 7 |
 8 | ||| Requires a TensorMonoid (Applicative) to even be stated
 9 | namespace RoseTree
10 |   public export
11 |   data RoseTreeShape : (0 c : Cont) -> TensorMonoid c => Type where
12 |     LeafS : TensorMonoid c => RoseTreeShape c
13 |     NodeS : TensorMonoid c => c `fullOf` (RoseTreeShape c) -> RoseTreeShape c
14 |
15 |   public export covering
16 |   numLeaves : TensorMonoid c => Foldable (Ext c) => RoseTreeShape c -> Nat
17 |   numLeaves LeafS = 1
18 |   numLeaves (NodeS exts) = sum (numLeaves <$> exts)
19 |
20 |   public export covering
21 |   numNodes : TensorMonoid c => Foldable (Ext c) => RoseTreeShape c -> Nat
22 |   numNodes LeafS = 0
23 |   numNodes (NodeS exts) = 1 + sum (numNodes <$> exts)
24 |
25 |   namespace NodesAndLeaves
26 |     ||| Positions corresponding to both nodes and leaves within a RoseTreeShape
27 |     public export
28 |     data RoseTreePos :
29 |       (0 c : Cont) -> TensorMonoid c => RoseTreeShape c -> Type where
30 |       AtLeaf : TensorMonoid c => RoseTreePos c LeafS
31 |       AtNode : TensorMonoid c => {ts : c `fullOf` (RoseTreeShape c)} ->
32 |         RoseTreePos c (NodeS ts)
33 |       SubTree : TensorMonoid c => {ts : c `fullOf` (RoseTreeShape c)} ->
34 |         (ps : c.Pos (shapeExt ts)) -> -- position in a given list
35 |         RoseTreePos c (index ts ps) -> -- position in the shape of RoseTree at a location specified by ps
36 |         RoseTreePos c (NodeS ts)
37 |
38 |
39 |   namespace Nodes
40 |     public export
41 |     data RoseTreePosNode :
42 |       (0 c : Cont) -> TensorMonoid c => RoseTreeShape c -> Type where
43 |       AtNode : TensorMonoid c => {ts : c `fullOf` (RoseTreeShape c)} ->
44 |         RoseTreePosNode c (NodeS ts)
45 |       SubTree : TensorMonoid c => {ts : c `fullOf` (RoseTreeShape c)} ->
46 |         (ps : c.Pos (shapeExt ts)) -> -- position in a given list
47 |         RoseTreePosNode c (index ts ps) -> -- position in the sub-tree at the above defined position
48 |         RoseTreePosNode c (NodeS ts)
49 |
50 |   namespace Leaves
51 |     public export
52 |     data RoseTreePosLeaf :
53 |       (0 c : Cont) -> TensorMonoid c => RoseTreeShape c -> Type where
54 |       AtLeaf : TensorMonoid c => RoseTreePosLeaf c LeafS
55 |       SubTree : TensorMonoid c => {ts : c `fullOf` (RoseTreeShape c)} ->
56 |         (ps : c.Pos (shapeExt ts)) -> -- position in a given list
57 |         RoseTreePosLeaf c (index ts ps) -> -- position in the sub-tree at the above defined position
58 |         RoseTreePosLeaf c (NodeS ts)
59 |