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 | 2 | ||||
| -rw-r--r-- | language/l2_parse.ml | 1 | ||||
| -rw-r--r-- | language/l2_parse.ott | 2 |
5 files changed, 7 insertions, 0 deletions
diff --git a/language/l2.lem b/language/l2.lem index fb8b7731..d82fbbc7 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -232,6 +232,7 @@ type exp_aux 'a = (* Expression *) | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *) + | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *) | E_list of list (exp 'a) (* list *) | E_cons of (exp 'a) * (exp 'a) (* cons *) | E_record of (fexps 'a) (* struct *) diff --git a/language/l2.ml b/language/l2.ml index 3ce5cac3..76b27874 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -246,6 +246,7 @@ type | E_vector_subrange of 'a exp * 'a exp * 'a exp (* subvector extraction *) | E_vector_update of 'a exp * 'a exp * 'a exp (* vector functional update *) | E_vector_update_subrange of 'a exp * 'a exp * 'a exp * 'a exp (* vector subrange update (with vector) *) + | E_vector_append of 'a exp * 'a exp (* vector concatenation *) | E_list of ('a exp) list (* list *) | E_cons of 'a exp * 'a exp (* cons *) | E_record of 'a fexps (* struct *) diff --git a/language/l2.ott b/language/l2.ott index a880527c..f0edda3f 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -583,6 +583,8 @@ exp :: 'E_' ::= {{ com vector subrange update (with vector)}} % do we want a functional update form with a comma-separated list of such? + | exp : exp2 :: :: vector_append + {{ com vector concatenation }} % lists | [|| exp1 , .. , expn ||] :: :: list diff --git a/language/l2_parse.ml b/language/l2_parse.ml index a283b605..c68c92b9 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -213,6 +213,7 @@ exp_aux = (* Expression *) | E_vector_subrange of exp * exp * exp (* subvector extraction *) | E_vector_update of exp * exp * exp (* vector functional update *) | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *) + | E_vector_append of exp * exp (* vector concatenation *) | E_list of (exp) list (* list *) | E_cons of exp * exp (* cons *) | E_record of fexps (* struct *) diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 11b51f2a..d3e13c13 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -474,6 +474,8 @@ exp :: 'E_' ::= {{ com vector subrange update (with vector)}} % do we want a functional update form with a comma-separated list of such? + | exp : exp2 :: :: vector_append + {{ com vector concatenation }} % lists | [|| exp1 , .. , expn ||] :: :: list |