
  0 | module BarnesHut
  1 | 
  2 | import Data.Vect
  3 | 
  4 | record Position where
  5 |   x, y : Double
  6 | 
  7 | record QuadParameters where
  8 |   constructor MkQuadParam
  9 |   max_x : Double
 10 |   min_x : Double
 11 |   max_y : Double
 12 |   min_y : Double
 13 | %name QuadParameters qp, qp2, qp3
 14 | 
 15 | namespace QuadParameters
 16 |   public export
 17 |   (.top_right) : QuadParameters -> QuadParameters
 18 |   (.top_right) (MkQuadParam max_x min_x max_y min_y) =
 19 |     let x_mid = (max_x + min_x) / 2
 20 |         y_mid = (max_y + min_y) / 2
 21 |     in MkQuadParam max_x x_mid max_y y_mid
 22 | 
 23 |   public export
 24 |   (.top_left) : QuadParameters -> QuadParameters
 25 |   (.top_left) (MkQuadParam max_x min_x max_y min_y) =
 26 |     let x_mid = (max_x + min_x) / 2
 27 |         y_mid = (max_y + min_y) / 2
 28 |     in MkQuadParam x_mid min_x max_y y_mid
 29 | 
 30 |   public export
 31 |   (.bottom_right) : QuadParameters -> QuadParameters
 32 |   (.bottom_right) (MkQuadParam max_x min_x max_y min_y) =
 33 |     let x_mid = (max_x + min_x) / 2
 34 |         y_mid = (max_y + min_y) / 2
 35 |     in MkQuadParam max_x x_mid y_mid min_y
 36 | 
 37 |   public export
 38 |   (.bottom_left) : QuadParameters -> QuadParameters
 39 |   (.bottom_left) (MkQuadParam max_x min_x max_y min_y) =
 40 |     let x_mid = (max_x + min_x) / 2
 41 |         y_mid = (max_y + min_y) / 2
 42 |     in MkQuadParam x_mid min_x y_mid min_y
 43 | 
 44 | data Structure : QuadParameters -> Type where
 45 |   ILeaf : Structure qp
 46 |   INode : (top_right : Structure qp.top_right)
 47 |        -> (top_left : Structure qp.top_left)
 48 |        -> (bottom_right : Structure qp.bottom_right)
 49 |        -> (bottom_left : Structure qp.bottom_left)
 50 |        -> Structure qp
 51 | 
 52 | data Quadrant : (qp : QuadParameters) -> Structure qp -> Type -> Type where
 53 |   Empty : Quadrant qp ILeaf a
 54 |   Leaf : (pos : Position) -> (content : a) -> Quadrant qp ILeaf a
 55 |   Node : (top_right : Quadrant qp.top_right s_tr a)
 56 |       -> (top_left : Quadrant qp.top_left s_top_left a)
 57 |       -> (bottom_right : Quadrant qp.bottom_right s_bottom_right a)
 58 |       -> (bottom_left : Quadrant qp.bottom_left s_bottom_left a)
 59 |       -> Quadrant qp (INode s_tr s_tl s_br s_bl) a
 60 |