diff options
| author | Alasdair Armstrong | 2018-10-24 17:25:47 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-10-24 18:00:19 +0100 |
| commit | 5471af45fd04169eb184371dcd8f791e507eab6f (patch) | |
| tree | eb87790c74b3ac6076f4ef4f567055a3836ac962 /src/parse_ast.ml | |
| parent | e489f2d37efa4c320004d35c3025c77e0a0c60d0 (diff) | |
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).
Diffstat (limited to 'src/parse_ast.ml')
| -rw-r--r-- | src/parse_ast.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/parse_ast.ml b/src/parse_ast.ml index a4052d82..3317c196 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -176,6 +176,7 @@ n_constraint_aux = (* constraint over kind $_$ *) | NC_set of kid * (Big_int.num) list | NC_or of n_constraint * n_constraint | NC_and of n_constraint * n_constraint + | NC_app of id * atyp list | NC_true | NC_false @@ -566,6 +567,7 @@ def = (* Top-level definition *) | DEF_scattered of scattered_def (* scattered definition *) | DEF_reg_dec of dec_spec (* register declaration *) | DEF_pragma of string * string * l + | DEF_constraint of id * kid list * n_constraint | DEF_internal_mutrec of fundef list |