section basiclang

inductive Term : Type
| T : Term
| F : Term
| IfThenElse : Term -> Term -> Term -> Term
| O : Term
| S : Term -> Term
| P : Term -> Term
| IsZ : Term -> Term
| Error : Term

open Term

def isNumericVal : Term -> bool
| O := true
| (S t) := isNumericVal t
| _  := false

def eval : Term -> Term
| (IfThenElse T t2 t3) := t2
| (IfThenElse F t2 t3) := t3
| (IfThenElse t1 t2 t3) :=
  let t1' := eval t1 in (IfThenElse t1' t2 t3)
| (S t1) :=
  let t1' := eval t1 in (S t1')
| (P O) := O
| (P (S nv1)) := if (isNumericVal nv1) then nv1 else Error
| (P t1) :=
  let t1' := eval t1 in (P t1')
| (IsZ O) := T
| (IsZ (S nv1)) := if (isNumericVal nv1) then F else Error
| (IsZ t1) :=
  let t1' := eval t1 in (IsZ t1')
| _ := Error

#reduce eval $ P $ S $ P O
#reduce eval $ IsZ O
#reduce eval $ O
#reduce eval $ IfThenElse (IsZ O) (S O) (S $ S O)
---  s1 -> ns1
--- ---------------
---  S s1 -> S ns1

def ToNat : Term -> nat
| O := 0
| (S (n: Term)) := 1 + ToNat n
| _ := 1

#reduce ToNat (eval $ S $ S $ S $ O)
end basiclang

data Term
    = T
    | F
    | IfThenElse Term Term Term
    | O
    | S Term
    | P Term
    | IsZ Term
    | Error
    deriving (Show)

isNumericVal :: Term -> Bool
isNumericVal t = case t of O -> True
                           S t -> isNumericVal t
                           _ -> False
isNumericVal T
isNumericVal (S O)


eval :: Term -> Term
eval t = case t of IfThenElse T t2 t3 -> t2
                   IfThenElse F t2 t3 -> t3
                   IfThenElse t1 t2 t3 -> let t1' = eval t1 in IfThenElse t1' t2 t3
                   S t1 -> let t1' = eval t1 in S t1'
                   P O -> O
                   P (S nv1) -> if (isNumericVal nv1) then nv1 else Error
                   P t1 -> let t1' = eval t1 in P t1'
                   IsZ O -> T
                   IsZ (S nv1) -> if (isNumericVal nv1) then F else Error
                   IsZ t1 -> let t1' = eval t1 in IsZ t1'
                   _ -> Error
                   
eval (P $ S $ S $ O)