0 | module Data.Container.Base.TreeUtils
  1 |
  2 | import Decidable.Equality
  3 | import Language.Reflection
  4 | import Derive.Prelude
  5 |
  6 | import Data.Container.Base.Object.Definition
  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 |     ||| Check if a term is a subterm of another term
 70 |     ||| t1 < t2 means that t2 > t1
 71 |     public export
 72 |     MOrd (BinTreePos b) where
 73 |       mcompare AtLeaf AtLeaf = Just EQ
 74 |       mcompare AtNode AtNode = Just EQ
 75 |       mcompare (GoLeft b1) (GoLeft b2) = mcompare b1 b2
 76 |       mcompare (GoRight b1) (GoRight b2) = mcompare b1 b2
 77 |       mcompare AtNode (GoLeft _) = Just LT
 78 |       mcompare AtNode (GoRight _) = Just LT
 79 |       mcompare (GoLeft _) AtNode = Just GT
 80 |       mcompare (GoRight _) AtNode = Just GT
 81 |       mcompare (GoLeft _) (GoRight _) = Nothing -- they diverge
 82 |       mcompare (GoRight _) (GoLeft _) = Nothing -- they diverge
 83 |       -- for quantitave version of MOrd the last two should map to BinTreePos b extende with a negative direction
 84 |
 85 |
 86 |   namespace Nodes
 87 |     ||| Positions corresponding to nodes within a BinTreeNode shape.
 88 |     public export
 89 |     data BinTreePosNode : (b : BinTreeShape) -> Type where
 90 |       AtNode : {l, r : BinTreeShape} -> BinTreePosNode (NodeS l r)
 91 |       GoLeft  : {l, r : BinTreeShape} -> BinTreePosNode l -> BinTreePosNode (NodeS l r)
 92 |       GoRight  : {l, r : BinTreeShape} -> BinTreePosNode r -> BinTreePosNode (NodeS l r)
 93 |
 94 |     %runElab deriveIndexed "BinTreePosNode" [Eq, Show]
 95 |
 96 |     public export
 97 |     MOrd (BinTreePosNode b) where
 98 |       mcompare AtNode AtNode = Just EQ
 99 |       mcompare (GoLeft b1) (GoLeft b2) = mcompare b1 b2
100 |       mcompare (GoRight b1) (GoRight b2) = mcompare b1 b2
101 |       mcompare AtNode (GoLeft _) = Just LT
102 |       mcompare AtNode (GoRight _) = Just LT
103 |       mcompare (GoLeft _) AtNode = Just GT
104 |       mcompare (GoRight _) AtNode = Just GT
105 |       mcompare (GoLeft _) (GoRight _) = Nothing -- they diverge
106 |       mcompare (GoRight _) (GoLeft _) = Nothing -- they diverge
107 |   
108 |   namespace Leaves
109 |     ||| Positions corresponding to leaves within a BinTreeShape 
110 |     public export
111 |     data BinTreePosLeaf : (b : BinTreeShape) -> Type where
112 |       AtLeaf : BinTreePosLeaf LeafS
113 |       GoLeft : {l, r : BinTreeShape} -> BinTreePosLeaf l -> BinTreePosLeaf (NodeS l r)
114 |       GoRight : {l, r : BinTreeShape} -> BinTreePosLeaf r -> BinTreePosLeaf (NodeS l r)
115 |
116 |     %runElab deriveIndexed "BinTreePosLeaf" [Eq, Show]
117 |
118 |     public export
119 |     MOrd (BinTreePosLeaf b) where
120 |       mcompare AtLeaf AtLeaf = Just EQ
121 |       mcompare (GoLeft b1) (GoLeft b2) = mcompare b1 b2
122 |       mcompare (GoRight b1) (GoRight b2) = mcompare b1 b2
123 |       mcompare (GoLeft _) (GoRight _) = Nothing -- they diverge
124 |       mcompare (GoRight _) (GoLeft _) = Nothing -- they diverge