Parser tweaks and fixes

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

1 files changed, 1 insertions, 0 deletions

diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index eee0986f..e0081fb6 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -30,6 +30,7 @@
     (,(regexp-opt sail2-types 'symbols) . font-lock-type-face)
     (,(regexp-opt sail2-special 'symbols) . font-lock-preprocessor-face)
     ("~" . font-lock-negation-char-face)
+    ("\\(::\\)<" 1 font-lock-keyword-face)
     ("@" . font-lock-preprocessor-face)
     ("<->" . font-lock-negation-char-face)
     ("\'[a-zA-Z0-9_]+" . font-lock-variable-name-face)