    -----------------------------------------------------------------------------
    -- |
    -- 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

    -- | Symbolic variant of 'BinOp'.
    type SBinOp = SBV BinOp

    -- | Symbolic variant of 'UnOp'.
    type SUnOp  = SBV 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 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, "^")]

    -- | 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 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)

    -- | 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 (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

    -- | 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 :: 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)

    -- | 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 (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)   -- exponent is restricted to 0, so the value is 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)  -- argument is restricted to 4, so the value is 2
                                    , (UnOp
    Factorial, 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 evalutes 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 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 -- 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 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'

    -- | 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 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

            -- Make sure the result is correct!
            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

    -- | 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 [0 .. 20]