enum Term  {
    case `true`
    case `false`
    indirect case `if`(Term, Term, Term)
    case zero
    indirect case succ(Term)
    indirect case pred(Term)
    indirect case isZero(Term)
}

extension Term: CustomStringConvertible {
    var description: String {
        switch self {
        case .`true`:
            return "True"
        case .`false`:
            return "False"
        case .`if`(let t1, let t2 ,let t3):
            return "if \(t1) { \(t2) } else { \(t3) }"
        case .zero:
            return "Zero"
        case .succ(let t1):
            return "succ(\(t1))"
        case .pred(let t1):
            return "pred(\(t1))"
        case .isZero(let t1):
            return "isZero(\(t1))"
        }
    }
}

func isNumericVal(_ t: Term) -> Bool {
    switch t {
    case .zero:
        return true
    case .succ(let t1):
        return isNumericVal(t1)
    default:
        return false
    }
}

func isVal(_ t: Term) -> Bool {
    switch t {
    case .`true`, .`false`:
        return true
    default:
        return isNumericVal(t)
    }
}

func eval1(_ t: Term) -> Term {
    switch t {
    case .`if`(.`true`, let t2, _):
        return t2
    case .`if`(.`false`, _, let t3):
        return t3
    case .`if`(let t1, let t2, let t3):
        return .`if`(eval1(t1), t2, t3)
    case .succ(let t1):
        return .succ(eval1(t1))
    case .pred(.zero):
        return .zero
    case .pred(.succ(let t1)):
        if isNumericVal(t1) {
            return t1
        } else {
            fatalError("`\(t1)` is not numeric val.")
        }
    case .pred(let t1):
        return .pred((eval1(t1)))
    case .isZero(.zero):
        return .`true`
    case .isZero(.succ(let t1)):
        if isNumericVal(t1) {
            return .`false`
        } else {
            fatalError("`\(t1)` is not numeric val.")
        }
    case .isZero(let t1):
        return .isZero(eval1(t1))
    case .zero:
        return .zero
    default:
        fatalError("invalid term: `\(t)`.")
    }
}

eval1(Term.if(.`true`, .`false`, .`false`)) // False
eval1(Term.if(.`true`, .`true`, .`false`)) // True
eval1(Term.if(.isZero(.zero), .`true`, .`false`)) // if True { True } else { False }
eval1(Term.succ(.succ(.zero))) // succ(succ(Zero))
eval1(Term.succ(.pred(.zero))) // succ(Zero)
eval1(Term.pred(.succ(.zero))) // Zero
eval1(Term.isZero(.zero)) // True
eval1(Term.isZero(.succ(.zero))) // False
eval1(Term.isZero(.pred(.succ(.zero)))) //isZero(Zero)