Porting some minisail changes to sail2 branch

This commit primarily changes how existential types are bound in
letbindings. Essentially, the constraints on both numeric and
existentially quantified types are lifted into the surrounding type
context automatically, so in

```
val f : nat -> nat

let x = f(3)
```

whereas x would have had type nat by default before, it'll now have
type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh
type variable). This has several advantages: x can be passed to
functions expecting an atom argument, such as a vector indexing
operation without any clunky cast functions - ex_int, ex_nat, and
ex_range are no longer required. The let 'x = something() syntax is
also less needed, and is now only really required when we specifically
want a name to refer to x's type. This changes slightly the nature of
the type pattern syntax---whereas previously it was used to cause an
existential to be destructured, it now just provides names for an
automatically destructured binding. Usually however, this just works
the same.

Also:

- Fixed an issue where the rewrite_split_fun_constr_pats rewriting
  pass didn't add type paramemters for newly added type variables in
  generated function parameters.

- Updated string_of_ functions in ast_util to reflect syntax changes

- Fixed a C compilation issue where elements of union type
  constructors were not being coerced between big integers and 64-bit
  integers where appropriate

- Type annotations in patterns now generalise, rather than restrict
  the type of the pattern. This should be safer and easier to handle
  in the various backends. I don't think any code we had was relying
  on this behaviour anyway.

- Add inequality operator to lib/flow.sail

- Fix an issue whereby top-level let bindings with annotations were
  checked incorrectly

1 files changed, 10 insertions, 0 deletions

diff --git a/lib/flow.sail b/lib/flow.sail
index f1f24492..ad5f8760 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -29,12 +29,22 @@ val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm 'o 'p. (
 val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : (int, int) -> bool
 val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool"} : (bool, bool) -> bool
 
+val neq_range = {lem: "neq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
+function neq_range (x, y) = not_bool(neq_range(x, y))
+
+val neq_int = {lem: "neq"} : (int, int) -> bool
+function neq_int (x, y) = not_bool(eq_int(x, y))
+
+val neq_bool : (bool, bool) -> bool
+function neq_bool (x, y) = not_bool(eq_bool(x, y))
+
 val lteq_int = "lteq" : (int, int) -> bool
 val gteq_int = "gteq" : (int, int) -> bool
 val lt_int = "lt" : (int, int) -> bool
 val gt_int = "gt" : (int, int) -> bool
 
 overload operator == = {eq_atom, eq_range, eq_int, eq_bool}
+overload operator != = {neq_atom, neq_range, neq_int, neq_bool}
 overload operator | = {or_bool}
 overload operator & = {and_bool}