Rather than having a separate variable for each backend X,
opt_print_X, just have a single variable opt_print_target, where
target contains a string option, such as `Some "lem"` or `Some
"ocaml"`, then we have a function target that takes that string and
invokes the appropriate backend, so the main function in sail.ml goes
from being a giant if-then-else block to a single call to

target !opt_target ast env

This allows us to implement a :compile <target> command in the
interactive toplevel

Also implement a :rewrites <target> command which performs all the
rewrites for a specific target, so rather than doing e.g.

> sail -c -O -o out $FILES

one could instead interactively do

> sail -i
:option -undefined_gen
:load $FILES
:option -O
:option -o out
:rewrites c
:compile c
:quit

for the same result.

To support this the behavior of the interactive mode has changed
slightly. It no longer performs any rewrites at all, so a :rewrites
interpreter is currently needed to interpret functions in the
interactive toplevel, nor does it automatically set any other flags,
so -undefined_gen is needed in this case, which is usually implied by
the -c flag.

- 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.

Improved handling of try/catch

Better handling of unprovable constraints when the environment contains
false