Skip to content

Commit

Permalink
Change prints from impure to pure
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Timmmm committed Sep 9, 2024
1 parent 0cab9e6 commit ae1e75e
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions model/prelude.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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() = ()

Expand Down

0 comments on commit ae1e75e

Please sign in to comment.