{-# 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
data BinOp = Plus | Minus | Times | Divide | Expt
mkSymbolicEnumeration ''BinOp
data UnOp = Negate | Sqrt | Factorial
mkSymbolicEnumeration ''UnOp
type SBinOp = SBV BinOp
type SUnOp = SBV UnOp
data T b u = B b (T b u) (T b u)
| U u (T b u)
| F
instance Show (T BinOp UnOp) where
show :: T BinOp UnOp -> String
show F = "4"
show (U u :: UnOp
u t :: T BinOp UnOp
t) = case UnOp
u of
Negate -> "-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ T BinOp UnOp -> String
forall a. Show a => a -> String
show T BinOp UnOp
t
Sqrt -> "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]
++ ")"
Factorial -> T BinOp UnOp -> String
forall a. Show a => a -> String
show T BinOp UnOp
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ "!"
show (B o :: BinOp
o l :: T BinOp UnOp
l r :: T BinOp UnOp
r) = "(" 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
so String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " 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]
++ ")"
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
$ "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, "+"), (BinOp
Minus, "-"), (BinOp
Times, "*"), (BinOp
Divide, "/"), (BinOp
Expt, "^")]
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 4 T () ()
forall b u. T b u
F
where trees :: [T () ()] -> [T () ()]
trees :: [T () ()] -> [T () ()]
trees [x :: T () ()
x] = [T () ()
x, () -> T () () -> T () ()
forall b u. u -> T b u -> T b u
U () T () ()
x]
trees xs :: [T () ()]
xs = do (left :: [T () ()]
left, right :: [T () ()]
right) <- [([T () ()], [T () ()])]
splits
T () ()
t1 <- [T () ()] -> [T () ()]
trees [T () ()]
left
T () ()
t2 <- [T () ()] -> [T () ()]
trees [T () ()]
right
[T () ()] -> [T () ()]
trees [() -> T () () -> T () () -> T () ()
forall b u. b -> T b u -> T b u -> T b u
B () T () ()
t1 T () ()
t2]
where splits :: [([T () ()], [T () ()])]
splits = [([T () ()], [T () ()])] -> [([T () ()], [T () ()])]
forall a. [a] -> [a]
init ([([T () ()], [T () ()])] -> [([T () ()], [T () ()])])
-> [([T () ()], [T () ()])] -> [([T () ()], [T () ()])]
forall a b. (a -> b) -> a -> b
$ [([T () ()], [T () ()])] -> [([T () ()], [T () ()])]
forall a. [a] -> [a]
tail ([([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)
fill :: T () () -> Symbolic (T SBinOp SUnOp)
fill :: T () () -> Symbolic (T (SBV BinOp) (SBV UnOp))
fill (B _ l :: T () ()
l r :: T () ()
r) = SBV BinOp
-> T (SBV BinOp) (SBV UnOp)
-> T (SBV BinOp) (SBV UnOp)
-> T (SBV BinOp) (SBV UnOp)
forall b u. b -> T b u -> T b u -> T b u
B (SBV BinOp
-> T (SBV BinOp) (SBV UnOp)
-> T (SBV BinOp) (SBV UnOp)
-> T (SBV BinOp) (SBV UnOp))
-> SymbolicT IO (SBV BinOp)
-> SymbolicT
IO
(T (SBV BinOp) (SBV UnOp)
-> T (SBV BinOp) (SBV UnOp) -> T (SBV BinOp) (SBV UnOp))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolicT IO (SBV BinOp)
forall a. SymVal a => Symbolic (SBV a)
free_ SymbolicT
IO
(T (SBV BinOp) (SBV UnOp)
-> T (SBV BinOp) (SBV UnOp) -> T (SBV BinOp) (SBV UnOp))
-> Symbolic (T (SBV BinOp) (SBV UnOp))
-> SymbolicT
IO (T (SBV BinOp) (SBV UnOp) -> T (SBV BinOp) (SBV UnOp))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T () () -> Symbolic (T (SBV BinOp) (SBV UnOp))
fill T () ()
l SymbolicT IO (T (SBV BinOp) (SBV UnOp) -> T (SBV BinOp) (SBV UnOp))
-> Symbolic (T (SBV BinOp) (SBV UnOp))
-> Symbolic (T (SBV BinOp) (SBV UnOp))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T () () -> Symbolic (T (SBV BinOp) (SBV UnOp))
fill T () ()
r
fill (U _ t :: T () ()
t) = SBV UnOp -> T (SBV BinOp) (SBV UnOp) -> T (SBV BinOp) (SBV UnOp)
forall b u. u -> T b u -> T b u
U (SBV UnOp -> T (SBV BinOp) (SBV UnOp) -> T (SBV BinOp) (SBV UnOp))
-> SymbolicT IO (SBV UnOp)
-> SymbolicT
IO (T (SBV BinOp) (SBV UnOp) -> T (SBV BinOp) (SBV UnOp))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolicT IO (SBV UnOp)
forall a. SymVal a => Symbolic (SBV a)
free_ SymbolicT IO (T (SBV BinOp) (SBV UnOp) -> T (SBV BinOp) (SBV UnOp))
-> Symbolic (T (SBV BinOp) (SBV UnOp))
-> Symbolic (T (SBV BinOp) (SBV UnOp))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T () () -> Symbolic (T (SBV BinOp) (SBV UnOp))
fill T () ()
t
fill F = T (SBV BinOp) (SBV UnOp) -> Symbolic (T (SBV BinOp) (SBV UnOp))
forall (m :: * -> *) a. Monad m => a -> m a
return T (SBV BinOp) (SBV UnOp)
forall b u. T b u
F
sCase :: (Eq a, SymVal a, Mergeable v) => SBV a -> [(a, v)] -> v
sCase :: SBV a -> [(a, v)] -> v
sCase k :: SBV a
k = [(a, v)] -> v
forall a. Mergeable a => [(a, a)] -> a
walk
where walk :: [(a, a)] -> a
walk [] = String -> a
forall a. HasCallStack => String -> a
error "sCase: Expected a non-empty list of cases!"
walk [(_, v :: a
v)] = a
v
walk ((k1 :: a
k1, v1 :: a
v1):rest :: [(a, a)]
rest) = SBool -> a -> a -> a
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) a
v1 ([(a, a)] -> a
walk [(a, a)]
rest)
eval :: T SBinOp SUnOp -> Symbolic SInteger
eval :: T (SBV BinOp) (SBV UnOp) -> Symbolic SInteger
eval tree :: T (SBV BinOp) (SBV UnOp)
tree = case T (SBV BinOp) (SBV UnOp)
tree of
B b :: SBV BinOp
b l :: T (SBV BinOp) (SBV UnOp)
l r :: T (SBV BinOp) (SBV UnOp)
r -> T (SBV BinOp) (SBV UnOp) -> Symbolic SInteger
eval T (SBV BinOp) (SBV UnOp)
l Symbolic SInteger
-> (SInteger -> Symbolic SInteger) -> Symbolic SInteger
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \l' :: SInteger
l' -> T (SBV BinOp) (SBV UnOp) -> Symbolic SInteger
eval T (SBV BinOp) (SBV UnOp)
r Symbolic SInteger
-> (SInteger -> Symbolic SInteger) -> Symbolic SInteger
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \r' :: SInteger
r' -> SBV BinOp -> SInteger -> SInteger -> Symbolic SInteger
binOp SBV BinOp
b SInteger
l' SInteger
r'
U u :: SBV UnOp
u t :: T (SBV BinOp) (SBV UnOp)
t -> T (SBV BinOp) (SBV UnOp) -> Symbolic SInteger
eval T (SBV BinOp) (SBV UnOp)
t Symbolic SInteger
-> (SInteger -> Symbolic SInteger) -> Symbolic SInteger
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SBV UnOp -> SInteger -> Symbolic SInteger
uOp SBV UnOp
u
F -> SInteger -> Symbolic SInteger
forall (m :: * -> *) a. Monad m => a -> m a
return 4
where binOp :: SBinOp -> SInteger -> SInteger -> Symbolic SInteger
binOp :: SBV BinOp -> SInteger -> SInteger -> Symbolic SInteger
binOp o :: SBV BinOp
o l :: SInteger
l r :: SInteger
r = do SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV BinOp
o SBV BinOp -> SBV BinOp -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== BinOp -> SBV BinOp
forall a. SymVal a => a -> SBV a
literal BinOp
Divide SBool -> SBool -> SBool
.=> SInteger
r SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 4 SBool -> SBool -> SBool
.|| SInteger
r SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 2
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV BinOp
o SBV BinOp -> SBV BinOp -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== BinOp -> SBV BinOp
forall a. SymVal a => a -> SBV a
literal BinOp
Expt SBool -> SBool -> SBool
.=> SInteger
r SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 0
SInteger -> Symbolic SInteger
forall (m :: * -> *) a. Monad m => a -> m a
return (SInteger -> Symbolic SInteger) -> SInteger -> Symbolic SInteger
forall a b. (a -> b) -> a -> b
$ SBV BinOp -> [(BinOp, SInteger)] -> SInteger
forall a v. (Eq a, SymVal a, Mergeable v) => SBV a -> [(a, v)] -> v
sCase SBV BinOp
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, 1)
]
uOp :: SUnOp -> SInteger -> Symbolic SInteger
uOp :: SBV UnOp -> SInteger -> Symbolic SInteger
uOp o :: SBV UnOp
o v :: SInteger
v = do SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV UnOp
o SBV UnOp -> SBV UnOp -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== UnOp -> SBV UnOp
forall a. SymVal a => a -> SBV a
literal UnOp
Sqrt SBool -> SBool -> SBool
.=> SInteger
v SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 4
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV UnOp
o SBV UnOp -> SBV UnOp -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== UnOp -> SBV UnOp
forall a. SymVal a => a -> SBV a
literal UnOp
Factorial SBool -> SBool -> SBool
.=> SInteger
v SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 4
SInteger -> Symbolic SInteger
forall (m :: * -> *) a. Monad m => a -> m a
return (SInteger -> Symbolic SInteger) -> SInteger -> Symbolic SInteger
forall a b. (a -> b) -> a -> b
$ SBV UnOp -> [(UnOp, SInteger)] -> SInteger
forall a v. (Eq a, SymVal a, Mergeable v) => SBV a -> [(a, v)] -> v
sCase SBV UnOp
o
[ (UnOp
Negate, -SInteger
v)
, (UnOp
Sqrt, 2)
, (UnOp
Factorial, 24)
]
generate :: Integer -> T () () -> IO (Maybe (T BinOp UnOp))
generate :: Integer -> T () () -> IO (Maybe (T BinOp UnOp))
generate i :: Integer
i t :: 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 T (SBV BinOp) (SBV UnOp)
symT <- T () () -> Symbolic (T (SBV BinOp) (SBV UnOp))
fill T () ()
t
SInteger
val <- T (SBV BinOp) (SBV UnOp) -> Symbolic SInteger
eval T (SBV BinOp) (SBV UnOp)
symT
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger
val SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
i
Query (Maybe (T BinOp UnOp)) -> Symbolic (Maybe (T BinOp UnOp))
forall a. Query a -> Symbolic a
query (Query (Maybe (T BinOp UnOp)) -> Symbolic (Maybe (T BinOp UnOp)))
-> Query (Maybe (T BinOp UnOp)) -> Symbolic (Maybe (T BinOp UnOp))
forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
case CheckSatResult
cs of
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 (SBV BinOp) (SBV UnOp) -> QueryT IO (T BinOp UnOp)
forall u b.
(SymVal u, SymVal b) =>
T (SBV b) (SBV u) -> QueryT IO (T b u)
construct T (SBV BinOp) (SBV UnOp)
symT
_ -> Maybe (T BinOp UnOp) -> Query (Maybe (T BinOp UnOp))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (T BinOp UnOp)
forall a. Maybe a
Nothing
where
construct :: T (SBV b) (SBV u) -> QueryT IO (T b u)
construct F = T b u -> QueryT IO (T b u)
forall (m :: * -> *) a. Monad m => a -> m a
return T b u
forall b u. T b u
F
construct (U o :: SBV u
o s' :: T (SBV b) (SBV u)
s') = do u
uo <- SBV u -> Query u
forall a. SymVal a => SBV a -> Query a
getValue SBV u
o
u -> T b u -> T b u
forall b u. u -> T b u -> T b u
U u
uo (T b u -> T b u) -> QueryT IO (T b u) -> QueryT IO (T b u)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> T (SBV b) (SBV u) -> QueryT IO (T b u)
construct T (SBV b) (SBV u)
s'
construct (B b :: SBV b
b l' :: T (SBV b) (SBV u)
l' r' :: T (SBV b) (SBV u)
r') = do b
bo <- SBV b -> Query b
forall a. SymVal a => SBV a -> Query a
getValue SBV b
b
b -> T b u -> T b u -> T b u
forall b u. b -> T b u -> T b u -> T b u
B b
bo (T b u -> T b u -> T b u)
-> QueryT IO (T b u) -> QueryT IO (T b u -> T b u)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> T (SBV b) (SBV u) -> QueryT IO (T b u)
construct T (SBV b) (SBV u)
l' QueryT IO (T b u -> T b u)
-> QueryT IO (T b u) -> QueryT IO (T b u)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T (SBV b) (SBV u) -> QueryT IO (T b u)
construct T (SBV b) (SBV u)
r'
find :: Integer -> IO ()
find :: Integer -> IO ()
find target :: 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]
++ ": No solution found."
go (t :: T () ()
t:ts :: [T () ()]
ts) = do Maybe (T BinOp UnOp)
chk <- Integer -> T () () -> IO (Maybe (T BinOp UnOp))
generate Integer
target T () ()
t
case Maybe (T BinOp UnOp)
chk of
Nothing -> [T () ()] -> IO ()
go [T () ()]
ts
Just r :: 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 " [OK]: " else " [BAD]: "
sh :: a -> String
sh i :: a
i | a
i a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< 10 = ' ' 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
concEval :: T BinOp UnOp -> Integer
concEval :: T BinOp UnOp -> Integer
concEval F = 4
concEval (U u :: UnOp
u t :: T BinOp UnOp
t) = UnOp -> Integer -> Integer
uEval UnOp
u (T BinOp UnOp -> Integer
concEval T BinOp UnOp
t)
concEval (B b :: BinOp
b l :: T BinOp UnOp
l r :: 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 Negate i :: Integer
i = -Integer
i
uEval Sqrt i :: Integer
i = if Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 4 then 2 else String -> Integer
forall a. HasCallStack => String -> a
error (String -> Integer) -> String -> Integer
forall a b. (a -> b) -> a -> b
$ "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 Factorial i :: Integer
i = if Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 4 then 24 else String -> Integer
forall a. HasCallStack => String -> a
error (String -> Integer) -> String -> Integer
forall a b. (a -> b) -> a -> b
$ "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 Plus i :: Integer
i j :: Integer
j = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j
bEval Minus i :: Integer
i j :: Integer
j = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j
bEval Times i :: Integer
i j :: Integer
j = Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j
bEval Divide i :: Integer
i j :: Integer
j = Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
j
bEval Expt i :: Integer
i j :: Integer
j = Integer
i Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
j
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 [0 .. 20]