diff options
| author | Alasdair Armstrong | 2018-12-04 14:53:23 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-04 14:53:23 +0000 |
| commit | df3ea2e6da387ead7cba1e27632768e563696502 (patch) | |
| tree | 1643e82c6191e4a252d747daca8e3be269cb8a43 /language | |
| parent | 945c8b10a9498d0606f4226bc18d03ef806184f2 (diff) | |
Remove FES_Fexps constructor
This makes dealing with records and field expressions in Sail much
nicer because the constructors are no longer stacked together like
matryoshka dolls with unnecessary layers. Previously to get the fields
of a record it would be either
E_aux (E_record (FES_aux (FES_Fexps (fexps, _), _)), _)
but now it is simply:
E_aux (E_record fexps, _)
Diffstat (limited to 'language')
| -rw-r--r-- | language/sail.ott | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/language/sail.ott b/language/sail.ott index 4ce08415..168998ad 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -683,11 +683,11 @@ exp :: 'E_' ::= % TODO - | { fexps } :: :: record + | { fexp0 , ... , fexpn } :: :: record {{ com struct }} - | { exp with fexps } :: :: record_update + | { exp with fexp0 , ... , fexpn } :: :: record_update {{ com functional update of struct }} - | exp . id :: :: field + | exp . id :: :: field {{ com field projection from struct }} %Expressions for creating and accessing vectors @@ -754,11 +754,6 @@ fexp :: 'FE_' ::= {{ aux _ annot }} {{ auxparam 'a }} | id = exp :: :: Fexp -fexps :: 'FES_' ::= - {{ com field expression list }} - {{ aux _ annot }} {{ auxparam 'a }} - | fexp1 ; ... ; fexpn semi_opt :: :: Fexps - opt_default :: 'Def_val_' ::= {{ com optional default value for indexed vector expressions }} %, to define a default value for any unspecified positions in a sparse map {{ aux _ annot }} {{ auxparam 'a }} |