-- Code from Section 12.1

module Term where
import Prelude hiding (succ)
import PhantomTypes

data Term t =            Zero   (Int  :=: t)
            |            Succ   (Int  :=: t) (Term Int)
            |            Pred   (Int  :=: t) (Term Int)
            |            IsZero (Bool :=: t) (Term Int)
            | forall a . If     (a    :=: t) (Term Bool) (Term a) (Term a)

eval :: forall t . Term t -> t
eval (Zero p) = applyId p 0
eval (Succ p e) = applyId p $ eval e + 1
eval (Pred p e) = applyId p $ eval e - 1
eval (IsZero p e) =  applyId p $ eval e == 0
eval (If p e1 e2 e3) = applyId p $ if eval e1 then eval e2 else eval e3

zero = Zero refl
succ = Succ refl
pred = Pred refl
iszero = IsZero refl
if' = If refl