diff options
| author | Kathy Gray | 2014-05-12 13:37:14 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-05-12 13:37:14 +0100 |
| commit | 314205cc12f9872b5c11ca76d4eb74a12d85cda7 (patch) | |
| tree | 4b3d0de31c28935dd196cef12584ed4e39361fe8 /src/lem_interp/Interp_interface.lem | |
| parent | 18bf3d43acc1d34219fa87ed579c2c7de809ae52 (diff) | |
More interface support
Diffstat (limited to 'src/lem_interp/Interp_interface.lem')
| -rw-r--r-- | src/lem_interp/Interp_interface.lem | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/src/lem_interp/Interp_interface.lem b/src/lem_interp/Interp_interface.lem index b58db89b..0767ea79 100644 --- a/src/lem_interp/Interp_interface.lem +++ b/src/lem_interp/Interp_interface.lem @@ -25,7 +25,7 @@ type outcome = | Done | Error of string -val build_context : Interp.defs -> context +val build_context : Interp.defs Interp.tannot -> context val initial_instruction_state : context -> string -> value -> instruction_state type interp_mode = <| eager_eval : bool |> @@ -33,3 +33,20 @@ val interp : instruction_state -> interp_mode -> outcome val interp_exhaustive : instruction_state -> list outcome (*not sure what event was ment to be*) +val intern_value : value -> Interp.value +val extern_value : Interp.value -> value + +let build_context defs = Interp.to_top_env defs + +let intern_value v = match v with + | Bitvector bs -> Interp.V_vector 0 true (List.map (fun | 0 -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown)) + | _ -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown))) bs) + | Unknown -> Interp.V_unknown + +let extern_value v = match v with + | Interp.V_vector _ true bits -> Bitvector (List.map (fun | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> 0 + | _ -> 1) bits) + | _ -> Unknown + +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 |