Coq: real built-ins for AArch64

2 files changed, 20 insertions, 20 deletions

diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v
index 67d165cd..45c5e3ce 100644
--- a/aarch64/aarch64_extras.v
+++ b/aarch64/aarch64_extras.v
@@ -3,8 +3,8 @@ Require Import Sail2_values.
 Require Import Sail2_operators_bitlists.
 Require Import Sail2_prompt_monad.
 Require Import Sail2_prompt.
+Require Import Sail2_real.
 
-Axiom real : Type.
 Axiom slice : forall {m} (_ : mword m) (_ : Z) (n : Z) `{ArithFact (m >= 0)} `{ArithFact (n >= 0)}, mword n.
 Axiom set_slice : forall (n : Z) (m : Z), mword n -> Z -> mword m -> mword n.
 Definition length {n} (x : mword n) := length_mword x.
@@ -96,7 +96,7 @@ Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mw
 (*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
 Definition undefined_bits {rv e} := @undefined_bitvector rv e.
 Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU.
-(*Definition undefined_real {rv e} (_:unit) : monad rv real e := returnm (realFromFrac 0 1).*)
+Definition undefined_real {rv e} (_:unit) : monad rv R e := returnm (realFromFrac 0 1).
 Definition undefined_range {rv e} i j `{ArithFact (i <= j)} : monad rv {z : Z & ArithFact (i <= z /\ z <= j)} e := returnm (build_ex i).
 Definition undefined_atom {rv e} i : monad rv Z e := returnm i.
 Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii).
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index a1bddec1..8cd18fac 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -12,7 +12,7 @@ val eq_vec = {ocaml: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : fo
 
 val eq_string = {ocaml: "eq_string", lem: "eq", c: "eq_string", coq: "generic_eq"} : (string, string) -> bool
 
-val eq_real = {ocaml: "eq_real", lem: "eq", c: "eq_real"} : (real, real) -> bool
+val eq_real = {ocaml: "eq_real", lem: "eq", c: "eq_real", coq: "Reqb"} : (real, real) -> bool
 
 val eq_anything = {
   ocaml: "(fun (x, y) -> x = y)",
@@ -217,7 +217,7 @@ val xor_vec = {
 
 val int_power = {lem: "pow"} : (int, int) -> int
 
-val real_power = {ocaml: "real_power", lem: "realPowInteger", c: "real_power"} : (real, int) -> real
+val real_power = {ocaml: "real_power", lem: "realPowInteger", c: "real_power", coq: "powerRZ"} : (real, int) -> real
 
 overload operator ^ = {xor_vec, int_power, real_power}
 
@@ -235,7 +235,7 @@ val add_vec_int = {
   coq: "add_vec_int"
 } : forall 'n. (bits('n), int) -> bits('n)
 
-val add_real = {ocaml: "add_real", lem: "realAdd", c: "add_real"} : (real, real) -> real
+val add_real = {ocaml: "add_real", lem: "realAdd", c: "add_real", coq: "Rplus"} : (real, real) -> real
 
 overload operator + = {add_vec, add_vec_int, add_real}
 
@@ -248,47 +248,47 @@ val sub_vec_int = {
   coq: "sub_vec_int"
 } : forall 'n. (bits('n), int) -> bits('n)
 
-val sub_real = {ocaml: "sub_real", lem: "realMinus", c: "sub_real"} : (real, real) -> real
+val sub_real = {ocaml: "sub_real", lem: "realMinus", c: "sub_real", coq: "Rminus"} : (real, real) -> real
 
-val negate_real = {ocaml: "negate_real", lem: "realNegate", c: "neg_real"} : real -> real
+val negate_real = {ocaml: "negate_real", lem: "realNegate", c: "neg_real", coq: "Ropp"} : real -> real
 
 overload operator - = {sub_vec, sub_vec_int, sub_real}
 
 overload negate = {negate_real}
 
-val mult_real = {ocaml: "mult_real", lem: "realMult", c: "mult_real"} : (real, real) -> real
+val mult_real = {ocaml: "mult_real", lem: "realMult", c: "mult_real", coq: "Rmult"} : (real, real) -> real
 
 overload operator * = {mult_real}
 
-val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt", c: "sqrt_real"} : real -> real
+val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt", c: "sqrt_real", coq: "sqrt"} : real -> real
 
-val gteq_real = {ocaml: "gteq_real", lem: "gteq", c: "gteq_real"} : (real, real) -> bool
+val gteq_real = {ocaml: "gteq_real", lem: "gteq", c: "gteq_real", coq: "gteq_real"} : (real, real) -> bool
 
 overload operator >= = {gteq_atom, gteq_int, gteq_real}
 
-val lteq_real = {ocaml: "lteq_real", lem: "lteq", c: "lteq_real"} : (real, real) -> bool
+val lteq_real = {ocaml: "lteq_real", lem: "lteq", c: "lteq_real", coq: "lteq_real"} : (real, real) -> bool
 
 overload operator <= = {lteq_atom, lteq_int, lteq_real}
 
-val gt_real = {ocaml: "gt_real", lem: "gt", c: "gt_real"} : (real, real) -> bool
+val gt_real = {ocaml: "gt_real", lem: "gt", c: "gt_real", coq: "gt_real"} : (real, real) -> bool
 
 overload operator > = {gt_atom, gt_int, gt_real}
 
-val lt_real = {ocaml: "lt_real", lem: "lt", c: "lt_real"} : (real, real) -> bool
+val lt_real = {ocaml: "lt_real", lem: "lt", c: "lt_real", coq: "lt_real"} : (real, real) -> bool
 
 overload operator < = {lt_atom, lt_int, lt_real}
 
-val RoundDown = {ocaml: "round_down", lem: "realFloor", c: "round_down"} : real -> int
+val RoundDown = {ocaml: "round_down", lem: "realFloor", c: "round_down", coq: "Zfloor"} : real -> int
 
-val RoundUp = {ocaml: "round_up", lem: "realCeiling", c: "round_up"} : real -> int
+val RoundUp = {ocaml: "round_up", lem: "realCeiling", c: "round_up", coq: "Zceil"} : real -> int
 
-val abs_real = "abs_real" : real -> real
+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"} : (real, real) -> real
+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
 
@@ -298,15 +298,15 @@ val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem
 
 overload operator % = {modulus}
 
-val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real"} : int -> real
+val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real", coq: "IZR"} : int -> real
 
 val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat
 
-val min_int = {ocaml: "min_int", lem: "min", c: "min_int", coq: "min_int"} : (int, int) -> int
+val min_int = {ocaml: "min_int", lem: "min", c: "min_int", coq: "Z.min"} : (int, int) -> int
 
 val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat
 
-val max_int = {ocaml: "max_int", lem: "max", c: "max_int", coq: "min_int"} : (int, int) -> int
+val max_int = {ocaml: "max_int", lem: "max", c: "max_int", coq: "Z.max"} : (int, int) -> int
 
 overload min = {min_nat, min_int}