module Core
    ( Term(..)
    , isNumericVal
    , isVal
    , eval
    ) where

data Term = TmTrue
          | TmFalse
          | TmIf Term Term Term
          | TmZero
          | TmSucc Term
          | TmPred Term
          | TmIsZero Term

instance Show Term where
    show TmTrue          = "true"
    show TmFalse         = "false"
    show (TmIf t1 t2 t3) = "if " ++ show t1 ++ " then " ++ show t2 ++ " else " ++ show t3
    show TmZero          = "0"
    show (TmSucc t)      = "succ " ++ show t
    show (TmPred t)      = "pred " ++ show t
    show (TmIsZero t)    = "iszero " ++ show t

isNumericVal :: Term -> Bool
isNumericVal TmZero      = True
isNumericVal (TmSucc t1) = isNumericVal t1
isNumericVal _           = False

isVal :: Term -> Bool
isVal TmTrue  = True
isVal TmFalse = True
isVal t       = isNumericVal t

eval1 :: Term -> Maybe Term
eval1 (TmIf TmTrue  t2 t3) = Just t2
eval1 (TmIf TmFalse t2 t3) = Just t3
eval1 (TmIf t1      t2 t3) = do
    t1' <- eval1 t1
    return $ TmIf t1' t2 t3
eval1 (TmSucc t1) = do
    t1' <- eval1 t1
    return $ TmSucc t1'
eval1 (TmPred TmZero)                          = Just $ TmZero
eval1 (TmPred (TmSucc nv1)) | isNumericVal nv1 = Just nv1
eval1 (TmPred t1)                              = do
    t1' <- eval1 t1
    return $ TmPred t1'
eval1 (TmIsZero TmZero)                          = Just $ TmTrue
eval1 (TmIsZero (TmSucc nv1)) | isNumericVal nv1 = Just $ TmFalse
eval1 (TmIsZero t1)                              = do
    t1' <- eval1 t1
    return $ TmIsZero t1'
eval1 _ = Nothing

eval :: Term -> Term
eval t = case eval1 t of
    Just t' -> eval t'
    Nothing -> t