[spectec] Clean up IL semantics and elaborator (WIP)

[rossberg]

This PR cleans up and tightens SpecTec IL scoping and validation and revamps the frontend elaborator accordingly.

The relevant tweaks to the IL are as follows (see also the diff on il/ast.ml):

• Binders are renamed to quantifiers and share the same AST type with parameters.
• Dependent tuple types (x1:t1,...,xN:tN)now bind just variables, not expressions. Furthermore, these variables are properly locally scoped. That implies that they no longer show up in outer binder lists. They scope over field types to the right as expected.
• As a special case, when a tuple type occurs as the parameter of a variant or record constructor, its names also scope over any premises of that arm. For example, in syntax t = C(a : t, b : u(a)) -- if $p(a, b), the variables a and b scope over the premise.
• Consequently, it is no longer necessary that the binders list of variant and record constructors scopes over their parameter type and can instead be treated solely as an existential quantifier for the free variables in the premises. As such, it moves to the right of the parameter and can depend on it, as in syntax t = C(a : t, b : u(a)) {c : v(b)} -- if $f(a, b) = c.
• Iteration variables (both i and j in e^(i<n){j <- k} are now properly locally scoped (this was a bit ambiguous before). That implies that they also no longer show up in outer binder lists.

The net effect of these changes is that all scoping now is much more standard and there no longer is any duplication between "binders" and parameters. As a concrete example, this e.g. is how the elaboration of the type name simplifies:

 syntax name =
-  | `%`{`char*` : char*}(char*{char <- `char*`} : char*)
+  | `%`(`char*` : char*)
     -- if (|$utf8(char*{char <- `char*`})| < (2 ^ 32))

There are only very few cases left where quantifiers on variants actually still show up (for example, the SUBNORM constructor for floats). Note that quantifiers remain heavily used for function definitions and their argument patterns.

• In addition to the above, the internal representation of mixfix operators changes from a list of atoms to a tree of atoms, in order to preserve knowledge about precedences (needed in the elaborator). Backends that do not construct/deconstruct mixops should be unaffected.

Currently there still is a test failure on the AL interpreter.

[f52985]

Fixed the issues on AL interpreter.

The issues were:

1. FUNC comptype representation
For the comptype FUNC rt1 -> rt2, the AL CaseV representation is now ->(rt1, rt2) instead of FUNC(rt1, rt2), since the Mixop.head of the mixop returns "->". Previously, some components relied on the hardcoded string "FUNC", (e.g., backend-interpreter/construct.ml). All uses are now standardized to use "->" as the constructor name for this CaseV.

2. IterE with indexed ListN
The interpreter backend previously assumed that if IterE uses ListN with an index variable, the bound variables (xes) must also include that index variable. Since this assumption no longer holds, the translation and the interpretation logic were fixed to correctly handle such case.