-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Queries.FourFours
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A query based solution to the four-fours puzzle.
-- Inspired by <http://www.gigamonkeys.com/trees/>
--
-- @
-- Try to make every number between 0 and 20 using only four 4s and any
-- mathematical operation, with all four 4s being used each time.
-- @
--
-- We pretty much follow the structure of <http://www.gigamonkeys.com/trees/>,
-- with the exception that we generate the trees filled with symbolic operators
-- and ask the SMT solver to find the appropriate fillings.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Queries.FourFours where

import Data.SBV
import Data.SBV.Control

import Data.List (inits, tails)
import Data.Maybe

-- | Supported binary operators. To keep the search-space small, we will only allow division by @2@ or @4@,
-- and exponentiation will only be to the power @0@. This does restrict the search space, but is sufficient to
-- solve all the instances.
data BinOp = Plus | Minus | Times | Divide | Expt

-- | Make 'BinOp' a symbolic value.
mkSymbolicEnumeration ''BinOp

-- | Supported unary operators. Similar to 'BinOp' case, we will restrict square-root and factorial to
-- be only applied to the value @4.
data UnOp  = Negate | Sqrt | Factorial

-- | Make 'UnOp' a symbolic value.
mkSymbolicEnumeration ''UnOp

-- | The shape of a tree, either a binary node, or a unary node, or the number @4@, represented hear by
-- the constructor @F@. We parameterize by the operator type: When doing symbolic computations, we'll fill
-- those with 'SBinOp' and 'SUnOp'. When finding the shapes, we will simply put unit values, i.e., holes.
data T b u = B b (T b u) (T b u)
           | U u (T b u)
           | F

-- | A rudimentary 'Show' instance for trees, nothing fancy.
instance Show (T BinOp UnOp) where
   show :: T BinOp UnOp -> String
show T BinOp UnOp
F       = String
"4"
   show (U UnOp
u T BinOp UnOp
t) = case UnOp
u of
                    UnOp
Negate    -> String
"-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ T BinOp UnOp -> String
forall a. Show a => a -> String
show T BinOp UnOp
t
                    UnOp
Sqrt      -> String
"sqrt(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ T BinOp UnOp -> String
forall a. Show a => a -> String
show T BinOp UnOp
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
                    UnOp
Factorial -> T BinOp UnOp -> String
forall a. Show a => a -> String
show T BinOp UnOp
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"!"
   show (B BinOp
o T BinOp UnOp
l T BinOp UnOp
r) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ T BinOp UnOp -> String
forall a. Show a => a -> String
show T BinOp UnOp
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
so String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T BinOp UnOp -> String
forall a. Show a => a -> String
show T BinOp UnOp
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
     where so :: String
so = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe (ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Unexpected operator: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BinOp -> String
forall a. Show a => a -> String
show BinOp
o)
                        (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ BinOp
o BinOp -> [(BinOp, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(BinOp
Plus, String
"+"), (BinOp
Minus, String
"-"), (BinOp
Times, String
"*"), (BinOp
Divide, String
"/"), (BinOp
Expt, String
"^")]

-- | Construct all possible tree shapes. The argument here follows the logic in <http://www.gigamonkeys.com/trees/>:
-- We simply construct all possible shapes and extend with the operators. The number of such trees is:
--
-- >>> length allPossibleTrees
-- 640
--
-- Note that this is a /lot/ smaller than what is generated by <http://www.gigamonkeys.com/trees/>. (There, the
-- number of trees is 10240000: 16000 times more than what we have to consider!)
allPossibleTrees :: [T () ()]
allPossibleTrees :: [T () ()]
allPossibleTrees = [T () ()] -> [T () ()]
trees ([T () ()] -> [T () ()]) -> [T () ()] -> [T () ()]
forall a b. (a -> b) -> a -> b
$ Int -> T () () -> [T () ()]
forall a. Int -> a -> [a]
replicate Int
4 T () ()
forall b u. T b u
F
  where trees :: [T () ()] -> [T () ()]
        trees :: [T () ()] -> [T () ()]
trees [T () ()
x] = [T () ()
x, () -> T () () -> T () ()
forall b u. u -> T b u -> T b u
U () T () ()
x]
        trees [T () ()]
xs  = do (left, right) <- [([T () ()], [T () ()])]
splits
                       t1            <- trees left
                       t2            <- trees right
                       trees [B () t1 t2]
          where splits :: [([T () ()], [T () ()])]
splits = [([T () ()], [T () ()])] -> [([T () ()], [T () ()])]
forall a. HasCallStack => [a] -> [a]
init ([([T () ()], [T () ()])] -> [([T () ()], [T () ()])])
-> [([T () ()], [T () ()])] -> [([T () ()], [T () ()])]
forall a b. (a -> b) -> a -> b
$ Int -> [([T () ()], [T () ()])] -> [([T () ()], [T () ()])]
forall a. Int -> [a] -> [a]
drop Int
1 ([([T () ()], [T () ()])] -> [([T () ()], [T () ()])])
-> [([T () ()], [T () ()])] -> [([T () ()], [T () ()])]
forall a b. (a -> b) -> a -> b
$ [[T () ()]] -> [[T () ()]] -> [([T () ()], [T () ()])]
forall a b. [a] -> [b] -> [(a, b)]
zip ([T () ()] -> [[T () ()]]
forall a. [a] -> [[a]]
inits [T () ()]
xs) ([T () ()] -> [[T () ()]]
forall a. [a] -> [[a]]
tails [T () ()]
xs)

-- | Given a tree with hols, fill it with symbolic operators. This is the /trick/ that allows
-- us to consider only 640 trees as opposed to over 10 million.
fill :: T () () -> Symbolic (T SBinOp SUnOp)
fill :: T () () -> Symbolic (T SBinOp SUnOp)
fill (B ()
_ T () ()
l T () ()
r) = SBinOp -> T SBinOp SUnOp -> T SBinOp SUnOp -> T SBinOp SUnOp
forall b u. b -> T b u -> T b u -> T b u
B (SBinOp -> T SBinOp SUnOp -> T SBinOp SUnOp -> T SBinOp SUnOp)
-> SymbolicT IO SBinOp
-> SymbolicT
     IO (T SBinOp SUnOp -> T SBinOp SUnOp -> T SBinOp SUnOp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolicT IO SBinOp
forall a. SymVal a => Symbolic (SBV a)
free_ SymbolicT IO (T SBinOp SUnOp -> T SBinOp SUnOp -> T SBinOp SUnOp)
-> Symbolic (T SBinOp SUnOp)
-> SymbolicT IO (T SBinOp SUnOp -> T SBinOp SUnOp)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T () () -> Symbolic (T SBinOp SUnOp)
fill T () ()
l SymbolicT IO (T SBinOp SUnOp -> T SBinOp SUnOp)
-> Symbolic (T SBinOp SUnOp) -> Symbolic (T SBinOp SUnOp)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T () () -> Symbolic (T SBinOp SUnOp)
fill T () ()
r
fill (U ()
_ T () ()
t)   = SUnOp -> T SBinOp SUnOp -> T SBinOp SUnOp
forall b u. u -> T b u -> T b u
U (SUnOp -> T SBinOp SUnOp -> T SBinOp SUnOp)
-> SymbolicT IO SUnOp
-> SymbolicT IO (T SBinOp SUnOp -> T SBinOp SUnOp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolicT IO SUnOp
forall a. SymVal a => Symbolic (SBV a)
free_ SymbolicT IO (T SBinOp SUnOp -> T SBinOp SUnOp)
-> Symbolic (T SBinOp SUnOp) -> Symbolic (T SBinOp SUnOp)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T () () -> Symbolic (T SBinOp SUnOp)
fill T () ()
t
fill T () ()
F         = T SBinOp SUnOp -> Symbolic (T SBinOp SUnOp)
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return T SBinOp SUnOp
forall b u. T b u
F

-- | Minor helper for writing "symbolic" case statements. Simply walks down a list
-- of values to match against a symbolic version of the key.
sCase :: (Eq a, SymVal a, Mergeable v) => SBV a -> [(a, v)] -> v
sCase :: forall a v. (Eq a, SymVal a, Mergeable v) => SBV a -> [(a, v)] -> v
sCase SBV a
k = [(a, v)] -> v
forall {t}. Mergeable t => [(a, t)] -> t
walk
  where walk :: [(a, t)] -> t
walk []              = String -> t
forall a. HasCallStack => String -> a
error String
"sCase: Expected a non-empty list of cases!"
        walk [(a
_, t
v)]        = t
v
        walk ((a
k1, t
v1):[(a, t)]
rest) = SBool -> t -> t -> t
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
k SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
k1) t
v1 ([(a, t)] -> t
walk [(a, t)]
rest)

-- | Evaluate a symbolic tree, obtaining a symbolic value. Note how we structure
-- this evaluation so we impose extra constraints on what values square-root, divide
-- etc. can take. This is the power of the symbolic approach: We can put arbitrary
-- symbolic constraints as we evaluate the tree.
eval :: T SBinOp SUnOp -> Symbolic SInteger
eval :: T SBinOp SUnOp -> Symbolic SInteger
eval T SBinOp SUnOp
tree = case T SBinOp SUnOp
tree of
              B SBinOp
b T SBinOp SUnOp
l T SBinOp SUnOp
r -> T SBinOp SUnOp -> Symbolic SInteger
eval T SBinOp SUnOp
l Symbolic SInteger
-> (SInteger -> Symbolic SInteger) -> Symbolic SInteger
forall a b.
SymbolicT IO a -> (a -> SymbolicT IO b) -> SymbolicT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SInteger
l' -> T SBinOp SUnOp -> Symbolic SInteger
eval T SBinOp SUnOp
r Symbolic SInteger
-> (SInteger -> Symbolic SInteger) -> Symbolic SInteger
forall a b.
SymbolicT IO a -> (a -> SymbolicT IO b) -> SymbolicT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SInteger
r' -> SBinOp -> SInteger -> SInteger -> Symbolic SInteger
binOp SBinOp
b SInteger
l' SInteger
r'
              U SUnOp
u T SBinOp SUnOp
t   -> T SBinOp SUnOp -> Symbolic SInteger
eval T SBinOp SUnOp
t Symbolic SInteger
-> (SInteger -> Symbolic SInteger) -> Symbolic SInteger
forall a b.
SymbolicT IO a -> (a -> SymbolicT IO b) -> SymbolicT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SUnOp -> SInteger -> Symbolic SInteger
uOp SUnOp
u
              T SBinOp SUnOp
F       -> SInteger -> Symbolic SInteger
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SInteger
4

  where binOp :: SBinOp -> SInteger -> SInteger -> Symbolic SInteger
        binOp :: SBinOp -> SInteger -> SInteger -> Symbolic SInteger
binOp SBinOp
o SInteger
l SInteger
r = do SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBinOp
o SBinOp -> SBinOp -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBinOp
sDivide SBool -> SBool -> SBool
.=> SInteger
r SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
4 SBool -> SBool -> SBool
.|| SInteger
r SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2
                         SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBinOp
o SBinOp -> SBinOp -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBinOp
sExpt   SBool -> SBool -> SBool
.=> SInteger
r SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0
                         SInteger -> Symbolic SInteger
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SInteger -> Symbolic SInteger) -> SInteger -> Symbolic SInteger
forall a b. (a -> b) -> a -> b
$ SBinOp -> [(BinOp, SInteger)] -> SInteger
forall a v. (Eq a, SymVal a, Mergeable v) => SBV a -> [(a, v)] -> v
sCase SBinOp
o
                                    [ (BinOp
Plus,    SInteger
lSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r)
                                    , (BinOp
Minus,   SInteger
lSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
r)
                                    , (BinOp
Times,   SInteger
lSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
r)
                                    , (BinOp
Divide,  SInteger
l SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
`sDiv` SInteger
r)
                                    , (BinOp
Expt,    SInteger
1)   -- exponent is restricted to 0, so the value is 1
                                    ]

        uOp :: SUnOp -> SInteger -> Symbolic SInteger
        uOp :: SUnOp -> SInteger -> Symbolic SInteger
uOp SUnOp
o SInteger
v = do SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SUnOp
o SUnOp -> SUnOp -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SUnOp
sSqrt      SBool -> SBool -> SBool
.=> SInteger
v SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
4
                     SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SUnOp
o SUnOp -> SUnOp -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SUnOp
sFactorial SBool -> SBool -> SBool
.=> SInteger
v SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
4
                     SInteger -> Symbolic SInteger
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SInteger -> Symbolic SInteger) -> SInteger -> Symbolic SInteger
forall a b. (a -> b) -> a -> b
$ SUnOp -> [(UnOp, SInteger)] -> SInteger
forall a v. (Eq a, SymVal a, Mergeable v) => SBV a -> [(a, v)] -> v
sCase SUnOp
o
                                [ (UnOp
Negate,    -SInteger
v)
                                , (UnOp
Sqrt,       SInteger
2)  -- argument is restricted to 4, so the value is 2
                                , (UnOp
Factorial, SInteger
24)  -- argument is restricted to 4, so the value is 24
                                ]

-- | In the query mode, find a filling of a given tree shape /t/, such that it evaluates to the
-- requested number /i/. Note that we return back a concrete tree.
generate :: Integer -> T () () -> IO (Maybe (T BinOp UnOp))
generate :: Integer -> T () () -> IO (Maybe (T BinOp UnOp))
generate Integer
i T () ()
t = Symbolic (Maybe (T BinOp UnOp)) -> IO (Maybe (T BinOp UnOp))
forall a. Symbolic a -> IO a
runSMT (Symbolic (Maybe (T BinOp UnOp)) -> IO (Maybe (T BinOp UnOp)))
-> Symbolic (Maybe (T BinOp UnOp)) -> IO (Maybe (T BinOp UnOp))
forall a b. (a -> b) -> a -> b
$ do symT <- T () () -> Symbolic (T SBinOp SUnOp)
fill T () ()
t
                           val  <- eval symT
                           constrain $ val .== literal i
                           query $ do cs <- checkSat
                                      case cs of
                                        CheckSatResult
Sat -> T BinOp UnOp -> Maybe (T BinOp UnOp)
forall a. a -> Maybe a
Just (T BinOp UnOp -> Maybe (T BinOp UnOp))
-> QueryT IO (T BinOp UnOp) -> Query (Maybe (T BinOp UnOp))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> T SBinOp SUnOp -> QueryT IO (T BinOp UnOp)
forall {u} {b}.
(SymVal u, SymVal b) =>
T (SBV b) (SBV u) -> QueryT IO (T b u)
construct T SBinOp SUnOp
symT
                                        CheckSatResult
_   -> Maybe (T BinOp UnOp) -> Query (Maybe (T BinOp UnOp))
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (T BinOp UnOp)
forall a. Maybe a
Nothing
    where -- Walk through the tree, ask the solver for
          -- the assignment to symbolic operators and fill back.
          construct :: T (SBV b) (SBV u) -> QueryT IO (T b u)
construct T (SBV b) (SBV u)
F           = T b u -> QueryT IO (T b u)
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return T b u
forall b u. T b u
F
          construct (U SBV u
o T (SBV b) (SBV u)
s')    = do uo <- SBV u -> Query u
forall a. SymVal a => SBV a -> Query a
getValue SBV u
o
                                     U uo <$> construct s'
          construct (B SBV b
b T (SBV b) (SBV u)
l' T (SBV b) (SBV u)
r') = do bo <- SBV b -> Query b
forall a. SymVal a => SBV a -> Query a
getValue SBV b
b
                                     B bo <$> construct l' <*> construct r'

-- | Given an integer, walk through all possible tree shapes (at most 640 of them), and find a
-- filling that solves the puzzle.
find :: Integer -> IO ()
find :: Integer -> IO ()
find Integer
target = [T () ()] -> IO ()
go [T () ()]
allPossibleTrees
  where go :: [T () ()] -> IO ()
go []     = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show Integer
target String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": No solution found."
        go (T () ()
t:[T () ()]
ts) = do chk <- Integer -> T () () -> IO (Maybe (T BinOp UnOp))
generate Integer
target T () ()
t
                       case chk of
                         Maybe (T BinOp UnOp)
Nothing -> [T () ()] -> IO ()
go [T () ()]
ts
                         Just T BinOp UnOp
r  -> do let ok :: Bool
ok  = T BinOp UnOp -> Integer
concEval T BinOp UnOp
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
target
                                           tag :: String
tag = if Bool
ok then String
" [OK]: " else String
" [BAD]: "
                                           sh :: a -> String
sh a
i | a
i a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
10 = Char
' ' Char -> ShowS
forall a. a -> [a] -> [a]
: a -> String
forall a. Show a => a -> String
show a
i
                                                | Bool
True   =       a -> String
forall a. Show a => a -> String
show a
i

                                       String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall {a}. (Ord a, Num a, Show a) => a -> String
sh Integer
target String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
tag String -> ShowS
forall a. [a] -> [a] -> [a]
++ T BinOp UnOp -> String
forall a. Show a => a -> String
show T BinOp UnOp
r

        -- Make sure the result is correct!
        concEval :: T BinOp UnOp -> Integer
        concEval :: T BinOp UnOp -> Integer
concEval T BinOp UnOp
F         = Integer
4
        concEval (U UnOp
u T BinOp UnOp
t)   = UnOp -> Integer -> Integer
uEval UnOp
u (T BinOp UnOp -> Integer
concEval T BinOp UnOp
t)
        concEval (B BinOp
b T BinOp UnOp
l T BinOp UnOp
r) = BinOp -> Integer -> Integer -> Integer
bEval BinOp
b (T BinOp UnOp -> Integer
concEval T BinOp UnOp
l) (T BinOp UnOp -> Integer
concEval T BinOp UnOp
r)

        uEval :: UnOp -> Integer -> Integer
        uEval :: UnOp -> Integer -> Integer
uEval UnOp
Negate    Integer
i = -Integer
i
        uEval UnOp
Sqrt      Integer
i = if Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
4 then  Integer
2 else String -> Integer
forall a. HasCallStack => String -> a
error (String -> Integer) -> String -> Integer
forall a b. (a -> b) -> a -> b
$ String
"uEval: Found sqrt applied to value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i
        uEval UnOp
Factorial Integer
i = if Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
4 then Integer
24 else String -> Integer
forall a. HasCallStack => String -> a
error (String -> Integer) -> String -> Integer
forall a b. (a -> b) -> a -> b
$ String
"uEval: Found factorial applied to value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i

        bEval :: BinOp -> Integer -> Integer -> Integer
        bEval :: BinOp -> Integer -> Integer -> Integer
bEval BinOp
Plus   Integer
i Integer
j = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j
        bEval BinOp
Minus  Integer
i Integer
j = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j
        bEval BinOp
Times  Integer
i Integer
j = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j
        bEval BinOp
Divide Integer
i Integer
j = Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
j
        bEval BinOp
Expt   Integer
i Integer
j = Integer
i Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
j

-- | Solution to the puzzle. When you run this puzzle, the solver can produce different results
-- than what's shown here, but the expressions should still be all valid!
--
-- @
-- ghci> puzzle
--  0 [OK]: (4 - (4 + (4 - 4)))
--  1 [OK]: (4 / (4 + (4 - 4)))
--  2 [OK]: sqrt((4 + (4 * (4 - 4))))
--  3 [OK]: (4 - (4 ^ (4 - 4)))
--  4 [OK]: (4 + (4 * (4 - 4)))
--  5 [OK]: (4 + (4 ^ (4 - 4)))
--  6 [OK]: (4 + sqrt((4 * (4 / 4))))
--  7 [OK]: (4 + (4 - (4 / 4)))
--  8 [OK]: (4 - (4 - (4 + 4)))
--  9 [OK]: (4 + (4 + (4 / 4)))
-- 10 [OK]: (4 + (4 + (4 - sqrt(4))))
-- 11 [OK]: (4 + ((4 + 4!) / 4))
-- 12 [OK]: (4 * (4 - (4 / 4)))
-- 13 [OK]: (4! + ((sqrt(4) - 4!) / sqrt(4)))
-- 14 [OK]: (4 + (4 + (4 + sqrt(4))))
-- 15 [OK]: (4 + ((4! - sqrt(4)) / sqrt(4)))
-- 16 [OK]: (4 * (4 * (4 / 4)))
-- 17 [OK]: (4 + ((sqrt(4) + 4!) / sqrt(4)))
-- 18 [OK]: -(4 + (4 - (sqrt(4) + 4!)))
-- 19 [OK]: -(4 - (4! - (4 / 4)))
-- 20 [OK]: (4 * (4 + (4 / 4)))
-- @
puzzle :: IO ()
puzzle :: IO ()
puzzle = (Integer -> IO ()) -> [Integer] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Integer -> IO ()
find [Integer
0 .. Integer
20]