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).
---
 src/initial_check.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/initial_check.ml')

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4e6e941d..36513ba1 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -370,6 +370,9 @@ and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint)
                 NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
              | Parse_ast.NC_and (nc1, nc2) ->
                 NC_and (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
+             | Parse_ast.NC_app (id, typs) ->
+                let nexps = List.map (to_ast_nexp k_env) typs in
+                NC_app (to_ast_id id, nexps)
              | Parse_ast.NC_true -> NC_true
              | Parse_ast.NC_false -> NC_false
     ), l)
@@ -907,6 +910,11 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
   | Parse_ast.DEF_reg_dec(dec) ->
      let d = to_ast_dec envs dec in
      ((Finished(DEF_reg_dec(d))),envs),partial_defs
+  | Parse_ast.DEF_constraint (id, kids, nc) ->
+     let id = to_ast_id id in
+     let kids = List.map to_ast_var kids in
+     let nc = to_ast_nexp_constraint k_env nc in
+     ((Finished (DEF_constraint (id, kids, nc))), envs), partial_defs
   | Parse_ast.DEF_pragma (_, _, l) ->
      typ_error l "Encountered preprocessor directive in initial check" None None None
   | Parse_ast.DEF_internal_mutrec _ ->
-- 
cgit v1.2.3