gistfile1.ml

let rec eval2 t = match t with
    t1 when isval(t1) ->
      t1
  | TmIf(_, t1, t2, t3) -> 
      (match eval2 t1 with 
          TmTrue(_) -> eval2 t2 
        | TmFalse(_) -> eval2 t3
        | _ -> raise NoRuleApplies)
  | TmSucc(fi, t1) ->
      (match eval2 t1 with
          t1' when isnumericval t1' -> TmSucc(fi, t1')
        | _ -> raise NoRuleApplies)
  | TmPred(_, t1) ->
      (match eval2 t1 with
          TmZero(_) -> TmZero(dummyinfo)
        | TmSucc(_, nv1) -> eval2 nv1 
        | _ -> raise NoRuleApplies)
  | TmIsZero(_, t1) ->
      (match eval2 t1 with
          TmZero(_) ->
            TmTrue(dummyinfo)
        | TmSucc(_, _) ->
            TmFalse(dummyinfo)
        | _ ->
            raise NoRuleApplies)
  | _ -> raise NoRuleApplies