diff options
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/aarch64_extras.v | 4 | ||||
| -rwxr-xr-x | aarch64/prelude.sail | 36 |
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} |