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.Extension.Definition
  8 |
  9 | import Data.Container.SubTerm
 10 |
 11 | %language ElabReflection
 12 |
 13 | {-------------------------------------------------------------------------------
 14 | {-------------------------------------------------------------------------------
 15 | This file defines the types of shapes and positions 
 16 | for various tree types for usage in containers.
 17 | All of the trees here are *finite*.
 18 |
 19 | Specifically, this file defines the type of shapes of 
 20 | * Binary trees, together with the type of positions for
 21 |   * Binary trees with data stored both at nodes and leaves
 22 |   * Binary trees with data stored at nodes only
 23 |   * Binary trees with data stored at leaves only
 24 | * Rose trees, together with the type of positions for
 25 |   * Rose trees with data stored both at nodes and leaves
 26 |   * Rose trees with data stored at nodes only
 27 |   * Rose trees with data stored at leaves only
 28 | -------------------------------------------------------------------------------}
 29 | -------------------------------------------------------------------------------}
 30 |
 31 |
 32 | namespace BinaryTrees
 33 |   ||| Shapes of binary trees
 34 |   public export
 35 |   data BinTreeShape : Type where
 36 |     LeafS : BinTreeShape
 37 |     NodeS : BinTreeShape -> BinTreeShape -> BinTreeShape
 38 |
 39 |   %runElab derive "BinTreeShape" [Eq, Show]
 40 |   %name BinTreeShape b, b1, b2, b3, b4, b5
 41 |
 42 |   public export
 43 |   numLeaves : BinTreeShape -> Nat
 44 |   numLeaves LeafS = 1
 45 |   numLeaves (NodeS lt rt) = numLeaves lt + numLeaves rt
 46 |   
 47 |   public export
 48 |   numNodes : BinTreeShape -> Nat
 49 |   numNodes LeafS = 0
 50 |   numNodes (NodeS lt rt) = numNodes lt + (1 + numNodes rt)
 51 |
 52 |   public export
 53 |   numNodesAndLeaves : BinTreeShape -> Nat
 54 |   numNodesAndLeaves LeafS = 1
 55 |   numNodesAndLeaves (NodeS lt rt)
 56 |     = numNodesAndLeaves lt + (1 + numNodesAndLeaves rt)
 57 |   
 58 |   namespace NodesAndLeaves
 59 |     ||| Positions corresponding to both nodes and leaves within a BinTreeShape
 60 |     public export
 61 |     data BinTreePos : (b : BinTreeShape) -> Type where
 62 |       AtLeaf : BinTreePos LeafS
 63 |       AtNode : {l, r : BinTreeShape} -> BinTreePos (NodeS l r)
 64 |       GoLeft : {l, r : BinTreeShape} -> BinTreePos l -> BinTreePos (NodeS l r)
 65 |       GoRight : {l, r : BinTreeShape} -> BinTreePos r -> BinTreePos (NodeS l r)
 66 |
 67 |     %runElab deriveIndexed "BinTreePos" [Eq, Show]
 68 |
 69 |     public export
 70 |     DecEq (BinTreePos b) where
 71 |       decEq AtLeaf AtLeaf = Yes Refl
 72 |       decEq AtNode AtNode = Yes Refl
 73 |       decEq (GoLeft p) (GoLeft q) = case decEq p q of
 74 |         Yes Refl => Yes Refl
 75 |         No contra => No (\Refl => contra Refl)
 76 |       decEq (GoRight p) (GoRight q) = case decEq p q of
 77 |         Yes Refl => Yes Refl
 78 |         No contra => No (\Refl => contra Refl)
 79 |       decEq AtNode (GoLeft _) = No (\case Refl impossible)
 80 |       decEq AtNode (GoRight _) = No (\case Refl impossible)
 81 |       decEq (GoLeft _) AtNode = No (\case Refl impossible)
 82 |       decEq (GoLeft _) (GoRight _) = No (\case Refl impossible)
 83 |       decEq (GoRight _) AtNode = No (\case Refl impossible)
 84 |       decEq (GoRight _) (GoLeft _) = No (\case Refl impossible)
 85 |
 86 |     ||| Check if a term is a subterm of another term
 87 |     ||| t1 < t2 means that t2 > t1
 88 |     public export
 89 |     MOrd (BinTreePos b) where
 90 |       mcompare AtLeaf AtLeaf = Just EQ
 91 |       mcompare AtNode AtNode = Just EQ
 92 |       mcompare (GoLeft b1) (GoLeft b2) = mcompare b1 b2
 93 |       mcompare (GoRight b1) (GoRight b2) = mcompare b1 b2
 94 |       mcompare AtNode (GoLeft _) = Just LT
 95 |       mcompare AtNode (GoRight _) = Just LT
 96 |       mcompare (GoLeft _) AtNode = Just GT
 97 |       mcompare (GoRight _) AtNode = Just GT
 98 |       mcompare (GoLeft _) (GoRight _) = Nothing -- they diverge
 99 |       mcompare (GoRight _) (GoLeft _) = Nothing -- they diverge
100 |       -- for quantitave version of MOrd the last two should map to BinTreePos b extende with a negative direction
101 |
102 |
103 |   namespace Nodes
104 |     ||| Positions corresponding to nodes within a BinTreeNode shape.
105 |     public export
106 |     data BinTreePosNode : (b : BinTreeShape) -> Type where
107 |       AtNode : {l, r : BinTreeShape} -> BinTreePosNode (NodeS l r)
108 |       GoLeft  : {l, r : BinTreeShape} -> BinTreePosNode l -> BinTreePosNode (NodeS l r)
109 |       GoRight  : {l, r : BinTreeShape} -> BinTreePosNode r -> BinTreePosNode (NodeS l r)
110 |
111 |     %runElab deriveIndexed "BinTreePosNode" [Eq, Show]
112 |
113 |     public export
114 |     DecEq (BinTreePosNode b) where
115 |       decEq AtNode AtNode = Yes Refl
116 |       decEq (GoLeft p) (GoLeft q) = case decEq p q of
117 |         Yes Refl => Yes Refl
118 |         No contra => No (\Refl => contra Refl)
119 |       decEq (GoRight p) (GoRight q) = case decEq p q of
120 |         Yes Refl => Yes Refl
121 |         No contra => No (\Refl => contra Refl)
122 |       decEq AtNode (GoLeft _) = No (\case Refl impossible)
123 |       decEq AtNode (GoRight _) = No (\case Refl impossible)
124 |       decEq (GoLeft _) AtNode = No (\case Refl impossible)
125 |       decEq (GoLeft _) (GoRight _) = No (\case Refl impossible)
126 |       decEq (GoRight _) AtNode = No (\case Refl impossible)
127 |       decEq (GoRight _) (GoLeft _) = No (\case Refl impossible)
128 |
129 |     public export
130 |     {b : BinTreeShape} -> Finite (BinTreePosNode b) where
131 |       values {b = LeafS} = []
132 |       values {b = (NodeS l r)} =
133 |         let tl = GoLeft <$> values {a=BinTreePosNode l}
134 |             tr = GoRight <$> values {a=BinTreePosNode r}
135 |         in tl ++ [AtNode] ++ tr
136 |
137 |     public export
138 |     MOrd (BinTreePosNode b) where
139 |       mcompare AtNode AtNode = Just EQ
140 |       mcompare (GoLeft b1) (GoLeft b2) = mcompare b1 b2
141 |       mcompare (GoRight b1) (GoRight b2) = mcompare b1 b2
142 |       mcompare AtNode (GoLeft _) = Just LT
143 |       mcompare AtNode (GoRight _) = Just LT
144 |       mcompare (GoLeft _) AtNode = Just GT
145 |       mcompare (GoRight _) AtNode = Just GT
146 |       mcompare (GoLeft _) (GoRight _) = Nothing -- they diverge
147 |       mcompare (GoRight _) (GoLeft _) = Nothing -- they diverge
148 |   
149 |   namespace Leaves
150 |     ||| Positions corresponding to leaves within a BinTreeShape 
151 |     public export
152 |     data BinTreePosLeaf : (b : BinTreeShape) -> Type where
153 |       AtLeaf : BinTreePosLeaf LeafS
154 |       GoLeft : {l, r : BinTreeShape} -> BinTreePosLeaf l -> BinTreePosLeaf (NodeS l r)
155 |       GoRight : {l, r : BinTreeShape} -> BinTreePosLeaf r -> BinTreePosLeaf (NodeS l r)
156 |
157 |     %runElab deriveIndexed "BinTreePosLeaf" [Eq, Show]
158 |
159 |     public export
160 |     DecEq (BinTreePosLeaf b) where
161 |       decEq AtLeaf AtLeaf = Yes Refl
162 |       decEq (GoLeft p) (GoLeft q) = case decEq p q of
163 |         Yes Refl => Yes Refl
164 |         No contra => No (\Refl => contra Refl)
165 |       decEq (GoRight p) (GoRight q) = case decEq p q of
166 |         Yes Refl => Yes Refl
167 |         No contra => No (\Refl => contra Refl)
168 |       decEq (GoLeft _) (GoRight _) = No (\case Refl impossible)
169 |       decEq (GoRight _) (GoLeft _) = No (\case Refl impossible)
170 |
171 |     ||| Assumes a choice of traversal
172 |     public export
173 |     {b : BinTreeShape} -> Finite (BinTreePosLeaf b) where
174 |       values {b = LeafS} = [AtLeaf]
175 |       values {b = (NodeS l r)} =
176 |         let tl = GoLeft <$> values {a=BinTreePosLeaf l}
177 |             tr = GoRight <$> values {a=BinTreePosLeaf r}
178 |         in tl ++ tr
179 |
180 |     public export
181 |     MOrd (BinTreePosLeaf b) where
182 |       mcompare AtLeaf AtLeaf = Just EQ
183 |       mcompare (GoLeft b1) (GoLeft b2) = mcompare b1 b2
184 |       mcompare (GoRight b1) (GoRight b2) = mcompare b1 b2
185 |       mcompare (GoLeft _) (GoRight _) = Nothing -- they diverge
186 |       mcompare (GoRight _) (GoLeft _) = Nothing -- they diverge