diff options
| author | Thomas Bauereiss | 2018-02-07 14:11:42 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-02-07 16:09:24 +0000 |
| commit | b7c7675e78738f356716ba27d212225e60d5a856 (patch) | |
| tree | 70bdca0d9b8acd4097768cfcec8dcc69a22c0a5d /riscv | |
| parent | e7471c23826487457e87099664e2b19aa699c94e (diff) | |
Add some printing functions to Lem shallow embedding
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 4 | ||||
| -rw-r--r-- | riscv/riscv_extras_embed_sequential.lem | 3 |
2 files changed, 5 insertions, 2 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index a0d3d3a1..89221596 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -151,13 +151,13 @@ val putchar = "putchar" : forall ('a : Type). 'a -> unit val concat_str = {ocaml: "concat_str", lem: "stringAppend"} : (string, string) -> string -val string_of_int = "string_of_int" : int -> string +val string_of_int = {ocaml: "string_of_int", lem: "stringFromInteger"} : int -> string val DecStr : int -> string val HexStr : int -> string -val BitStr = "string_of_bits" : forall 'n. bits('n) -> string +val BitStr = {ocaml: "string_of_bits", lem: "string_of_vec"} : forall 'n. bits('n) -> string val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) diff --git a/riscv/riscv_extras_embed_sequential.lem b/riscv/riscv_extras_embed_sequential.lem index 4ef3ed36..cc2a5277 100644 --- a/riscv/riscv_extras_embed_sequential.lem +++ b/riscv/riscv_extras_embed_sequential.lem @@ -65,6 +65,9 @@ val prerr_endline : string -> unit let prerr_endline _ = () declare ocaml target_rep function prerr_endline = `prerr_endline` +val print_string : string -> string -> unit +let print_string msg s = prerr_endline (msg ^ s) + val print_int : string -> integer -> unit let print_int msg i = prerr_endline (msg ^ (stringFromInteger i)) |