From a4c90a9c3ed05ead786e5e3fc06ad7e6bbd77b57 Mon Sep 17 00:00:00 2001 From: Nathan Ringo Date: Wed, 24 Jan 2024 19:13:45 -0600 Subject: Better letrec reductions. However... this is now no longer doing capture-avoiding substitution for letrecs... and making the variable the redex kinda makes it harder to do the substitution... Maybe it's time to switch to using pointers in variables. --- discocaml/discocaml.ml | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'discocaml/discocaml.ml') diff --git a/discocaml/discocaml.ml b/discocaml/discocaml.ml index ba407c1..a3f34f7 100644 --- a/discocaml/discocaml.ml +++ b/discocaml/discocaml.ml @@ -44,28 +44,31 @@ let handle_request { expr; command } : response = let buf = Lexing.from_string expr in let expr = Parse.expression buf in let expr = expr_of_parsetree expr in + let binders = get_binders expr in let expr_response ?(note : string option) (expr : expr ast) : response = `Expr { expr = show_expr expr; - has_redex = Option.is_some (Eval.find_redex_cbn expr); + has_redex = Option.is_some (Eval.find_redex_cbn expr binders); note; } in - let step_with (find_redex : expr ast -> expr index option) (expr : expr ast) - : expr ast = - match find_redex expr with - | Some i -> Eval.reduce expr i + let step_with + (find_redex : expr ast -> binder_info option array -> expr index option) + (expr : expr ast) : expr ast = + match find_redex expr binders with + | Some i -> Eval.reduce expr binders i | None -> failwith "no redex" in - let run_with (find_redex : expr ast -> expr index option) : - expr ast -> expr ast Seq.t = + let run_with + (find_redex : expr ast -> binder_info option array -> expr index option) + : expr ast -> expr ast Seq.t = let rec loop (expr : expr ast) : expr ast Seq.t = Seq.cons expr (fun () -> - match find_redex expr with - | Some i -> loop (Eval.reduce expr i) () + match find_redex expr binders with + | Some i -> loop (Eval.reduce expr binders i) () | None -> Nil) in loop -- cgit v1.2.3