-Since what we need is access to the subterms, we do pattern matching
-on the input term. If the input is simple (the first three `match`
-cases), we return it without further processing. But if the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex at the top level. To understand how this works, follow
-the trace carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 --> I
-
- reduce2 <-- K ; third
- reduce2 --> K
- reduce2 --> K
+Since we need access to the subterms, we do pattern matching on the
+input. If the input is simple (the first three `match` cases), we
+return it without further processing. But if the input is complex, we
+first process the subexpressions, and only then see if we have a redex
+at the top level. To understand how this works, follow the trace
+carefully:
+
+ # reduce (App(App(I,I),K));;
+ reduce <-- App (App (I, I), K)
+
+ reduce <-- K ; first main recursive call
+ reduce --> K
+
+ reduce <-- App (I, I) ; second main recursive call
+ reduce <-- I
+ reduce --> I
+ reduce <-- I
+ reduce --> I
+ reduce <-- I
+ reduce --> I
+ reduce --> I
+
+ reduce <-- K ; third
+ reduce --> K
+ reduce --> K