summaryrefslogtreecommitdiff
path: root/aarch64
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64')
-rwxr-xr-xaarch64/prelude.sail78
1 files changed, 45 insertions, 33 deletions
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 431ad1f7..21fcbe92 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -6,11 +6,11 @@ $include <arith.sail>
type bits ('n : Int) = vector('n, dec, bit)
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_vec = {ocaml: "eq_list", interpreter: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
-val eq_string = {ocaml: "eq_string", lem: "eq", c: "eq_string", coq: "generic_eq"} : (string, string) -> bool
+val eq_string = {ocaml: "eq_string", interpreter: "eq_string", lem: "eq", c: "eq_string", coq: "generic_eq"} : (string, string) -> bool
-val eq_real = {ocaml: "eq_real", lem: "eq", c: "eq_real", coq: "Reqb"} : (real, real) -> bool
+val eq_real = {ocaml: "eq_real", interpreter: "eq_real", lem: "eq", c: "eq_real", coq: "Reqb"} : (real, real) -> bool
val eq_anything = {
ocaml: "(fun (x, y) -> x = y)",
@@ -21,8 +21,8 @@ val eq_anything = {
} : forall ('a : Type). ('a, 'a) -> bool
val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
-val vector_length = {ocaml: "length", lem: "length_list", c: "length", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
-val list_length = {ocaml: "length", lem: "length_list", c: "length", coq: "length_list"} : forall ('a : Type). list('a) -> int
+val vector_length = {ocaml: "length", interpreter: "length", lem: "length_list", c: "length", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
+val list_length = {ocaml: "length", interpreter: "length", lem: "length_list", c: "length", coq: "length_list"} : forall ('a : Type). list('a) -> int
overload length = {bitvector_length, vector_length, list_length}
@@ -30,6 +30,7 @@ overload operator == = {eq_vec, eq_string, eq_real, eq_anything}
val vector_subrange_A = {
ocaml: "subrange",
+ interpreter: "subrange",
lem: "subrange_vec_dec",
c: "vector_subrange",
coq: "subrange_vec_dec"
@@ -38,6 +39,7 @@ val vector_subrange_A = {
val vector_subrange_B = {
ocaml: "subrange",
+ interpreter: "subrange",
lem: "subrange_vec_dec",
c: "vector_subrange"
} : forall ('n : Int) ('m : Int) ('o : Int).
@@ -47,6 +49,7 @@ overload vector_subrange = {vector_subrange_A, vector_subrange_B}
val bitvector_access_A = {
ocaml: "access",
+ interpreter: "access",
lem: "access_vec_dec",
c: "vector_access",
coq: "access_vec_dec"
@@ -54,6 +57,7 @@ val bitvector_access_A = {
val bitvector_access_B = {
ocaml: "access",
+ interpreter: "access",
lem: "access_vec_dec",
c: "vector_access",
coq: "access_vec_dec"
@@ -61,6 +65,7 @@ val bitvector_access_B = {
val vector_access_A = {
ocaml: "access",
+ interpreter: "access",
lem: "access_list_dec",
c: "vector_access",
coq: "vec_access_dec"
@@ -68,22 +73,24 @@ val vector_access_A = {
val vector_access_B = {
ocaml: "access",
+ interpreter: "access",
lem: "access_list_dec",
c: "vector_access"
} : forall ('n : Int) ('a : Type). (vector('n, dec, 'a), int) -> 'a
overload vector_access = {bitvector_access_A, bitvector_access_B, vector_access_A, vector_access_B}
-val bitvector_update_B = {ocaml: "update", lem: "update_vec_dec", c: "vector_update", coq: "update_vec_dec"} : forall 'n.
+val bitvector_update_B = {ocaml: "update", interpreter: "update", lem: "update_vec_dec", c: "vector_update", coq: "update_vec_dec"} : forall 'n.
(bits('n), int, bit) -> bits('n)
-val vector_update_B = {ocaml: "update", lem: "update_list_dec", c: "vector_update", coq: "vec_update_dec"} : forall 'n ('a : Type).
+val vector_update_B = {ocaml: "update", interpreter: "update", lem: "update_list_dec", c: "vector_update", coq: "vec_update_dec"} : forall 'n ('a : Type).
(vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
overload vector_update = {bitvector_update_B, vector_update_B}
val vector_update_subrange = {
ocaml: "update_subrange",
+ interpreter: "update_subrange",
lem: "update_subrange_vec_dec",
c: "vector_update_subrange",
coq: "update_subrange_vec_dec"
@@ -92,16 +99,17 @@ val vector_update_subrange = {
val vcons : forall ('n : Int) ('a : Type).
('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a)
-val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = {ocaml: "append", interpreter: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
(bits('n), bits('m)) -> bits('n + 'm)
-val vector_concat = {ocaml: "append", lem: "append_list", coq: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
+val vector_concat = {ocaml: "append", interpreter: "append", lem: "append_list", coq: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
(vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
overload append = {bitvector_concat, vector_concat}
val not_vec = {
ocaml: "not_vec",
+ interpreter: "not_vec",
lem: "not_vec",
c: "not_bits",
coq: "not_vec"
@@ -119,7 +127,7 @@ function neq_anything (x, y) = not_bool(x == y)
overload operator != = {neq_vec, neq_anything}
-val builtin_and_vec = {ocaml: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_and_vec = {ocaml: "and_vec", interpreter: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -127,7 +135,7 @@ function and_vec (xs, ys) = builtin_and_vec(xs, ys)
overload operator & = {and_vec}
-val builtin_or_vec = {ocaml: "or_vec", c: "or_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_or_vec = {ocaml: "or_vec", interpreter: "or_vec", c: "or_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec"}: forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -194,7 +202,7 @@ val putchar = {
coq: "putchar"
} : int -> unit
-val concat_str = {ocaml: "concat_str", lem: "stringAppend", c: "concat_str", coq: "String.append"} : (string, string) -> string
+val concat_str = {ocaml: "concat_str", interpreter: "concat_str", lem: "stringAppend", c: "concat_str", coq: "String.append"} : (string, string) -> string
val DecStr = "dec_str" : int -> string
@@ -208,6 +216,7 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
val xor_vec = {
ocaml: "xor_vec",
+ interpreter: "xor_vec",
lem: "xor_vec",
c: "xor_bits",
coq: "xor_vec"
@@ -215,12 +224,13 @@ val xor_vec = {
val int_power = {lem: "pow"} : (int, int) -> int
-val real_power = {ocaml: "real_power", lem: "realPowInteger", c: "real_power", coq: "powerRZ"} : (real, int) -> real
+val real_power = {ocaml: "real_power", interpreter: "real_power", lem: "realPowInteger", c: "real_power", coq: "powerRZ"} : (real, int) -> real
overload operator ^ = {xor_vec, int_power, real_power}
val add_vec = {
ocaml: "add_vec",
+ interpreter: "add_vec",
lem: "add_vec",
c: "add_bits",
coq: "add_vec"
@@ -228,12 +238,13 @@ val add_vec = {
val add_vec_int = {
ocaml: "add_vec_int",
+ interpreter: "add_vec_int",
lem: "add_vec_int",
c: "add_bits_int",
coq: "add_vec_int"
} : forall 'n. (bits('n), int) -> bits('n)
-val add_real = {ocaml: "add_real", lem: "realAdd", c: "add_real", coq: "Rplus"} : (real, real) -> real
+val add_real = {ocaml: "add_real", interpreter: "add_real", lem: "realAdd", c: "add_real", coq: "Rplus"} : (real, real) -> real
overload operator + = {add_vec, add_vec_int, add_real}
@@ -241,64 +252,65 @@ val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) ->
val sub_vec_int = {
ocaml: "sub_vec_int",
+ interpreter: "sub_vec_int",
lem: "sub_vec_int",
c: "sub_bits_int",
coq: "sub_vec_int"
} : forall 'n. (bits('n), int) -> bits('n)
-val sub_real = {ocaml: "sub_real", lem: "realMinus", c: "sub_real", coq: "Rminus"} : (real, real) -> real
+val sub_real = {ocaml: "sub_real", interpreter: "sub_real", lem: "realMinus", c: "sub_real", coq: "Rminus"} : (real, real) -> real
-val negate_real = {ocaml: "negate_real", lem: "realNegate", c: "neg_real", coq: "Ropp"} : real -> real
+val negate_real = {ocaml: "negate_real", interpreter: "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", coq: "Rmult"} : (real, real) -> real
+val mult_real = {ocaml: "mult_real", interpreter: "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", coq: "sqrt"} : real -> real
+val Sqrt = {ocaml: "sqrt_real", interpreter: "sqrt_real", lem: "realSqrt", c: "sqrt_real", coq: "sqrt"} : real -> real
-val gteq_real = {ocaml: "gteq_real", lem: "gteq", c: "gteq_real", coq: "gteq_real"} : (real, real) -> bool
+val gteq_real = {ocaml: "gteq_real", interpreter: "gteq_real", lem: "gteq", c: "gteq_real", coq: "gteq_real"} : (real, real) -> bool
overload operator >= = {gteq_real}
-val lteq_real = {ocaml: "lteq_real", lem: "lteq", c: "lteq_real", coq: "lteq_real"} : (real, real) -> bool
+val lteq_real = {ocaml: "lteq_real", interpreter: "lteq_real", lem: "lteq", c: "lteq_real", coq: "lteq_real"} : (real, real) -> bool
overload operator <= = {lteq_real}
-val gt_real = {ocaml: "gt_real", lem: "gt", c: "gt_real", coq: "gt_real"} : (real, real) -> bool
+val gt_real = {ocaml: "gt_real", interpreter: "gt_real", lem: "gt", c: "gt_real", coq: "gt_real"} : (real, real) -> bool
overload operator > = {gt_real}
-val lt_real = {ocaml: "lt_real", lem: "lt", c: "lt_real", coq: "lt_real"} : (real, real) -> bool
+val lt_real = {ocaml: "lt_real", interpreter: "lt_real", lem: "lt", c: "lt_real", coq: "lt_real"} : (real, real) -> bool
overload operator < = {lt_real}
-val RoundDown = {ocaml: "round_down", lem: "realFloor", c: "round_down", coq: "Zfloor"} : real -> int
+val RoundDown = {ocaml: "round_down", interpreter: "round_down", lem: "realFloor", c: "round_down", coq: "Zfloor"} : real -> int
-val RoundUp = {ocaml: "round_up", lem: "realCeiling", c: "round_up", coq: "Zceil"} : real -> int
+val RoundUp = {ocaml: "round_up", interpreter: "round_up", lem: "realCeiling", c: "round_up", coq: "Zceil"} : real -> int
val abs_real = {coq: "Rabs", _: "abs_real"} : real -> real
overload abs = {abs_atom, abs_real}
-val quotient_real = {ocaml: "quotient_real", lem: "realDiv", c: "div_real", coq: "Rdiv"} : (real, real) -> real
+val quotient_real = {ocaml: "quotient_real", interpreter: "quotient_real", lem: "realDiv", c: "div_real", coq: "Rdiv"} : (real, real) -> real
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
+val Real = {ocaml: "to_real", interpreter: "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_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat
-val min_int = {ocaml: "min_int", lem: "min", c: "min_int", coq: "Z.min"} : (int, int) -> int
+val min_int = {ocaml: "min_int", interpreter: "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_nat = {ocaml: "max_int", interpreter: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat
-val max_int = {ocaml: "max_int", lem: "max", c: "max_int", coq: "Z.max"} : (int, int) -> int
+val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", c: "max_int", coq: "Z.max"} : (int, int) -> int
overload min = {min_nat, min_int}
@@ -355,11 +367,11 @@ union option ('a : Type) = {
}
*/
-val __SleepRequest = {ocaml: "sleep_request", lem: "sleep_request", smt: "sleep_request", interpreter: "sleep_request", c: "sleep_request"}: unit -> unit effect {rreg, undef}
+val __SleepRequest = {ocaml: "sleep_request", interpreter: "sleep_request", lem: "sleep_request", smt: "sleep_request", interpreter: "sleep_request", c: "sleep_request"}: unit -> unit effect {rreg, undef}
-val __WakeupRequest = {ocaml: "wakeup_request", lem: "wakeup_request", smt: "wakeup_request", interpreter: "wakeup_request", c: "wakeup_request"}: unit -> unit effect {rreg, undef}
+val __WakeupRequest = {ocaml: "wakeup_request", interpreter: "wakeup_request", lem: "wakeup_request", smt: "wakeup_request", interpreter: "wakeup_request", c: "wakeup_request"}: unit -> unit effect {rreg, undef}
-val __Sleeping = {ocaml: "sleeping", lem: "sleeping", smt: "sleeping", interpreter: "sleeping", c: "sleeping"}: unit -> bool effect {rreg, undef}
+val __Sleeping = {ocaml: "sleeping", interpreter: "sleeping", lem: "sleeping", smt: "sleeping", interpreter: "sleeping", c: "sleeping"}: unit -> bool effect {rreg, undef}
val __GetVerbosity = {c: "sail_get_verbosity"}: unit -> bits(64) effect {rreg, undef}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:03:40 +0000