summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKathy Gray2014-05-20 15:00:35 +0100
committerKathy Gray2014-05-20 15:00:35 +0100
commit8cd3f794d59170d519f5000cc13f6a3c9cde849c (patch)
tree326f33ab210505caa16e8ed3eac8feb9b8932e48
parentf293cedf36c3fc256015fa8811ff7ce72e0be3a9 (diff)
Fix interp compiling bug
-rw-r--r--src/lem_interp/interp.lem8
-rw-r--r--src/lem_interp/interp_inter_imp.lem15
2 files changed, 14 insertions, 9 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 84bf6960..efd2f866 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -427,9 +427,9 @@ let rec to_exp v =
if (inc && n=0)
then E_vector (List.map to_exp vals)
else if inc then
- E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
+ E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals))) (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))
else
- E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals))
+ E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals)) (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))
| V_record t ivals ->
E_record(FES_aux (FES_Fexps
(List.map (fun (id,value) -> (FE_aux (FE_Fexp id (to_exp value)) (Unknown,Nothing))) ivals) false)
@@ -964,12 +964,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
| E_vector(exps) ->
exp_list mode t_level (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
- | E_vector_indexed(iexps) ->
+ | E_vector_indexed iexps default ->
let (indexes,exps) = List.unzip iexps in
let is_inc = match typ with
| T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
| _ -> false end in
- exp_list mode t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)) (l,annot)))
+ exp_list mode t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es) default) (l,annot)))
(fun vals -> V_vector (List_extra.head indexes) is_inc vals) l_env l_mem [] exps
| E_block(exps) -> interp_block mode t_level l_env l_env l_mem exps
| E_app f args ->
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 028b5def..59acb04a 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -6,17 +6,21 @@ import Num
val intern_value : value -> Interp.value
val extern_value : Interp.value -> value
+val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name
let build_context defs = Interp.to_top_env defs
-let to_bits l = (List.map (fun | false -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown))
- | true -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown))) l)
-let from_bits l = (List.map (fun | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> false
- | _ -> true) l)
+let to_bits l = (List.map (fun b -> match b with
+ | false -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown))
+ | true -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown)) end) l)
+let from_bits l = (List.map (fun b -> match b with
+ | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> false
+ | _ -> true end) l)
let rec to_bytes l = match l with
| [] -> []
| (a::b::c::d::e::f::g::h::rest) ->
(integerFromBoolList [a;b;c;d;e;f;g;h])::(to_bytes rest)
+end
let intern_value v = match v with
| Bitvector bs -> Interp.V_vector 0 true (to_bits bs)
@@ -36,6 +40,7 @@ let extern_reg r slice = match (r,slice) with
| (Interp.Reg(Id_aux (Id x,_)),Nothing) -> Reg x
| (Interp.Reg(Id_aux (Id x,_)),Just(i1,i2)) -> Reg_slice x (i1,i2)
| (Interp.SubReg (Id_aux (Id x,_)) (Interp.Reg(Id_aux (Id y,_))) (Interp_ast.BF_aux(Interp_ast.BF_single i) _),Nothing) -> Reg_field x y (i,i)
+end
let initial_instruction_state top_level main arg =
Interp.Frame Nothing (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [ intern_value arg ]) (Interp_ast.Unknown, Nothing)) top_level [] Interp.emem
@@ -53,6 +58,6 @@ let interp mode i_state =
-> Read_mem Interp.Read_plain (extern_value value) (fun v -> Interp.add_answer_to_stack (intern_value v) next_state)
| Interp.Write_mem (Id_aux (id i) _) loc_val slice write_val ->
Write_mem Interp.Write_plain (extern_value loc_val) (extern_value write_val) next_state
- | Interp.Call_extern id value -> (*Connect here to a list of external functions*)
+ | Interp.Call_extern id value -> (*Connect here to a list of external functions*) foo
end
end