diff options
| author | Kathy Gray | 2014-03-31 19:15:17 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-03-31 19:17:06 +0100 |
| commit | be24c3bebe32b41847338f2dc31c06b593ec1251 (patch) | |
| tree | 2c4912377f61a60f499f332bd530e5f397eccd10 /src/lem_interp | |
| parent | a4a5c1248c7a467ea9d1f8dfa77bc187803ae374 (diff) | |
Extend constraint checking, and add casts for base of a vector shifts (i.e. from 0 to 32 etc, doesn't change order yet.).
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp.lem | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 8a9ebfe5..50d84556 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -621,7 +621,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) = | E_lit lit -> if is_lit_vector lit then (Value (litV_to_vec lit) Tag_empty,l_mem,l_env) else (Value (V_lit lit) Tag_empty, l_mem,l_env) - | E_cast typ exp -> + | E_cast ((Typ_aux typ _) as ctyp) exp -> resolve_outcome (interp_main t_level l_env l_mem exp) (fun v lm le -> match (tag,v) with @@ -629,8 +629,15 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) = (Action (Read_reg regform Nothing) (Frame (id_of_string "0") (E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) le lm Top), lm,le) + | (_,V_vector start inc items) -> + (match typ with + | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] -> + if start = i + then (Value v tag,lm,le) + else (Value (V_vector i inc items) tag,lm,le) + | _ -> (Value v tag,lm,le) end) | _ -> (Value v Tag_empty,lm,le) end) - (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_cast typ e) (l,annot))))) + (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_cast ctyp e) (l,annot))))) (* TODO introduce coercions to change offset of vectors *) | E_id id -> let name = get_id id in |