7.3 Evaluation

---

7.3 Evaluation

As in Chapter 3, the evaluation function depends on an auxiliary predicate isval:

   let rec isval ctx t = match t with       TmAbs(_,_,_)  true     | _ → false 

The single-step evaluation function is a direct transcription of the evaluation rules, except that we pass a context ctx along with the term. This argument is not used in the present eval1 function, but it is needed by some of the more complex evaluators later on.

   let rec eval1 ctx t = match t with       TmApp(fi,TmAbs(_,x,t12),v2) when isval ctx v2 →         termSubstTop v2 t12     | TmApp(fi,v1,t2) when isval ctx v1 →         let t2' = eval1 ctx t2 in         TmApp(fi, v1, t2')     | TmApp(fi,t1,t2) →         let t1' = eval1 ctx t1 in         TmApp(fi, t1', t2)     | _ →         raise NoRuleApplies 

The multi-step evaluation function is the same as before, except for the ctx argument:

   let rec eval ctx t =     try let t' = eval1 ctx t         in eval ctx t'     with NoRuleApplies → t 

7.3.1 Exercise [Recommended, ⋆⋆⋆ ↛]

Change this implementation to use the "big-step" style of evaluation introduced in Exercise 5.3.8.

---