chap4: init

2026-06-26 18:21:52 +09:00
parent 02f45c80cd
commit ed434ca123
1 changed files with 137 additions and 0 deletions
@@ -0,0 +1,137 @@
+type info = { line : int; column : int }
+
+let dummyinfo = { line = 0; column = 0 }
+
+type term =
+    TmTrue of info
+  | TmFalse of info
+  | TmIf of info * term * term * term
+  | TmZero of info
+  | TmSucc of info * term
+  | TmPred of info * term
+  | TmIsZero of info * term
+
+let rec is_numeric_val t =
+  match t with
+  | TmZero(_) -> true
+  | TmSucc(_, t1) -> is_numeric_val t1
+  | _ -> false
+
+let rec is_val t =
+  match t with
+  | TmTrue(_) -> true
+  | TmFalse(_) -> true
+  | t when is_numeric_val t -> true
+  | _ -> false
+
+exception NoRuleApplies
+
+let rec eval1 t =
+  match t with
+  | TmIf(_, TmTrue(_), t2, _) -> t2
+  | TmIf(_, TmFalse(_), _, t3) -> t3
+  | TmIf(fi, t1, t2, t3) ->
+      let t1' = eval1 t1 in
+      TmIf(fi, t1', t2, t3)
+  | TmSucc(fi, t1) ->
+      let t1' = eval1 t1 in
+      TmSucc(fi, t1')
+  | TmPred(_, TmZero(_)) -> TmZero(dummyinfo)
+  | TmPred(_, TmSucc(_, nv1)) when is_numeric_val nv1 -> nv1
+  | TmPred(fi, t1) ->
+      let t1' = eval1 t1 in
+      TmPred(fi, t1')
+  | TmIsZero(_, TmZero(_)) -> TmTrue(dummyinfo)
+  | TmIsZero(_, TmSucc(_, nv1)) when is_numeric_val nv1 -> TmFalse(dummyinfo)
+  | TmIsZero(fi, t1) ->
+      let t1' = eval1 t1 in
+      TmIsZero(fi, t1')
+  | _ -> raise NoRuleApplies
+
+let rec eval t =
+  try
+    let t' = eval1 t in
+    eval t'
+  with NoRuleApplies -> t
+
+(* 4.2.2 *)
+let rec eval_big_step t =
+  match t with
+  (* B-IfTrue *)
+  | TmIf(_, TmTrue(_), t2, _) when is_val (eval_big_step t2) -> eval_big_step t2
+
+  (* B-IfFalse *)
+  | TmIf(_, TmFalse(_), _, t3) when is_val (eval_big_step t3) -> eval_big_step t3
+
+  (* B-If *)
+  | TmIf(fi, t1, t2, t3) ->
+      let t1' = eval_big_step t1 in
+      eval_big_step (TmIf(fi, t1', t2, t3))
+
+  (* B-Succ *)
+  | TmSucc(fi, t1) when is_numeric_val (eval_big_step t1) -> TmSucc(fi, eval_big_step t1)
+
+  (* B-PredZero *)
+  | TmPred(fi, t1) when eval_big_step t1 = TmZero(fi) -> TmZero(dummyinfo)
+
+  (* B-PredSucc *)
+  | TmPred(fi, t1) when (
+    match eval_big_step t1 with
+    | TmSucc(_, nv1) when is_numeric_val nv1 -> true
+    | _ -> false
+  ) -> (
+    let nv1 = eval_big_step t1 in
+    match nv1 with
+    | TmSucc(_, nv1') -> nv1'
+    (* Should never happen *)
+    | _ -> raise NoRuleApplies
+  )
+
+  (* B-IsZeroZero *)
+  | TmIsZero(fi, t1) when eval_big_step t1 = TmZero(fi) -> TmTrue(dummyinfo)
+
+  (* B-IsZeroSucc *)
+  | TmIsZero(fi, t1) when (
+    match eval_big_step t1 with
+    | TmSucc(_, nv1) when is_numeric_val nv1 -> true
+    | _ -> false
+  ) -> TmFalse(dummyinfo)
+
+  (* B-Value *)
+  | _ -> t
+
+let rec stringify_term t =
+  match t with
+  | TmTrue(_) -> "true"
+  | TmFalse(_) -> "false"
+  | TmIf(_, t1, t2, t3) ->
+      "if " ^ (stringify_term t1) ^ " then " ^ (stringify_term t2) ^ " else " ^ (stringify_term t3)
+  | TmZero(_) -> "0"
+  | TmSucc(_, t1) -> "succ(" ^ (stringify_term t1) ^ ")"
+  | TmPred(_, t1) -> "pred(" ^ (stringify_term t1) ^ ")"
+  | TmIsZero(_, t1) -> "iszero(" ^ (stringify_term t1) ^ ")"
+
+let () =
+  let t1 = TmIf(dummyinfo, TmTrue(dummyinfo), TmZero(dummyinfo), TmSucc(dummyinfo, TmZero(dummyinfo))) in
+  let t2 = TmIf(dummyinfo, TmFalse(dummyinfo), TmZero(dummyinfo), TmSucc(dummyinfo, TmZero(dummyinfo))) in
+  let t3 = TmIsZero(dummyinfo, TmZero(dummyinfo)) in
+  let t4 = TmIsZero(dummyinfo, TmSucc(dummyinfo, TmZero(dummyinfo))) in
+  let r1 = eval t1 in
+  let r1_big = eval_big_step t1 in
+  let r2 = eval t2 in
+  let r2_big = eval_big_step t2 in
+  let r3 = eval t3 in
+  let r3_big = eval_big_step t3 in
+  let r4 = eval t4 in
+  let r4_big = eval_big_step t4 in
+  print_endline "Small-step evaluation results:";
+  print_endline ("t1 evaluates to: " ^ (stringify_term r1));
+  print_endline ("t2 evaluates to: " ^ (stringify_term r2));
+  print_endline ("t3 evaluates to: " ^ (stringify_term r3));
+  print_endline ("t4 evaluates to: " ^ (stringify_term r4));
+  print_endline "";
+  print_endline "Big-step evaluation results:";
+  print_endline ("t1 evaluates to: " ^ (stringify_term r1_big));
+  print_endline ("t2 evaluates to: " ^ (stringify_term r2_big));
+  print_endline ("t4 evaluates to: " ^ (stringify_term r3_big));
+  print_endline ("t4 evaluates to: " ^ (stringify_term r4_big));