Formalize a P-plus with patterns, side conditions, and pattern guards

[nrnrnr]

Let's have a syntax and semantics for the left-hand side of the arm of a case expression in P-plus. Currently only a pattern can appear in that position. Let's add side conditions and pattern guards. N.B. Once you have pattern guards, side conditions can't simply appear last---because a side condition might be needed to prevent the engine from trying to evaluate an expression in a pattern guard.

Let's use the judgment form from section 8.8 of my book, "⟨p,v⟩ ↣ r," except instead of "p" we'll want the new syntax.

[rogerburtonpatel]

How do you feel about baking side conditions and guards in with patterns? Something like:

pattern ::= 
... 
| (pattern when boolexp)                                 side condition
| (pattern ; {boolexp | (pattern <- expr))               pattern guard 

That way, we could still use the ⟨p,v⟩ ↣ r form of judgement. Although we might want to make the separation of patterns and intermediated guard expressions a bit more distinct. What this does buy us is the ability to side-condition any kind of pattern, and guards themselves subsume the when keyword.

Btw, I think the idea of a boolexp, an expression that must evaluate to a boolean (limited by the grammar, not the type system) will be powerful in solving our intervening e issue.

[nrnrnr]

I feel OK, but it could be simpler. How simple can you make it?

If it helps, programmer ergonomics is not the top issue. Our goal is to make things as simple as possible for the theorist (and your readers!), while not screwing over the programmers too badly.

[rogerburtonpatel]

Done.