diff options
Diffstat (limited to 'discocaml')
| -rw-r--r-- | discocaml/discocaml.ml | 21 | ||||
| -rw-r--r-- | discocaml/eval.ml | 49 |
2 files changed, 47 insertions, 23 deletions
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 diff --git a/discocaml/eval.ml b/discocaml/eval.ml index 9f94e41..6bb21ad 100644 --- a/discocaml/eval.ml +++ b/discocaml/eval.ml @@ -109,13 +109,16 @@ let%expect_test "get_fresh_in" = exception FoundRedex of expr index -let check_redex (ast : expr ast) (i : expr index) : unit = +let check_redex (ast : expr ast) (binders : binder_info option array) + (i : expr index) : unit = match get_subexpr ast i with | App (f, _) -> ( match get_subexpr ast f with Lam _ -> raise (FoundRedex i) | _ -> ()) | If (cond, _, _) -> ( match get_subexpr ast cond with Bool _ -> raise (FoundRedex i) | _ -> ()) - | Let (_, _, _, _) -> raise (FoundRedex i) + | Let (false, _, _, _) -> raise (FoundRedex i) + | Let (true, name, _, body) -> + if not (has_free_var ast body name) then raise (FoundRedex i) | Prim (Add, (l, r)) | Prim (Sub, (l, r)) | Prim (Mul, (l, r)) -> ( match (get_subexpr ast l, get_subexpr ast r) with | Int _, Int _ -> raise (FoundRedex i) @@ -125,10 +128,17 @@ let check_redex (ast : expr ast) (i : expr index) : unit = | Bool _, Bool _ -> raise (FoundRedex i) | Int _, Int _ -> raise (FoundRedex i) | _ -> ()) - | Var _ -> () + | Var _ -> ( + match binders.(i.index) with + | Some (`Bound j) -> ( + match get_subexpr ast j with + | Let (true, _, _, _) -> raise (FoundRedex i) + | _ -> ()) + | _ -> ()) | Bool _ | Cons _ | Int _ | Lam _ | Nil -> () -let find_redex_cbv_in (ast : expr ast) : expr index -> unit = +let find_redex_cbv_in (ast : expr ast) (binders : binder_info option array) : + expr index -> unit = let rec loop (i : expr index) : unit = (match get_subexpr ast i with | App (f, x) -> @@ -147,13 +157,14 @@ let find_redex_cbv_in (ast : expr ast) : expr index -> unit = loop r | Var _ -> () | Bool _ | Cons _ | Int _ | Lam _ | Nil -> ()); - check_redex ast i + check_redex ast binders i in loop -let find_redex_cbn_in (ast : expr ast) : expr index -> unit = +let find_redex_cbn_in (ast : expr ast) (binders : binder_info option array) : + expr index -> unit = let rec loop (i : expr index) : unit = - check_redex ast i; + check_redex ast binders i; match get_subexpr ast i with | App (f, x) -> loop f; @@ -171,15 +182,17 @@ let find_redex_cbn_in (ast : expr ast) : expr index -> unit = in loop -let find_redex_cbv (ast : expr ast) : expr index option = +let find_redex_cbv (ast : expr ast) (binders : binder_info option array) : + expr index option = try - find_redex_cbv_in ast ast.root; + find_redex_cbv_in ast binders ast.root; None with FoundRedex i -> Some i -let find_redex_cbn (ast : expr ast) : expr index option = +let find_redex_cbn (ast : expr ast) (binders : binder_info option array) : + expr index option = try - find_redex_cbn_in ast ast.root; + find_redex_cbn_in ast binders ast.root; None with FoundRedex i -> Some i @@ -229,7 +242,8 @@ let rec subst (ast : expr ast) (from : string) (to_ : expr index) : in loop -let reduce (ast : expr ast) (i : expr index) : expr ast = +let reduce (ast : expr ast) (binders : binder_info option array) + (i : expr index) : expr ast = let fail () = raise (NotARedex { ast with root = i }) in let ast = copy ast in let must_int j = match get_subexpr ast j with Int n -> n | _ -> fail () in @@ -246,8 +260,8 @@ let reduce (ast : expr ast) (i : expr index) : expr ast = | _ -> fail ()) | Let (_, name, _, body) when not (has_free_var ast body name) -> get_subexpr ast body - | Let (recursive, name, bound, body) -> - Let (recursive, name, bound, subst ast name bound body) + | Let (false, name, bound, body) -> + get_subexpr ast (subst ast name bound body) | Prim (Add, (l, r)) -> Int (must_int l + must_int r) | Prim (Sub, (l, r)) -> Int (must_int l - must_int r) | Prim (Mul, (l, r)) -> Int (must_int l * must_int r) @@ -266,5 +280,12 @@ let reduce (ast : expr ast) (i : expr index) : expr ast = | `GTE -> l >= r | `EQ -> l = r | `NE -> l <> r) + | Var _ -> ( + match binders.(i.index) with + | Some (`Bound j) -> ( + match get_subexpr ast j with + | Let (true, _, bound, _) -> get_subexpr ast bound + | _ -> fail ()) + | _ -> fail ()) | _ -> fail ()); ast |