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

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

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

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

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

evalOp :: Maybe Integer -> (Integer->Integer->Integer) -> Maybe Integer
                        -> (Integer->Integer->Bool)    -> Maybe Integer
evalOp (Just x) op (Just y) p | p x y = Just (x `op` y)
evalOp _        _  _        p         = Nothing

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

combos :: [Integer] -> [Expr]
combos ns = [ Num (read (concat (map show ns))) ]
         ++ [ a `op` b
            | length ns > 1
            , 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
       a <- arbExpr (digits year)
       return (YearExpr year a)
   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 a) =
  let mn = eval a in
    isJust mn ==>
      isJust (solve year (fromJust mn))

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