chap7: init

src/chap7.ml

@@ -0,0 +1,144 @@
+type info = { line : int; column : int }
+let dummyinfo: info = { line = 0; column = 0 }
+
+type context_len = int
+type varname = string
+
+type term =
+    TmVar of info * int * context_len
+  | TmAbs of info * varname * term
+  | TmApp of info * term * term
+
+type binding = NameBind
+type context = (varname * binding) list
+let emptycontext : context = []
+let ctxlength = List.length
+
+(** Shifts the de Bruijn indices of variables in [t] by [d] *)
+let termShift (d : int) (t : term) : term =
+  let rec walk c t =
+    match t with
+    | TmVar(fi, x, n) -> if x >= c then TmVar(fi, x + d, n + d)
+                          else TmVar(fi, x, n + d)
+    | TmAbs(fi, x, t1) -> TmAbs(fi, x, walk (c + 1) t1)
+    | TmApp(fi, t1, t2) -> TmApp(fi, walk c t1, walk c t2)
+  in walk 0 t
+
+(** Substitute the [j]th variable in [t] with [s],
+    where [j] is the de Bruijn index of the variable to be replaced. *)
+let termSubst (j : int) (s : term) (t : term) : term =
+  let rec walk c t =
+    match t with
+    | TmVar(fi, x, n) -> if x = j + c then termShift c s
+                          else TmVar(fi, x, n)
+    | TmAbs(fi, x, t1) -> TmAbs(fi, x, walk (c + 1) t1)
+    | TmApp(fi, t1, t2) -> TmApp(fi, walk c t1, walk c t2)
+  in walk 0 t
+
+(** Substitute the top-level variable in [t] with [s] *)
+let termSubstTop (s : term) (t : term) : term =
+  termShift (-1) (termSubst 0 (termShift 1 s) t)
+
+let rec isval (ctx : context) (t : term) : bool =
+  match t with
+  | TmAbs(_, _, _) -> true
+  | _ -> false
+
+exception NoRuleApplies
+
+let rec eval1 (ctx : context) (t : term) : term =
+  match t with
+  | TmApp(fi, TmAbs(_, _, t12), v2) when isval ctx v2 ->
+      termSubstTop v2 t12
+  | TmApp(fi, v1, t2) when isval ctx v1 ->
+      let t2' = eval1 ctx t2 in
+      TmApp(fi, v1, t2')
+  | TmApp(fi, t1, t2) ->
+      let t1' = eval1 ctx t1 in
+      TmApp(fi, t1', t2)
+  | _ -> raise NoRuleApplies
+
+let rec eval (ctx : context) (t : term) : term =
+  try
+    let t' = eval1 ctx t in
+    eval ctx t'
+  with NoRuleApplies -> t
+
+let rec eval_big_step (ctx : context) (t : term) : term =
+  match t with
+  | TmApp(fi, t1, t2) when (
+    match eval_big_step ctx t1 with
+    | TmAbs(_, x, t12) -> (
+      let t2_eval_result = eval_big_step ctx t2 in
+      let t12_subst_eval_result = eval_big_step ctx (termSubstTop t2_eval_result t12) in
+      isval ctx t2_eval_result && isval ctx t12_subst_eval_result
+    )
+    | _ -> false
+  ) -> (
+    match eval_big_step ctx t1 with
+    | TmAbs(_, x, t12) ->
+        eval_big_step ctx (termSubstTop (eval_big_step ctx t2) t12)
+    (* Should never happen *)
+    | _ -> raise NoRuleApplies
+  )
+  | TmAbs(fi, x, t1) -> TmAbs(fi, x, t1)
+  | _ -> raise NoRuleApplies
+
+(**
+  Picks a fresh name [x] in the context [ctx] and returns the new name and the updated context.
+  If [x] is already in the context, it appends a number to [x] to make it unique.
+  For example, if [x] is "x" and "x" is already in the context, it will return "x0", "x1", etc
+  until it finds a unique name.
+*)
+let pickfreshname (ctx : context) (x : varname) : context * varname =
+  if List.exists (fun (y, _) -> y = x) ctx then
+    let rec aux n =
+      let x' = x ^ string_of_int n in
+      if List.exists (fun (y, _) -> y = x') ctx then aux (n + 1)
+      else ( (x', NameBind) :: ctx, x' )
+    in aux 0
+  else
+    ( (x, NameBind) :: ctx, x )
+
+(**
+  Looks up the name of the variable at de Bruijnindex [x] in the context [ctx].
+  If the index is out of bounds, it raises an error.
+*)
+let index2name (fi : info) (ctx : context) (x : int) : varname =
+  try
+    let (xn, _) = List.nth ctx x in
+    xn
+  with Failure _ -> failwith ("Variable lookup failure: offset: " ^ string_of_int x ^ ", ctx size: " ^ string_of_int (List.length ctx))
+
+let pr : string -> unit = print_string
+
+let rec printtm (ctx : context) (t : term) : unit =
+  match t with
+  | TmAbs(fi, x, t1) ->
+      let (ctx', x') = pickfreshname ctx x in
+      pr "(lambda "; pr x'; pr ". "; printtm ctx' t1; pr ")"
+  | TmApp(fi, t1, t2) ->
+      pr "("; printtm ctx t1; pr " "; printtm ctx t2; pr ")"
+  | TmVar(fi, x, n) ->
+      if ctxlength ctx = n then
+        pr (index2name fi ctx x)
+      else
+        pr "[bad index]"
+
+let () =
+  let ctx = emptycontext in
+  let fn = TmAbs(dummyinfo, "x", TmVar(dummyinfo, 0, 1)) in
+  let nested_fn = TmAbs(dummyinfo, "x", TmApp(dummyinfo, termShift 1 fn, TmVar(dummyinfo, 0, 1))) in
+  let arg = TmAbs(dummyinfo, "y", TmVar(dummyinfo, 0, 1)) in
+  let app = TmApp(dummyinfo, nested_fn, arg) in
+  pr "Original term: ";
+  printtm ctx app;
+  pr "\n";
+  let t' = eval ctx app in
+  let t'_big = eval_big_step ctx app in
+  pr "Evaluated term (small-step): ";
+  printtm ctx t';
+  pr "\n";
+  pr "Evaluated term (big-step): ";
+  printtm ctx t'_big;
+  pr "\n"