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