- | _, AA -> TODO
- | _, BB ->
-
-We've supplied some of the guts of this function, especially the fiddly bits about how to deal with primitives and literals. But you need to fill in the gaps yourself to make it work. As mentioned before, don't worry about the environments. They're needed to see if variables are associated with any toplevel declarations, but we've filled in that part of the code ourselves. You don't need to worry about the primitives or literals, either.
+ | _,TermLambda _
+ | _,TermPrimfun _
+ | _,TermConstructor _
+ | _,TermDestructor _
+ | _,TermLiteral _ -> AlreadyResult (result_of_term term)
+
+ | fi,TermVar var -> ...
+
+ (* notice we never evaluate a yes/no branch until it is chosen *)
+ | _,TermIf((_,TermLiteral(Bool true)),yes,no) ->
+ ReducedTo yes
+ | _,TermIf((_,TermLiteral(Bool false)),yes,no) ->
+ ReducedTo no
+ | fi,TermIf(test,yes,no) ->
+ (match reduce_head_once test env with
+ | AlreadyResult _ -> StuckAt term (* if test was not reducible to a bool, the if-term is not reducible at all *)
+ | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
+ | ReducedTo test' -> ReducedTo(fi,TermIf(test',yes,no)))
+
+ | ...
+
+
+The homework asked you to fill in some of the gaps in this function. As mentioned before, the only role that environments play in this function is to see if variables are associated with any toplevel bindings. (If you're willing to forego those, you can select an implementation `Env0` of the environments that is guaranteed to do nothing.)