0 | module Data.Container.Applicative.Object.Instances
 1 |
 2 | import Data.Container.Base
 3 | import Data.Container.Applicative.TreeUtils
 4 |
 5 | ||| Generalisation of Rose trees with a container of subtrees instead of
 6 | ||| a list of subtrees. It's required that the container is a TensorMonoid
 7 | public export
 8 | ApplicativeRoseTree : {c : Cont} -> TensorMonoid c => Cont
 9 | ApplicativeRoseTree = (t : RoseTreeShape c) !> RoseTreePos c t
10 |
11 | ||| Same as above, but with data stored at nodes
12 | public export
13 | ApplicativeRoseTreeNode : {c : Cont} -> TensorMonoid c => Cont
14 | ApplicativeRoseTreeNode = (t : RoseTreeShape c) !> RoseTreePosNode c t
15 |
16 | ||| Same as above, but with data stored at leaf
17 | public export
18 | ApplicativeRoseTreeLeaf : {c : Cont} -> TensorMonoid c => Cont
19 | ApplicativeRoseTreeLeaf = (t : RoseTreeShape c) !> RoseTreePosNode c t
20 |
21 | ||| Rose trees with data stored at both nodes and leaves
22 | public export
23 | RoseTree : Cont
24 | RoseTree = ApplicativeRoseTree {c=List}
25 |   
26 | ||| Rose trees with data stored at nodes
27 | public export
28 | RoseTreeNode : Cont
29 | RoseTreeNode = ApplicativeRoseTreeNode {c=List}
30 |   
31 | ||| Rose trees with data stored at leaves
32 | public export
33 | RoseTreeLeaf : Cont
34 | RoseTreeLeaf = ApplicativeRoseTreeLeaf {c=List}
35 |
36 |
37 | {-
38 | old rose tree implementation
39 | namespace RoseTrees
40 |   ||| Rose tree, a tree with a variable number of children.
41 |   ||| This can likely be generalised to other Applicatives than List
42 |   public export
43 |   data RoseTreeShape : Type where
44 |     LeafS : RoseTreeShape
45 |     NodeS : List RoseTreeShape -> RoseTreeShape
46 |
47 |   %runElab derive "RoseTreeShape" [Eq, Show]
48 |   %name RoseTreeShape t, t1, t2, t3
49 |
50 |   public export
51 |   numLeaves : RoseTreeShape -> Nat
52 |   numLeaves LeafS = 1
53 |   numLeaves (NodeS ts) = sum (numLeaves <$> ts)
54 |   
55 |   public export
56 |   numNodes : RoseTreeShape -> Nat
57 |   numNodes LeafS = 0
58 |   numNodes (NodeS ts) = 1 + sum (numNodes <$> ts)
59 |
60 |   namespace NodesAndLeaves
61 |     ||| Positions corresponding to both nodes and leaves within a RoseTreeShape
62 |     public export
63 |     data RoseTreePos : (t : RoseTreeShape) -> Type where
64 |       AtLeaf : RoseTreePos LeafS
65 |       AtNode : {ts : List RoseTreeShape} -> RoseTreePos (NodeS ts)
66 |       SubTree : {ts : List RoseTreeShape} ->
67 |         (i : Fin (length ts)) -> -- which subtree
68 |         RoseTreePos (index' ts i) -> -- position in that subtree
69 |         RoseTreePos (NodeS ts)
70 |
71 |     -- For some reason the line below breaks?
72 |     -- %runElab deriveIndexed "RoseTreePos" [Eq, Show]
73 |
74 |   namespace Nodes
75 |     ||| Positions corresponding to internal nodes within a RoseTreeNode shape.
76 |     public export
77 |     data RoseTreePosNode : (t : RoseTreeShape) -> Type where
78 |       Done : {ts : List RoseTreeShape} -> RoseTreePosNode (NodeS ts)
79 |       SubTree : {ts : List RoseTreeShape} ->
80 |         (i : Fin (length ts)) -> -- which subtree
81 |         RoseTreePosNode (index' ts i) -> -- position in that subtree
82 |         RoseTreePosNode (NodeS ts)
83 |
84 |     -- %runElab deriveIndexed "RoseTreePosNode" [Eq, Show]
85 |   
86 |   namespace Leaves
87 |     ||| Positions corresponding to leaves within a RoseTreeLeaf shape.
88 |     public export
89 |     data RoseTreePosLeaf : (t : RoseTreeShape) -> Type where
90 |       Done : RoseTreePosLeaf LeafS
91 |       SubTree : {ts : List RoseTreeShape} ->
92 |         (i : Fin (length ts)) -> -- which subtree
93 |         RoseTreePosLeaf (index' ts i) -> -- position in that subtree
94 |         RoseTreePosLeaf (NodeS ts)
95 |   
96 |     -- %runElab deriveIndexed "RoseTreePosLeaf" [Eq, Show]
97 |  -}