diff options
Diffstat (limited to 'discocaml/eval.ml')
-rw-r--r-- | discocaml/eval.ml | 24 |
1 files changed, 19 insertions, 5 deletions
diff --git a/discocaml/eval.ml b/discocaml/eval.ml index 81709e6..f1e5a2b 100644 --- a/discocaml/eval.ml +++ b/discocaml/eval.ml @@ -9,10 +9,14 @@ let has_free_var (ast : expr ast) (i : expr index) (name : string) : bool = | App (f, x) -> loop f; loop x + | Bool _ | Int _ | Nil -> () | Cons (hd, tl) -> loop hd; loop tl - | Int _ | Nil -> () + | If (cond, then_, else_) -> + loop cond; + loop then_; + loop else_ | Lam (x, b) -> if not (String.equal name x) then loop b | Let (recursive, name', bound, body) -> if not (String.equal name name') then loop body; @@ -64,13 +68,15 @@ 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 _ -> raise (FoundRedex i) | _ -> ()) + | If (cond, _, _) -> ( + match get_subexpr ast cond with Bool _ -> raise (FoundRedex i) | _ -> ()) | Let (_, _, _, _) -> 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) | _ -> ()) | Var _ -> () - | Cons _ | Int _ | Lam _ | Nil -> () + | Bool _ | Cons _ | Int _ | Lam _ | Nil -> () let find_redex_cbv_in (ast : expr ast) : expr index -> unit = let rec loop (i : expr index) : unit = @@ -78,12 +84,13 @@ let find_redex_cbv_in (ast : expr ast) : expr index -> unit = | App (f, x) -> loop f; loop x + | If (cond, _, _) -> loop cond | Let (_, _, bound, _) -> loop bound | Prim (Add, (l, r)) | Prim (Sub, (l, r)) | Prim (Mul, (l, r)) -> loop l; loop r | Var _ -> () - | Cons _ | Int _ | Lam _ | Nil -> ()); + | Bool _ | Cons _ | Int _ | Lam _ | Nil -> ()); check_redex ast i in loop @@ -95,12 +102,13 @@ let find_redex_cbn_in (ast : expr ast) : expr index -> unit = | App (f, x) -> loop f; loop x + | If (cond, _, _) -> loop cond | Let (_, _, _, body) -> loop body | Prim (Add, (l, r)) | Prim (Sub, (l, r)) | Prim (Mul, (l, r)) -> loop l; loop r | Var _ -> () - | Cons _ | Int _ | Lam _ | Nil -> () + | Bool _ | Cons _ | Int _ | Lam _ | Nil -> () in loop @@ -131,8 +139,9 @@ let subst (ast : expr ast) (from : string) (to_ : expr index) : in match get_subexpr ast i with | App (f, x) -> add (App (loop f, loop x)) + | Bool _ | Int _ | Nil -> i | Cons (hd, tl) -> add (Cons (loop hd, loop tl)) - | Int _ | Nil -> i + | If (cond, then_, else_) -> add (If (loop cond, loop then_, loop else_)) | Lam (x, b) -> if String.equal from x then i else add (Lam (x, loop b)) | Let (false, name, bound, body) -> add @@ -156,6 +165,11 @@ let reduce (ast : expr ast) (i : expr index) : expr ast = match get_subexpr ast f with | Lam (x', b) -> get_subexpr ast (subst ast x' x b) | _ -> fail ()) + | If (cond, then_, else_) -> ( + match get_subexpr ast cond with + | Bool true -> get_subexpr ast then_ + | Bool false -> get_subexpr ast else_ + | _ -> fail ()) | Let (_, name, _, body) when not (has_free_var ast body name) -> get_subexpr ast body | Let (recursive, name, bound, body) -> |