Matching vs. splits

[ndanger000]

Here is a possible approach to handle the analysis of fast reverse that maybe doesn't require quite as much writing. Start off defining the split version of rev. Immediately notice that we could use some nice syntactic sugar, restricting to this particular setting rather than trying to define it in general. Say that you'll come back to this sugar after working through most of the analysis with split. Do the analysis with split, until you get ||rev||. Then observe that ||rev|| also admits the same kind of syntactic sugar as rev did. Now you have the sugared version of ||rev||, and you continue the analysis from there. You also make clear that we can always do this, and so from now on you will just use sugared versions.

[ndanger000]

You need to give the reader some help when you start talking about syntactic sugar (bottom of p. 12):

• Define the syntactic sugar. I.e., what source language expression does rec(e, Nil |-> e0, Cons |-> <y, <ys, r>>.e1) abbreviate?
• Define the expected evaluation rule for the sugared expression.
• Prove that the expected rule is in fact a derived rule by showing that if e is a sugared rec and e evaluates to v with your expected rule, then e' evaluates to v, where e' is the desugared expression.

[ndanger000]

The more I think about this, the more I think the discussion of syntactic sugar belongs in Chapter 2. After you have formally defined the source and complexity languages and the extraction function, then describe the syntactic sugar for the list data type as described in the previous comment. Also give a sugared clause for the extraction function (i.e., ||rec(...)|| = XXX, where ... and XXX are sugared expressions) and show that it is derived from the non-sugared extraction function. Then you can have just the sugared expressions in Chapter 3.