diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 1 | ||||
| -rw-r--r-- | language/l2.ml | 1 | ||||
| -rw-r--r-- | language/l2.ott | 3 |
3 files changed, 4 insertions, 1 deletions
diff --git a/language/l2.lem b/language/l2.lem index 51831898..20d5c7b7 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -188,6 +188,7 @@ and exp = (* Expression *) and lexp = (* lvalue expression *) | LEXP_id of id (* identifier *) + | LEXP_memory of id * exp (* memory write via function call *) | LEXP_vector of lexp * exp (* vector element *) | LEXP_vector_range of lexp * exp * exp (* subvector *) | LEXP_field of lexp * id (* struct field *) diff --git a/language/l2.ml b/language/l2.ml index bf5ecf31..786d04ab 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -248,6 +248,7 @@ and 'a exp = and 'a lexp_aux = (* lvalue expression *) LEXP_id of id (* identifier *) + | LEXP_memory of id * 'a exp (* memory write via function call *) | LEXP_vector of 'a lexp * 'a exp (* vector element *) | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *) | LEXP_field of 'a lexp * id (* struct field *) diff --git a/language/l2.ott b/language/l2.ott index 198e6e7a..3b1e95b7 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -820,8 +820,9 @@ fundef :: 'FD_' ::= letbind :: 'LB_' ::= {{ com Let binding }} {{ aux _ annot }} {{ auxparam 'a }} - | typschm pat = exp :: :: val_explicit + | let typschm pat = exp :: :: val_explicit {{ com value binding, explicit type ([[pat]] must be total)}} +% at the moment, we cannot parse the following, so perhaps we shouldn't keep this form here | let pat = exp :: :: val_implicit {{ com value binding, implicit type ([[pat]] must be total)}} |