
   0 | module Geom.Bounds
   1 | 
   2 | import Geom.Angle
   3 | import Geom.Point
   4 | import Geom.Scale
   5 | import Geom.Vector
   6 | import Text.Molfile.Types
   7 | 
   8 | %default total
   9 | 
  10 | ||| Bounds along one axis in an affine space
  11 | export
  12 | data Bounds : Type where
  13 |   ||| Bounds without extent. Contains no points.
  14 |   Empty    : Bounds
  15 | 
  16 |   ||| Concrete bounds.
  17 |   Rng      : (min, max : Double) -> Bounds
  18 | 
  19 | ||| Extract the inner structure of a `Bounds` values.
  20 | |||
  21 | ||| Mostly useful for debugging.
  22 | export
  23 | getBounds : Bounds -> Maybe (Double,Double)
  24 | getBounds Empty     = Nothing
  25 | getBounds (Rng x y) = Just (x,y)
  26 | 
  27 | ||| The empty bounds.
  28 | export %inline
  29 | empty : Bounds
  30 | empty = Empty
  31 | 
  32 | ||| A single point on an axis.
  33 | export
  34 | val : Double -> Bounds
  35 | val v = Rng v v
  36 | 
  37 | ||| the range between two points on a line
  38 | export
  39 | range : (min,max : Double) -> Bounds
  40 | range l u = if l <= u then Rng l u else Empty
  41 | 
  42 | ||| Return the smallest `Bounds` containing all points in both
  43 | ||| argument bounds.
  44 | export
  45 | expand : Bounds -> Bounds -> Bounds
  46 | expand (Rng mi1 ma1) (Rng mi2 ma2) = Rng (min mi1 mi2) (max ma1 ma2)
  47 | expand Empty         v             = v
  48 | expand v             Empty         = v
  49 | 
  50 | ||| Checks if a value is within the given bounds.
  51 | export
  52 | inBounds1D : {default 0.0 margin : Double} -> Double -> Bounds -> Bool
  53 | inBounds1D x (Rng min max) = (min - margin) <= x && x <= (max + margin)
  54 | inBounds1D x Empty         = False
  55 | 
  56 | ||| Computes the middle (center) of a range. Returns `Nothing` if the `Bounds`
  57 | ||| are empty.
  58 | export
  59 | middle : Bounds -> Maybe Double
  60 | middle (Rng min max) = Just $ (max + min) / 2
  61 | middle Empty         = Nothing
  62 | 
  63 | ||| Computes the width of some bounds. Returns `0` if the `Bounds` are empty
  64 | export
  65 | width : Bounds -> Double
  66 | width (Rng min max) = max - min
  67 | width Empty         = 0.0
  68 | 
  69 | ||| Computes half of the width of some bounds.
  70 | ||| Returns `0` if the `Bounds` are empty
  71 | export
  72 | halfWidth : Bounds -> Double
  73 | halfWidth bs = width bs / 2.0
  74 | 
  75 | export %inline
  76 | Semigroup Bounds where (<+>) = expand
  77 | 
  78 | export %inline
  79 | Monoid Bounds where neutral = Empty
  80 | 
  81 | ||| Compounds the overlapping region between two bounds in
  82 | ||| one direction.
  83 | export
  84 | overlap : {default 0.0 margin : Double} -> Bounds -> Bounds -> Bounds
  85 | overlap (Rng mi1 ma1) (Rng mi2 ma2) =
  86 |   range (max mi1 mi2 - margin) (min ma1 ma2 + margin)
  87 | overlap _             _             = Empty
  88 | 
  89 | --------------------------------------------------------------------------------
  90 | --          Bounds 2D
  91 | --------------------------------------------------------------------------------
  92 | 
  93 | ||| Bounds in two dimensions.
  94 | public export
  95 | record Bounds2D (t : AffineTransformation) where
  96 |   constructor BS
  97 |   x : Bounds
  98 |   y : Bounds
  99 | 
 100 | export
 101 | Semigroup (Bounds2D t) where
 102 |   BS x1 y1 <+> BS x2 y2 = BS (x1 <+> x2) (y1 <+> y2)
 103 | 
 104 | export
 105 | Monoid (Bounds2D t) where neutral = BS empty empty
 106 | 
 107 | namespace Bounds2D
 108 |   export
 109 |   width : Bounds2D t -> Double
 110 |   width = width . x
 111 | 
 112 |   export
 113 |   height : Bounds2D t -> Double
 114 |   height = width . y
 115 | 
 116 |   ||| Computes the overlapping rectangle between 2D bounds.
 117 |   export
 118 |   overlap : {default 0.0 margin : Double} -> Bounds2D t -> Bounds2D t -> Bounds2D t
 119 |   overlap (BS x1 y1) (BS x2 y2) = BS (overlap {margin} x1 x2) (overlap {margin} y1 y2)
 120 | 
 121 | ||| Checks, if the point is in within some bounds in its affine space
 122 | ||| by two points.
 123 | export
 124 | inBounds : {default 0.0 margin : Double} -> (p : Point t) -> Bounds2D t -> Bool
 125 | inBounds p (BS x y) = inBounds1D {margin} p.x x && inBounds1D {margin} p.y y
 126 | 
 127 | ||| Return the corners of a bounding rectangle (if any)
 128 | export
 129 | corners : Bounds2D t -> Maybe (Point t, Point t)
 130 | corners (BS (Rng xmin xmax) (Rng ymin ymax)) = Just (P xmin ymin, P xmax ymax)
 131 | corners _                                    = Nothing
 132 | 
 133 | --------------------------------------------------------------------------------
 134 | --          Bounded
 135 | --------------------------------------------------------------------------------
 136 | 
 137 | public export
 138 | interface Bounded (0 a : Type) where
 139 |   constructor BD
 140 |   btrans : AffineTransformation
 141 |   bounds : a -> Bounds2D btrans
 142 | 
 143 | public export %inline
 144 | {t : _} -> Bounded (Bounds2D t) where
 145 |   btrans = t
 146 |   bounds = id
 147 | 
 148 | public export
 149 | Foldable f => (b : Bounded a) => Bounded (f a) where
 150 |   btrans = btrans @{b}
 151 |   bounds = foldMap bounds
 152 | 
 153 | public export %inline
 154 | (g : GetPoint a) => Bounded a where
 155 |   btrans   = gtrans @{g}
 156 |   bounds v = let P x y := point v in BS (val x) (val y)
 157 | 
 158 | export
 159 | convertBounds : {s,t : _} -> Bounds2D s -> Bounds2D t
 160 | convertBounds bs =
 161 |   case corners bs of
 162 |     Just (x,y) => bounds (convert {s,t} x) <+> bounds (convert {s,t} y)
 163 |     Nothing    => neutral
 164 | 
 165 | ||| Calculates the center in a collection of bounded values.
 166 | |||
 167 | ||| Returns the origin in case of an object with empty bounds.
 168 | export
 169 | center : (b : Bounded a) => a -> Point (btrans @{b})
 170 | center ts = case bounds ts of
 171 |   BS x y => fromMaybe origin [| P (middle x) (middle y) |]
 172 | 
 173 | ||| Checks, if the point is in or on the line of a rectangel defined
 174 | ||| by two points.
 175 | export
 176 | inRectangle : {t : _} -> (p, edge1, edge2 : Point t) -> Bool
 177 | inRectangle p e1 e2 = inBounds p (bounds $ the (List _) [e1,e2])
 178 | 
 179 | ||| Translates a bounded value so that the lower-left corner of its
 180 | ||| bound will come to lie at the origin.
 181 | export
 182 | translatePositive : ModPoint a => Bounded a => a -> a
 183 | translatePositive v =
 184 |   case corners $ bounds v of
 185 |     Nothing         => v
 186 |     Just (P x y, _) => translate (V (-x) (-y)) v
 187 | 
 188 | --------------------------------------------------------------------------------
 189 | --          Utilities
 190 | --------------------------------------------------------------------------------
 191 | 
 192 | ||| Computes the distance of a point `p` from the line segment
 193 | ||| between points `pl1` and `pl2`.
 194 | export
 195 | distanceToLineSegment : {t : _} -> (p, pl1, pl2 : Point t) -> Double
 196 | distanceToLineSegment p pl1 pl2 =
 197 |   let pp   := perpendicularPoint p (translate (pl1 - pl2) p) 1 True
 198 |       dflt := min (distance p pl1) (distance p pl2)
 199 |    in case intersect pl1 pl2 p pp of
 200 |         Just i  => if inRectangle i pl1 pl2 then distance p i else dflt
 201 |         Nothing => dflt
 202 | 
 203 | --------------------------------------------------------------------------------
 204 | --          Packing
 205 | --------------------------------------------------------------------------------
 206 | 
 207 | record BVal a where
 208 |   constructor BV
 209 |   val    : a
 210 |   width  : Double
 211 |   height : Double
 212 | 
 213 | record Pos a where
 214 |   constructor P
 215 |   val : a
 216 |   x   : Double
 217 |   y   : Double
 218 | 
 219 | area : BVal a -> Double
 220 | area b = b.width * b.height
 221 | 
 222 | record Rect where
 223 |   constructor R
 224 |   x      : Double
 225 |   y      : Double
 226 |   width  : Double
 227 |   height : Double
 228 | 
 229 | zrect : Rect
 230 | zrect = R 0 0 0 0
 231 | 
 232 | mid : Rect -> Rect -> Rect
 233 | mid s l = R 0 0 ((s.width + l.width)/2) ((s.height + l.height)/2)
 234 | 
 235 | close : Rect -> Rect -> Bool
 236 | close s l = abs (s.width-l.width) <= 0.00001 || abs (s.height-l.height) <= 0.00001
 237 | 
 238 | Bounded Rect where
 239 |   btrans = Id
 240 |   bounds (R x y w h) = BS (range x (x+w)) (range y (y+h))
 241 | 
 242 | rect : (x,y,w,h : Double) -> List Rect
 243 | rect x y w h = if w > 0 && h > 0 then [R x y w h] else []
 244 | 
 245 | public export
 246 | record PackParams where
 247 |   [noHints]
 248 |   constructor PP
 249 |   ||| Horizontal gap between adjacent rectangles
 250 |   gapX  : Double
 251 | 
 252 |   ||| Vertical gap between adjacent rectangles
 253 |   gapY  : Double
 254 | 
 255 |   ||| Maximum number of iterations used in the binary search
 256 |   ||| to find the ideal packaging size
 257 |   iter  : Nat
 258 | 
 259 |   ||| Width-to-height ratio used when aligning the containers
 260 |   ratio : Double
 261 | 
 262 | dflt : PackParams
 263 | dflt = PP 5 2.5 64 1.61803
 264 | 
 265 | ini : PackParams -> List (BVal a) -> Rect
 266 | ini p vs =
 267 |  let l := cast {to = Double} $ length vs
 268 |      w := sum (map width vs)  + l * p.gapX
 269 |      h := sum (map height vs) + l * p.gapY
 270 |      d := max w h
 271 |   in if p.ratio >= 1 then R 0 0 (d * p.ratio) d else R 0 0 d (d / p.ratio)
 272 | 
 273 | 0 Rects : Type
 274 | Rects = List Rect
 275 | 
 276 | fits : BVal a -> Rect -> Bool
 277 | fits bv r = bv.width <= r.width && bv.height <= r.height
 278 | 
 279 | score : BVal a -> Rect -> Double
 280 | score bv r = (r.width - bv.width) * (r.height - bv.height)
 281 | 
 282 | split : BVal a -> Rect -> List Rect
 283 | split (BV v w h) (R x y rw rh) =
 284 |   case rw - w >= rh - h of
 285 |     True  => rect (x+w) y (rw-w) rh ++ rect x (y+h) w  (rh-h)
 286 |     False => rect (x+w) y (rw-w) h  ++ rect x (y+h) rw (rh-h)
 287 | 
 288 | best1 : BVal a -> SnocList Rect -> Rect -> Double -> Rects -> (Pos a, Rects)
 289 | best1 x sr b sc []        = (P x.val b.x b.y, sr <>> split x b)
 290 | best1 x sr b sc (r :: rs) =
 291 |   case fits x r of
 292 |     False => best1 x (sr:<r) b sc rs
 293 |     True  =>
 294 |      let s := score x r
 295 |       in if s < sc then best1 x (sr:<b) r s rs else best1 x (sr:<r) b sc rs
 296 | 
 297 | best : BVal a -> SnocList Rect -> Rects -> Maybe (Pos a, Rects)
 298 | best x sr []        = Nothing
 299 | best x sr (r :: rs) =
 300 |   if fits x r then Just $ best1 x sr r (score x r) rs else best x (sr:<r) rs
 301 | 
 302 | guillotine : SnocList (Pos a) -> List (BVal a) -> Rects -> Maybe (List $ Pos a)
 303 | guillotine sp []        rs = Just (sp <>> [])
 304 | guillotine sp (v :: vs) rs =
 305 |   case best v [<] rs of
 306 |     Just (p,rs2) => guillotine (sp:<p) vs rs2
 307 |     Nothing      => Nothing
 308 | 
 309 | pack : PackParams -> List (BVal a) -> Maybe (List $ Pos a)
 310 | pack p vs = go p.iter zrect (ini p vs) . reverse $ sortBy (comparing area) vs
 311 |   where
 312 |     go : Nat -> (s,l : Rect) -> List (BVal a) -> Maybe (List $ Pos a)
 313 |     go 0     s r vs = guillotine [<] vs [r]
 314 |     go (S k) s r vs =
 315 |       case close s r of
 316 |         True  => guillotine [<] vs [r]
 317 |         False =>
 318 |          let m := mid s r
 319 |           in case guillotine [<] vs [m] of
 320 |                Just rs => go k s m vs
 321 |                Nothing => go k m r vs
 322 | 
 323 | parameters {default dflt p : PackParams}
 324 |            {auto bnd : Bounded a}
 325 |            {auto mp  : ModPoint a}
 326 | 
 327 |   bval : a -> BVal a
 328 |   bval v =
 329 |    let bs := bounds v
 330 |     in BV v (width bs + p.gapX) (height bs + p.gapY)
 331 | 
 332 |   position : Pos a -> a
 333 |   position (P v x y) = Point.translate (V x y) (translatePositive v)
 334 | 
 335 |   ||| Packs rectangular objects in a grid using a guillotine cutting
 336 |   ||| algorithm.
 337 |   |||
 338 |   ||| The minimal size of the rectangle required to pack the items is
 339 |   ||| computed via a binary search (maximum number of iterations is
 340 |   ||| given via the `PackParams` argument).
 341 |   |||
 342 |   ||| Gap sizes in both directions can be specified by the provided
 343 |   ||| `PackParams` argument.
 344 |   export
 345 |   align : List a -> List a
 346 |   align []  = []
 347 |   align [v] = [v]
 348 |   align vs  = maybe vs (map position) $ pack p (map bval vs)
 349 |