TaPL 演習 3.5.17

bigstep_eval.ml

type info = string
type term =
  | TmTrue
  | TmFalse
  | TmIf of term * term * term
  | TmZero
  | TmSucc of term
  | TmPred of term
  | TmIsZero of term

let rec isnumericalval t = match t with
  | TmZero   -> true
  | TmSucc a -> isnumericalval a
  | _        -> false

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

exception NoRuleApplies

let d = "dummy"

let rec evalbig t = match t with
  | v when (isval v) -> v
  | TmIf(t1, t2, t3) -> begin
    match evalbig(t1) with
      | TmTrue  -> evalbig t2
      | TmFalse -> evalbig t3
      | _ -> raise NoRuleApplies
    end

  | TmSucc t1 -> begin
    match evalbig(t1) with
      | nv1 when (isnumericalval nv1) -> TmSucc nv1
      | _ -> raise NoRuleApplies
    end

  | TmPred t1 -> begin
    match evalbig(t1) with
      | TmZero     -> TmZero
      | TmSucc nv1 -> nv1
      | _ -> raise NoRuleApplies
    end

  | TmIsZero t1 -> begin
    match evalbig(t1) with
      | TmZero     -> TmTrue
      | TmSucc nv1 -> TmFalse
      | _ -> raise NoRuleApplies
    end

  | _ -> raise NoRuleApplies

let (|>) x f = f x;;


(* Test *)
let testcases = [
  (* (評価されるもの * 期待される結果) *)
  (TmTrue, TmTrue);
  (TmFalse, TmFalse);
  (TmIf(TmTrue, TmTrue, TmFalse), TmTrue);
  (TmIf(TmFalse, TmTrue, TmFalse), TmFalse);
  (TmIf(TmIf(TmTrue, TmTrue, TmFalse), TmTrue, TmFalse), TmTrue);
  (TmIf(TmIf(TmFalse, TmTrue, TmFalse), TmTrue, TmFalse), TmFalse);
  (TmZero, TmZero);
  (TmSucc(TmPred TmZero), TmSucc TmZero);
  (TmIsZero(TmSucc TmZero), TmFalse);
  (TmIsZero(TmPred(TmSucc TmZero)), TmTrue);
  (TmIsZero(TmPred(TmSucc(TmSucc TmZero))), TmFalse);
  (* (TmIsZero TmTrue, TmIsZero TmTrue); # NoRuleApplies! *)
  (* (TmSucc TmTrue, TmSucc TmTrue); # NoRuleApplies! *)
];;


testcases
  |> List.for_all (fun (term, expect) -> evalbig term = expect)
  |> string_of_bool
  |> print_string