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, 19 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 75668417..06ee1f65 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1092,13 +1092,14 @@ let generate_initialize_registers vs_ids (Defs defs) =
 let generate_enum_functions vs_ids (Defs defs) =
   let rec gen_enums = function
     | DEF_type (TD_aux (TD_enum (id, _, elems, _), _)) as enum :: defs ->
-       let enum_val_spec name typ =
-         mk_val_spec (VS_val_spec (mk_typschm (mk_typquant []) typ, name, (fun _ -> None), !opt_enum_casts))
+       let enum_val_spec name quants typ =
+         mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts))
        in
-       let enum_range = range_typ (nint 0) (nint (List.length elems - 1)) in
+       let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) in
 
        (* Create a function that converts a number to an enum. *)
        let to_enum =
+         let kid = mk_kid "e" in
          let name = append_id id "_of_num" in
          let pexp n id =
            let pat =
@@ -1117,12 +1118,16 @@ let generate_enum_functions vs_ids (Defs defs) =
          let range = range_typ (nint 0) (nint (List.length elems - 1)) in
          if IdSet.mem name vs_ids then []
          else
-           [ enum_val_spec name (function_typ enum_range (mk_typ (Typ_id id)) no_effect);
+           [ enum_val_spec name
+              [mk_qi_id BK_nat kid; mk_qi_nc (range_constraint kid)]
+              (function_typ (atom_typ (nvar kid)) (mk_typ (Typ_id id)) no_effect);
              mk_fundef [funcl] ]
        in
 
        (* Create a function that converts from an enum to a number. *)
        let from_enum =
+         let kid = mk_kid "e" in
+         let to_typ = mk_typ (Typ_exist ([kid], range_constraint kid, atom_typ (nvar kid))) in
          let name = prepend_id "num_of_" id in
          let pexp n id = mk_pexp (Pat_exp (mk_pat (P_id id), mk_lit_exp (L_num (Big_int.of_int n)))) in
          let funcl =
@@ -1132,22 +1137,8 @@ let generate_enum_functions vs_ids (Defs defs) =
          in
          if IdSet.mem name vs_ids then []
          else
-           [ enum_val_spec name (function_typ (mk_typ (Typ_id id)) enum_range no_effect);
+           [ enum_val_spec name [] (function_typ (mk_typ (Typ_id id)) to_typ no_effect);
              mk_fundef [funcl] ]
-         (* This is the simple way to generate this function, but the
-            rewriter and backends are all kinds of broken for function clause
-            patterns.
-         let name = prepend_id "num_of_" id in
-         let funcl n id =
-           mk_funcl name
-             (mk_pat (P_id id))
-             (mk_lit_exp (L_num (Big_int.of_int n)))
-         in
-         if IdSet.mem name vs_ids then []
-         else
-           [ enum_val_spec name (function_typ (mk_typ (Typ_id id)) enum_range no_effect);
-             mk_fundef (List.mapi funcl elems) ]
-          *)
        in
        enum :: to_enum @ from_enum @ gen_enums defs