(** A simple call-by-value evaluator for lambda-terms. *) type term = | Tvar of int | Tint of int | Tfun of int * term | Tapp of term * term let rec subst x v t = match t with | Tvar y -> if x = y then v else t | Tint _ -> t | Tfun(y,b) -> Tfun(y, if x = y then b else subst x v b) | Tapp(t1,t2) -> Tapp(subst x v t1, subst x v t2) let rec eval t = match t with | Tvar y -> failwith "dandling free variables" | Tapp(t1,t2) -> let Tfun(y,b) = eval t1 in eval (subst y (eval t2) b) | _ -> t (** Remark: the binding [let Tfun(y,b) = eval t1 in] raises a warning in Caml "non-exhaustive pattern". We are not concerned with such a warning since we prove that the evaluation of well-behaved programs will always satisfy the pattern [Tfun(y,b)]. *)