aboutsummaryrefslogtreecommitdiff
path: root/model/prelude.sail
diff options
context:
space:
mode:
authorPrashanth Mundkur <prashanth.mundkur@gmail.com>2019-07-11 11:33:24 -0700
committerPrashanth Mundkur <prashanth.mundkur@gmail.com>2019-07-11 11:33:24 -0700
commite2c413be2bbbb6745978bb4437d23279262ddeeb (patch)
treeff7d136948f295cdae0517fd770518ddeceeb0f8 /model/prelude.sail
parentc01474489b68fc9e6aa4a96295db03df3dcc99a6 (diff)
downloadsail-riscv-e2c413be2bbbb6745978bb4437d23279262ddeeb.zip
sail-riscv-e2c413be2bbbb6745978bb4437d23279262ddeeb.tar.gz
sail-riscv-e2c413be2bbbb6745978bb4437d23279262ddeeb.tar.bz2
Undo get_config workarounds.
Diffstat (limited to 'model/prelude.sail')
-rw-r--r--model/prelude.sail14
1 files changed, 10 insertions, 4 deletions
diff --git a/model/prelude.sail b/model/prelude.sail
index 63c896c..c67ec3c 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -101,10 +101,16 @@ val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline",
val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
-val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", _:"get_config_print_instr"} : unit -> bool
-val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", _:"get_config_print_reg"} : unit -> bool
-val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", _:"get_config_print_mem"} : unit -> bool
-val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", _:"get_config_print_platform"} : unit -> bool
+val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool
+val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool
+val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool
+
+val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool
+// defaults for other backends
+function get_config_print_instr () = false
+function get_config_print_reg () = false
+function get_config_print_mem () = false
+function get_config_print_platform () = false
val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)