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 let is_redex (ast : expr ast) (i : expr index) : bool = match get_subexpr ast i with | App (f, _) -> ( match get_subexpr ast f with Lam (_, _) -> true | _ -> false) | Int _ -> false | Lam (_, _) -> false | 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 let find_redex_cbv_in (_ast : expr ast) (_i : expr index) : expr index option = None 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 in loop let find_redex_cbv (ast : expr ast) : expr index option = find_redex_cbv_in ast ast.root let find_redex_cbn (ast : expr ast) : expr index option = find_redex_cbn_in ast ast.root let reduce (ast : expr ast) (_i : expr index) : expr ast = let ast = copy ast in ast