『プログラミング言語の基礎概念』の演習システムの導出木生成用DSLのサブセット

derivetree_DSL_small_subset.ml

(** ペアノ数 **)
type nat = Z | S of nat
let rec nat_of_string = function
  | Z -> "Z"
  | S n -> "S(" ^ nat_of_string n ^ ")"


(*** DSL ***)
(* syntax *)
type exp = Plus of nat * nat    (* _1 plus _2 *)
type prop = Eq of exp * nat     (* _1 is _2 *)


(** 処理系 **)
type derive_tree = 
    PZero of nat                              (* Z plus _1 is _1 *)
  | PSucc of (nat * nat * nat) * derive_tree  (* (_1 plus _2 is _3) と部分木 *)

let rec prop_to_derivetree: prop -> derive_tree = function
  | Eq (left, right) -> (
      match left with
      | Plus(Z, n) ->
        if n = right then PZero n
        else failwith "not equal"
      | Plus(S n, m) -> (
          match right with
          | Z -> failwith "not equal"
          | S o ->
            let premise = Eq (Plus (n, m), o)
            in PSucc ((S n, m, S o), prop_to_derivetree premise)
        )
    )

let derivetree_printer: derive_tree -> string = fun derivetree ->
  let rec printer derivetree tab =
    match derivetree with
    | PZero n ->
        let res = nat_of_string n
        in tab ^ "Z plus " ^ res ^ " is " ^ res ^ " by P-Zero {}"
    | PSucc ((n, m, o), subtree) ->
        let nos = nat_of_string in
        let (a, b, c) = (nos n, nos m, nos o) in
        tab ^ a ^ " plus " ^ b ^ " is " ^ c ^ " by P-Succ {\n"
        ^ printer subtree (tab ^ "  ") ^ "\n"
        ^ tab ^ "}"
  in printer derivetree ""


(* compiler *)
let compile prop =
  prop
  |> prop_to_derivetree
  |> derivetree_printer
  |> print_endline

例えば、命題 S (S Z) plus Z is S (S Z) の導出木をこんな感じに吐ける

# let _ = compile @@ Eq (Plus(S (S Z), Z), S (S Z));;
S(S(Z)) plus Z is S(S(Z)) by P-Succ {
  S(Z) plus Z is S(Z) by P-Succ {
    Z plus Z is Z by P-Zero {}
  }
}
- : unit = ()