import Data.Typeable
import Data.Maybe

cast' :: (Typeable a, Typeable b) => a -> b
cast' = fromJust . cast

data Term a = Lit Int
            | Inc (Term Int)
            | forall a. Typeable a => If (Term Bool) (Term a) (Term a)
            | IsZ (Term Int)
            | forall a b. (Typeable a, Typeable b) => Pair (Term a) (Term b)
            | forall a b. (Typeable a, Typeable b) => Fst (Term (a, b))
            | forall a b. (Typeable a, Typeable b) => Snd (Term (a, b))

lit :: Int -> Term Int
lit = Lit

inc :: Term Int -> Term Int
inc = Inc

if' :: (Typeable a) => Term Bool -> Term a -> Term a -> Term a
if' = If

isZ :: Term Int -> Term Bool
isZ = IsZ

pair :: (Typeable a, Typeable b) => Term a -> Term b -> Term (a, b)
pair = Pair

fst' :: (Typeable a, Typeable b) => Term (a, b) -> Term a
fst' = Fst

snd' :: (Typeable a, Typeable b) => Term (a, b) -> Term b
snd' = Snd

eval :: Typeable a => Term a -> a
eval (Lit n) = cast' n
eval (Inc t) = cast' $ (eval t) + 1
eval (If g a b) = cast' $ if eval g then eval a else eval b
eval (IsZ t) = cast' $ eval t == 0
eval (Pair a b) = cast' $ (eval a, eval b)
eval (Fst t) = cast' $ fst $ eval t
eval (Snd t) = cast' $ snd $ eval t