First pass over surface language

[rolyp]

Explain/motivate the surface language and relevance to the overall problem. Some definitions will have to move to the appendix.

Code/example todos:

• example that shows constructed values consuming constructed values (e.g. tree nodes needing list nodes)
• verify annotations on values prettyprinted correctly
  • consolidate prettyprinting special cases on pairs and lists
  • prettyprint lists as nil, cons nodes
  • add highlightIf logic for constructors

Done/dropped:

• move core definitions to the appendix
• two-column format for syntax fig
• rules for forward/backward sugaring (Slicing rules for desugaring #41)
• example figure with source code highlighting
• Core language serves as a useful "core" language but lacks realistic features. Motivate need for a surface language which can support examples given earlier but still with the ability to track dependencies back to source code
• New example containing list comprehensions (w/ generators), clauses, totalise, etc
• Afterwards, explain that to support the requirement of tracking constructor dependencies back to source code, we need not only the typical desugaring process of general languages, but an extra bidirectional stage on top of the bidirectional analysis of the core language
• In the forwards direction, it must specify how annotations on surface language expressions can be correspondingly positioned on the core language expressions that they desugar to.
• Explain the desugaring of our example in chronological order, making reference to and elaborating on the necessary forward desugaring rules when necessary for terms, clauses, and totalise (Figure ??).
• Introduce the syntactic constructs required in the surface language (Figure 15).
• Introduce the "raw" vs. selectable notion (and conventions) from Section 3, for surface terms.
• In the backwards direction, it must use the original surface-language expression as a trace t in order to reconstruct the original surface-level program, and specify how annotations on the core language propagate backwards to form annotations on the surface language
• Explain the backwards desugaring similarly -- perhaps explain each rule of interest by giving the backward and forward cases together?
• State that the relevant functions form Galois connections, and fwd reference the theorems in the appendix (see section 3 again for how to do this).
• Mention but probably don't need to explain typing rules.
• explain why we can get away without a separate (non-slicing) definition of desugaring (can we?)
• In the explanatory text, give the signature of the forward and backward slicing functions, similar to what we did in section 3 for eval, pattern-matching, env lookup, etc. Use the same notational conventions.
• future work: defining a "sugaring" embedding for values into the surface language (for intermediate values), and also a semantics which (modularly) interleaves desugaring with evaluation
• Maybe comment on piecewise definitions, which help motivate eliminators. For clauses we will need the notion of a "partial" eliminator.