diff options
| -rw-r--r-- | discocaml/eval.ml | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/discocaml/eval.ml b/discocaml/eval.ml index f8f7dc2..a5cfe41 100644 --- a/discocaml/eval.ml +++ b/discocaml/eval.ml @@ -15,8 +15,19 @@ let is_redex (ast : expr ast) (i : expr index) : bool = | _ -> false) | Var _ -> false -let find_redex_cbv_in (_ast : expr ast) (_i : expr index) : expr index option = - None +let find_redex_cbv_in (ast : expr ast) : expr index -> expr index option = + let rec loop (i : expr index) : expr index option = + or_else + (match get_subexpr ast i with + | App (f, x) -> or_else (loop f) (lazy (loop x)) + | Int _ -> None + | Lam (_, _) -> None + | Prim (Add, (l, r)) | Prim (Sub, (l, r)) | Prim (Mul, (l, r)) -> + or_else (loop l) (lazy (loop r)) + | Var _ -> None) + (lazy (if is_redex ast i then Some i else None)) + in + loop let find_redex_cbn_in (ast : expr ast) : expr index -> expr index option = let rec loop (i : expr index) : expr index option = |