module Arithmetic.Model where

import Control.Applicative
import Text.Trifecta

data Term =
    TmTrue
  | TmFalse
  | TmIf Term Term Term
  | TmZero
  | TmSucc Term
  | TmPred Term
  | TmIsZero Term
  deriving (Eq, Show)

isNumeric :: Term -> Bool
isNumeric TmZero = True
isNumeric (TmSucc t) = isNumeric t
isNumeric _ = False

isValue :: Term -> Bool
isValue TmTrue = True
isValue TmFalse = True
isValue t
  | isNumeric t = True
isValue _ = False

step :: Term -> Maybe Term
step (TmIf TmTrue t _) = Just t
step (TmIf TmFalse _ t) = Just t
step (TmIf t1 t2 t3) =
  TmIf <$> step t1 <*> Just t2 <*> Just t3
step (TmSucc t) = TmSucc <$> step t
step (TmPred TmZero) = Just TmZero
step (TmPred (TmSucc vt))
  | isNumeric vt = Just vt
  | otherwise = TmPred . TmSucc <$> step vt
step (TmIsZero TmZero) = Just TmTrue
step (TmIsZero vt)
  | isNumeric vt = Just vt
  | otherwise = TmIsZero <$> step vt
step _ = Nothing

eval :: Term -> Maybe Term
eval t
  | isValue t = Just t
  | otherwise = step t >>= eval
