diff options
| author | Jon French | 2018-05-10 15:46:15 +0100 |
|---|---|---|
| committer | Jon French | 2018-05-10 15:46:15 +0100 |
| commit | 99a22fbf21a2a6cf0a556daf9f781b91c513e5b7 (patch) | |
| tree | df8079388daa6a7f7d5f9c7027698da343ffc708 /src | |
| parent | 6e8be09fbb93ec22d5f5088dae351c24904dec03 (diff) | |
Type_check: special case appending an empty vector
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 268183fe..58bd0d17 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -3272,6 +3272,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_vector_access (v, n) -> infer_exp env (E_aux (E_app (mk_id "vector_access", [v; n]), (l, ()))) | E_vector_update (v, n, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update", [v; n; exp]), (l, ()))) | E_vector_update_subrange (v, n, m, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update_subrange", [v; n; m; exp]), (l, ()))) + | E_vector_append (v1, E_aux (E_vector [], _)) -> infer_exp env v1 | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "append", [v1; v2]), (l, ()))) | E_vector_subrange (v, n, m) -> infer_exp env (E_aux (E_app (mk_id "vector_subrange", [v; n; m]), (l, ()))) | E_vector [] -> typ_error l "Cannot infer type of empty vector" |