From 61e6bc97a7d5efb58f9b91738f1dd64404091137 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 7 Nov 2018 18:40:57 +0000 Subject: 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. --- test/typecheck/pass/inline_typ.sail | 2 +- test/typecheck/pass/nat_set.sail | 2 +- test/typecheck/pass/option_either.sail | 6 +++--- test/typecheck/pass/or_pattern.sail | 16 ---------------- test/typecheck/pass/or_pattern/v1.expect | 5 ----- test/typecheck/pass/or_pattern/v1.sail | 14 -------------- 6 files changed, 5 insertions(+), 40 deletions(-) delete mode 100644 test/typecheck/pass/or_pattern.sail delete mode 100644 test/typecheck/pass/or_pattern/v1.expect delete mode 100644 test/typecheck/pass/or_pattern/v1.sail (limited to 'test/typecheck') 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 - -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 - -let x : int = 5 - -val main : unit -> unit - -function main() = { - match x { - y | z => (), - _ => () - } -} \ No newline at end of file -- cgit v1.2.3