[spectec] Define IL semantics for pattern matching

[rossberg]

This formalises SpecTec IL pattern matching.

Turned out to be a bit more tricky than anticipated. Usually in a small-step semantics, pattern matching is formulated by iteratively reducing a match expression, ideally using evaluation context to focus on the next subpattern to consider. In SpecTec we neither (a) have match expressions, nor (b) can use evaluation contexts.

To address (a), I introduced a match expression, as a sort of administrative expression (we could discuss making it a regular part of the IL), such that function application first reduces into a match. To handle type family application, an analogous approach is used for type reduction. To address (b), the match forms can match sequences of arguments; this allows the equivalent of a "bubbling" semantics, by iteratively splitting matches into more sub-matches, until pattern variables reach the top.

Other changes:

• Had to add type ascriptions on exppull, in order to be able to synthesise quantifiers from them (needed when reducing iteration patterns).
• Changed reduction rules not to use Expand_typ, since that was sneaking big-step into the otherwise small-step rules.
• Added missing contextual rules for path reduction.
• Added negated premises.
• Added (non-computational) reduction rule for relational premises.
• As a minor simplification, removed the optionality of the iteration variable (i in e^(i<n)); _ or a fresh variable is equivalent.
• Renamed RULE to REL premise.

@DCupello1, @sukyoung, @zilinc, @jihongmin63, @conrad-watt, @slindley

[jihongmin63]

There is a typo in the Step_typ/MATCH-match-fail rule: a'' should be a.

Additionally, I have a question regarding the Step_expmatch_plain/UN-PLUS and UN-MINUS rules. These rules appear to reject the matching of num and e when num carries a specific sign. However, my understanding is that $numun simply maintains or reverses the sign. Does the current SpecTec definition imply that numun is responsible for normalizing the sign as specified?

[rossberg]

@jihongmin63, thanks, typo is fixed.

Regarding signs, the rules require that the l.h.s. has already been reduced to a plain number, which you could think of as normalising signs because they are internalised into the number, i.e. can't be unops anymore. The rules just check their signs and then proceed with the absolute value of the number. (Not sure if that answers your question.)