Fix an issue where zeros function defined in sail conflicted with lem builtin (lem backend does not do z encoding) and add default get_config_print_xxx builtins mappings to lem build (now there is no longer a sail definition of the function because of -Oconstant_fold bug). Also remove FEATURE_IMPLICITS ifdef that was required for backwards compatibility with long obsolete sail versions.

1 files changed, 7 insertions, 24 deletions

diff --git a/model/prelude.sail b/model/prelude.sail
index 5ec0b92..63c896c 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -101,41 +101,24 @@ 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", 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
+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
 
-$ifndef FEATURE_IMPLICITS
-val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
-val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
-function EXTS v = sail_sign_extend(v, sizeof('m))
-function EXTZ v = sail_zero_extend(v, sizeof('m))
-
-val zeros_implicit : forall 'n, 'n >= 0 . unit -> bits('n)
-function zeros_implicit () = sail_zeros('n)
-overload zeros = {zeros_implicit, sail_zeros}
-
-val ones_implicit : forall 'n, 'n >= 0 . unit -> bits('n)
-function ones_implicit () = sail_ones ('n)
-
-overload ones = {ones_implicit, sail_ones}
-
-$else
 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)
 
 function EXTS(m, v) = sail_sign_extend(v, m)
 function EXTZ(m, v) = sail_zero_extend(v, m)
 
-val zeros : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
-function zeros (n) = sail_zeros(n)
+val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
+function zeros_implicit (n) = sail_zeros(n)
+overload zeros = {zeros_implicit}
 
 val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
 function ones (n) = sail_ones (n)
 
-$endif
-
 val cast bool_to_bits : bool -> bits(1)
 function bool_to_bits x = if x then 0b1 else 0b0