let rec eval' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VAbs(x, e)) | App(e1, e2) -> bind (eval' env e1) (fun v -> match v with | VAbs(x, e) -> bind (eval' env e2) (fun v -> eval' (Cons((x, v), env)) e) | VTup _ -> None) | Tup e -> bind (eval' env e) (fun v -> Some (VTup v)) | Proj e -> bind (eval' env e) (fun v -> match v with | VAbs(_, _) -> None | VTup e -> Some e) type value' = | VClos' of id * (id * value') list * expr | VTup' of value' let rec eval'' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VClos'(x, env, e)) | App(e1, e2) -> bind (eval'' env e1) (fun v -> match v with | VClos'(x, _, e) -> bind (eval'' env e2) (fun v -> eval'' (Cons((x, v), env)) e) | VTup' _ -> None) | Tup e -> bind (eval'' env e) (fun v -> Some (VTup' v)) | Proj e -> bind (eval'' env e) (fun v -> match v with | VClos'(_, _, _) -> None | VTup' v -> Some v) let rec eval'' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VClos'(x, #37, e)) | App(e1, e2) -> bind (eval'' env e1) (fun v -> match v with | VClos'(x, _, e) -> bind (eval'' env e2) (fun v -> eval'' (Cons((x, v), env)) e) | VTup' _ -> None) | Tup e -> bind (eval'' env e) (fun v -> Some (VTup' v)) | Proj e -> bind (eval'' env e) (fun v -> match v with | VClos'(_, _, _) -> None | VTup' v -> Some v) let rec eval'' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VClos'(x, env, e)) | App(e1, e2) -> bind (eval'' env e1) (fun v -> match v with | VClos'(x, _, e) -> bind (eval'' env e2) (fun v -> eval'' (Cons((x, v), env)) e) | VTup' _ -> None) | Tup e -> bind (eval'' env e) (fun v -> Some (VTup' v)) | Proj e -> bind (eval'' env e) (fun v -> match v with | VClos'(_, _, _) -> None | VTup' v -> Some v) type expr' = | Var' of id | Abs' of id * expr' | Closure' of id * (id * expr') list * expr' | App' of expr' * expr' | Tup' of expr' | Proj' of expr' let rec eval' env e = match e with | Var' x -> assoc x env | (Abs'(x, e) | Closure'(x, _, e)) -> Some (Closure'(x, env, e)) | App'(e1, e2) -> bind (eval' env e1) (fun v -> match v with | ((Var' _ | App'(_, _)) | Proj' _) -> fail () | Abs'(x, e) -> bind (eval' env e2) (fun v -> eval' (Cons((x, v), env)) e) | Closure'(x, _, e) -> bind (eval' env e2) (fun v -> eval' (Cons((x, v), env)) e) | Tup' _ -> None) | Tup' e -> bind (eval' env e) (fun v -> Some (Tup' v)) | Proj' e -> bind (eval' env e) (fun v -> match v with | ((Var' _ | App'(_, _)) | Proj' _) -> fail () | (Abs'(_, _) | Closure'(_, _, _)) -> None | Tup' e -> Some e) let rec eval'' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VClos'(x, env, e)) | App(e1, e2) -> bind (eval'' env e1) (fun v -> match v with | VClos'(x, env1, e) -> bind (eval'' env e2) (fun v -> eval'' (Cons((x, v), env1)) e) | VTup' _ -> None) | Tup e -> bind (eval'' env e) (fun v -> Some (VTup' v)) | Proj e -> bind (eval'' env e) (fun v -> match v with | VClos'(_, _, _) -> None | VTup' e -> Some e)