combine all cesk simplifications

[kostmo]

This is a flattening of the three stacked PRs:

1. Use SKPair in CESK constructors #1276
2. Introduce 'Go' constructor to factor out SKPair #1281
3. code simplification in CESK state machine #1302

As I was working on this, I realized that certain adjacent cases inside the stepCESK function read like a dialogue (e.g. evaluating the terms of a pair), so it wouldn't make sense to separate them by grouping all of the In and all of the Out cases together.

I also realized that the pattern matching in stepCESK often considers the combination of the Go and SKPair fields, so this limits the opportunities to group into sub-cases by field.

The obvious wins in this refactoring are in prettyPrec and getStore, but in terms of code volume they may be overshadowed by the extra constructors in the stepCESK function.

To mitigate the overhead of these extra constructors, I introduced helper functions where possible: returnVal, returnResult, returnException, and pushFrame. Eventually, applying Pattern Synonyms may get us even more mileage out of this refactoring.

Overall, @byorgey I'll let you be the judge if this refactoring as a whole is worth it, or if perhaps just parts of it should be split off.

[mergify]

⚠️ The sha of the head commit of this PR conflicts with #1302. Mergify cannot evaluate rules on this PR. ⚠️

[byorgey]

@kostmo, I appreciate all your work on this, and it was worth a try, but unfortunately this doesn't seem worth it to me. The extra constructors introduce a lot of noise (definitely far more than what we save in functions like prettyCESK) and I think the functions you introduced to try to mitigate this (returnVal et al) actually make things worse, in the sense of making the code harder to read (especially when thinking about a new contributor trying to read the code). Before, to understand what the stepCESK function was doing you just had to know about the different CESK constructors and you could see it literally sending certain states to other states. Now you have to understand several nested data types and what constructors will be output by the various functions like returnVal.

The SKPair type doesn't really seem meaningful beyond "the part of the machine that we always have no matter which state we're in" (well, except for when we are Waiting... and except for when we are Suspended (#1087 )...). Perhaps Go is meaningful, as in, "we are in a state where the machine is actively doing something", but overall splitting up the CESK into so many sub-types seems to just make it harder to understand, without any big benefits that I can see (though I'm very open to being corrected as far as benefits go... perhaps there are benefits to the refactoring that I've missed).

There are some typo fixes, extra comments etc. in here which should obviously be split out into a separate PR and merged. Whether there is anything else worth splitting out I'm not sure; open to suggestions.

[kostmo]

Yes, that's a fair assessment, and I appreciate you spending the time to review the changes. If nothing else, this exercise did help me understand the CESK machine! In trying to "improve" it, I got a better sense of why it is written the way it was.

[byorgey]

If nothing else, this exercise did help me understand the CESK machine! In trying to "improve" it, I got a better sense of why it is written the way it was.

If you can think of any extra comments that could be added to help preserve your insights for others reading the code later, that would be a great thing to include in a new PR.