import Data.Maybe
import Data.Char
import Test.QuickCheck

------------------------------------------------------------------------------

{-
This exercise will demonstrate several important topics from the course:

  * Recursive data types (and thus recursive functions and pattern matching)
  * Lambda expressions
  * List comprehension
  * Back-tracking search
  * Higher-order functions
  * QuickCheck properties and generators

Problem: Given a year `y` and a number `n`, find an expression whose value is
equal to `n`. The expression consists of subsequences of the digits in `y`
combined using addition, subtraction, multiplication, integer division and
power. The digits of `y` must appear in order in the expression.

For example, if `y = 4823` and `n = 40`, valid expressions are

    48-(2^3)
    (4*8)+(2^3)
-}

------------------------------------------------------------------------------

data Expr
  = Add Expr Expr
  | Sub Expr Expr
  | Mul Expr Expr
  | Div Expr Expr
  | Pow Expr Expr
  | Num Integer

instance Show Expr where
  show (Add a b) = showOp a "+" b
  show (Sub a b) = showOp a "-" b
  show (Div a b) = showOp a "/" b
  show (Mul a b) = showOp a "*" b
  show (Pow a b) = showOp a "^" b
  show (Num n)   = show n

showOp :: Expr -> String -> Expr -> String
showOp a op b = "(" ++ show a ++ op ++ show b ++ ")"

------------------------------------------------------------------------------

-- Evaluate an expression. Expressions that don't have a value (e.g. `1/0`) or
-- that don't have an integer value are represented by `Nothing`.
eval :: Expr -> Maybe Integer
eval (Add a b) = evalOp (eval a) (+) (eval b) (\_ _ -> True)
eval (Sub a b) = evalOp (eval a) (-) (eval b) (\_ _ -> True)
eval (Mul a b) = evalOp (eval a) (*) (eval b) (\_ _ -> True)
eval (Div a b) = evalOp (eval a) div (eval b) (\x y -> y/=0 && x`mod`y==0)
eval (Pow a b) = evalOp (eval a) (^) (eval b) (\x y -> y>=0 && (x/=0 || y/=0)
                                                    && (y<=100 || abs x<=1))
eval (Num n)   = Just n
  -- We cheat a bit by saying `x^y` is not representable if `x>1` and `y>100`.
  -- This is to avoid expressions like `2^(3^(4^5))` which are too big to
  -- compute.

evalOp :: Maybe Integer                    -- First operand
       -> (Integer -> Integer -> Integer)  -- Operation
       -> Maybe Integer                    -- Second operand
       -> (Integer -> Integer -> Bool)     -- Result representable?
       -> Maybe Integer                    -- Result
evalOp (Just x) op (Just y) p | p x y = Just (x `op` y)
evalOp _        _  _        _         = Nothing

------------------------------------------------------------------------------

-- All possible expressions involving the given list of numbers in order
combos :: [Integer] -> [Expr]
combos ns = [ Num (read (concat (map show ns))) ]
         ++ [ a `op` b
            | k  <- [1..length ns-1]
            , a  <- combos (take k ns)
            , b  <- combos (drop k ns)
            , op <- [Add,Sub,Mul,Div,Pow]
            ]

solve :: Integer -> Integer -> Maybe Expr
solve year n = listToMaybe [ a | a <- combos (digits year), eval a == Just n ]

digits :: Integer -> [Integer]
digits = map (fromIntegral . digitToInt) . show

------------------------------------------------------------------------------

-- Soundness: a found solution is correct

data Year = Year Integer deriving ( Show )

instance Arbitrary Year where
  arbitrary = Year `fmap` choose (1000,9999)

prop_Sound :: Year -> Integer -> Property
prop_Sound (Year year) n =
  let ma = solve year n in
    isJust ma ==>
      eval (fromJust ma) == Just n

------------------------------------------------------------------------------

-- Completeness: if there is a solution, there will be a solution found

data YearExpr = YearExpr Integer Expr deriving ( Show )

instance Arbitrary YearExpr where
  arbitrary =
    do Year year <- arbitrary
       e <- arbExpr (digits year)
       return (YearExpr year e)
   where
    arbExpr ns =
      frequency
       [ (1, do return (Num (read (concat (map show ns)))))
       , (s, do k  <- choose (1,length ns-1)
                a  <- arbExpr (take k ns)
                b  <- arbExpr (drop k ns)
                op <- elements [Add, Sub, Mul, Div, Pow]
                return (a `op` b))
       ]
     where
      s = length ns - 1

prop_Complete :: YearExpr -> Property
prop_Complete (YearExpr year e) =
  let mn = eval e in
    isJust mn ==>
      isJust (solve year (fromJust mn))

------------------------------------------------------------------------------