From 1f8aafca4b8d57b4bd9fe29348c06894309d8841 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 10 Apr 2018 14:17:18 +0100
Subject: 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
---
 aarch64/no_vector/spec.sail | 4 ++--
 aarch64/prelude.sail        | 6 +-----
 2 files changed, 3 insertions(+), 7 deletions(-)

(limited to 'aarch64')

diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index d8a05777..ccf8aba1 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -6984,7 +6984,7 @@ function __TakeColdReset () = {
 val AArch64_TakeException : (bits(2), ExceptionRecord, bits(64), int) -> unit effect {escape, rreg, undef, wreg}
 
 function AArch64_TakeException (target_el, exception, preferred_exception_return, vect_offset__arg) = {
-  vect_offset = vect_offset__arg;
+  vect_offset : int = vect_offset__arg;
   SynchronizeContext();
   assert((HaveEL(target_el) & ~(ELUsingAArch32(target_el))) & UInt(target_el) >= UInt(PSTATE.EL), "((HaveEL(target_el) && !(ELUsingAArch32(target_el))) && (UInt(target_el) >= UInt((PSTATE).EL)))");
   from_32 : bool = UsingAArch32();
@@ -8507,7 +8507,7 @@ val aarch64_memory_vector_single_nowb : forall ('esize : Int) ('selem : Int).
 
 function aarch64_memory_vector_single_nowb (datasize, esize, index, m, memop, n, replicate, selem, t__arg, wback) = {
   assert(constraint('selem >= 1 & 'esize >= 0));
-  t = t__arg;
+  t : int = t__arg;
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
   offs : bits(64) = undefined;
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 902f448f..5cf4ce48 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -103,10 +103,6 @@ val not_vec = {
 
 overload ~ = {not_bool, not_vec}
 
-val neq_int = {lem: "neq"} : (int, int) -> bool
-
-function neq_int (x, y) = not_bool(eq_int(x, y))
-
 val neq_vec = {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
 
 function neq_vec (x, y) = not_bool(eq_vec(x, y))
@@ -115,7 +111,7 @@ val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool
 
 function neq_anything (x, y) = not_bool(x == y)
 
-overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
+overload operator != = {neq_vec, neq_anything}
 
 val builtin_and_vec = {ocaml: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-- 
cgit v1.2.3