Last active
August 19, 2017 04:26
-
-
Save Gobi03/fb313cb88cd072cb870e5a5e65d97e0b to your computer and use it in GitHub Desktop.
『プログラミング言語の基礎概念』の演習システム用の導出木生成DSL
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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);; | |
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)"
こっちに移した
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
例えば、命題
S (S Z) plus Z is S (S Z)
の導出木をこんな感じに吐ける