TaPL 演習4.2.2

問題

arithの実装におけるeval関数の定義を、大ステップスタイルに変えよ。

答案

もう少しうまく書きたい。

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

感想

軽く試した感じは、ちゃんと動いてる。ただ正確に動くかどうかはCoq等で証明すべきなんだろうな。 あとは関数名をeval'とかにすべきだったかも。