type to emphasize the parallels with the untyped interpreter. *)
type reduceOutcome = AlreadyReduced | ReducedTo of term
- let reduce_if_redex (t : term) : term = match t with
+ let reduce_if_redex (t : term) : reduceOutcome = match t with
| App(I,a) -> ReducedTo a
| App(App(K,a),b) -> ReducedTo a
| App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
| K -> K
| S -> S
| App(a, b) ->
- let t' = App(reduce_try3 a, reduce_try b) in
+ let t' = App(reduce_try4 a, reduce_try4 b) in
(match reduce_if_redex t' with
| ReducedTo t'' -> reduce_try4 t''
| AlreadyReduced -> t')
type reduceOutcome = AlreadyReduced | ReducedTo of term
- let rec reduce_once (t : term) : term = match t with
+ let rec reduce_once (t : term) : reduceOutcome = match t with
| App(a, b) -> (match reduce_once a with
| ReducedTo a' -> ReducedTo (App(a',b))
| AlreadyReduced -> (match reduce_once b with
| App(App(App(S,_),_),_) -> true
| _ -> false
- let rec reduce_head_once (t : term) : term = match t with
+ let rec reduce_head_once (t : term) : reduceOutcome = match t with
| App(a, b) -> (match reduce_head_once a with
| ReducedTo a' -> ReducedTo (App(a',b))
(* now we only try to reduce b when App(a,b) is a redex *)