diff options
| author | Robert Norton | 2017-06-22 15:53:30 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-06-22 15:53:30 +0100 |
| commit | 60cf08670218f114539118d9e189509bb5f18695 (patch) | |
| tree | 356913cb36b899727b488588e027b1065c2f9f91 | |
| parent | ccbd64bf8f4223e1934d9f6d73e172c986e5563d (diff) | |
add a 'print' built-in function handy for writing sail tests.
| -rw-r--r-- | src/gen_lib/sail_values.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 6 | ||||
| -rw-r--r-- | src/type_internal.ml | 1 |
3 files changed, 9 insertions, 0 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index e2ddd3e9..cc1979a1 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -24,6 +24,8 @@ type value = exception Sail_exit exception Sail_return +let _print s = print_string s + let string_of_bit = function | Vone -> "1" | Vzero -> "0" diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 36a31f3f..fe87c9e1 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -54,6 +54,11 @@ open import Bool type signed = Unsigned | Signed +val debug_print : string -> unit +declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s + +let print s = let _ = debug_print (string_of_value s) in V_lit(L_aux L_unit Unknown) + let hardware_mod (a: integer) (b:integer) : integer = if a < 0 && b < 0 then (abs a) mod (abs b) @@ -1012,6 +1017,7 @@ let library_functions direction = [ ("quot_overflow_vec", arith_op_overflow_vec_no0 hardware_quot "quot" Unsigned 1); ("quot_vec_signed", arith_op_vec_no0 hardware_quot "quot" Signed 1); ("quot_overflow_vec_signed", arith_op_overflow_vec_no0 hardware_quot "quot" Signed 1); + ("print", print); ("power", arith_op power); ("eq", eq); ("eq_vec", eq_vec); diff --git a/src/type_internal.ml b/src/type_internal.ml index 2932cf33..30e86f8a 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -2769,6 +2769,7 @@ let initial_typ_env_list : (string * ((string * tannot) list)) list = (External None),[],pure_e,pure_e,nob)); ("to_vec_dec",Base(([("a",{k=K_Typ})],{t=Tfn(nat_typ,{t=Tvar "a"},IP_none,pure_e)}), (External None),[],pure_e,pure_e,nob)); + ("print",Base(([],(mk_pure_fun string_t unit_t)),(External None),[],pure_e,pure_e,nob)); (* XXX not actually pure... *) ]; |