Implement type indexing and adapt spec

[rossberg]

Sorry for this large PR, this change became a bit of a rabbit hole needing many changes.

PTAL at the spec changes in particular.

Changes to the EL:

• Added type family declarations: syntax id(params); type definitions then define cases for it, by pattern-matching on their args (analogous to function definitions).
• Added local variable declarations as a new form of premise: -- var x : t (due to the possibility of local type indices, global var declarations are no longer sufficient). This is ignored in rendering.
• Renamed Syn to Typ throughout the AST, for more consistency.
• Added !% hole for suppressing an operand in pretty-printing (only for show hints).

Changes to the IL:

• Type identifiers can have arguments now: id(args), or VarT of id * arg list.
• Type definitions define a parameter type and a list of instances, to represent families by pattern matching on arguments (analogous to function clauses).
• Calls are now n-ary and take a list of "arguments", which can be either expressions or types.
• Function definitions likewise have a parameter list for their domain.
• Similarly, bindings can be variable or type identifiers.
• Tuple types can bind identifiers to account for dependencies (this isn't quite the right level, may clean this up).
• Renamed Syn to Typ throughout the AST, for more consistency.

Changes to AL:

• Eliminate VecV.

Changes to specs:

• Values are now indexed by type, e.g. num_(numtype), lane_(lanetype) etc., which allows checking that the correct kind of constant is used everywhere. This uncovered a couple of problems in the rules, e.g.
  • array.new/init_data not distinguishing between CONST and VCONST in its reduction (this is glossed over in the real spec, because it happens to work syntactically),
  • splat and replace_lane not wrapping their operands for packed types (bug in the real spec).
• Operators are indexed by type, e.g., binop_(numtype) etc., which makes checking tighter, gets rid of all the xyzopXXX definitions, as well as the tedious _I and _F injections (which we would have needed for every constant otherwise, now that we distinguish between int and float values properly).
• Edit: Refactored dot, extmul and extadd instructions into generic extunop and extbinop instructions, for more regularity and clarity.
• Narrowed types of some of the AST definitions to rule out unsupported cases, either by using more refined types or by inserting side conditions. Added a few TODOs with more refinements needed.
• Refined the types of numeric parameters of various meta functions, e.g., def $vcvtop(shape_1, shape_2, vcvtop, sx?, lnum_($lanetype(shape_1))) : lnum_($lanetype(shape_2)).
• Some parameter reordering in meta functions to account for type dependencies.
• Changed reduction of VRELOP to be more abstract, analogous to VBINOP.
• Had to add a few local variable declarations where the types cannot be deduced.
• $concat is now a polymorphic operation. :)
• Added various TODOs.

Many corresponding changes in front- and middlend, some adaptation in backends.

Caveats, as mentioned:

• I deactivated the subtype elimination pass, since it does not work correctly with type indices. (Arguably, it was already broken, because it happily introduced function invocations in argument patterns on the LHS of definitions.)

• The interpreter now fails 85% of tests. I suspect this is mostly due to the refactoring of the constant and operator syntax that it hard-codes. I tried to fix the obvious places, but there seem to be other causes that I was not able to debug.

[rossberg]

Is anybody opposed to merging this PR? Not sure if anybody has been looking at it, but f you need more time for that, please let me know. If not, I'd like to merge it early next week. (It contains various changes that kind of block most of the follow-up clean-ups that I have on my TODO list.)

[rossberg]

D'oh, sorry. I just noticed that I accidentally committed one change here the other day that I meant to upload separately, namely refactoring dot/extmul/extadd into generic ext{un/bin}op instructions (a change I wanted to do for a while already). But perhaps that's for the better, putting all breaking changes to the operator/interpreter interplay in one place... :)

[rossberg]

OK, landing now. CI is red because I did not update test expectations for the interpreter to include the failures.