From f290fca1afab9bf8aeb58ce0789b4d810abc9f66 Mon Sep 17 00:00:00 2001 From: Nathan Ringo Date: Wed, 24 Jan 2024 00:37:06 -0600 Subject: Adds space for letrec, some capture avoidance, remove binder arrows. --- discocaml/draw_tree.ml | 28 ++++---------------- discocaml/dune | 2 +- discocaml/eval.ml | 72 ++++++++++++++++++++++++++++++++++++++++++++------ discocaml/util.ml | 19 +++++++++++++ 4 files changed, 89 insertions(+), 32 deletions(-) create mode 100644 discocaml/util.ml diff --git a/discocaml/draw_tree.ml b/discocaml/draw_tree.ml index ecf1b71..6b6ce91 100644 --- a/discocaml/draw_tree.ml +++ b/discocaml/draw_tree.ml @@ -1,29 +1,10 @@ open Ast module IntSet = Set.Make (Int) -let break_to_subscript (s : string) : (string * string) option = - let rec loop (i : int) : (string * string) option = - if i < 0 then None - else - let ch = String.get s i in - if '0' <= ch && ch <= '9' then loop (i - 1) - else - let name = String.sub s 0 (i + 1) - and sub = String.sub s (i + 1) (String.length s - i - 1) in - if sub = "" then None else Some (name, sub) - in - loop (String.length s - 1) - -let%test "break_to_subscript fail" = break_to_subscript "x1y" = None -let%test "break_to_subscript simple" = break_to_subscript "x1" = Some ("x", "1") -let%test "break_to_subscript empty" = break_to_subscript "" = None -let%test "break_to_subscript number" = break_to_subscript "123" = None -let%test "break_to_subscript multi" = break_to_subscript "x12" = Some ("x", "12") - let fmt_with_possible_subscript (fmt : Format.formatter) (s : string) : unit = - match break_to_subscript s with + match Util.break_to_subscript s with | Some (name, sub) -> - Format.fprintf fmt "<%s%s>" name + Format.fprintf fmt "<%s%d>" name sub | None -> Format.fprintf fmt "%S" s @@ -51,7 +32,7 @@ let add_node (fmt : Format.formatter) (i : expr index) (expr : expr) : unit = Format.fprintf fmt " expr%d [fontname=\"CMU Typewriter Text Bold\", label=\"%s\"];\n" i.index - (if recursive then "letrec" else "let") + (if recursive then "let rec" else "let") | Nil -> Format.fprintf fmt " expr%d [fontname=\"CMU Typewriter Text Bold\", label=\"[]\"];\n" @@ -128,6 +109,7 @@ let draw_tree (ast : expr ast) : string = add_node fmt i (get_subexpr ast i)) !nodes; + (* get_binders ast |> Array.iteri (fun i -> function | Some j -> @@ -135,7 +117,7 @@ let draw_tree (ast : expr ast) : string = " expr%d -> expr%d_var [color=\"#cccccc\", constraint=false];\n" i j.index | None -> ()); - + *) Format.fprintf fmt "}\n"; Format.pp_print_flush fmt (); Buffer.contents buf diff --git a/discocaml/dune b/discocaml/dune index bd96d64..61bd035 100644 --- a/discocaml/dune +++ b/discocaml/dune @@ -2,7 +2,7 @@ (name discocaml) (inline_tests) (libraries compiler-libs.common yojson) - (modules arraylist ast discocaml draw_tree eval) + (modules arraylist ast discocaml draw_tree eval util) (package discocaml) (preprocess (pps ppx_deriving.show ppx_deriving_yojson ppx_expect))) 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))) diff --git a/discocaml/util.ml b/discocaml/util.ml new file mode 100644 index 0000000..9c70a1a --- /dev/null +++ b/discocaml/util.ml @@ -0,0 +1,19 @@ +let break_to_subscript (s : string) : (string * int) option = + let rec loop (i : int) : (string * int) option = + if i < 0 then None + else + let ch = String.get s i in + if '0' <= ch && ch <= '9' then loop (i - 1) + else + let name = String.sub s 0 (i + 1) + and sub = String.sub s (i + 1) (String.length s - i - 1) in + if sub = "" then None + else int_of_string_opt sub |> Option.map (fun i -> (name, i)) + in + loop (String.length s - 1) + +let%test "break_to_subscript fail" = break_to_subscript "x1y" = None +let%test "break_to_subscript simple" = break_to_subscript "x1" = Some ("x", 1) +let%test "break_to_subscript empty" = break_to_subscript "" = None +let%test "break_to_subscript number" = break_to_subscript "123" = None +let%test "break_to_subscript multi" = break_to_subscript "x12" = Some ("x", 12) -- cgit v1.2.3