diff options
| author | Tim Hutt <timothy.hutt@codasip.com> | 2024-09-09 16:03:16 +0100 |
|---|---|---|
| committer | Tim Hutt <timothy.hutt@codasip.com> | 2024-09-09 16:03:16 +0100 |
| commit | ae1e75e82bfd0bdffffc00a3db705053b7860bd5 (patch) | |
| tree | ec1e62a763186c2c415e6abf62e5ff0da4133f5c | |
| parent | 0cab9e68ac24efce8a9ef4165319eb75b2ba38c0 (diff) | |
| download | sail-riscv-ae1e75e82bfd0bdffffc00a3db705053b7860bd5.zip sail-riscv-ae1e75e82bfd0bdffffc00a3db705053b7860bd5.tar.gz sail-riscv-ae1e75e82bfd0bdffffc00a3db705053b7860bd5.tar.bz2 | |
Change prints from impure to pure
From the Sail model's perspective the output is not observable so these are pure. Also the pure/impure is used for formal backends which don't actually print anything anyway.
| -rw-r--r-- | model/prelude.sail | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/model/prelude.sail b/model/prelude.sail index ea83700..4788a60 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -56,14 +56,14 @@ overload operator % = {emod_int} overload min = {min_int} overload max = {max_int} -val print_string = impure "print_string" : (string, string) -> unit +val print_string = pure "print_string" : (string, string) -> unit -val print_instr = impure {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_reg = impure {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_mem = impure {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_platform = impure {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_instr = pure {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_reg = pure {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_mem = pure {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_platform = pure {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_step = impure {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit +val print_step = pure {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit function print_step() = () |