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

judge_base.ml

open Printf

(** ペアノ数 **)
type nat = Z | S of nat

let rec string_of_nat = function
  | Z -> "Z"
  | S n -> sprintf "S(%s)" @@ string_of_nat n
let rec int_of_nat = function
  | Z -> 0
  | S n -> 1 + int_of_nat n
let rec plus n m =
  match n with
  | Z -> m
  | S n' -> S (plus n' m)
let rec minus: nat -> nat -> nat option =
  fun n m ->                    (* n - m *)
    match (n, m) with
    | (Z, S _) -> None
    | (n', Z) -> Some n'
    | (S n', S m') -> minus n' m'
let times n m =
  let rec calc x res =
    match x with
    | Z -> res
    | S x' -> calc x' @@ plus m res
  in calc n Z


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


(** 処理系 **)
let string_of_exp: exp -> string = function
  | Plus (n, m) ->
    let (ns, ms) = (string_of_nat n, string_of_nat m) in
    ns ^ " plus " ^ ms
  | Times (n, m) ->
    let (ns, ms) = (string_of_nat n, string_of_nat m) in
    ns ^ " times " ^ ms

let exp_run: exp -> nat = function
  | Plus (n, m) -> plus n m
  | Times (n, m) -> times n m


(* AST *)
type derive_tree = 
    PZero of nat                              (* Z plus _1 is _1 *)
  | PSucc of (nat * nat * nat) * derive_tree  (* (_1 plus _2 is _3) と部分木 *)
  | TZero of nat                              (* Z times n is Z *)
  | TSucc of (nat * nat * nat) * (derive_tree * derive_tree)  (* [_1 times _2 is ?; _2 plus ? is _3] と部分木の組 *)


let rec gen_eqtree: exp -> nat -> derive_tree = fun 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 -> PSucc ((S n, m, S o), gen_eqtree (Plus (n, m)) o)
    )
  | Times (Z, n) -> (
      match right with
      | Z -> TZero n
      | S _ -> failwith "not equal"
    )
  | Times (S n1, n2) ->
      let n4 = right in
      let n3 =
        let res = minus n4 n2 in (
          match res with
          | None -> failwith "not equal"
          | Some res' -> res'
        ) in
      let nextl = gen_eqtree (Times(n1, n2)) n3
      and nextr = gen_eqtree (Plus(n2, n3)) n4
      in TSucc ((S n1, n2, n4), (nextl, nextr))

let prop_to_derivetree: prop -> derive_tree = function
  | Eq (left, right) -> gen_eqtree left right

let paren: string -> string -> string -> string =
  fun indent node subtreestr ->
    indent ^ node ^ " {\n" ^ subtreestr ^ "\n" ^ indent ^ "}"

let derivetree_printer: derive_tree -> string = fun derivetree ->
  let rec printer derivetree indent =
    match derivetree with
    | PZero n ->
        let res = string_of_nat n
        in indent ^ "Z plus " ^ res ^ " is " ^ res ^ " by P-Zero {}"
    | PSucc ((n, m, o), subtree) ->
        let son = string_of_nat in
        let (a, b, c) = (son n, son m, son o) in
        let node = a ^ " plus " ^ b ^ " is " ^ c ^ " by P-Succ"
        and subtreestr = printer subtree (indent ^ "  ") in
        paren indent node subtreestr
    | TZero n ->
        let res = string_of_nat n
        in indent ^ "Z times " ^ res ^ " is Z by P-Zero {}"
    | TSucc ((n, m, o), (subL, subR)) ->
        let son = string_of_nat in
        let (a, b, c) = (son n, son m, son o) in
        let node = a ^ " times " ^ b ^ " is " ^ c ^ " by T-Succ"
        and subLstr = printer subL (indent ^ "  ")
        and subRstr = printer subR (indent ^ "  ") in
        paren indent node @@ subLstr ^ ";\n" ^ indent ^ subRstr
  in printer derivetree ""


let generator: prop -> unit = fun prop ->
  prop
  |> prop_to_derivetree
  |> derivetree_printer
  |> print_endline

let exp_interpreter: exp -> nat = exp_run
let prop_interpreter: prop -> bool = function
  | Eq (l, r) -> exp_run l = r

let exp_printer: exp -> string = string_of_exp
let prop_printer: prop -> string = function
  | Eq (l, r) -> string_of_exp l ^ " is " ^ string_of_nat r


(*** example ***)
let _ = generator @@ Eq (Plus(Z, S (S Z)), S (S Z));;
let _ = generator @@ Eq (Plus(S (S Z), Z), S (S Z));;

let _ = generator @@ Eq (Times(S Z, S Z), S Z);;

let _ = exp_interpreter @@ Plus(S (S Z), Z);;
let _ = prop_printer @@ Eq (Times(S Z, S Z), S Z);;

例えば、命題 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 = ()

times に対応.

ex) 命題: S Z times S Z is S Z

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

インタプリタとプリティプリンタ

# let _ = exp_interpreter @@ Plus(S (S Z), Z);;
- : nat = S (S Z)
# let _ = prop_printer @@ Eq (Times(S Z, S Z), S Z);;
- : string = "S(Z) times S(Z) is S(Z)"

こっちに移した