core.ml

open Format
open Syntax
open Support.Error
open Support.Pervasive

(* ------------------------   EVALUATION  ------------------------ *)

exception NoRuleApplies

let rec isnumericval t = match t with
    TmZero(_) -> true
  | TmSucc(_,t1) -> isnumericval t1
  | _ -> false

let rec isval t = match t with
    TmTrue(_)  -> true
  | TmFalse(_) -> true
  | t when isnumericval t  -> true
  | _ -> false

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


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

(* let rec eval t =
  try let t' = eval1 t
      in eval t'
  with NoRuleApplies -> t *)

let rec eval t =
  try eval2 t
  with NoRuleApplies -> t