import Maybe

data Term = TTrue 
          | TFalse 
          | TZero
          | TIf Term Term Term
          | TSucc Term 
          | TPred Term
          | TIsZero Term
            deriving (Show, Eq)

isValue TTrue = True
isValue TFalse = True
isValue t = isNumericValue t

isNumericValue TZero = True
isNumericValue (TSucc t) = isNumericValue t
isNumericValue _ = False

eval1 :: Term -> Maybe Term
eval1 (TIf TTrue t2 t3) = Just t2
eval1 (TIf TFalse t2 t3) = Just t3
eval1 (TIf t1 t2 t3) | not (isValue t1) = Just $ TIf ((fromJust . eval1) t1) t2 t3
eval1 (TSucc t) | not (isValue t) = Just $ TSucc ((fromJust . eval1) t)
eval1 (TPred t) | not (isValue t) = Just $ TPred ((fromJust . eval1) t)
eval1 (TPred TZero) = Just TZero
eval1 (TPred (TSucc nv)) | isNumericValue nv = Just nv
eval1 (TIsZero TZero) = Just TTrue
eval1 (TIsZero (TSucc nv)) = Just TFalse
eval1 (TIsZero t) | (not (isValue t)) = Just $ TIsZero ((fromJust . eval1) t)
eval1 _ = Nothing

eval t =
    let t' = eval1 t
    in case t' of Just t'' -> eval t''
                  Nothing -> t 

t1 = TIf (TIsZero (TSucc TZero)) TFalse (TIsZero (TSucc TZero))

data Type = TyBool
          | TyNat
            deriving (Show, Eq)

typeof :: Term -> Maybe Type
typeof TTrue = Just TyBool
typeof TFalse = Just TyBool
typeof TZero = Just TyNat
typeof (TSucc t) | typeof t == Just TyNat = Just TyNat
typeof (TPred t) | typeof t == Just TyNat = Just TyNat
typeof (TIsZero t) | typeof t == Just TyNat = Just TyBool
typeof (TIf t1 t2 t3) | typeof t1 == Just TyBool =
                          let ty2 = typeof t2
                          in if (ty2 == (typeof t3)) then ty2 else Nothing
typeof _ = Nothing

            
safeEval t = 
    case typeof t of
      Just _ -> eval t
      Nothing -> error "Type Error!"