diff options
| author | Kathy Gray | 2015-05-17 12:23:39 +0100 |
|---|---|---|
| committer | Kathy Gray | 2015-05-17 12:23:39 +0100 |
| commit | edaee3304bfff4e51b36e952b4250a8479c58da4 (patch) | |
| tree | 6d0dac71bc460839e8926c13d1bcec2188de0dcd /src | |
| parent | 81b0bcac17be23b605d840c907421f9c09ae73c0 (diff) | |
extend a missing case
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 1177216c..6396f51e 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -462,6 +462,7 @@ val access_vector : value -> nat -> value let access_vector v n = retaint v (match (detaint v) with | V_unknown -> V_unknown + | V_lit (L_aux L_undef _) -> v | V_vector m dir vs -> list_nth vs (if is_inc(dir) then (n - m) else (m - n)) | V_vector_sparse _ _ _ vs d -> @@ -631,10 +632,8 @@ let update_vector_start default_dir new_start expected_size v = | V_lit (L_aux L_one _) -> V_vector new_start default_dir [v] | V_vector m inc vs -> V_vector new_start inc vs (*Note, may need to shrink and check if still sparse *) | V_vector_sparse m n dir vals d -> V_vector_sparse new_start n dir vals d - | V_unknown -> - V_vector new_start default_dir (List.replicate expected_size V_unknown) - | V_lit (L_aux L_undef _) -> - V_vector new_start default_dir (List.replicate expected_size v) + | V_unknown -> V_vector new_start default_dir (List.replicate expected_size V_unknown) + | V_lit (L_aux L_undef _) -> V_vector new_start default_dir (List.replicate expected_size v) end) val in_ctors : list (id * typ) -> id -> maybe typ |