Add an extra argument for Type_check.prove for the location of the prove
call (as prove __POS__) to help debug SMT related issues

- Completely remove the nexp = nexp syntax in favour of nexp ==
  nexp. All our existing specs have already switched over. As part of
  this fix every test that used the old syntax, and update the
  generated aarch64 specs

- Remove the `type when constraint` syntax. It just makes changing the
  parser in any way really awkward.

- Change the syntax for declaring new types with multiple type
  parameters from:

  type foo('a : Type) ('n : Int), constraint = ...

  to

  type foo('a: Type, 'n: Int), constraint = ...

  This makes type declarations mimic function declarations, and makes
  the syntax for declaring types match the syntax for using types, as
  foo is used as foo(type, nexp). None of our specifications use types
  with multiple type parameters so this change doesn't actually break
  anything, other than some tests. The brackets around the type
  parameters are now mandatory.

- Experiment with splitting Type/Order type parameters from Int type
  parameters in the parser.

  Currently in a type bar(x, y, z) all of x, y, and z could be either
  numeric expressions, orders, or types. This means that in the parser
  we are severely restricted in what we can parse in numeric
  expressions because everything has to be parseable as a type (atyp)
  - it also means we can't introduce boolean type
  variables/expressions or other minisail features (like removing
  ticks from type variables!) because we are heavily constrained by
  what we can parse unambigiously due to how these different type
  parameters can be mixed and interleaved.

  There is now experimental syntax: vector::<'o, 'a>('n) <-->
  vector('n, 'o, 'a) which splits the type argument list into two
  between Type/Order-polymorphic arguments and Int-polymorphic
  arguments. The exact choice of delimiters isn't set in stone - ::<
  and > match generics in Rust. The obvious choices of < and > / [ and
  ] are ambigious in various ways.

  Using this syntax right now triggers a warning.

- Fix undefined behaviour in C compilation when concatenating a
  0-length vector with a 64-length vector.

Requires a recent Lem version that supports generating session-qualified
imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860

Move the utility functions for graph generation and pretty printing of
intermediate representation instructions into a separate file,
bytecode_util.ml, by analogy with ast_util.ml.

Add an optimization pass that searches for specific patterns of struct
updates and removes uncessary copying of the structs involved. With
this optimisation pass the time taken for u-boot to run approx
57,000,000 instructions goes down from about 11-12 minutes to 8
minutes (about 120,000 IPS).

Also add an additional -Oz3 flag that uses z3 to optimize some
additional types. This is currently very experimental and doesn't
fully work yet.