{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns #-}
module Documentation.SBV.Examples.Puzzles.U2Bridge where
import Control.Monad (unless)
import Control.Monad.State (State, runState, put, get, gets, modify, evalState)
import Data.List(sortOn)
import GHC.Generics (Generic)
import Data.SBV
data U2Member = Bono | Edge | Adam | Larry
mkSymbolicEnumeration ''U2Member
type Time = Word32
type STime = SBV Time
crossTime :: U2Member -> Time
crossTime :: U2Member -> Time
crossTime U2Member
Bono = Time
1
crossTime U2Member
Edge = Time
2
crossTime U2Member
Adam = Time
5
crossTime U2Member
Larry = Time
10
sCrossTime :: SU2Member -> STime
sCrossTime :: SU2Member -> STime
sCrossTime SU2Member
m = SBool -> STime -> STime -> STime
forall a. Mergeable a => SBool -> a -> a -> a
ite (SU2Member
m SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sBono) (Time -> STime
forall a. SymVal a => a -> SBV a
literal (U2Member -> Time
crossTime U2Member
Bono))
(STime -> STime) -> STime -> STime
forall a b. (a -> b) -> a -> b
$ SBool -> STime -> STime -> STime
forall a. Mergeable a => SBool -> a -> a -> a
ite (SU2Member
m SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sEdge) (Time -> STime
forall a. SymVal a => a -> SBV a
literal (U2Member -> Time
crossTime U2Member
Edge))
(STime -> STime) -> STime -> STime
forall a b. (a -> b) -> a -> b
$ SBool -> STime -> STime -> STime
forall a. Mergeable a => SBool -> a -> a -> a
ite (SU2Member
m SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sAdam) (Time -> STime
forall a. SymVal a => a -> SBV a
literal (U2Member -> Time
crossTime U2Member
Adam))
(Time -> STime
forall a. SymVal a => a -> SBV a
literal (U2Member -> Time
crossTime U2Member
Larry))
data Location = Here | There
mkSymbolicEnumeration ''Location
data Status = Status { Status -> STime
time :: STime
, Status -> SLocation
flash :: SLocation
, Status -> SLocation
lBono :: SLocation
, Status -> SLocation
lEdge :: SLocation
, Status -> SLocation
lAdam :: SLocation
, Status -> SLocation
lLarry :: SLocation
} deriving ((forall x. Status -> Rep Status x)
-> (forall x. Rep Status x -> Status) -> Generic Status
forall x. Rep Status x -> Status
forall x. Status -> Rep Status x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Status -> Rep Status x
from :: forall x. Status -> Rep Status x
$cto :: forall x. Rep Status x -> Status
to :: forall x. Rep Status x -> Status
Generic, Bool -> SBool -> Status -> Status -> Status
(Bool -> SBool -> Status -> Status -> Status)
-> (forall b.
(Ord b, SymVal b, Num b) =>
[Status] -> Status -> SBV b -> Status)
-> Mergeable Status
forall b.
(Ord b, SymVal b, Num b) =>
[Status] -> Status -> SBV b -> Status
forall a.
(Bool -> SBool -> a -> a -> a)
-> (forall b. (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a)
-> Mergeable a
$csymbolicMerge :: Bool -> SBool -> Status -> Status -> Status
symbolicMerge :: Bool -> SBool -> Status -> Status -> Status
$cselect :: forall b.
(Ord b, SymVal b, Num b) =>
[Status] -> Status -> SBV b -> Status
select :: forall b.
(Ord b, SymVal b, Num b) =>
[Status] -> Status -> SBV b -> Status
Mergeable)
start :: Status
start :: Status
start = Status { time :: STime
time = STime
0
, flash :: SLocation
flash = SLocation
sHere
, lBono :: SLocation
lBono = SLocation
sHere
, lEdge :: SLocation
lEdge = SLocation
sHere
, lAdam :: SLocation
lAdam = SLocation
sHere
, lLarry :: SLocation
lLarry = SLocation
sHere
}
type Move a = State Status a
instance Mergeable a => Mergeable (Move a) where
symbolicMerge :: Bool -> SBool -> Move a -> Move a -> Move a
symbolicMerge Bool
f SBool
t Move a
a Move a
b
= do Status
s <- StateT Status Identity Status
forall s (m :: * -> *). MonadState s m => m s
get
let (a
ar, Status
s1) = Move a -> Status -> (a, Status)
forall s a. State s a -> s -> (a, s)
runState Move a
a Status
s
(a
br, Status
s2) = Move a -> Status -> (a, Status)
forall s a. State s a -> s -> (a, s)
runState Move a
b Status
s
Status -> Move ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Status -> Move ()) -> Status -> Move ()
forall a b. (a -> b) -> a -> b
$ Bool -> SBool -> Status -> Status -> Status
forall a. Mergeable a => Bool -> SBool -> a -> a -> a
symbolicMerge Bool
f SBool
t Status
s1 Status
s2
a -> Move a
forall a. a -> StateT Status Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Move a) -> a -> Move a
forall a b. (a -> b) -> a -> b
$ Bool -> SBool -> a -> a -> a
forall a. Mergeable a => Bool -> SBool -> a -> a -> a
symbolicMerge Bool
f SBool
t a
ar a
br
peek :: (Status -> a) -> Move a
peek :: forall a. (Status -> a) -> Move a
peek = (Status -> a) -> StateT Status Identity a
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets
whereIs :: SU2Member -> Move SLocation
whereIs :: SU2Member -> Move SLocation
whereIs SU2Member
p = SBool -> Move SLocation -> Move SLocation -> Move SLocation
forall a. Mergeable a => SBool -> a -> a -> a
ite (SU2Member
p SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sBono) ((Status -> SLocation) -> Move SLocation
forall a. (Status -> a) -> Move a
peek Status -> SLocation
lBono)
(Move SLocation -> Move SLocation)
-> Move SLocation -> Move SLocation
forall a b. (a -> b) -> a -> b
$ SBool -> Move SLocation -> Move SLocation -> Move SLocation
forall a. Mergeable a => SBool -> a -> a -> a
ite (SU2Member
p SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sEdge) ((Status -> SLocation) -> Move SLocation
forall a. (Status -> a) -> Move a
peek Status -> SLocation
lEdge)
(Move SLocation -> Move SLocation)
-> Move SLocation -> Move SLocation
forall a b. (a -> b) -> a -> b
$ SBool -> Move SLocation -> Move SLocation -> Move SLocation
forall a. Mergeable a => SBool -> a -> a -> a
ite (SU2Member
p SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sAdam) ((Status -> SLocation) -> Move SLocation
forall a. (Status -> a) -> Move a
peek Status -> SLocation
lAdam)
((Status -> SLocation) -> Move SLocation
forall a. (Status -> a) -> Move a
peek Status -> SLocation
lLarry)
xferFlash :: Move ()
xferFlash :: Move ()
xferFlash = (Status -> Status) -> Move ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Status -> Status) -> Move ()) -> (Status -> Status) -> Move ()
forall a b. (a -> b) -> a -> b
$ \Status
s -> Status
s{flash = ite (flash s .== sHere) sThere sHere}
xferPerson :: SU2Member -> Move ()
xferPerson :: SU2Member -> Move ()
xferPerson SU2Member
p = do ~[SLocation
lb, SLocation
le, SLocation
la, SLocation
ll] <- ((Status -> SLocation) -> Move SLocation)
-> [Status -> SLocation] -> StateT Status Identity [SLocation]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Status -> SLocation) -> Move SLocation
forall a. (Status -> a) -> Move a
peek [Status -> SLocation
lBono, Status -> SLocation
lEdge, Status -> SLocation
lAdam, Status -> SLocation
lLarry]
let move :: SLocation -> SLocation
move SLocation
l = SBool -> SLocation -> SLocation -> SLocation
forall a. Mergeable a => SBool -> a -> a -> a
ite (SLocation
l SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
sHere) SLocation
sThere SLocation
sHere
lb' :: SLocation
lb' = SBool -> SLocation -> SLocation -> SLocation
forall a. Mergeable a => SBool -> a -> a -> a
ite (SU2Member
p SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sBono) (SLocation -> SLocation
move SLocation
lb) SLocation
lb
le' :: SLocation
le' = SBool -> SLocation -> SLocation -> SLocation
forall a. Mergeable a => SBool -> a -> a -> a
ite (SU2Member
p SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sEdge) (SLocation -> SLocation
move SLocation
le) SLocation
le
la' :: SLocation
la' = SBool -> SLocation -> SLocation -> SLocation
forall a. Mergeable a => SBool -> a -> a -> a
ite (SU2Member
p SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sAdam) (SLocation -> SLocation
move SLocation
la) SLocation
la
ll' :: SLocation
ll' = SBool -> SLocation -> SLocation -> SLocation
forall a. Mergeable a => SBool -> a -> a -> a
ite (SU2Member
p SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sLarry) (SLocation -> SLocation
move SLocation
ll) SLocation
ll
(Status -> Status) -> Move ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Status -> Status) -> Move ()) -> (Status -> Status) -> Move ()
forall a b. (a -> b) -> a -> b
$ \Status
s -> Status
s{lBono = lb', lEdge = le', lAdam = la', lLarry = ll'}
bumpTime1 :: SU2Member -> Move ()
bumpTime1 :: SU2Member -> Move ()
bumpTime1 SU2Member
p = (Status -> Status) -> Move ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Status -> Status) -> Move ()) -> (Status -> Status) -> Move ()
forall a b. (a -> b) -> a -> b
$ \Status
s -> Status
s{time = time s + sCrossTime p}
bumpTime2 :: SU2Member -> SU2Member -> Move ()
bumpTime2 :: SU2Member -> SU2Member -> Move ()
bumpTime2 SU2Member
p1 SU2Member
p2 = (Status -> Status) -> Move ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Status -> Status) -> Move ()) -> (Status -> Status) -> Move ()
forall a b. (a -> b) -> a -> b
$ \Status
s -> Status
s{time = time s + sCrossTime p1 `smax` sCrossTime p2}
whenS :: SBool -> Move () -> Move ()
whenS :: SBool -> Move () -> Move ()
whenS SBool
t Move ()
a = SBool -> Move () -> Move () -> Move ()
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
t Move ()
a (() -> Move ()
forall a. a -> StateT Status Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
move1 :: SU2Member -> Move ()
move1 :: SU2Member -> Move ()
move1 SU2Member
p = do SLocation
f <- (Status -> SLocation) -> Move SLocation
forall a. (Status -> a) -> Move a
peek Status -> SLocation
flash
SLocation
l <- SU2Member -> Move SLocation
whereIs SU2Member
p
SBool -> Move () -> Move ()
whenS (SLocation
f SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
l) (Move () -> Move ()) -> Move () -> Move ()
forall a b. (a -> b) -> a -> b
$ do SU2Member -> Move ()
bumpTime1 SU2Member
p
Move ()
xferFlash
SU2Member -> Move ()
xferPerson SU2Member
p
move2 :: SU2Member -> SU2Member -> Move ()
move2 :: SU2Member -> SU2Member -> Move ()
move2 SU2Member
p1 SU2Member
p2 = do SLocation
f <- (Status -> SLocation) -> Move SLocation
forall a. (Status -> a) -> Move a
peek Status -> SLocation
flash
SLocation
l1 <- SU2Member -> Move SLocation
whereIs SU2Member
p1
SLocation
l2 <- SU2Member -> Move SLocation
whereIs SU2Member
p2
SBool -> Move () -> Move ()
whenS (SLocation
f SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
l1 SBool -> SBool -> SBool
.&& SLocation
f SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
l2) (Move () -> Move ()) -> Move () -> Move ()
forall a b. (a -> b) -> a -> b
$ do SU2Member -> SU2Member -> Move ()
bumpTime2 SU2Member
p1 SU2Member
p2
Move ()
xferFlash
SU2Member -> Move ()
xferPerson SU2Member
p1
SU2Member -> Move ()
xferPerson SU2Member
p2
type Actions = [(SBool, SU2Member, SU2Member)]
run :: Actions -> Move [Status]
run :: Actions -> Move [Status]
run = ((SBool, SU2Member, SU2Member) -> StateT Status Identity Status)
-> Actions -> Move [Status]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (SBool, SU2Member, SU2Member) -> StateT Status Identity Status
step
where step :: (SBool, SU2Member, SU2Member) -> StateT Status Identity Status
step (SBool
b, SU2Member
p1, SU2Member
p2) = SBool -> Move () -> Move () -> Move ()
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
b (SU2Member -> Move ()
move1 SU2Member
p1) (SU2Member -> SU2Member -> Move ()
move2 SU2Member
p1 SU2Member
p2) Move ()
-> StateT Status Identity Status -> StateT Status Identity Status
forall a b.
StateT Status Identity a
-> StateT Status Identity b -> StateT Status Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT Status Identity Status
forall s (m :: * -> *). MonadState s m => m s
get
isValid :: Actions -> SBool
isValid :: Actions -> SBool
isValid Actions
as = Status -> STime
time Status
end STime -> STime -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= STime
17 SBool -> SBool -> SBool
.&& ((SBool, SU2Member, SU2Member) -> SBool) -> Actions -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll (SBool, SU2Member, SU2Member) -> SBool
check Actions
as SBool -> SBool -> SBool
.&& [SLocation] -> [SLocation] -> SBool
forall {b}. EqSymbolic b => [b] -> [b] -> SBool
zigZag ([SLocation] -> [SLocation]
forall a. HasCallStack => [a] -> [a]
cycle [SLocation
sThere, SLocation
sHere]) ((Status -> SLocation) -> [Status] -> [SLocation]
forall a b. (a -> b) -> [a] -> [b]
map Status -> SLocation
flash [Status]
states) SBool -> SBool -> SBool
.&& (SLocation -> SBool) -> [SLocation] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll (SLocation -> SLocation -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SLocation
sThere) [Status -> SLocation
lBono Status
end, Status -> SLocation
lEdge Status
end, Status -> SLocation
lAdam Status
end, Status -> SLocation
lLarry Status
end]
where check :: (SBool, SU2Member, SU2Member) -> SBool
check (SBool
s, SU2Member
p1, SU2Member
p2) = (SBool -> SBool
sNot SBool
s SBool -> SBool -> SBool
.=> SU2Member
p1 SU2Member -> SU2Member -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SU2Member
p2)
SBool -> SBool -> SBool
.&& (SBool
s SBool -> SBool -> SBool
.=> SU2Member
p2 SU2Member -> SU2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SU2Member
sBono)
states :: [Status]
states = Move [Status] -> Status -> [Status]
forall s a. State s a -> s -> a
evalState (Actions -> Move [Status]
run Actions
as) Status
start
end :: Status
end = [Status] -> Status
forall a. HasCallStack => [a] -> a
last [Status]
states
zigZag :: [b] -> [b] -> SBool
zigZag [b]
reqs [b]
locs = [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ (b -> b -> SBool) -> [b] -> [b] -> [SBool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith b -> b -> SBool
forall a. EqSymbolic a => a -> a -> SBool
(.==) [b]
locs [b]
reqs
solveN :: Int -> IO Bool
solveN :: Int -> IO Bool
solveN Int
n = do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Checking for solutions with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" move" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. (Eq a, Num a) => a -> String
plu Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
let genAct :: SymbolicT IO (SBool, SU2Member, SU2Member)
genAct = do SBool
b <- SymbolicT IO SBool
forall a. SymVal a => Symbolic (SBV a)
free_
SU2Member
p1 <- Symbolic SU2Member
forall a. SymVal a => Symbolic (SBV a)
free_
SU2Member
p2 <- Symbolic SU2Member
forall a. SymVal a => Symbolic (SBV a)
free_
(SBool, SU2Member, SU2Member)
-> SymbolicT IO (SBool, SU2Member, SU2Member)
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool
b, SU2Member
p1, SU2Member
p2)
AllSatResult
res <- SymbolicT IO SBool -> IO AllSatResult
forall a. Satisfiable a => a -> IO AllSatResult
allSat (SymbolicT IO SBool -> IO AllSatResult)
-> SymbolicT IO SBool -> IO AllSatResult
forall a b. (a -> b) -> a -> b
$ Actions -> SBool
isValid (Actions -> SBool) -> SymbolicT IO Actions -> SymbolicT IO SBool
forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Int -> SymbolicT IO (SBool, SU2Member, SU2Member))
-> [Int] -> SymbolicT IO Actions
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (SymbolicT IO (SBool, SU2Member, SU2Member)
-> Int -> SymbolicT IO (SBool, SU2Member, SU2Member)
forall a b. a -> b -> a
const SymbolicT IO (SBool, SU2Member, SU2Member)
genAct) [Int
1..Int
n]
Int
cnt <- ([(Bool, [(Bool, U2Member, U2Member)])]
-> [(Bool, [(Bool, U2Member, U2Member)])])
-> (Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ())
-> AllSatResult
-> IO Int
forall a.
SatModel a =>
([(Bool, a)] -> [(Bool, a)])
-> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels (((Bool, [(Bool, U2Member, U2Member)]) -> String)
-> [(Bool, [(Bool, U2Member, U2Member)])]
-> [(Bool, [(Bool, U2Member, U2Member)])]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Bool, [(Bool, U2Member, U2Member)]) -> String
forall a. Show a => a -> String
show) Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ()
disp AllSatResult
res
if Int
cnt Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
else do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
cnt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" solution" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. (Eq a, Num a) => a -> String
plu Int
cnt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" move" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. (Eq a, Num a) => a -> String
plu Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
where plu :: a -> String
plu a
v = if a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
1 then String
"" else String
"s"
disp :: Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ()
disp :: Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ()
disp Int
i (Bool
_, [(Bool, U2Member, U2Member)]
ss)
| Int
lss Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
n = String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Expected " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" results; got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
lss
| Bool
True = do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Solution #" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": "
Bool -> Time -> [(Bool, U2Member, U2Member)] -> IO ()
go Bool
False Time
0 [(Bool, U2Member, U2Member)]
ss
() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where lss :: Int
lss = [(Bool, U2Member, U2Member)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Bool, U2Member, U2Member)]
ss
go :: Bool -> Time -> [(Bool, U2Member, U2Member)] -> IO ()
go Bool
_ Time
t [] = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Total time: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Time -> String
forall a. Show a => a -> String
show Time
t
go Bool
l Time
t ((Bool
True, U2Member
a, U2Member
_):[(Bool, U2Member, U2Member)]
rest) = do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Time -> String
forall a. Show a => a -> String
sh2 Time
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
shL Bool
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ U2Member -> String
forall a. Show a => a -> String
show U2Member
a
Bool -> Time -> [(Bool, U2Member, U2Member)] -> IO ()
go (Bool -> Bool
not Bool
l) (Time
t Time -> Time -> Time
forall a. Num a => a -> a -> a
+ U2Member -> Time
crossTime U2Member
a) [(Bool, U2Member, U2Member)]
rest
go Bool
l Time
t ((Bool
False, U2Member
a, U2Member
b):[(Bool, U2Member, U2Member)]
rest) = do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Time -> String
forall a. Show a => a -> String
sh2 Time
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
shL Bool
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ U2Member -> String
forall a. Show a => a -> String
show U2Member
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ U2Member -> String
forall a. Show a => a -> String
show U2Member
b
Bool -> Time -> [(Bool, U2Member, U2Member)] -> IO ()
go (Bool -> Bool
not Bool
l) (Time
t Time -> Time -> Time
forall a. Num a => a -> a -> a
+ U2Member -> Time
crossTime U2Member
a Time -> Time -> Time
forall a. Ord a => a -> a -> a
`max` U2Member -> Time
crossTime U2Member
b) [(Bool, U2Member, U2Member)]
rest
sh2 :: p -> String
sh2 p
t = let s :: String
s = p -> String
forall a. Show a => a -> String
show p
t in if String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 then Char
' ' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s else String
s
shL :: Bool -> String
shL Bool
False = String
" --> "
shL Bool
True = String
" <-- "
solveU2 :: IO ()
solveU2 :: IO ()
solveU2 = Int -> IO ()
go Int
1
where go :: Int -> IO ()
go Int
i = do Bool
p <- Int -> IO Bool
solveN Int
i
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
p (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> IO ()
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)