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.

2 files changed, 13 insertions, 13 deletions

diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 2bcc9797..434f79d5 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -4,11 +4,11 @@
  * to MMIO regions can be dispatched.
  */
 
-function is_aligned_addr (addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool =
   unsigned(addr) % width == 0
 
 // only used for actual memory regions, to avoid MMIO effects
-function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n, 'n >= 0. MemoryOpResult(bits(8 * 'n)) =
+function phys_mem_read forall 'n, 'n >= 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) =
   match (t, __RISCV_read(addr, width, aq, rl, res)) {
     (Instruction, None()) => MemException(E_Fetch_Access_Fault),
     (Data, None())        => MemException(E_Load_Access_Fault),
@@ -16,7 +16,7 @@ function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : boo
                                MemValue(v) }
   }
 
-function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) =
+function checked_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
   /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */
   if   t == Data & within_mmio_readable(addr, width)
   then mmio_read(addr, width)
@@ -89,13 +89,13 @@ function mem_write_ea (addr, width, aq, rl, con) = {
 }
 
 // only used for actual memory regions, to avoid MMIO effects
-function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(bool) = {
+function phys_mem_write forall 'n. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = {
   print("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
   MemValue(__RISCV_write(addr, width, data))
 }
 
 // dispatches to MMIO regions or physical memory regions depending on physical memory map
-function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(bool) =
+function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
   if   within_mmio_writable(addr, width)
   then mmio_write(addr, width, data)
   else if within_phys_mem(addr, width)
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 3020d23d..25b09bcd 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -47,7 +47,7 @@ function phys_mem_segments() =
 
 /* Physical memory map predicates */
 
-function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool = {
+function within_phys_mem forall 'n. (addr : xlenbits, width : atom('n)) -> bool = {
   let ram_base = plat_ram_base ();
   let rom_base = plat_rom_base ();
   let ram_size = plat_ram_size ();
@@ -70,14 +70,14 @@ function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
   }
 }
 
-function within_clint(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+function within_clint forall 'n. (addr : xlenbits, width : atom('n)) -> bool =
     plat_clint_base() <=_u addr
   & (addr + sizeof('n)) <=_u (plat_clint_base() + plat_clint_size())
 
-function within_htif_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+function within_htif_writable forall 'n. (addr : xlenbits, width : atom('n)) -> bool =
     plat_htif_tohost() == addr
 
-function within_htif_readable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+function within_htif_readable forall 'n. (addr : xlenbits, width : atom('n)) -> bool =
     plat_htif_tohost() == addr
 
 /* CLINT (Core Local Interruptor), based on Spike. */
@@ -238,20 +238,20 @@ function htif_tick() = {
 
 /* Top-level MMIO dispatch */
 
-function within_mmio_readable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+function within_mmio_readable forall 'n. (addr : xlenbits, width : atom('n)) -> bool =
   within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n)
 
-function within_mmio_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+function within_mmio_writable forall 'n. (addr : xlenbits, width : atom('n)) -> bool =
   within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8)
 
-function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) =
+function mmio_read forall 'n, 'n > 0. (addr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) =
   if   within_clint(addr, width)
   then clint_load(addr, width)
   else if within_htif_readable(addr, width) & (1 <= 'n)
   then htif_load(addr, width)
   else MemException(E_Load_Access_Fault)
 
-function mmio_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(bool) =
+function mmio_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
   if   within_clint(addr, width)
   then clint_store(addr, width, data)
   else if within_htif_writable(addr, width) & 'n <= 8