diff options
| author | Alastair Reid | 2018-07-25 18:42:26 +0100 |
|---|---|---|
| committer | Alastair Reid | 2018-07-26 13:14:33 +0100 |
| commit | 92373cfb9dd6a9a3d450a315d462378b7de20a71 (patch) | |
| tree | 33e2c2f257d5d18e0e4371912176e05c805b4c70 /src/rewriter.mli | |
| parent | 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414 (diff) | |
Patterns: add or and not patterns
These match the new ASL pattern constructors:
- !p matches if the pattern p does not match
- { p1, ... pn } matches if any of the patterns p1 ... pn match
We desugar the set pattern "{p1, ... pn}" into "p1 | (p2 | ... pn)".
ASL does not have pattern binding but Sail does. The rules at the
moment are that none of the pattern can contain patterns. This could
be relaxed by allowing "p1 | p2" to bind variables provided p1 and p2
both bind the same variables.
Diffstat (limited to 'src/rewriter.mli')
| -rw-r--r-- | src/rewriter.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/rewriter.mli b/src/rewriter.mli index eed22376..3e582071 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -84,6 +84,8 @@ val rewrite_fun : tannot rewriters -> tannot fundef -> tannot fundef type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = { p_lit : lit -> 'pat_aux ; p_wild : 'pat_aux + ; p_or : 'pat * 'pat -> 'pat_aux + ; p_not : 'pat -> 'pat_aux ; p_as : 'pat * id -> 'pat_aux ; p_typ : Ast.typ * 'pat -> 'pat_aux ; p_id : id -> 'pat_aux |