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.

14 files changed, 88 insertions, 78 deletions

diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index de8c3d11..ac3c199c 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -9,7 +9,7 @@
     "overload" "cast" "sizeof" "constraint" "default" "assert" "newtype" "from"
     "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to"
     "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield"
-    "mapping" "where"))
+    "mapping" "where" "with"))
 
 (defconst sail2-kinds
   '("Int" "Type" "Order" "inc" "dec"
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
 
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
diff --git a/src/initial_check.ml b/src/initial_check.ml
index f98b11d8..897f3ec2 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -251,6 +251,11 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
                   let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in
                   let exist_typ = to_ast_typ k_env def_ord atyp in
                   Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ)
+               | Parse_ast.ATyp_with (atyp, nc) ->
+                  let exist_typ = to_ast_typ k_env def_ord atyp in
+                  let kids = KidSet.elements (tyvars_of_typ exist_typ) in
+                  let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in
+                  Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ)
                | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None
               ), l)
 
diff --git a/src/lexer.mll b/src/lexer.mll
index 8b229772..de8eed7f 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -97,8 +97,7 @@ let operators = ref
   (List.fold_left
      (fun r (x, y) -> M.add x y r)
      M.empty
-     [ ("==", mk_operator Infix 4 "==");
-       ("/", mk_operator InfixL 7 "/");
+     [ ("/", mk_operator InfixL 7 "/");
        ("%", mk_operator InfixL 7 "%");
      ])
 
@@ -224,9 +223,7 @@ rule token = parse
   | ","                                 { Comma }
   | ".."                                { DotDot }
   | "."                                 { Dot }
-  | "==" as op
-    { try M.find op !operators
-      with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) }
+  | "=="                                { EqEq(r"==") }
   | "="                                 { (Eq(r"=")) }
   | ">"					{ (Gt(r">")) }
   | "-"					{ Minus }
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index d19e85ed..30f87bc3 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -156,6 +156,7 @@ atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders
  | ATyp_tup of (atyp) list (* Tuple type *)
  | ATyp_app of id * (atyp) list (* type constructor application *)
  | ATyp_exist of kid list * n_constraint * atyp
+ | ATyp_with of atyp * n_constraint
 
 and atyp = 
    ATyp_aux of atyp_aux * l
diff --git a/src/parser.mly b/src/parser.mly
index bd7c2f62..12286e13 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -197,6 +197,7 @@ let rec desugar_rchain chain s e =
 
 %token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit
 %token <string> Colon ColonColon (* CaretCaret *) TildeTilde ExclEq
+%token <string> EqEq
 %token <string> GtEq
 %token <string> LtEq
 
@@ -260,6 +261,7 @@ id:
   | Op Plus { mk_id (DeIid "+") $startpos $endpos }
   | Op Minus { mk_id (DeIid "-") $startpos $endpos }
   | Op Star { mk_id (DeIid "*") $startpos $endpos }
+  | Op EqEq { mk_id (DeIid "==") $startpos $endpos }
   | Op ExclEq { mk_id (DeIid "!=") $startpos $endpos }
   | Op Lt { mk_id (DeIid "<") $startpos $endpos }
   | Op Gt { mk_id (DeIid ">") $startpos $endpos }
@@ -337,9 +339,12 @@ atomic_nc:
     { mk_nc NC_true $startpos $endpos }
   | False
     { mk_nc NC_false $startpos $endpos }
-  | typ Eq typ
+  | typ0 Eq typ0
+    { Util.warn ("Deprecated syntax, use == instead at " ^ Reporting.loc_to_string (loc $startpos($2) $endpos($2)) ^ "\n");
+      mk_nc (NC_equal ($1, $3)) $startpos $endpos }
+  | typ0 EqEq typ0
     { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
-  | typ ExclEq typ
+  | typ0 ExclEq typ0
     { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
   | nc_lchain
     { desugar_lchain $1 $startpos $endpos }
@@ -350,6 +355,38 @@ atomic_nc:
   | kid In Lcurly num_list Rcurly
     { mk_nc (NC_set ($1, $4)) $startpos $endpos }
 
+new_nc:
+  | new_nc Bar new_nc_and
+    { mk_nc (NC_or ($1, $3)) $startpos $endpos }
+  | nc_and
+    { $1 }
+
+new_nc_and:
+  | new_nc_and Amp new_atomic_nc
+    { mk_nc (NC_and ($1, $3)) $startpos $endpos }
+  | new_atomic_nc
+    { $1 }
+
+new_atomic_nc:
+  | Where id Lparen typ_list Rparen
+    { mk_nc (NC_app ($2, $4)) $startpos $endpos }
+  | True
+    { mk_nc NC_true $startpos $endpos }
+  | False
+    { mk_nc NC_false $startpos $endpos }
+  | typ0 EqEq typ0
+    { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
+  | typ0 ExclEq typ0
+    { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
+  | nc_lchain
+    { desugar_lchain $1 $startpos $endpos }
+  | nc_rchain
+    { desugar_rchain $1 $startpos $endpos }
+  | Lparen new_nc Rparen
+    { $2 }
+  | kid In Lcurly num_list Rcurly
+    { mk_nc (NC_set ($1, $4)) $startpos $endpos }
+
 num_list:
   | Num
     { [$1] }
@@ -357,28 +394,30 @@ num_list:
     { $1 :: $3 }
 
 nc_lchain:
-  | typ LtEq typ
+  | typ0 LtEq typ0
     { [LC_nexp $1; LC_lteq; LC_nexp $3] }
-  | typ Lt typ
+  | typ0 Lt typ0
     { [LC_nexp $1; LC_lt; LC_nexp $3] }
-  | typ LtEq nc_lchain
+  | typ0 LtEq nc_lchain
     { LC_nexp $1 :: LC_lteq :: $3 }
-  | typ Lt nc_lchain
+  | typ0 Lt nc_lchain
     { LC_nexp $1 :: LC_lt :: $3 }
 
 nc_rchain:
-  | typ GtEq typ
+  | typ0 GtEq typ0
     { [RC_nexp $1; RC_gteq; RC_nexp $3] }
-  | typ Gt typ
+  | typ0 Gt typ0
     { [RC_nexp $1; RC_gt; RC_nexp $3] }
-  | typ GtEq nc_rchain
+  | typ0 GtEq nc_rchain
     { RC_nexp $1 :: RC_gteq :: $3 }
-  | typ Gt nc_rchain
+  | typ0 Gt nc_rchain
     { RC_nexp $1 :: RC_gt :: $3 }
 
 typ:
   | typ0
     { $1 }
+  | typ0 With new_nc
+    { mk_typ (ATyp_with ($1, $3)) $startpos $endpos }
 
 /* The following implements all nine levels of user-defined precedence for
 operators in types, with both left, right and non-associative operators */
@@ -677,8 +716,8 @@ pat_string_append:
 pat1:
   | atomic_pat
     { $1 }
-  | atomic_pat Bar pat1
-    { mk_pat (P_or ($1, $3)) $startpos $endpos }
+  (* | atomic_pat Bar pat1
+    { mk_pat (P_or ($1, $3)) $startpos $endpos } *)
   | atomic_pat At pat_concat
     { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
   | atomic_pat ColonColon pat1
@@ -890,6 +929,7 @@ exp4:
   | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp5 ExclEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "!=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 EqEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "==") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp5 { $1 }
@@ -1104,12 +1144,14 @@ funcl_patexp:
 funcl_patexp_typ:
   | pat Eq exp
     { (mk_pexp (Pat_exp ($1, $3)) $startpos $endpos, mk_tannotn) }
-  | pat MinusGt funcl_typ Eq exp
-    { (mk_pexp (Pat_exp ($1, $5)) $startpos $endpos, $3) }
+  | pat MinusGt typ Eq exp
+    { (mk_pexp (Pat_exp ($1, $5)) $startpos $endpos, mk_tannot mk_typqn $3 $startpos $endpos($3)) }
+  | Forall typquant Dot pat MinusGt typ Eq exp
+    { (mk_pexp (Pat_exp ($4, $8)) $startpos $endpos, mk_tannot $2 $6 $startpos $endpos($6)) }
   | Lparen pat If_ exp Rparen Eq exp
     { (mk_pexp (Pat_when ($2, $4, $7)) $startpos $endpos, mk_tannotn) }
-  | Lparen pat If_ exp Rparen MinusGt funcl_typ Eq exp
-    { (mk_pexp (Pat_when ($2, $4, $9)) $startpos $endpos, $7) }
+  | Forall typquant Dot Lparen pat If_ exp Rparen MinusGt typ Eq exp
+    { (mk_pexp (Pat_when ($5, $7, $12)) $startpos $endpos, mk_tannot $2 $10 $startpos $endpos($10)) }
 
 funcl:
   | id funcl_patexp
diff --git a/test/typecheck/pass/inline_typ.sail b/test/typecheck/pass/inline_typ.sail
index dd761b83..95be790c 100644
--- a/test/typecheck/pass/inline_typ.sail
+++ b/test/typecheck/pass/inline_typ.sail
@@ -1,2 +1,2 @@
 
-function test (x : atom('n), y : atom('m)) -> forall 'n 'm. atom('m + 'n) = undefined
\ No newline at end of file
+function test forall 'n 'm. (x : int('n), y : int('m)) -> int('m + 'n) = undefined
\ No newline at end of file
diff --git a/test/typecheck/pass/nat_set.sail b/test/typecheck/pass/nat_set.sail
index a12e81da..f171eb9b 100644
--- a/test/typecheck/pass/nat_set.sail
+++ b/test/typecheck/pass/nat_set.sail
@@ -1,4 +1,4 @@
-function test x : atom('n) -> forall 'n. bool = true
+function test forall 'n, 'n in {1, 3}. x : atom('n) -> bool = true
 
 let x = test(1)
 
diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail
index de4458ed..24e50259 100644
--- a/test/typecheck/pass/option_either.sail
+++ b/test/typecheck/pass/option_either.sail
@@ -2,11 +2,11 @@ default Order inc
 
 union option ('a : Type) = {None : unit, Some : 'a}
 
-function none () -> forall ('a : Type). option('a) = None()
+function none forall ('a : Type). () -> option('a) = None()
 
-function some x : 'a -> forall ('a : Type). option('a) = Some(x)
+function some forall ('a : Type). x : 'a -> option('a) = Some(x)
 
-function test x : option('a) -> forall ('a : Type). range(0, 1) = match x {
+function test forall ('a : Type). x : option('a) -> range(0, 1) = match x {
   None() => 0,
   Some(y) => 1
 }
diff --git a/test/typecheck/pass/or_pattern.sail b/test/typecheck/pass/or_pattern.sail
deleted file mode 100644
index a6e11ecd..00000000
--- a/test/typecheck/pass/or_pattern.sail
+++ /dev/null
@@ -1,16 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-let x : int = 5
-
-val main : unit -> unit
-
-function main() = {
-  match x {
-    3 | 4       => (),
-    (1 | 2) | 3 => (),
-    1 | (2 | 3) => (),
-    _           => ()
-  }
-}
\ No newline at end of file
diff --git a/test/typecheck/pass/or_pattern/v1.expect b/test/typecheck/pass/or_pattern/v1.expect
deleted file mode 100644
index edf07f03..00000000
--- a/test/typecheck/pass/or_pattern/v1.expect
+++ /dev/null
@@ -1,5 +0,0 @@
-Type error at file "or_pattern/v1.sail", line 11, character 5 to line 11, character 5
-
-    y | z       => (),
-
-Bindings are not allowed in this context
diff --git a/test/typecheck/pass/or_pattern/v1.sail b/test/typecheck/pass/or_pattern/v1.sail
deleted file mode 100644
index 21bc87e8..00000000
--- a/test/typecheck/pass/or_pattern/v1.sail
+++ /dev/null
@@ -1,14 +0,0 @@
-default Order dec
-
-$include <prelude.sail>
-
-let x : int = 5
-
-val main : unit -> unit
-
-function main() = {
-  match x {
-    y | z       => (),
-    _           => ()
-  }
-}
\ No newline at end of file