aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--discocaml/draw_tree.ml28
-rw-r--r--discocaml/dune2
-rw-r--r--discocaml/eval.ml72
-rw-r--r--discocaml/util.ml19
4 files changed, 89 insertions, 32 deletions
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<FONT POINT-SIZE=\"12\"><SUB>%s</SUB></FONT>>" name
+ Format.fprintf fmt "<%s<FONT POINT-SIZE=\"12\"><SUB>%d</SUB></FONT>>" 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)
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-28 14:11:03 +0000