From 5471af45fd04169eb184371dcd8f791e507eab6f Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 24 Oct 2018 17:25:47 +0100 Subject: Add constraint synonyms Currently not enabled by default, the flag -Xconstraint_synonyms enables them For generating constraints in ASL parser, we want to be able to give names to the constraints that we attach to certain variables. It's slightly awkward right now when constraints get long complicated because the entire constraint always has to be typed out in full whenever it appears, and there's no way to abstract away from that. This adds constraint synonyms, which work much like type synonyms except for constraints, e.g. constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256 these constraints can then be used instead of the full constraint, e.g. val f : forall 'n, where Size('n). int('n) -> unit Unfortunatly we need to have a keyword to 'call' the constraint synonym otherwise the grammer stops being LR(1). This could be resolved by parsing all constraints into Parse_ast.atyp and then de-sugaring them into constraints, which is what happens for n-expressions already, but that would require quite a bit of work on the parser. To avoid this forcing changes to any other parts of Sail, the intended invariant is that all constraints appearing anywhere in a type-checked AST have no constraint synonyms, so they don't have to worry about matching on NC_app, or calling Env.expand_typquant_synonyms (which isn't even exported for this reason). --- test/typecheck/pass/constraint_sym.sail | 7 +++++++ test/typecheck/pass/constraint_sym/v1.expect | 5 +++++ test/typecheck/pass/constraint_sym/v1.sail | 7 +++++++ test/typecheck/pass/constraint_sym/v2.expect | 5 +++++ test/typecheck/pass/constraint_sym/v2.sail | 7 +++++++ test/typecheck/pass/constraint_sym/v3.expect | 5 +++++ test/typecheck/pass/constraint_sym/v3.sail | 7 +++++++ test/typecheck/pass/constraint_sym/v4.expect | 5 +++++ test/typecheck/pass/constraint_sym/v4.sail | 6 ++++++ test/typecheck/pass/global_type_var/v3.expect | 2 +- 10 files changed, 55 insertions(+), 1 deletion(-) create mode 100644 test/typecheck/pass/constraint_sym.sail create mode 100644 test/typecheck/pass/constraint_sym/v1.expect create mode 100644 test/typecheck/pass/constraint_sym/v1.sail create mode 100644 test/typecheck/pass/constraint_sym/v2.expect create mode 100644 test/typecheck/pass/constraint_sym/v2.sail create mode 100644 test/typecheck/pass/constraint_sym/v3.expect create mode 100644 test/typecheck/pass/constraint_sym/v3.sail create mode 100644 test/typecheck/pass/constraint_sym/v4.expect create mode 100644 test/typecheck/pass/constraint_sym/v4.sail (limited to 'test/typecheck') diff --git a/test/typecheck/pass/constraint_sym.sail b/test/typecheck/pass/constraint_sym.sail new file mode 100644 index 00000000..6d212e40 --- /dev/null +++ b/test/typecheck/pass/constraint_sym.sail @@ -0,0 +1,7 @@ +$option -Xconstraint_synonyms + +constraint Size('n) = 'n in {32, 64} + +constraint Nat('n) = 'n >= 0 + +val foo : forall 'n, where Size('n). int('n) -> unit diff --git a/test/typecheck/pass/constraint_sym/v1.expect b/test/typecheck/pass/constraint_sym/v1.expect new file mode 100644 index 00000000..71fd6f30 --- /dev/null +++ b/test/typecheck/pass/constraint_sym/v1.expect @@ -0,0 +1,5 @@ +Type error at file "constraint_sym/v1.sail", line 3, character 23 to line 3, character 24 + +constraint Size('n) = 'm in {32, 64} + +No type variable 'm diff --git a/test/typecheck/pass/constraint_sym/v1.sail b/test/typecheck/pass/constraint_sym/v1.sail new file mode 100644 index 00000000..4421ee77 --- /dev/null +++ b/test/typecheck/pass/constraint_sym/v1.sail @@ -0,0 +1,7 @@ +$option -Xconstraint_synonyms + +constraint Size('n) = 'm in {32, 64} + +constraint Nat('n) = 'n >= 0 + +val foo : forall 'n, where Size('n). int('n) -> unit diff --git a/test/typecheck/pass/constraint_sym/v2.expect b/test/typecheck/pass/constraint_sym/v2.expect new file mode 100644 index 00000000..58a0f416 --- /dev/null +++ b/test/typecheck/pass/constraint_sym/v2.expect @@ -0,0 +1,5 @@ +Type error at file "constraint_sym/v2.sail", line 7, character 22 to line 7, character 34 + +val foo : forall 'n, where Siz('n). int('n) -> unit + +Constraint synonym Siz is not defined diff --git a/test/typecheck/pass/constraint_sym/v2.sail b/test/typecheck/pass/constraint_sym/v2.sail new file mode 100644 index 00000000..1d98e3e4 --- /dev/null +++ b/test/typecheck/pass/constraint_sym/v2.sail @@ -0,0 +1,7 @@ +$option -Xconstraint_synonyms + +constraint Size('n) = 'n in {32, 64} + +constraint Nat('n) = 'n >= 0 + +val foo : forall 'n, where Siz('n). int('n) -> unit diff --git a/test/typecheck/pass/constraint_sym/v3.expect b/test/typecheck/pass/constraint_sym/v3.expect new file mode 100644 index 00000000..ab4526dc --- /dev/null +++ b/test/typecheck/pass/constraint_sym/v3.expect @@ -0,0 +1,5 @@ +Type error at file "constraint_sym/v3.sail", line 7, character 42 to line 7, character 43 + +val foo : forall ('n : Type), where Size('n). int('n) -> unit + +Constraint is badly formed, 'n has kind Type but should have kind Int diff --git a/test/typecheck/pass/constraint_sym/v3.sail b/test/typecheck/pass/constraint_sym/v3.sail new file mode 100644 index 00000000..886acbe4 --- /dev/null +++ b/test/typecheck/pass/constraint_sym/v3.sail @@ -0,0 +1,7 @@ +$option -Xconstraint_synonyms + +constraint Size('n) = 'n in {32, 64} + +constraint Nat('n) = 'n >= 0 + +val foo : forall ('n : Type), where Size('n). int('n) -> unit diff --git a/test/typecheck/pass/constraint_sym/v4.expect b/test/typecheck/pass/constraint_sym/v4.expect new file mode 100644 index 00000000..c8374baf --- /dev/null +++ b/test/typecheck/pass/constraint_sym/v4.expect @@ -0,0 +1,5 @@ +Type error at file "constraint_sym/v4.sail", line 2, character 12 to line 2, character 15 + +constraint Size('n) = 'n in {32, 64} + +Use -Xconstraint_synonyms to enable constraint synonyms diff --git a/test/typecheck/pass/constraint_sym/v4.sail b/test/typecheck/pass/constraint_sym/v4.sail new file mode 100644 index 00000000..96bf5e82 --- /dev/null +++ b/test/typecheck/pass/constraint_sym/v4.sail @@ -0,0 +1,6 @@ + +constraint Size('n) = 'n in {32, 64} + +constraint Nat('n) = 'n >= 0 + +val foo : forall 'n, where Size('n). int('n) -> unit diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect index 8014f88a..c7e06dc7 100644 --- a/test/typecheck/pass/global_type_var/v3.expect +++ b/test/typecheck/pass/global_type_var/v3.expect @@ -2,4 +2,4 @@ Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, ch val test : forall 'size. atom('size) -> unit -Kind identifier 'size is already bound +type variable 'size is already bound -- cgit v1.2.3