{-# Language StandaloneDeriving, BlockArguments, KindSignatures, GADTs, DataKinds, MonadComprehensions #-}
module Advent.Box where
import Control.Monad (foldM)
import Data.Functor.Compose (Compose(Compose, getCompose))
import Data.Kind (Type)
import Data.List (foldl1')
import GHC.Stack (HasCallStack)
import Advent.Nat (Nat(S,Z), FromNatural, UnfoldNat(unfoldNat))
import Advent.ReadS (pread, preadParen, tok, P(unP))
type Box' n = Box (FromNatural n)
data Box :: Nat -> Type where
Pt :: Box 'Z
Dim :: !Int ->
!Int ->
Box n ->
Box ('S n)
deriving instance Show (Box n)
deriving instance Eq (Box n)
deriving instance Ord (Box n)
size :: Box n -> Int
size :: forall (n :: Nat). Box n -> Int
size Box n
Pt = Int
1
size (Dim Int
lo Int
hi Box n
box) = (Int
hi Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lo) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Box n -> Int
forall (n :: Nat). Box n -> Int
size Box n
box
intersectBox :: Box n -> Box n -> Maybe (Box n)
intersectBox :: forall (n :: Nat). Box n -> Box n -> Maybe (Box n)
intersectBox Box n
Pt Box n
Pt = Box n -> Maybe (Box n)
forall a. a -> Maybe a
Just Box n
Box 'Z
Pt
intersectBox (Dim Int
a Int
b Box n
xs) (Dim Int
c Int
d Box n
ys) =
[Int -> Int -> Box n -> Box ('S n)
forall (n :: Nat). Int -> Int -> Box n -> Box ('S n)
Dim Int
x Int
y Box n
zs | let x :: Int
x = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
a Int
c, let y :: Int
y = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
b Int
d, Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
y, Box n
zs <- Box n -> Box n -> Maybe (Box n)
forall (n :: Nat). Box n -> Box n -> Maybe (Box n)
intersectBox Box n
xs Box n
Box n
ys]
intersectBoxes :: HasCallStack => [Box n] -> Maybe (Box n)
intersectBoxes :: forall (n :: Nat). HasCallStack => [Box n] -> Maybe (Box n)
intersectBoxes [] = String -> Maybe (Box n)
forall a. HasCallStack => String -> a
error String
"intersectBoxes: empty intersection"
intersectBoxes (Box n
x:[Box n]
xs) = (Box n -> Box n -> Maybe (Box n))
-> Box n -> [Box n] -> Maybe (Box n)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Box n -> Box n -> Maybe (Box n)
forall (n :: Nat). Box n -> Box n -> Maybe (Box n)
intersectBox Box n
x [Box n]
xs
subtractBox ::
Box n ->
Box n ->
[Box n]
subtractBox :: forall (n :: Nat). Box n -> Box n -> [Box n]
subtractBox Box n
b1 Box n
b2 =
case Box n -> Box n -> Maybe (Box n)
forall (n :: Nat). Box n -> Box n -> Maybe (Box n)
intersectBox Box n
b1 Box n
b2 of
Maybe (Box n)
Nothing -> [Box n
b2]
Just Box n
b -> Box n -> Box n -> [Box n]
forall (n :: Nat). Box n -> Box n -> [Box n]
subtractBox' Box n
b Box n
b2
subtractBox' :: Box n -> Box n -> [Box n]
subtractBox' :: forall (n :: Nat). Box n -> Box n -> [Box n]
subtractBox' Box n
Pt Box n
Pt = []
subtractBox' (Dim Int
a Int
b Box n
xs) (Dim Int
c Int
d Box n
ys) =
[Int -> Int -> Box n -> Box ('S n)
forall (n :: Nat). Int -> Int -> Box n -> Box ('S n)
Dim Int
c Int
a Box n
ys | Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
a] [Box n] -> [Box n] -> [Box n]
forall a. [a] -> [a] -> [a]
++
[Int -> Int -> Box n -> Box ('S n)
forall (n :: Nat). Int -> Int -> Box n -> Box ('S n)
Dim Int
a Int
b Box n
zs | Box n
zs <- Box n -> Box n -> [Box n]
forall (n :: Nat). Box n -> Box n -> [Box n]
subtractBox' Box n
xs Box n
Box n
ys] [Box n] -> [Box n] -> [Box n]
forall a. [a] -> [a] -> [a]
++
[Int -> Int -> Box n -> Box ('S n)
forall (n :: Nat). Int -> Int -> Box n -> Box ('S n)
Dim Int
b Int
d Box n
ys | Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
d]
coverBox :: Box n -> Box n -> Box n
coverBox :: forall (n :: Nat). Box n -> Box n -> Box n
coverBox (Dim Int
a Int
b Box n
x) (Dim Int
c Int
d Box n
y) = Int -> Int -> Box n -> Box ('S n)
forall (n :: Nat). Int -> Int -> Box n -> Box ('S n)
Dim (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
a Int
c) (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
b Int
d) (Box n -> Box n -> Box n
forall (n :: Nat). Box n -> Box n -> Box n
coverBox Box n
x Box n
Box n
y)
coverBox Box n
Pt Box n
Pt = Box n
Box 'Z
Pt
coverBoxes :: HasCallStack => [Box n] -> Box n
coverBoxes :: forall (n :: Nat). HasCallStack => [Box n] -> Box n
coverBoxes = (Box n -> Box n -> Box n) -> [Box n] -> Box n
forall a. HasCallStack => (a -> a -> a) -> [a] -> a
foldl1' Box n -> Box n -> Box n
forall (n :: Nat). Box n -> Box n -> Box n
coverBox
unionBoxes :: [Box a] -> [Box a]
unionBoxes :: forall (a :: Nat). [Box a] -> [Box a]
unionBoxes = (Box a -> [Box a] -> [Box a]) -> [Box a] -> [Box a] -> [Box a]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Box a -> [Box a] -> [Box a]
forall {t :: * -> *} {n :: Nat}.
Foldable t =>
Box n -> t (Box n) -> [Box n]
add []
where
add :: Box n -> t (Box n) -> [Box n]
add Box n
box t (Box n)
rest = Box n
box Box n -> [Box n] -> [Box n]
forall a. a -> [a] -> [a]
: (Box n -> [Box n]) -> t (Box n) -> [Box n]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Box n -> Box n -> [Box n]
forall (n :: Nat). Box n -> Box n -> [Box n]
subtractBox Box n
box) t (Box n)
rest
instance UnfoldNat n => Read (Box n) where
readsPrec :: Int -> ReadS (Box n)
readsPrec Int
p = P (Box n) -> ReadS (Box n)
forall a. P a -> ReadS a
unP (Compose P Box n -> P (Box n)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose P Box 'Z
-> (forall (m :: Nat). Compose P Box m -> Compose P Box ('S m))
-> Compose P Box n
forall (n :: Nat) (f :: Nat -> *).
UnfoldNat n =>
f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f n
forall (f :: Nat -> *).
f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f n
unfoldNat Compose P Box 'Z
pt Compose P Box m -> Compose P Box ('S m)
forall (m :: Nat). Compose P Box m -> Compose P Box ('S m)
dim))
where
pt :: Compose P Box 'Z
pt :: Compose P Box 'Z
pt = P (Box 'Z) -> Compose P Box 'Z
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Bool -> P (Box 'Z) -> P (Box 'Z)
forall a. Bool -> P a -> P a
preadParen Bool
False (Box 'Z
Pt Box 'Z -> P String -> P (Box 'Z)
forall a b. a -> P b -> P a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> P String
tok String
"Pt"))
dim :: Compose P Box m -> Compose P Box ('S m)
dim :: forall (m :: Nat). Compose P Box m -> Compose P Box ('S m)
dim (Compose P (Box m)
more) = P (Box ('S m)) -> Compose P Box ('S m)
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Bool -> P (Box ('S m)) -> P (Box ('S m))
forall a. Bool -> P a -> P a
preadParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
(Int -> Int -> Box m -> Box ('S m)
forall (n :: Nat). Int -> Int -> Box n -> Box ('S n)
Dim (Int -> Int -> Box m -> Box ('S m))
-> P String -> P (Int -> Int -> Box m -> Box ('S m))
forall a b. a -> P b -> P a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> P String
tok String
"Dim" P (Int -> Int -> Box m -> Box ('S m))
-> P Int -> P (Int -> Box m -> Box ('S m))
forall a b. P (a -> b) -> P a -> P b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> P Int
forall a. Read a => P a
pread P (Int -> Box m -> Box ('S m)) -> P Int -> P (Box m -> Box ('S m))
forall a b. P (a -> b) -> P a -> P b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> P Int
forall a. Read a => P a
pread P (Box m -> Box ('S m)) -> P (Box m) -> P (Box ('S m))
forall a b. P (a -> b) -> P a -> P b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> P (Box m)
more))