A few simplifications to the semantics

[OwenConoly]

I noticed that the type-context parameter to eval_expr is redundant (all the information in it should be contained in the evaluation context, anyway), so I removed it.

Is it okay to do this? Obviously the type-context parameter wasn't important for current functionality, but is it important for some yet-to-be-implemented functionality? Or was the type context there for aesthetic reasons?

For context, I am currently trying to prove the correctness of a transformation from PHOAS ATLexprs to regular ATLexprs. Doing this requires juggling some contexts. Contexts (like balls) are easier to juggle when there are fewer of them, so I felt motivated to get rid of the type-context parameter.

(This is on top of the changes in #3, which is why Github reports a big diff for this PR. In reality, the only extra change is b2436b1, which only changes about 400 lines.)

[OwenConoly]

In addition to the changes described in my initial comment, there is now also ebb9c89, which is probably self-explanatory.

These two changes (b2436b1 and ebb9c89) are entirely independent/unrelated, and either one would make my attempts at reifying ATL programs go a bit more smoothly

[OwenConoly]

Unlike other changes here, 9f3c0ad actually changes the semantics in a non-meaning-preserving way. I think the old meaning was buggy (i.e., out of sync with semantics of shallowly embedded programs).

In contrast, it seems quite subjective whether 389314e is a good idea. My subjective opinion is that it makes things prettier, and my objective-ish observation is that it makes things easier.