From f290fca1afab9bf8aeb58ce0789b4d810abc9f66 Mon Sep 17 00:00:00 2001
From: Nathan Ringo <nathan@remexre.com>
Date: Wed, 24 Jan 2024 00:37:06 -0600
Subject: Adds space for letrec, some capture avoidance, remove binder arrows.

---
 discocaml/eval.ml | 72 ++++++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 64 insertions(+), 8 deletions(-)

(limited to 'discocaml/eval.ml')

diff --git a/discocaml/eval.ml b/discocaml/eval.ml
index cdcb727..0d2e14d 100644
--- a/discocaml/eval.ml
+++ b/discocaml/eval.ml
@@ -1,7 +1,5 @@
 open Ast
 
-exception FoundRedex of expr index
-
 let has_free_var (ast : expr ast) (i : expr index) (name : string) : bool =
   let exception FoundIt in
   let rec loop (i : expr index) =
@@ -67,6 +65,50 @@ let%expect_test "has_free_var shadowing tests" =
     let rec x = x in x: false
   |}]
 
+let bump_var (name : string) : string =
+  match Util.break_to_subscript name with
+  | Some (base, i) -> Format.sprintf "%s%d" base (i + 1)
+  | None -> name ^ "0"
+
+let%test _ = bump_var "x" = "x0"
+let%test _ = bump_var "x0" = "x1"
+let%test _ = bump_var "x123" = "x124"
+
+let get_fresh_in (ast : expr ast) (is : expr index list) : string -> string =
+  let rec loop (name : string) : string =
+    if List.exists (fun i -> has_free_var ast i name) is then
+      loop (bump_var name)
+    else name
+  in
+  loop
+
+let%expect_test "get_fresh_in" =
+  let ast = new_ast () in
+  let add (expr : expr) : expr index =
+    let index = Arraylist.length ast.subexprs in
+    Arraylist.push ast.subexprs expr;
+    { index }
+  in
+
+  let x = add (Var "x") and x0 = add (Var "x0") and x1 = add (Var "x1") in
+
+  let xx0 = add (Prim (Add, (x, x0))) in
+  let xx0x1 = add (Prim (Add, (xx0, x1))) in
+
+  Printf.printf "%S\n" (get_fresh_in ast [ xx0x1 ] "x");
+  Printf.printf "%S\n" (get_fresh_in ast [ xx0 ] "x");
+  Printf.printf "%S\n" (get_fresh_in ast [ x; x1 ] "x");
+  Printf.printf "%S\n" (get_fresh_in ast [ x; x1 ] "y");
+
+  [%expect {|
+    "x2"
+    "x1"
+    "x0"
+    "y"
+  |}]
+
+exception FoundRedex of expr index
+
 let check_redex (ast : expr ast) (i : expr index) : unit =
   match get_subexpr ast i with
   | App (f, _) -> (
@@ -140,8 +182,7 @@ let find_redex_cbn (ast : expr ast) : expr index option =
 
 exception NotARedex of expr ast
 
-(* TODO: Be capture-avoiding! *)
-let subst (ast : expr ast) (from : string) (to_ : expr index) :
+let rec subst (ast : expr ast) (from : string) (to_ : expr index) :
     expr index -> expr index =
   let rec loop (i : expr index) : expr index =
     let add (expr : expr) : expr index =
@@ -156,12 +197,27 @@ let subst (ast : expr ast) (from : string) (to_ : expr index) :
     | Bool _ | Int _ | Nil -> i
     | Cons (hd, tl) -> add (Cons (loop hd, loop tl))
     | If (cond, then_, else_) -> add (If (loop cond, loop then_, loop else_))
-    | Lam (x, b) -> if String.equal from x then i else add (Lam (x, loop b))
+    | Lam (x, b) ->
+        if String.equal from x then i
+        else if has_free_var ast to_ x then
+          let x' = get_fresh_in ast [ b; to_ ] x in
+          add (Lam (x', loop (subst ast x (add (Var x')) b)))
+        else add (Lam (x, loop b))
     | Let (false, name, bound, body) ->
-        add
-          (Let (false, name, loop bound, if name = from then body else loop body))
+        if String.equal from name then add (Let (false, name, loop bound, body))
+        else if has_free_var ast to_ name then
+          let name' = get_fresh_in ast [ body; to_ ] name in
+          let body' = subst ast name (add (Var name')) body in
+          add (Let (false, name', loop bound, loop body'))
+        else add (Let (false, name, loop bound, loop body))
     | Let (true, name, bound, body) ->
-        if name = from then i else add (Let (true, name, loop bound, loop body))
+        if String.equal from name then i
+        else if has_free_var ast to_ name then
+          let name' = get_fresh_in ast [ bound; body; to_ ] name in
+          let bound' = subst ast name (add (Var name')) bound
+          and body' = subst ast name (add (Var name')) body in
+          add (Let (true, name', loop bound', loop body'))
+        else add (Let (true, name, loop bound, loop body))
     | Prim (Add, (l, r)) -> add (Prim (Add, (loop l, loop r)))
     | Prim (Sub, (l, r)) -> add (Prim (Sub, (loop l, loop r)))
     | Prim (Mul, (l, r)) -> add (Prim (Mul, (loop l, loop r)))
-- 
cgit v1.2.3