0 | module Data.Container.Base.TreeUtils
  1 |
  2 | import Decidable.Equality
  3 | import Language.Reflection
  4 | import Derive.Prelude
  5 | import Data.Finite
  6 |
  7 | import Data.Container.Base.Object.Definition
  8 | import Data.Container.Base.Extension.Definition
  9 |
 10 | import Data.Container.SubTerm
 11 |
 12 | %language ElabReflection
 13 |
 14 | {-------------------------------------------------------------------------------
 15 | {-------------------------------------------------------------------------------
 16 | This file defines the types of shapes and positions 
 17 | for various tree types for usage in containers.
 18 | All of the trees here are *finite*.
 19 |
 20 | Specifically, this file defines the type of shapes of 
 21 | * Binary trees, together with the type of positions for
 22 |   * Binary trees with data stored both at nodes and leaves
 23 |   * Binary trees with data stored at nodes only
 24 |   * Binary trees with data stored at leaves only
 25 | * Rose trees, together with the type of positions for
 26 |   * Rose trees with data stored both at nodes and leaves
 27 |   * Rose trees with data stored at nodes only
 28 |   * Rose trees with data stored at leaves only
 29 | -------------------------------------------------------------------------------}
 30 | -------------------------------------------------------------------------------}
 31 |
 32 |
 33 | namespace BinaryTrees
 34 |   ||| Shapes of binary trees
 35 |   public export
 36 |   data BinTreeShape : Type where
 37 |     LeafS : BinTreeShape
 38 |     NodeS : BinTreeShape -> BinTreeShape -> BinTreeShape
 39 |
 40 |   %runElab derive "BinTreeShape" [Eq, Show]
 41 |   %name BinTreeShape b, b1, b2, b3, b4, b5
 42 |
 43 |   public export
 44 |   numLeaves : BinTreeShape -> Nat
 45 |   numLeaves LeafS = 1
 46 |   numLeaves (NodeS lt rt) = numLeaves lt + numLeaves rt
 47 |   
 48 |   public export
 49 |   numNodes : BinTreeShape -> Nat
 50 |   numNodes LeafS = 0
 51 |   numNodes (NodeS lt rt) = numNodes lt + (1 + numNodes rt)
 52 |
 53 |   public export
 54 |   numNodesAndLeaves : BinTreeShape -> Nat
 55 |   numNodesAndLeaves LeafS = 1
 56 |   numNodesAndLeaves (NodeS lt rt)
 57 |     = numNodesAndLeaves lt + (1 + numNodesAndLeaves rt)
 58 |   
 59 |   namespace NodesAndLeaves
 60 |     ||| Positions corresponding to both nodes and leaves within a BinTreeShape
 61 |     public export
 62 |     data BinTreePos : (b : BinTreeShape) -> Type where
 63 |       AtLeaf : BinTreePos LeafS
 64 |       AtNode : {l, r : BinTreeShape} -> BinTreePos (NodeS l r)
 65 |       GoLeft : {l, r : BinTreeShape} -> BinTreePos l -> BinTreePos (NodeS l r)
 66 |       GoRight : {l, r : BinTreeShape} -> BinTreePos r -> BinTreePos (NodeS l r)
 67 |
 68 |     %runElab deriveIndexed "BinTreePos" [Eq, Show]
 69 |
 70 |     ||| Check if a term is a subterm of another term
 71 |     ||| t1 < t2 means that t2 > t1
 72 |     public export
 73 |     MOrd (BinTreePos b) where
 74 |       mcompare AtLeaf AtLeaf = Just EQ
 75 |       mcompare AtNode AtNode = Just EQ
 76 |       mcompare (GoLeft b1) (GoLeft b2) = mcompare b1 b2
 77 |       mcompare (GoRight b1) (GoRight b2) = mcompare b1 b2
 78 |       mcompare AtNode (GoLeft _) = Just LT
 79 |       mcompare AtNode (GoRight _) = Just LT
 80 |       mcompare (GoLeft _) AtNode = Just GT
 81 |       mcompare (GoRight _) AtNode = Just GT
 82 |       mcompare (GoLeft _) (GoRight _) = Nothing -- they diverge
 83 |       mcompare (GoRight _) (GoLeft _) = Nothing -- they diverge
 84 |       -- for quantitave version of MOrd the last two should map to BinTreePos b extende with a negative direction
 85 |
 86 |
 87 |   namespace Nodes
 88 |     ||| Positions corresponding to nodes within a BinTreeNode shape.
 89 |     public export
 90 |     data BinTreePosNode : (b : BinTreeShape) -> Type where
 91 |       AtNode : {l, r : BinTreeShape} -> BinTreePosNode (NodeS l r)
 92 |       GoLeft  : {l, r : BinTreeShape} -> BinTreePosNode l -> BinTreePosNode (NodeS l r)
 93 |       GoRight  : {l, r : BinTreeShape} -> BinTreePosNode r -> BinTreePosNode (NodeS l r)
 94 |
 95 |     %runElab deriveIndexed "BinTreePosNode" [Eq, Show]
 96 |
 97 |     public export
 98 |     {b : BinTreeShape} -> Finite (BinTreePosNode b) where
 99 |       values {b = LeafS} = []
100 |       values {b = (NodeS l r)} =
101 |         let tl = GoLeft <$> values {a=BinTreePosNode l}
102 |             tr = GoRight <$> values {a=BinTreePosNode r}
103 |         in tl ++ [AtNode] ++ tr
104 |
105 |     public export
106 |     MOrd (BinTreePosNode b) where
107 |       mcompare AtNode AtNode = Just EQ
108 |       mcompare (GoLeft b1) (GoLeft b2) = mcompare b1 b2
109 |       mcompare (GoRight b1) (GoRight b2) = mcompare b1 b2
110 |       mcompare AtNode (GoLeft _) = Just LT
111 |       mcompare AtNode (GoRight _) = Just LT
112 |       mcompare (GoLeft _) AtNode = Just GT
113 |       mcompare (GoRight _) AtNode = Just GT
114 |       mcompare (GoLeft _) (GoRight _) = Nothing -- they diverge
115 |       mcompare (GoRight _) (GoLeft _) = Nothing -- they diverge
116 |   
117 |   namespace Leaves
118 |     ||| Positions corresponding to leaves within a BinTreeShape 
119 |     public export
120 |     data BinTreePosLeaf : (b : BinTreeShape) -> Type where
121 |       AtLeaf : BinTreePosLeaf LeafS
122 |       GoLeft : {l, r : BinTreeShape} -> BinTreePosLeaf l -> BinTreePosLeaf (NodeS l r)
123 |       GoRight : {l, r : BinTreeShape} -> BinTreePosLeaf r -> BinTreePosLeaf (NodeS l r)
124 |
125 |     %runElab deriveIndexed "BinTreePosLeaf" [Eq, Show]
126 |
127 |     ||| Assumes a choice of traversal
128 |     public export
129 |     {b : BinTreeShape} -> Finite (BinTreePosLeaf b) where
130 |       values {b = LeafS} = [AtLeaf]
131 |       values {b = (NodeS l r)} =
132 |         let tl = GoLeft <$> values {a=BinTreePosLeaf l}
133 |             tr = GoRight <$> values {a=BinTreePosLeaf r}
134 |         in tl ++ tr
135 |
136 |     public export
137 |     MOrd (BinTreePosLeaf b) where
138 |       mcompare AtLeaf AtLeaf = Just EQ
139 |       mcompare (GoLeft b1) (GoLeft b2) = mcompare b1 b2
140 |       mcompare (GoRight b1) (GoRight b2) = mcompare b1 b2
141 |       mcompare (GoLeft _) (GoRight _) = Nothing -- they diverge
142 |       mcompare (GoRight _) (GoLeft _) = Nothing -- they diverge