Move inline forall in function definitions

* Previously we allowed the following bizarre syntax for a forall
  quantifier on a function:

  val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit

  this commit changes this to the more sane:

  val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit

  Having talked about it today, we could consider adding the syntax

  val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit

  which would avoid the forall (by implicitly quantifying variables in
  the constraint), and be slightly more friendly especially for
  documentation purposes. Only RISC-V used this syntax, so all uses of
  it there have been switched to the new style.

* Second, there is a new (somewhat experimental) syntax for
  existentials, that is hopefully more readable and closer to
  minisail:

  val foo(x: int, y: int) -> int('m) with 'm >= 2

  "type('n) with constraint" is equivalent to minisail: {'n: type | constraint}
  the type variables in typ are implicitly quantified, so this is equivalent to
  {'n, constraint. typ('n)}

  In order to make this syntax non-ambiguous we have to use == in
  constraints rather than =, but this is a good thing anyway because
  the previous situation where = was type level equality and == term
  level equality was confusing. Now all the type type-level and
  term-level operators can be consistent. However, to avoid breaking
  anything = is still allowed in non-with constraints, and produces a
  deprecated warning when parsed.

6 files changed, 5 insertions, 40 deletions

diff --git a/test/typecheck/pass/inline_typ.sail b/test/typecheck/pass/inline_typ.sail
index dd761b83..95be790c 100644
--- a/test/typecheck/pass/inline_typ.sail
+++ b/test/typecheck/pass/inline_typ.sail
@@ -1,2 +1,2 @@
 
-function test (x : atom('n), y : atom('m)) -> forall 'n 'm. atom('m + 'n) = undefined
\ No newline at end of file
+function test forall 'n 'm. (x : int('n), y : int('m)) -> int('m + 'n) = undefined
\ No newline at end of file
diff --git a/test/typecheck/pass/nat_set.sail b/test/typecheck/pass/nat_set.sail
index a12e81da..f171eb9b 100644
--- a/test/typecheck/pass/nat_set.sail
+++ b/test/typecheck/pass/nat_set.sail
@@ -1,4 +1,4 @@
-function test x : atom('n) -> forall 'n. bool = true
+function test forall 'n, 'n in {1, 3}. x : atom('n) -> bool = true
 
 let x = test(1)
 
diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail
index de4458ed..24e50259 100644
--- a/test/typecheck/pass/option_either.sail
+++ b/test/typecheck/pass/option_either.sail
@@ -2,11 +2,11 @@ default Order inc
 
 union option ('a : Type) = {None : unit, Some : 'a}
 
-function none () -> forall ('a : Type). option('a) = None()
+function none forall ('a : Type). () -> option('a) = None()
 
-function some x : 'a -> forall ('a : Type). option('a) = Some(x)
+function some forall ('a : Type). x : 'a -> option('a) = Some(x)
 
-function test x : option('a) -> forall ('a : Type). range(0, 1) = match x {
+function test forall ('a : Type). x : option('a) -> range(0, 1) = match x {
   None() => 0,
   Some(y) => 1
 }
diff --git a/test/typecheck/pass/or_pattern.sail b/test/typecheck/pass/or_pattern.sail
deleted file mode 100644
index a6e11ecd..00000000
--- a/test/typecheck/pass/or_pattern.sail
+++ /dev/null
@@ -1,16 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-let x : int = 5
-
-val main : unit -> unit
-
-function main() = {
-  match x {
-    3 | 4       => (),
-    (1 | 2) | 3 => (),
-    1 | (2 | 3) => (),
-    _           => ()
-  }
-}
\ No newline at end of file
diff --git a/test/typecheck/pass/or_pattern/v1.expect b/test/typecheck/pass/or_pattern/v1.expect
deleted file mode 100644
index edf07f03..00000000
--- a/test/typecheck/pass/or_pattern/v1.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Type error at file "or_pattern/v1.sail", line 11, character 5 to line 11, character 5
-
-    y | z       => (),
-
-Bindings are not allowed in this context
diff --git a/test/typecheck/pass/or_pattern/v1.sail b/test/typecheck/pass/or_pattern/v1.sail
deleted file mode 100644
index 21bc87e8..00000000
--- a/test/typecheck/pass/or_pattern/v1.sail
+++ /dev/null
@@ -1,14 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-let x : int = 5
-
-val main : unit -> unit
-
-function main() = {
-  match x {
-    y | z       => (),
-    _           => ()
-  }
-}
\ No newline at end of file