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.

1 files changed, 3 insertions, 3 deletions

diff --git a/lib/smt.sail b/lib/smt.sail
index efcbe48c..c57f7bd1 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -9,7 +9,7 @@ val div = {
   lem: "integerDiv",
   c: "tdiv_int",
   coq: "div_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == div('n, 'm). atom('o)}
 
 overload operator / = {div}
 
@@ -19,7 +19,7 @@ val mod = {
   lem: "integerMod",
   c: "tmod_int",
   coq: "mod_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)}
 
 overload operator % = {mod}
 
@@ -29,7 +29,7 @@ val abs_atom = {
   lem: "abs_int",
   c: "abs_int",
   coq: "abs_with_eq"
-} : forall 'n. atom('n) -> {'o, 'o = abs_atom('n). atom('o)}
+} : forall 'n. atom('n) -> {'o, 'o == abs_atom('n). atom('o)}
 
 $ifdef TEST