diff options
| -rw-r--r-- | discocaml/eval.ml | 77 |
1 files changed, 44 insertions, 33 deletions
diff --git a/discocaml/eval.ml b/discocaml/eval.ml index a5cfe41..aa90d41 100644 --- a/discocaml/eval.ml +++ b/discocaml/eval.ml @@ -1,53 +1,64 @@ open Ast -let or_else (type a) (l : a option) (r : a option Lazy.t) : a option = - match l with Some x -> Some x | None -> Lazy.force r +exception FoundRedex of expr index -let is_redex (ast : expr ast) (i : expr index) : bool = +let check_redex (ast : expr ast) (i : expr index) : unit = match get_subexpr ast i with | App (f, _) -> ( - match get_subexpr ast f with Lam (_, _) -> true | _ -> false) - | Int _ -> false - | Lam (_, _) -> false + match get_subexpr ast f with + | Lam (_, _) -> raise (FoundRedex i) + | _ -> ()) + | Int _ -> () + | Lam (_, _) -> () | Prim (Add, (l, r)) | Prim (Sub, (l, r)) | Prim (Mul, (l, r)) -> ( match (get_subexpr ast l, get_subexpr ast r) with - | Int _, Int _ -> true - | _ -> false) - | Var _ -> false + | Int _, Int _ -> raise (FoundRedex i) + | _ -> ()) + | Var _ -> () -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)) +let find_redex_cbv_in (ast : expr ast) : expr index -> unit = + let rec loop (i : expr index) : unit = + (match get_subexpr ast i with + | App (f, x) -> + loop f; + loop x + | Int _ -> () + | Lam (_, _) -> () + | Prim (Add, (l, r)) | Prim (Sub, (l, r)) | Prim (Mul, (l, r)) -> + loop l; + loop r + | Var _ -> ()); + check_redex ast i in loop -let find_redex_cbn_in (ast : expr ast) : expr index -> expr index option = - let rec loop (i : expr index) : expr index option = - if is_redex ast i then Some i - 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 +let find_redex_cbn_in (ast : expr ast) : expr index -> unit = + let rec loop (i : expr index) : unit = + check_redex ast i; + match get_subexpr ast i with + | App (f, x) -> + loop f; + loop x + | Int _ -> () + | Lam (_, _) -> () + | Prim (Add, (l, r)) | Prim (Sub, (l, r)) | Prim (Mul, (l, r)) -> + loop l; + loop r + | Var _ -> () in loop let find_redex_cbv (ast : expr ast) : expr index option = - find_redex_cbv_in ast ast.root + try + find_redex_cbv_in ast ast.root; + None + with FoundRedex i -> Some i let find_redex_cbn (ast : expr ast) : expr index option = - find_redex_cbn_in ast ast.root + try + find_redex_cbn_in ast ast.root; + None + with FoundRedex i -> Some i exception NotARedex of expr ast |