diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/mips_extras.lem | 4 | ||||
| -rw-r--r-- | mips/prelude.sail | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem index bed8cd39..d4c79d7a 100644 --- a/mips/mips_extras.lem +++ b/mips/mips_extras.lem @@ -91,8 +91,8 @@ val putchar : integer -> unit let putchar _ = () declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i))) -let sign_extend bits len = maybe_failwith (of_bits (exts_bv len bits)) -let zero_extend bits len = maybe_failwith (of_bits (extz_bv len bits)) +let _sign_extend bits len = maybe_failwith (of_bits (exts_bv len bits)) +let _zero_extend bits len = maybe_failwith (of_bits (extz_bv len bits)) let shift_bits_left v n = let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftl_bv v n)) in diff --git a/mips/prelude.sail b/mips/prelude.sail index 63fed9c4..05e4cfe0 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -311,8 +311,8 @@ union exception = { Error_internal_error : unit } -val _sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) -val _zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val _sign_extend = {ocaml: "sign_extend", lem: "_sign_extend"} : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val _zero_extend = {ocaml: "zero_extend", lem: "_zero_extend"} : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) val sign_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) val zero_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) |