diff options
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/aarch64_extras.lem | 2 | ||||
| -rwxr-xr-x | aarch64/prelude.sail | 12 |
2 files changed, 4 insertions, 10 deletions
diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem index d22ece00..b662e230 100644 --- a/aarch64/aarch64_extras.lem +++ b/aarch64/aarch64_extras.lem @@ -78,7 +78,7 @@ val write_ram : forall 'rv 'e. integer -> integer -> list bitU -> list bitU -> list bitU -> monad 'rv unit 'e let write_ram addrsize size hexRAM address value = write_mem_ea Write_plain address size >> - write_mem_val value >>= fun _ -> + write_mem Write_plain address size value >>= fun _ -> return () val read_ram : forall 'rv 'e. diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index f4f7dc75..431ad1f7 100755 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -284,17 +284,11 @@ val abs_real = {coq: "Rabs", _: "abs_real"} : real -> real overload abs = {abs_atom, abs_real} -val quotient_nat = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int"} : (nat, nat) -> nat - val quotient_real = {ocaml: "quotient_real", lem: "realDiv", c: "div_real", coq: "Rdiv"} : (real, real) -> real -val quotient = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int - -overload operator / = {quotient_nat, quotient, quotient_real} - -val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int - -overload operator % = {modulus} +overload operator / = {ediv_int, quotient_real} +overload div = {ediv_int} +overload operator % = {emod_int} val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real", coq: "IZR"} : int -> real |