diff options
| author | Ana | 2020-12-01 08:52:12 +0000 |
|---|---|---|
| committer | Ana | 2021-02-26 13:32:41 +0000 |
| commit | 4302a75d82b9ac983cd89dd01c742c36777d921b (patch) | |
| tree | 8f6f437bb65bc3534e7f0f9851cdb05627ec885e | |
| parent | 15074f171cdf250880bd0f7a2806356040c89f36 (diff) | |
Signed primitive integers
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
53 files changed, 1532 insertions, 149 deletions
diff --git a/META.coq.in b/META.coq.in index 7a9818da08..39e35561ff 100644 --- a/META.coq.in +++ b/META.coq.in @@ -500,21 +500,6 @@ package "plugins" ( plugin(native) = "r_syntax_plugin.cmxs" ) - package "int63syntax" ( - - description = "Coq int63syntax plugin" - version = "8.14" - - requires = "" - directory = "syntax" - - archive(byte) = "int63_syntax_plugin.cmo" - archive(native) = "int63_syntax_plugin.cmx" - - plugin(byte) = "int63_syntax_plugin.cmo" - plugin(native) = "int63_syntax_plugin.cmxs" - ) - package "string_notation" ( description = "Coq string_notation plugin" diff --git a/Makefile.common b/Makefile.common index 415454df79..dc40413078 100644 --- a/Makefile.common +++ b/Makefile.common @@ -149,7 +149,6 @@ CCCMO:=plugins/cc/cc_plugin.cmo BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo SYNTAXCMO:=$(addprefix plugins/syntax/, \ - int63_syntax_plugin.cmo \ float_syntax_plugin.cmo \ number_string_notation_plugin.cmo) DERIVECMO:=plugins/derive/derive_plugin.cmo diff --git a/checker/values.ml b/checker/values.ml index 907f9f7e32..f7a367b986 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -240,7 +240,7 @@ let v_template_universes = v_tuple "template_universes" [|List(Opt v_level);v_context_set|] let v_primitive = - v_enum "primitive" 50 (* Number of "Primitive" in Int63.v and PrimFloat.v *) + v_enum "primitive" 54 (* Number of constructors of the CPrimitives.t type *) let v_cst_def = v_sum "constant_def" 0 diff --git a/doc/changelog/10-standard-library/13559-primitive_integers.rst b/doc/changelog/10-standard-library/13559-primitive_integers.rst new file mode 100644 index 0000000000..c3cad79bd2 --- /dev/null +++ b/doc/changelog/10-standard-library/13559-primitive_integers.rst @@ -0,0 +1,5 @@ +- **Added:** + Library for signed primitive integers, Sint63. The following operations were added to the kernel: division, remainder, comparison functions, and arithmetic shift right. Everything else works the same for signed and unsigned ints. + (`#13559 <https://github.com/coq/coq/pull/13559>`_, + fixes `#12109 <https://github.com/coq/coq/issues/12109>`_, + by Ana Borges, Guillaume Melquiond and Pierre Roux). diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst index 4505fc4b4d..7211d00dd0 100644 --- a/doc/sphinx/language/core/primitive.rst +++ b/doc/sphinx/language/core/primitive.rst @@ -8,15 +8,20 @@ Primitive Integers The language of terms features 63-bit machine integers as values. The type of such a value is *axiomatized*; it is declared through the following sentence -(excerpt from the :g:`Int63` module): +(excerpt from the :g:`PrimInt63` module): .. coqdoc:: Primitive int := #int63_type. -This type is equipped with a few operators, that must be similarly declared. -For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, -declared and specified as follows: +This type can be understood as representing either unsigned or signed integers, +depending on which module is imported or, more generally, which scope is open. +:g:`Int63` and :g:`int63_scope` refer to the unsigned version, while :g:`Sint63` +and :g:`sint63_scope` refer to the signed one. + +The :g:`PrimInt63` module declares the available operators for this type. +For instance, equality of two unsigned primitive integers can be determined using +the :g:`Int63.eqb` function, declared and specified as follows: .. coqdoc:: @@ -25,7 +30,9 @@ declared and specified as follows: Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. -The complete set of such operators can be obtained looking at the :g:`Int63` module. +The complete set of such operators can be found in the :g:`PrimInt63` module. +The specifications and notations are in the :g:`Int63` and :g:`Sint63` +modules. These primitive declarations are regular axioms. As such, they must be trusted and are listed by the :g:`Print Assumptions` command, as in the following example. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 609884ce1d..03571ad680 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1741,6 +1741,12 @@ Number notations sorts, primitive integers, primitive floats, primitive arrays and type constants for primitive types) will be considered for printing. + .. note:: + For example, :n:`@qualid__type` can be :n:`PrimInt63.int`, + in which case :n:`@qualid__print` takes :n:`PrimInt63.int_wrapper` as input + instead of :n:`PrimInt63.int`. See below for an + :ref:`example <example-number-notation-primitive-int>`. + .. _number-string-via: :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` @@ -2066,6 +2072,23 @@ The following errors apply to both string and number notations: Check 3. +.. _example-number-notation-primitive-int: + +.. example:: Number Notation for primitive integers + + This shows the use of the primitive + integers :n:`PrimInt63.int` as :n:`@qualid__type`. It is the way + parsing and printing of primitive integers are actually implemented + in `PrimInt63.v`. + + .. coqtop:: in reset + + Require Import Int63. + Definition parser (x : pos_neg_int63) : option int := + match x with Pos p => Some p | Neg _ => None end. + Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x). + Number Notation int parser printer : int63_scope. + .. _example-number-notation-non-inductive: .. example:: Number Notation for a non inductive type diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index cbe526be68..27eb64a83b 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -286,6 +286,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Cyclic/Int63/Cyclic63.v theories/Numbers/Cyclic/Int63/PrimInt63.v theories/Numbers/Cyclic/Int63/Int63.v + theories/Numbers/Cyclic/Int63/Sint63.v theories/Numbers/Cyclic/Int63/Ring63.v theories/Numbers/Cyclic/ZModulo/ZModulo.v </dd> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8138b4c6d9..4fb7861ca6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -969,7 +969,13 @@ let rec extern inctx ?impargs scopes vars r = with No_match -> extern inctx scopes vars r') | None -> - try extern_notations inctx scopes vars None r + let r' = match DAst.get r with + | GInt i when Coqlib.has_ref "num.int63.wrap_int" -> + let wrap = Coqlib.lib_ref "num.int63.wrap_int" in + DAst.make (GApp (DAst.make (GRef (wrap, None)), [r])) + | _ -> r in + + try extern_notations inctx scopes vars None r' with No_match -> let loc = r.CAst.loc in @@ -1123,7 +1129,7 @@ let rec extern inctx ?impargs scopes vars r = | GInt i -> extern_prim_token_delimiter_if_required - (Number (NumTok.Signed.of_int_string (Uint63.to_string i))) + (Number NumTok.(Signed.of_bigint CHex (Z.of_int64 (Uint63.to_int64 i)))) "int63" "int63_scope" (snd scopes) | GFloat f -> extern_float f (snd scopes) diff --git a/interp/notation.ml b/interp/notation.ml index d6002d71b5..ed605c994d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -548,11 +548,14 @@ type number_ty = hexadecimal : Names.inductive; number : Names.inductive } +type pos_neg_int63_ty = + { pos_neg_int63_ty : Names.inductive } + type target_kind = | Int of int_ty (* Coq.Init.Number.int + uint *) | UInt of int_ty (* Coq.Init.Number.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) - | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) + | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *) | Number of number_ty (* Coq.Init.Number.number + uint + int *) | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) @@ -1038,12 +1041,22 @@ let error_negative ?loc = let error_overflow ?loc n = CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Z.to_string n)) -let interp_int63 ?loc n = +let error_underflow ?loc n = + CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "underflow in int63 literal: " ++ str (Z.to_string n)) + +let coqpos_neg_int63_of_bigint ?loc ind (sign,n) = + let uint = int63_of_pos_bigint ?loc n in + let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in + mkApp (mkConstruct (ind, pos_neg), [|uint|]) + +let interp_int63 ?loc ind n = + let sign = if Z.(compare n zero >= 0) then SPlus else SMinus in + let n = Z.abs n in if Z.(leq zero n) then if Z.(lt n (pow z_two 63)) - then int63_of_pos_bigint ?loc n - else error_overflow ?loc n + then coqpos_neg_int63_of_bigint ?loc ind (sign,n) + else match sign with SPlus -> error_overflow ?loc n | SMinus -> error_underflow ?loc n else error_negative ?loc let bigint_of_int63 c = @@ -1051,6 +1064,15 @@ let bigint_of_int63 c = | Int i -> Z.of_int64 (Uint63.to_int64 i) | _ -> raise NotAValidPrimToken +let bigint_of_coqpos_neg_int63 c = + match Constr.kind c with + | App (c,[|c'|]) -> + (match Constr.kind c with + | Construct ((_,1), _) (* Pos *) -> bigint_of_int63 c' + | Construct ((_,2), _) (* Neg *) -> Z.neg (bigint_of_int63 c') + | _ -> raise NotAValidPrimToken) + | _ -> raise NotAValidPrimToken + let interp o ?loc n = begin match o.warning, n with | Warning threshold, n when NumTok.Signed.is_bigger_int_than n threshold -> @@ -1070,9 +1092,9 @@ let interp o ?loc n = with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) | Z z_pos_ty, Some n -> z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n) - | Int63, Some n -> - interp_int63 ?loc (NumTok.SignedNat.to_bigint n) - | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ -> + | Int63 pos_neg_int63_ty, Some n -> + interp_int63 ?loc pos_neg_int63_ty.pos_neg_int63_ty (NumTok.SignedNat.to_bigint n) + | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63 _), _ -> no_such_prim_token "number" ?loc o.ty_name | Number number_ty, _ -> coqnumber_of_rawnum number_ty n | Decimal number_ty, _ -> @@ -1100,7 +1122,7 @@ let uninterp o n = | (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c) | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c) | (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c) - | (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c) + | (Int63 _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_coqpos_neg_int63 c) | (Number _, c) -> rawnum_of_coqnumber c | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c) | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c) diff --git a/interp/notation.mli b/interp/notation.mli index 97955bf92e..77f245ae77 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -137,11 +137,14 @@ type number_ty = hexadecimal : Names.inductive; number : Names.inductive } +type pos_neg_int63_ty = + { pos_neg_int63_ty : Names.inductive } + type target_kind = | Int of int_ty (* Coq.Init.Number.int + uint *) | UInt of int_ty (* Coq.Init.Number.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) - | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) + | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *) | Number of number_ty (* Coq.Init.Number.number + uint + int *) | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) diff --git a/interp/numTok.ml b/interp/numTok.ml index 124a6cd249..12ef33717a 100644 --- a/interp/numTok.ml +++ b/interp/numTok.ml @@ -85,7 +85,7 @@ struct let string_of_nonneg_bigint c n = match c with | CDec -> Z.format "%d" n - | CHex -> Z.format "0x%x" n + | CHex -> Z.format "%#x" n let of_bigint c n = let sign, n = if Int.equal (-1) (Z.sign n) then (SMinus, Z.neg n) else (SPlus, n) in (sign, string_of_nonneg_bigint c n) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 95a334561f..704eb1ef98 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1426,6 +1426,41 @@ value coq_interprete Next; } + Instruct(CHECKDIVSINT63) { + print_instr("CHEKDIVSINT63"); + CheckInt2(); + int b; + Uint63_eq0(b, *sp); + if (b) { + accu = *sp++; + } + else { + Uint63_eqm1(b, *sp); + if (b) { + Uint63_neg(accu); + sp++; + } + else { + Uint63_divs(accu, *sp++); + } + } + Next; + } + + Instruct(CHECKMODSINT63) { + print_instr("CHEKMODSINT63"); + CheckInt2(); + int b; + Uint63_eq0(b, *sp); + if (b) { + accu = *sp++; + } + else { + Uint63_mods(accu,*sp++); + } + Next; + } + Instruct (CHECKDIV21INT63) { print_instr("DIV21INT63"); CheckInt3(); @@ -1473,6 +1508,13 @@ value coq_interprete Next; } + Instruct(CHECKASRINT63) { + print_instr("CHECKASRINT63"); + CheckInt2(); + Uint63_asr(accu,*sp++); + Next; + } + Instruct (CHECKADDMULDIVINT63) { print_instr("CHECKADDMULDIVINT63"); CheckInt3(); @@ -1508,6 +1550,24 @@ value coq_interprete Next; } + Instruct (CHECKLTSINT63) { + print_instr("CHECKLTSINT63"); + CheckInt2(); + int b; + Uint63_lts(b,accu,*sp++); + accu = b ? coq_true : coq_false; + Next; + } + + Instruct (CHECKLESINT63) { + print_instr("CHECKLESINT63"); + CheckInt2(); + int b; + Uint63_les(b,accu,*sp++); + accu = b ? coq_true : coq_false; + Next; + } + Instruct (CHECKCOMPAREINT63) { /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */ /* assumes Inductive _ : _ := Eq | Lt | Gt */ @@ -1526,6 +1586,24 @@ value coq_interprete Next; } + Instruct (CHECKCOMPARESINT63) { + /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */ + /* assumes Inductive _ : _ := Eq | Lt | Gt */ + print_instr("CHECKCOMPARESINT63"); + CheckInt2(); + int b; + Uint63_eq(b, accu, *sp); + if (b) { + accu = coq_Eq; + sp++; + } + else { + Uint63_lts(b, accu, *sp++); + accu = b ? coq_Lt : coq_Gt; + } + Next; + } + Instruct (CHECKHEAD0INT63) { print_instr("CHECKHEAD0INT63"); CheckInt1(); diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index dd9b9e55be..693716ee90 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -96,7 +96,10 @@ value uint63_##name##_ml(value x, value y, value z) { \ accu = uint63_return_value__; \ }while(0) +DECLARE_NULLOP(zero) DECLARE_NULLOP(one) +DECLARE_UNOP(neg) +#define Uint63_neg(x) CALL_UNOP(neg, x) DECLARE_BINOP(add) #define Uint63_add(x, y) CALL_BINOP(add, x, y) DECLARE_BINOP(addcarry) @@ -105,28 +108,40 @@ DECLARE_TEROP(addmuldiv) #define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z) DECLARE_BINOP(div) #define Uint63_div(x, y) CALL_BINOP(div, x, y) +DECLARE_BINOP(divs) +#define Uint63_divs(x, y) CALL_BINOP(divs, x, y) DECLARE_BINOP(eq) #define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y) DECLARE_UNOP(eq0) #define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x) +DECLARE_UNOP(eqm1) +#define Uint63_eqm1(r, x) CALL_PREDICATE(r, eqm1, x) DECLARE_UNOP(head0) #define Uint63_head0(x) CALL_UNOP(head0, x) DECLARE_BINOP(land) #define Uint63_land(x, y) CALL_BINOP(land, x, y) DECLARE_BINOP(leq) #define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y) +DECLARE_BINOP(les) +#define Uint63_les(r, x, y) CALL_RELATION(r, les, x, y) DECLARE_BINOP(lor) #define Uint63_lor(x, y) CALL_BINOP(lor, x, y) DECLARE_BINOP(lsl) #define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y) DECLARE_BINOP(lsr) #define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y) +DECLARE_BINOP(asr) +#define Uint63_asr(x, y) CALL_BINOP(asr, x, y) DECLARE_BINOP(lt) #define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y) +DECLARE_BINOP(lts) +#define Uint63_lts(r, x, y) CALL_RELATION(r, lts, x, y) DECLARE_BINOP(lxor) #define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y) DECLARE_BINOP(mod) #define Uint63_mod(x, y) CALL_BINOP(mod, x, y) +DECLARE_BINOP(mods) +#define Uint63_mods(x, y) CALL_BINOP(mods, x, y) DECLARE_BINOP(mul) #define Uint63_mul(x, y) CALL_BINOP(mul, x, y) DECLARE_BINOP(sub) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 731ae8f46e..da9ae7f147 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -12,21 +12,28 @@ #define uint_of_value(val) (((uint64_t)(val)) >> 1) #define uint63_of_value(val) ((uint64_t)(val) >> 1) +#define int63_of_value(val) ((int64_t)(val) >> 1) /* 2^63 * y + x as a value */ //#define Val_intint(x,y) ((value)(((uint64_t)(x)) << 1 + ((uint64_t)(y) << 64))) -#define uint63_zero ((value) 1) /* 2*0 + 1 */ +#define uint63_zero() ((value) 1) /* 2*0 + 1 */ #define uint63_one() ((value) 3) /* 2*1 + 1 */ #define uint63_eq(x,y) ((x) == (y)) #define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y)) #define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1)) +#define Uint63_eqm1(r,x) ((r) = ((x) == (uint64_t)(int64_t)(-1))) #define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y)) #define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y)) #define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y)) #define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y)) +#define uint63_lts(x,y) ((int64_t) (x) < (int64_t) (y)) +#define Uint63_lts(r,x,y) ((r) = uint63_lts(x,y)) +#define uint63_les(x,y) ((int64_t) (x) <= (int64_t) (y)) +#define Uint63_les(r,x,y) ((r) = uint63_les(x,y)) +#define Uint63_neg(x) (accu = (value)(2 - (uint64_t) x)) #define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1)) #define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1)) #define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1)) @@ -34,6 +41,8 @@ #define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y))) #define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y))) #define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y))) +#define Uint63_divs(x,y) (accu = Val_long(int63_of_value(x) / int63_of_value(y))) +#define Uint63_mods(x,y) (accu = Val_long(int63_of_value(x) % int63_of_value(y))) #define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1)) #define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y))) @@ -46,14 +55,21 @@ if (uint63_lsl_y__ < (uint64_t) 127) \ accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \ else \ - accu = uint63_zero; \ + accu = uint63_zero(); \ }while(0) #define Uint63_lsr(x,y) do{ \ value uint63_lsl_y__ = (y); \ if (uint63_lsl_y__ < (uint64_t) 127) \ accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \ else \ - accu = uint63_zero; \ + accu = uint63_zero(); \ + }while(0) +#define Uint63_asr(x,y) do{ \ + value uint63_asr_y__ = (y); \ + if (uint63_asr_y__ < (uint64_t) 127) \ + accu = (value)(((int64_t)(x) >> uint63_of_value(uint63_asr_y__)) | 1); \ + else \ + accu = uint63_zero(); \ }while(0) /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */ diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 5cd91b4e74..6ef0e9fa15 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -8,6 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* Note: don't forget to update v_primitive in checker/values.ml if the *) +(* number of primitives is changed. *) + open Univ type t = @@ -18,8 +21,11 @@ type t = | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -34,7 +40,10 @@ type t = | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq @@ -68,8 +77,11 @@ let parse = function | "int63_mul" -> Int63mul | "int63_div" -> Int63div | "int63_mod" -> Int63mod + | "int63_divs" -> Int63divs + | "int63_mods" -> Int63mods | "int63_lsr" -> Int63lsr | "int63_lsl" -> Int63lsl + | "int63_asr" -> Int63asr | "int63_land" -> Int63land | "int63_lor" -> Int63lor | "int63_lxor" -> Int63lxor @@ -84,7 +96,10 @@ let parse = function | "int63_eq" -> Int63eq | "int63_lt" -> Int63lt | "int63_le" -> Int63le + | "int63_lts" -> Int63lts + | "int63_les" -> Int63les | "int63_compare" -> Int63compare + | "int63_compares" -> Int63compares | "float64_opp" -> Float64opp | "float64_abs" -> Float64abs | "float64_eq" -> Float64eq @@ -163,6 +178,12 @@ let hash = function | Arrayset -> 46 | Arraycopy -> 47 | Arraylength -> 48 + | Int63lts -> 49 + | Int63les -> 50 + | Int63divs -> 51 + | Int63mods -> 52 + | Int63asr -> 53 + | Int63compares -> 54 (* Should match names in nativevalues.ml *) let to_string = function @@ -173,8 +194,11 @@ let to_string = function | Int63mul -> "mul" | Int63div -> "div" | Int63mod -> "rem" + | Int63divs -> "divs" + | Int63mods -> "rems" | Int63lsr -> "l_sr" | Int63lsl -> "l_sl" + | Int63asr -> "a_sr" | Int63land -> "l_and" | Int63lor -> "l_or" | Int63lxor -> "l_xor" @@ -189,7 +213,10 @@ let to_string = function | Int63eq -> "eq" | Int63lt -> "lt" | Int63le -> "le" + | Int63lts -> "lts" + | Int63les -> "les" | Int63compare -> "compare" + | Int63compares -> "compares" | Float64opp -> "fopp" | Float64abs -> "fabs" | Float64eq -> "feq" @@ -271,14 +298,15 @@ let types = | Int63head0 | Int63tail0 -> [int_ty; int_ty] | Int63add | Int63sub | Int63mul | Int63div | Int63mod - | Int63lsr | Int63lsl + | Int63divs | Int63mods + | Int63lsr | Int63lsl | Int63asr | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty] | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC -> [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)] | Int63mulc | Int63diveucl -> [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] - | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] - | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] + | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] + | Int63compare | Int63compares -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] | Int63div21 -> [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty] @@ -314,8 +342,11 @@ let params = function | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -330,7 +361,10 @@ let params = function | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq @@ -367,8 +401,11 @@ let univs = function | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -383,7 +420,10 @@ let univs = function | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 0db643faf4..de90179726 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -16,8 +16,11 @@ type t = | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -32,7 +35,10 @@ type t = | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index bda65956be..20220dd9d2 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -110,6 +110,8 @@ let opcodes = "CHECKMULCINT63", 1; "CHECKDIVINT63", 1; "CHECKMODINT63", 1; + "CHECKDIVSINT63", 1; + "CHECKMODSINT63", 1; "CHECKDIVEUCLINT63", 1; "CHECKDIV21INT63", 1; "CHECKLXORINT63", 1; @@ -117,11 +119,15 @@ let opcodes = "CHECKLANDINT63", 1; "CHECKLSLINT63", 1; "CHECKLSRINT63", 1; + "CHECKASRINT63", 1; "CHECKADDMULDIVINT63", 1; "CHECKEQINT63", 1; "CHECKLTINT63", 1; "CHECKLEINT63", 1; + "CHECKLTSINT63", 1; + "CHECKLESINT63", 1; "CHECKCOMPAREINT63", 1; + "CHECKCOMPARESINT63", 1; "CHECKHEAD0INT63", 1; "CHECKTAIL0INT63", 1; "CHECKOPPFLOAT", 1; diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index bd6241ae67..c986cb473d 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -333,6 +333,22 @@ let rem accu x y = if is_int x && is_int y then no_check_rem x y else accu x y +let no_check_divs x y = + mk_uint (Uint63.divs (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let divs accu x y = + if is_int x && is_int y then no_check_divs x y + else accu x y + +let no_check_rems x y = + mk_uint (Uint63.rems (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let rems accu x y = + if is_int x && is_int y then no_check_rems x y + else accu x y + let no_check_l_sr x y = mk_uint (Uint63.l_sr (to_uint x) (to_uint y)) [@@ocaml.inline always] @@ -349,6 +365,14 @@ let l_sl accu x y = if is_int x && is_int y then no_check_l_sl x y else accu x y +let no_check_a_sr x y = + mk_uint (Uint63.a_sr (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let a_sr accu x y = + if is_int x && is_int y then no_check_a_sr x y + else accu x y + let no_check_l_and x y = mk_uint (Uint63.l_and (to_uint x) (to_uint y)) [@@ocaml.inline always] @@ -502,6 +526,22 @@ let le accu x y = if is_int x && is_int y then no_check_le x y else accu x y +let no_check_lts x y = + mk_bool (Uint63.lts (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let lts accu x y = + if is_int x && is_int y then no_check_lts x y + else accu x y + +let no_check_les x y = + mk_bool (Uint63.les (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let les accu x y = + if is_int x && is_int y then no_check_les x y + else accu x y + let no_check_compare x y = match Uint63.compare (to_uint x) (to_uint y) with | x when x < 0 -> (Obj.magic CmpLt:t) @@ -512,6 +552,16 @@ let compare accu x y = if is_int x && is_int y then no_check_compare x y else accu x y +let no_check_compares x y = + match Uint63.compares (to_uint x) (to_uint y) with + | x when x < 0 -> (Obj.magic CmpLt:t) + | 0 -> (Obj.magic CmpEq:t) + | _ -> (Obj.magic CmpGt:t) + +let compares accu x y = + if is_int x && is_int y then no_check_compares x y + else accu x y + let print x = Printf.fprintf stderr "%s" (Uint63.to_string (to_uint x)); flush stderr; diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index b9b75a9d7c..98cf4219a0 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -158,9 +158,12 @@ val sub : t -> t -> t -> t val mul : t -> t -> t -> t val div : t -> t -> t -> t val rem : t -> t -> t -> t +val divs : t -> t -> t -> t +val rems : t -> t -> t -> t val l_sr : t -> t -> t -> t val l_sl : t -> t -> t -> t +val a_sr : t -> t -> t -> t val l_and : t -> t -> t -> t val l_xor : t -> t -> t -> t val l_or : t -> t -> t -> t @@ -179,7 +182,10 @@ val addMulDiv : t -> t -> t -> t -> t val eq : t -> t -> t -> t val lt : t -> t -> t -> t val le : t -> t -> t -> t +val lts : t -> t -> t -> t +val les : t -> t -> t -> t val compare : t -> t -> t -> t +val compares : t -> t -> t -> t val print : t -> t @@ -205,12 +211,21 @@ val no_check_div : t -> t -> t val no_check_rem : t -> t -> t [@@ocaml.inline always] +val no_check_divs : t -> t -> t +[@@ocaml.inline always] + +val no_check_rems : t -> t -> t +[@@ocaml.inline always] + val no_check_l_sr : t -> t -> t [@@ocaml.inline always] val no_check_l_sl : t -> t -> t [@@ocaml.inline always] +val no_check_a_sr : t -> t -> t +[@@ocaml.inline always] + val no_check_l_and : t -> t -> t [@@ocaml.inline always] @@ -253,8 +268,16 @@ val no_check_lt : t -> t -> t val no_check_le : t -> t -> t [@@ocaml.inline always] +val no_check_lts : t -> t -> t +[@@ocaml.inline always] + +val no_check_les : t -> t -> t +[@@ocaml.inline always] + val no_check_compare : t -> t -> t +val no_check_compares : t -> t -> t + (** Support for machine floating point values *) val is_float : t -> bool diff --git a/kernel/primred.ml b/kernel/primred.ml index f0b4d6d362..23b7e13ab8 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -223,10 +223,16 @@ struct let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.div i1 i2) | Int63mod -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rem i1 i2) + | Int63divs -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.divs i1 i2) + | Int63mods -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rems i1 i2) | Int63lsr -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sr i1 i2) | Int63lsl -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sl i1 i2) + | Int63asr -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.a_sr i1 i2) | Int63land -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_and i1 i2) | Int63lor -> @@ -276,6 +282,12 @@ struct | Int63le -> let i1, i2 = get_int2 evd args in E.mkBool env (Uint63.le i1 i2) + | Int63lts -> + let i1, i2 = get_int2 evd args in + E.mkBool env (Uint63.lts i1 i2) + | Int63les -> + let i1, i2 = get_int2 evd args in + E.mkBool env (Uint63.les i1 i2) | Int63compare -> let i1, i2 = get_int2 evd args in begin match Uint63.compare i1 i2 with @@ -283,6 +295,13 @@ struct | 0 -> E.mkEq env | _ -> E.mkGt env end + | Int63compares -> + let i1, i2 = get_int2 evd args in + begin match Uint63.compares i1 i2 with + | x when x < 0 -> E.mkLt env + | 0 -> E.mkEq env + | _ -> E.mkGt env + end | Float64opp -> let f = get_float1 evd args in E.mkFloat env (Float64.opp f) | Float64abs -> diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 6b2519918a..ff8d1eefb7 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -48,6 +48,7 @@ val l_xor : t -> t -> t val l_or : t -> t -> t (* Arithmetic operations *) +val a_sr : t -> t -> t val add : t -> t -> t val sub : t -> t -> t val mul : t -> t -> t @@ -56,6 +57,10 @@ val rem : t -> t -> t val diveucl : t -> t -> t * t + (* Signed arithmetic opeartions *) +val divs : t -> t -> t +val rems : t -> t -> t + (* Specific arithmetic operations *) val mulc : t -> t -> t * t val addmuldiv : t -> t -> t -> t @@ -71,6 +76,11 @@ val equal : t -> t -> bool val le : t -> t -> bool val compare : t -> t -> int + (* signed comparision *) +val lts : t -> t -> bool +val les : t -> t -> bool +val compares : t -> t -> int + (* head and tail *) val head0 : t -> t val tail0 : t -> t diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index 4f2cbc4262..9c8401105e 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -52,6 +52,15 @@ let lt x y = let le x y = Int64.compare x y <= 0 + (* signed comparison *) +(* We shift the arguments by 1 to the left so that the top-most bit is interpreted as a sign *) +(* The zero at the end doesn't change the order (it is stable by multiplication by 2) *) +let lts x y = + Int64.(compare (shift_left x 1) (shift_left y 1)) < 0 + +let les x y = + Int64.(compare (shift_left x 1) (shift_left y 1)) <= 0 + (* logical shift *) let l_sl x y = if le 0L y && lt y 63L then mask63 (Int64.shift_left x (Int64.to_int y)) else 0L @@ -59,6 +68,12 @@ let l_sl x y = let l_sr x y = if le 0L y && lt y 63L then Int64.shift_right x (Int64.to_int y) else 0L + (* arithmetic shift (for sint63) *) +let a_sr x y = + if les 0L y && lts y 63L then + mask63 (Int64.shift_right (Int64.shift_left x 1) ((Int64.to_int y) + 1)) + else 0L + let l_and x y = Int64.logand x y let l_or x y = Int64.logor x y let l_xor x y = Int64.logxor x y @@ -86,6 +101,15 @@ let rem x y = let diveucl x y = (div x y, rem x y) + (* signed division *) +let divs x y = + if y = 0L then 0L else mask63 Int64.(div (shift_left x 1) (shift_left y 1)) + + (* signed modulo *) +let rems x y = + if y = 0L then 0L else + Int64.shift_right_logical (Int64.(rem (shift_left x 1) (shift_left y 1))) 1 + let addmuldiv p x y = l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p)) @@ -139,6 +163,8 @@ let equal (x : t) y = x = y let compare x y = Int64.compare x y +let compares x y = Int64.(compare (shift_left x 1) (shift_left y 1)) + (* Number of leading zeroes *) let head0 x = let r = ref 0 in @@ -198,22 +224,30 @@ let () = Callback.register "uint63 addcarry" addcarry; Callback.register "uint63 addmuldiv" addmuldiv; Callback.register "uint63 div" div; + Callback.register "uint63 divs" divs; Callback.register "uint63 div21_ml" div21; Callback.register "uint63 eq" equal; Callback.register "uint63 eq0" (equal Int64.zero); + Callback.register "uint63 eqm1" (equal (sub zero one)); Callback.register "uint63 head0" head0; Callback.register "uint63 land" l_and; Callback.register "uint63 leq" le; + Callback.register "uint63 les" les; Callback.register "uint63 lor" l_or; Callback.register "uint63 lsl" l_sl; Callback.register "uint63 lsr" l_sr; + Callback.register "uint63 asr" a_sr; Callback.register "uint63 lt" lt; + Callback.register "uint63 lts" lts; Callback.register "uint63 lxor" l_xor; Callback.register "uint63 mod" rem; + Callback.register "uint63 mods" rems; Callback.register "uint63 mul" mul; Callback.register "uint63 mulc_ml" mulc; + Callback.register "uint63 zero" zero; Callback.register "uint63 one" one; Callback.register "uint63 sub" sub; + Callback.register "uint63 neg" (sub zero); Callback.register "uint63 subcarry" subcarry; Callback.register "uint63 tail0" tail0; Callback.register "uint63 of_float" of_float; diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 8d052d6593..d017dafd3c 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -53,6 +53,10 @@ let l_sl x y = let l_sr x y = if 0 <= y && y < 63 then x lsr y else 0 + (* arithmetic shift (for sint63) *) +let a_sr x y = + if 0 <= y && y < 63 then x asr y else 0 + let l_and x y = x land y [@@ocaml.inline always] @@ -84,6 +88,14 @@ let rem (x : int) (y : int) = let diveucl x y = (div x y, rem x y) + (* signed division *) +let divs (x : int) (y : int) = + if y = 0 then 0 else x / y + + (* modulo *) +let rems (x : int) (y : int) = + if y = 0 then 0 else x mod y + let addmuldiv p x y = l_or (l_sl x p) (l_sr y (uint_size - p)) @@ -96,6 +108,15 @@ let le (x : int) (y : int) = (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000) [@@ocaml.inline always] + (* signed comparison *) +let lts (x : int) (y : int) = + x < y +[@@ocaml.inline always] + +let les (x : int) (y : int) = + x <= y +[@@ocaml.inline always] + let to_int_min n m = if lt n m then n else m [@@ocaml.inline always] @@ -175,9 +196,10 @@ let equal (x : int) (y : int) = x = y let compare (x:int) (y:int) = let x = x lxor 0x4000000000000000 in let y = y lxor 0x4000000000000000 in - if x > y then 1 - else if y > x then -1 - else 0 + Int.compare x y + +let compares (x : int) (y : int) = + Int.compare x y (* head tail *) diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index d3af8bf09b..caa263432e 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -226,8 +226,11 @@ let check_prim_op = function | Int63mul -> opCHECKMULINT63 | Int63div -> opCHECKDIVINT63 | Int63mod -> opCHECKMODINT63 + | Int63divs -> opCHECKDIVSINT63 + | Int63mods -> opCHECKMODSINT63 | Int63lsr -> opCHECKLSRINT63 | Int63lsl -> opCHECKLSLINT63 + | Int63asr -> opCHECKASRINT63 | Int63land -> opCHECKLANDINT63 | Int63lor -> opCHECKLORINT63 | Int63lxor -> opCHECKLXORINT63 @@ -242,7 +245,10 @@ let check_prim_op = function | Int63eq -> opCHECKEQINT63 | Int63lt -> opCHECKLTINT63 | Int63le -> opCHECKLEINT63 + | Int63lts -> opCHECKLTSINT63 + | Int63les -> opCHECKLESINT63 | Int63compare -> opCHECKCOMPAREINT63 + | Int63compares -> opCHECKCOMPARESINT63 | Float64opp -> opCHECKOPPFLOAT | Float64abs -> opCHECKABSFLOAT | Float64eq -> opCHECKEQFLOAT diff --git a/plugins/syntax/dune b/plugins/syntax/dune index f930fc265a..ba53a439a0 100644 --- a/plugins/syntax/dune +++ b/plugins/syntax/dune @@ -6,13 +6,6 @@ (libraries coq.vernac)) (library - (name int63_syntax_plugin) - (public_name coq.plugins.int63_syntax) - (synopsis "Coq syntax plugin: int63") - (modules int63_syntax) - (libraries coq.vernac)) - -(library (name float_syntax_plugin) (public_name coq.plugins.float_syntax) (synopsis "Coq syntax plugin: float") diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml deleted file mode 100644 index 110b26581f..0000000000 --- a/plugins/syntax/int63_syntax.ml +++ /dev/null @@ -1,58 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "int63_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(* digit-based syntax for int63 *) - -open Names -open Libnames - -(*** Constants for locating int63 constructors ***) - -let q_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int" -let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.id_int" - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) - -(* int63 stuff *) -let int63_module = ["Coq"; "Numbers"; "Cyclic"; "Int63"; "PrimInt63"] -let int63_path = make_path int63_module "int" -let int63_scope = "int63_scope" - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -(* Actually declares the interpreter for int63 *) - -let _ = - let open Notation in - at_declare_ml_module - (fun () -> - let id_int63 = Nametab.locate q_id_int63 in - let o = { to_kind = Int63, Direct; - to_ty = id_int63; - to_post = [||]; - of_kind = Int63, Direct; - of_ty = id_int63; - ty_name = q_int63; - warning = Nop } in - enable_prim_token_interpretation - { pt_local = false; - pt_scope = int63_scope; - pt_interp_info = NumberNotation o; - pt_required = (int63_path, int63_module); - pt_refs = []; - pt_in_match = false }) - () diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml index 0e7640f430..80c11dc0d4 100644 --- a/plugins/syntax/number.ml +++ b/plugins/syntax/number.ml @@ -106,10 +106,12 @@ let locate_number () = let locate_int63 () = let int63n = "num.int63.type" in - if Coqlib.has_ref int63n + let pos_neg_int63n = "num.int63.pos_neg_int63" in + if Coqlib.has_ref int63n && Coqlib.has_ref pos_neg_int63n then - let q_int63 = qualid_of_ref int63n in - Some (mkRefC q_int63) + let q_pos_neg_int63 = qualid_of_ref pos_neg_int63n in + Some ({pos_neg_int63_ty = unsafe_locate_ind q_pos_neg_int63}, + mkRefC q_pos_neg_int63) else None let has_type env sigma f ty = @@ -121,13 +123,13 @@ let type_error_to f ty = CErrors.user_err (pr_qualid f ++ str " should go from Number.int to " ++ pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ - fnl () ++ str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).") + fnl () ++ str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).") let type_error_of g ty = CErrors.user_err (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ str " to Number.int or (option Number.int)." ++ fnl () ++ - str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).") + str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).") let warn_deprecated_decimal = CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" @@ -381,22 +383,37 @@ let elaborate_to_post_via env sigma ty_name ty_ind l = let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in to_post, pt_refs -let locate_global_inductive allow_params qid = - let locate_param_inductive qid = +type target_type = + | TargetInd of (inductive * GlobRef.t option list) + | TargetPrim of required_module + +let locate_global_inductive_with_params allow_params qid = + if not allow_params then raise Not_found else match Nametab.locate_extended qid with | Globnames.TrueGlobal _ -> raise Not_found | Globnames.SynDef kn -> match Syntax_def.search_syntactic_definition kn with - | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) when allow_params -> + | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) -> i, List.map (function | Notation_term.NRef (r,None) -> Some r | Notation_term.NHole _ -> None | _ -> raise Not_found) l - | _ -> raise Not_found in - try locate_param_inductive qid + | _ -> raise Not_found + +let locate_global_inductive allow_params qid = + try locate_global_inductive_with_params allow_params qid with Not_found -> Smartlocate.global_inductive_with_alias qid, [] +let locate_global_inductive_or_int63 allow_params qid = + try TargetInd (locate_global_inductive_with_params allow_params qid) + with Not_found -> + let int63n = "num.int63.type" in + if allow_params && Coqlib.has_ref int63n + && GlobRef.equal (Smartlocate.global_with_alias qid) (Coqlib.lib_ref int63n) + then TargetPrim (Nametab.path_of_global (Coqlib.lib_ref int63n), []) + else TargetInd (Smartlocate.global_inductive_with_alias qid, []) + let vernac_number_notation local ty f g opts scope = let rec parse_opts = function | [] -> None, Nop @@ -421,7 +438,7 @@ let vernac_number_notation local ty f g opts scope = let ty_name = ty in let ty, via = match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in - let tyc, params = locate_global_inductive (via = None) ty in + let tyc_params = locate_global_inductive_or_int63 (via = None) ty in let to_ty = Smartlocate.global_with_alias f in let of_ty = Smartlocate.global_with_alias g in let cty = mkRefC ty in @@ -451,11 +468,14 @@ let vernac_number_notation local ty f g opts scope = | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option | _ -> match int63_ty with - | Some cint63 when has_type env sigma f (arrow cint63 cty) -> Int63, Direct - | Some cint63 when has_type env sigma f (arrow cint63 (opt cty)) -> Int63, Option + | Some (pos_neg_int63_ty, cint63) when has_type env sigma f (arrow cint63 cty) -> Int63 pos_neg_int63_ty, Direct + | Some (pos_neg_int63_ty, cint63) when has_type env sigma f (arrow cint63 (opt cty)) -> Int63 pos_neg_int63_ty, Option | _ -> type_error_to f ty in (* Check the type of g *) + let cty = match tyc_params with + | TargetPrim _ -> mkRefC (qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int_wrapper") + | TargetInd _ -> cty in let of_kind = match num_ty with | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct @@ -476,8 +496,8 @@ let vernac_number_notation local ty f g opts scope = | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option | _ -> match int63_ty with - | Some cint63 when has_type env sigma g (arrow cty cint63) -> Int63, Direct - | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option + | Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty cint63) -> Int63 pos_neg_int63_ty, Direct + | Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty (opt cint63)) -> Int63 pos_neg_int63_ty, Option | _ -> type_error_of g ty in (match to_kind, of_kind with @@ -485,9 +505,14 @@ let vernac_number_notation local ty f g opts scope = | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> warn_deprecated_decimal () | _ -> ()); - let to_post, pt_refs = match via with - | None -> elaborate_to_post_params env sigma tyc params - | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in + let to_post, pt_required, pt_refs = match tyc_params with + | TargetPrim path -> [||], path, [Coqlib.lib_ref "num.int63.wrap_int"] + | TargetInd (tyc, params) -> + let to_post, pt_refs = + match via with + | None -> elaborate_to_post_params env sigma tyc params + | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in + to_post, (Nametab.path_of_global (GlobRef.IndRef tyc), []), pt_refs in let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; warning = opts } in @@ -498,7 +523,7 @@ let vernac_number_notation local ty f g opts scope = { pt_local = local; pt_scope = scope; pt_interp_info = NumberNotation o; - pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; + pt_required; pt_refs; pt_in_match = true } in diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index 7ca4de1e46..96af456891 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -15,9 +15,9 @@ 427 : int The command has indeed failed with message: -Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int +Cannot interpret this number as a value of type int The command has indeed failed with message: -Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int +Cannot interpret this number as a value of type int 0 : int 0 @@ -33,9 +33,11 @@ The reference x was not found in the current environment. add 2 2 : int The command has indeed failed with message: -int63 are only non-negative numbers. +Cannot interpret this number as a value of type int The command has indeed failed with message: overflow in int63 literal: 9223372036854775808 +0x1 + : int 2 : nat 2%int63 diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index 50910264f2..be0ee701af 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -20,6 +20,11 @@ Fail Check 0x. Check (PrimInt63.add 2 2). Fail Check -1. Fail Check 9223372036854775808. + +Set Printing All. +Check 1%int63. +Unset Printing All. + Open Scope nat_scope. Check 2. (* : nat *) Check 2%int63. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 3477a293e3..0b18981f4e 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -77,18 +77,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 184, characters 0-160: +File "stdin", line 187, characters 0-160: Warning: Notation "∀ _ .. _ , _" was already defined with a different format in scope type_scope. [notation-incompatible-format,parsing] ∀x : nat,x = x : Prop -File "stdin", line 197, characters 0-60: +File "stdin", line 200, characters 0-60: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 201, characters 0-64: +File "stdin", line 204, characters 0-64: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 206, characters 0-62: +File "stdin", line 209, characters 0-62: Warning: Lonely notation "_ %%%% _" was already defined with a different format. [notation-incompatible-format,parsing] 3 %% 4 @@ -97,10 +97,10 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 234, characters 0-61: +File "stdin", line 237, characters 0-61: Warning: The format modifier is irrelevant for only parsing rules. [irrelevant-format-only-parsing,parsing] -File "stdin", line 238, characters 0-63: +File "stdin", line 241, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] fun x : nat => U (S x) @@ -111,7 +111,7 @@ fun x : nat => V x : forall x : nat, nat * (?T -> ?T) where ?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) -File "stdin", line 255, characters 0-30: +File "stdin", line 258, characters 0-30: Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] 0 :=: 0 : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index ebad12af88..a5ec92fe3c 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -103,7 +103,10 @@ Module NumberNotations. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Number Notation myint63 of_int to_int : test17_scope. + Definition parse x := + match x with Pos x => Some (of_int x) | Neg _ => None end. + Definition print x := Pos (to_int x). + Number Notation myint63 parse print : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. End NumberNotations. diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out index 60682edec8..df9b39389c 100644 --- a/test-suite/output/NumberNotations.out +++ b/test-suite/output/NumberNotations.out @@ -260,28 +260,28 @@ The command has indeed failed with message: add is not a constructor of an inductive type. The command has indeed failed with message: Missing mapping for constructor Iempty. -File "stdin", line 574, characters 56-61: +File "stdin", line 577, characters 56-61: Warning: Type of I'sum seems incompatible with the type of sum. Expected type is: (I' -> I' -> I') instead of (I -> I' -> I'). This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] -File "stdin", line 579, characters 32-33: +File "stdin", line 582, characters 32-33: Warning: I was already mapped to Set, mapping it also to nat might yield ill typed terms when using the notation. [via-type-remapping,numbers] -File "stdin", line 579, characters 37-42: +File "stdin", line 582, characters 37-42: Warning: Type of Iunit seems incompatible with the type of O. Expected type is: I instead of I. This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] The command has indeed failed with message: 'via' and 'abstract' cannot be used together. -File "stdin", line 659, characters 21-23: +File "stdin", line 662, characters 21-23: Warning: Type of I1 seems incompatible with the type of Fin.F1. Expected type is: (nat -> I) instead of I. This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] -File "stdin", line 659, characters 35-37: +File "stdin", line 662, characters 35-37: Warning: Type of IS seems incompatible with the type of Fin.FS. Expected type is: (nat -> I -> I) instead of (I -> I). This might yield ill typed terms when using the notation. diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v index 718da13500..85400c2fd4 100644 --- a/test-suite/output/NumberNotations.v +++ b/test-suite/output/NumberNotations.v @@ -328,7 +328,10 @@ Module Test17. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Number Notation myint63 of_int to_int : test17_scope. + Definition parse x := + match x with Pos x => Some (of_int x) | Neg _ => None end. + Definition print x := Pos (to_int x). + Number Notation myint63 parse print : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. diff --git a/test-suite/output/Sint63Syntax.out b/test-suite/output/Sint63Syntax.out new file mode 100644 index 0000000000..db14658307 --- /dev/null +++ b/test-suite/output/Sint63Syntax.out @@ -0,0 +1,66 @@ +2%sint63 + : int +2 + : int +-3 + : int +4611686018427387903 + : int +-4611686018427387904 + : int +427 + : int +427 + : int +427 + : int +427 + : int +427 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +0 + : int +0 + : int +The command has indeed failed with message: +The reference xg was not found in the current environment. +The command has indeed failed with message: +The reference xG was not found in the current environment. +The command has indeed failed with message: +The reference x1 was not found in the current environment. +The command has indeed failed with message: +The reference x was not found in the current environment. +2 + 2 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +0x1%int63 + : int +0x7fffffffffffffff%int63 + : int +2 + : nat +2%sint63 + : int +t = 2%si63 + : int +t = 2%si63 + : int +2 + : nat +2 + : int +(2 + 2)%sint63 + : int +2 + 2 + : int + = 4 + : int + = 37151199385380486 + : int diff --git a/test-suite/output/Sint63Syntax.v b/test-suite/output/Sint63Syntax.v new file mode 100644 index 0000000000..b9ed596537 --- /dev/null +++ b/test-suite/output/Sint63Syntax.v @@ -0,0 +1,49 @@ +Require Import Sint63. + +Check 2%sint63. +Open Scope sint63_scope. +Check 2. +Check -3. +Check 4611686018427387903. +Check -4611686018427387904. +Check 0x1ab. +Check 0X1ab. +Check 0x1Ab. +Check 0x1aB. +Check 0x1AB. +Fail Check 0x1ap5. (* exponents not implemented (yet?) *) +Fail Check 0x1aP5. +Check 0x0. +Check 0x000. +Fail Check 0xg. +Fail Check 0xG. +Fail Check 00x1. +Fail Check 0x. +Check (PrimInt63.add 2 2). +Fail Check 4611686018427387904. +Fail Check -4611686018427387905. + +Set Printing All. +Check 1%sint63. +Check (-1)%sint63. +Unset Printing All. + +Open Scope nat_scope. +Check 2. (* : nat *) +Check 2%sint63. +Delimit Scope sint63_scope with si63. +Definition t := 2%sint63. +Print t. +Delimit Scope nat_scope with sint63. +Print t. +Check 2. +Close Scope nat_scope. +Check 2. +Close Scope sint63_scope. +Delimit Scope sint63_scope with sint63. + +Check (2 + 2)%sint63. +Open Scope sint63_scope. +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. diff --git a/test-suite/primitive/sint63/add.v b/test-suite/primitive/sint63/add.v new file mode 100644 index 0000000000..dcafd64181 --- /dev/null +++ b/test-suite/primitive/sint63/add.v @@ -0,0 +1,25 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 2 + 3 = 5). +Check (eq_refl 5 <: 2 + 3 = 5). +Check (eq_refl 5 <<: 2 + 3 = 5). +Definition compute1 := Eval compute in 2 + 3. +Check (eq_refl compute1 : 5 = 5). + +Check (eq_refl : 4611686018427387903 + 1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: + 4611686018427387903 + 1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: + 4611686018427387903 + 1 = -4611686018427387904). +Definition compute2 := Eval compute in 4611686018427387903 + 1. +Check (eq_refl compute2 : -4611686018427387904 = -4611686018427387904). + +Check (eq_refl : 2 - 3 = -1). +Check (eq_refl (-1) <: 2 - 3 = -1). +Check (eq_refl (-1) <<: 2 - 3 = -1). +Definition compute3 := Eval compute in 2 - 3. +Check (eq_refl compute3 : -1 = -1). diff --git a/test-suite/primitive/sint63/asr.v b/test-suite/primitive/sint63/asr.v new file mode 100644 index 0000000000..4524ae4e6f --- /dev/null +++ b/test-suite/primitive/sint63/asr.v @@ -0,0 +1,41 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : (-2305843009213693952) >> 61 = -1). +Check (eq_refl (-1) <: (-2305843009213693952) >> 61 = -1). +Check (eq_refl (-1) <<: (-2305843009213693952) >> 61 = -1). +Definition compute1 := Eval compute in (-2305843009213693952) >> 61. +Check (eq_refl compute1 : -1 = -1). + +Check (eq_refl : 2305843009213693952 >> 62 = 0). +Check (eq_refl 0 <: 2305843009213693952 >> 62 = 0). +Check (eq_refl 0 <<: 2305843009213693952 >> 62 = 0). +Definition compute2 := Eval compute in 2305843009213693952 >> 62. +Check (eq_refl compute2 : 0 = 0). + +Check (eq_refl : 4611686018427387903 >> 63 = 0). +Check (eq_refl 0 <: 4611686018427387903 >> 63 = 0). +Check (eq_refl 0 <<: 4611686018427387903 >> 63 = 0). +Definition compute3 := Eval compute in 4611686018427387903 >> 63. +Check (eq_refl compute3 : 0 = 0). + +Check (eq_refl : (-1) >> 1 = -1). +Check (eq_refl (-1) <: (-1) >> 1 = -1). +Check (eq_refl (-1) <<: (-1) >> 1 = -1). +Definition compute4 := Eval compute in (-1) >> 1. +Check (eq_refl compute4 : -1 = -1). + +Check (eq_refl : (-1) >> (-1) = 0). +Check (eq_refl 0 <: (-1) >> (-1) = 0). +Check (eq_refl 0 <<: (-1) >> (-1) = 0). +Definition compute5 := Eval compute in (-1) >> (-1). +Check (eq_refl compute5 : 0 = 0). + +Check (eq_refl : 73 >> (-2) = 0). +Check (eq_refl 0 <: 73 >> (-2) = 0). +Check (eq_refl 0 <<: 73 >> (-2) = 0). +Definition compute6 := Eval compute in 73 >> (-2). +Check (eq_refl compute6 : 0 = 0). diff --git a/test-suite/primitive/sint63/compare.v b/test-suite/primitive/sint63/compare.v new file mode 100644 index 0000000000..7a9882f1c8 --- /dev/null +++ b/test-suite/primitive/sint63/compare.v @@ -0,0 +1,36 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 ?= 1 = Eq). +Check (eq_refl Eq <: 1 ?= 1 = Eq). +Check (eq_refl Eq <<: 1 ?= 1 = Eq). +Definition compute1 := Eval compute in 1 ?= 1. +Check (eq_refl compute1 : Eq = Eq). + +Check (eq_refl : 1 ?= 2 = Lt). +Check (eq_refl Lt <: 1 ?= 2 = Lt). +Check (eq_refl Lt <<: 1 ?= 2 = Lt). +Definition compute2 := Eval compute in 1 ?= 2. +Check (eq_refl compute2 : Lt = Lt). + +Check (eq_refl : 4611686018427387903 ?= 0 = Gt). +Check (eq_refl Gt <: 4611686018427387903 ?= 0 = Gt). +Check (eq_refl Gt <<: 4611686018427387903 ?= 0 = Gt). +Definition compute3 := Eval compute in 4611686018427387903 ?= 0. +Check (eq_refl compute3 : Gt = Gt). + +Check (eq_refl : -1 ?= 1 = Lt). +Check (eq_refl Lt <: -1 ?= 1 = Lt). +Check (eq_refl Lt <<: -1 ?= 1 = Lt). +Definition compute4 := Eval compute in -1 ?= 1. +Check (eq_refl compute4 : Lt = Lt). + +Check (eq_refl : 4611686018427387903 ?= -4611686018427387904 = Gt). +Check (eq_refl Gt <: 4611686018427387903 ?= -4611686018427387904 = Gt). +Check (eq_refl Gt <<: 4611686018427387903 ?= -4611686018427387904 = Gt). +Definition compute5 := + Eval compute in 4611686018427387903 ?= -4611686018427387904. +Check (eq_refl compute5 : Gt = Gt). diff --git a/test-suite/primitive/sint63/div.v b/test-suite/primitive/sint63/div.v new file mode 100644 index 0000000000..9da628ce1e --- /dev/null +++ b/test-suite/primitive/sint63/div.v @@ -0,0 +1,61 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 6 / 3 = 2). +Check (eq_refl 2 <: 6 / 3 = 2). +Check (eq_refl 2 <<: 6 / 3 = 2). +Definition compute1 := Eval compute in 6 / 3. +Check (eq_refl compute1 : 2 = 2). + +Check (eq_refl : -6 / 3 = -2). +Check (eq_refl (-2) <: -6 / 3 = -2). +Check (eq_refl (-2) <<: -6 / 3 = -2). +Definition compute2 := Eval compute in -6 / 3. +Check (eq_refl compute2 : -2 = -2). + +Check (eq_refl : 6 / -3 = -2). +Check (eq_refl (-2) <: 6 / -3 = -2). +Check (eq_refl (-2) <<: 6 / -3 = -2). +Definition compute3 := Eval compute in 6 / -3. +Check (eq_refl compute3 : -2 = -2). + +Check (eq_refl : -6 / -3 = 2). +Check (eq_refl 2 <: -6 / -3 = 2). +Check (eq_refl 2 <<: -6 / -3 = 2). +Definition compute4 := Eval compute in -6 / -3. +Check (eq_refl compute4 : 2 = 2). + +Check (eq_refl : 3 / 2 = 1). +Check (eq_refl 1 <: 3 / 2 = 1). +Check (eq_refl 1 <<: 3 / 2 = 1). +Definition compute5 := Eval compute in 3 / 2. +Check (eq_refl compute5 : 1 = 1). + +Check (eq_refl : -3 / 2 = -1). +Check (eq_refl (-1) <: -3 / 2 = -1). +Check (eq_refl (-1) <<: -3 / 2 = -1). +Definition compute6 := Eval compute in -3 / 2. +Check (eq_refl compute6 : -1 = -1). + +Check (eq_refl : 3 / -2 = -1). +Check (eq_refl (-1) <: 3 / -2 = -1). +Check (eq_refl (-1) <<: 3 / -2 = -1). +Definition compute7 := Eval compute in 3 / -2. +Check (eq_refl compute7 : -1 = -1). + +Check (eq_refl : -3 / -2 = 1). +Check (eq_refl 1 <: -3 / -2 = 1). +Check (eq_refl 1 <<: -3 / -2 = 1). +Definition compute8 := Eval compute in -3 / -2. +Check (eq_refl compute8 : 1 = 1). + +Check (eq_refl : -4611686018427387904 / -1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: + -4611686018427387904 / -1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: + -4611686018427387904 / -1 = -4611686018427387904). +Definition compute9 := Eval compute in -4611686018427387904 / -1. +Check (eq_refl compute9 : -4611686018427387904 = -4611686018427387904). diff --git a/test-suite/primitive/sint63/eqb.v b/test-suite/primitive/sint63/eqb.v new file mode 100644 index 0000000000..4d365acf54 --- /dev/null +++ b/test-suite/primitive/sint63/eqb.v @@ -0,0 +1,17 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 =? 1 = true). +Check (eq_refl true <: 1 =? 1 = true). +Check (eq_refl true <<: 1 =? 1 = true). +Definition compute1 := Eval compute in 1 =? 1. +Check (eq_refl compute1 : true = true). + +Check (eq_refl : 4611686018427387903 =? 0 = false). +Check (eq_refl false <: 4611686018427387903 =? 0 = false). +Check (eq_refl false <<: 4611686018427387903 =? 0 = false). +Definition compute2 := Eval compute in 4611686018427387903 =? 0. +Check (eq_refl compute2 : false = false). diff --git a/test-suite/primitive/sint63/isint.v b/test-suite/primitive/sint63/isint.v new file mode 100644 index 0000000000..f1c9c2cfd1 --- /dev/null +++ b/test-suite/primitive/sint63/isint.v @@ -0,0 +1,50 @@ +(* This file tests the check that arithmetic operations use to know if their +arguments are ground. The various test cases correspond to possible +optimizations of these tests made by the compiler. *) +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Section test. + +Variable m n : int. + +Check (eq_refl : (fun x => x + 3) m = m + 3). +Check (eq_refl (m + 3) <: (fun x => x + 3) m = m + 3). +Check (eq_refl (m + 3) <<: (fun x => x + 3) m = m + 3). +Definition compute1 := Eval compute in (fun x => x + 3) m. +Check (eq_refl compute1 : m + 3 = m + 3). + +Check (eq_refl : (fun x => 3 + x) m = 3 + m). +Check (eq_refl (3 + m) <: (fun x => 3 + x) m = 3 + m). +Check (eq_refl (3 + m) <<: (fun x => 3 + x) m = 3 + m). +Definition compute2 := Eval compute in (fun x => 3 + x) m. +Check (eq_refl compute2 : 3 + m = 3 + m). + +Check (eq_refl : (fun x y => x + y) m n = m + n). +Check (eq_refl (m + n) <: (fun x y => x + y) m n = m + n). +Check (eq_refl (m + n) <<: (fun x y => x + y) m n = m + n). +Definition compute3 := Eval compute in (fun x y => x + y) m n. +Check (eq_refl compute3 : m + n = m + n). + +Check (eq_refl : (fun x y => x + y) 2 3 = 5). +Check (eq_refl 5 <: (fun x y => x + y) 2 3 = 5). +Check (eq_refl 5 <<: (fun x y => x + y) 2 3 = 5). +Definition compute4 := Eval compute in (fun x y => x + y) 2 3. +Check (eq_refl compute4 : 5 = 5). + +Check (eq_refl : (fun x => x + x) m = m + m). +Check (eq_refl (m + m) <: (fun x => x + x) m = m + m). +Check (eq_refl (m + m) <<: (fun x => x + x) m = m + m). +Definition compute5 := Eval compute in (fun x => x + x) m. +Check (eq_refl compute5 : m + m = m + m). + +Check (eq_refl : (fun x => x + x) 2 = 4). +Check (eq_refl 4 <: (fun x => x + x) 2 = 4). +Check (eq_refl 4 <<: (fun x => x + x) 2 = 4). +Definition compute6 := Eval compute in (fun x => x + x) 2. +Check (eq_refl compute6 : 4 = 4). + +End test. diff --git a/test-suite/primitive/sint63/leb.v b/test-suite/primitive/sint63/leb.v new file mode 100644 index 0000000000..dbe958e41d --- /dev/null +++ b/test-suite/primitive/sint63/leb.v @@ -0,0 +1,29 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 <=? 1 = true). +Check (eq_refl true <: 1 <=? 1 = true). +Check (eq_refl true <<: 1 <=? 1 = true). +Definition compute1 := Eval compute in 1 <=? 1. +Check (eq_refl compute1 : true = true). + +Check (eq_refl : 1 <=? 2 = true). +Check (eq_refl true <: 1 <=? 2 = true). +Check (eq_refl true <<: 1 <=? 2 = true). +Definition compute2 := Eval compute in 1 <=? 2. +Check (eq_refl compute2 : true = true). + +Check (eq_refl : 4611686018427387903 <=? 0 = false). +Check (eq_refl false <: 4611686018427387903 <=? 0 = false). +Check (eq_refl false <<: 4611686018427387903 <=? 0 = false). +Definition compute3 := Eval compute in 4611686018427387903 <=? 0. +Check (eq_refl compute3 : false = false). + +Check (eq_refl : 1 <=? -1 = false). +Check (eq_refl false <: 1 <=? -1 = false). +Check (eq_refl false <<: 1 <=? -1 = false). +Definition compute4 := Eval compute in 1 <=? -1. +Check (eq_refl compute4 : false = false). diff --git a/test-suite/primitive/sint63/lsl.v b/test-suite/primitive/sint63/lsl.v new file mode 100644 index 0000000000..082c42979a --- /dev/null +++ b/test-suite/primitive/sint63/lsl.v @@ -0,0 +1,43 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 3 << 61 = -2305843009213693952). +Check (eq_refl (-2305843009213693952) <: 3 << 61 = -2305843009213693952). +Check (eq_refl (-2305843009213693952) <<: 3 << 61 = -2305843009213693952). +Definition compute1 := Eval compute in 3 << 61. +Check (eq_refl compute1 : -2305843009213693952 = -2305843009213693952). + +Check (eq_refl : 2 << 62 = 0). +Check (eq_refl 0 <: 2 << 62 = 0). +Check (eq_refl 0 <<: 2 << 62 = 0). +Definition compute2 := Eval compute in 2 << 62. +Check (eq_refl compute2 : 0 = 0). + +Check (eq_refl : 4611686018427387903 << 63 = 0). +Check (eq_refl 0 <: 4611686018427387903 << 63 = 0). +Check (eq_refl 0 <<: 4611686018427387903 << 63 = 0). +Definition compute3 := Eval compute in 4611686018427387903 << 63. +Check (eq_refl compute3 : 0 = 0). + +Check (eq_refl : 4611686018427387903 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: + 4611686018427387903 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: + 4611686018427387903 << 62 = -4611686018427387904). +Definition compute4 := Eval compute in 4611686018427387903 << 62. +Check (eq_refl compute4 : -4611686018427387904 = -4611686018427387904). + +Check (eq_refl : 1 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: 1 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: 1 << 62 = -4611686018427387904). +Definition compute5 := Eval compute in 1 << 62. +Check (eq_refl compute5 : -4611686018427387904 = -4611686018427387904). + +Check (eq_refl : -1 << 1 = -2). +Check (eq_refl (-2) <: -1 << 1 = -2). +Check (eq_refl (-2) <<: -1 << 1 = -2). +Definition compute6 := Eval compute in -1 << 1. +Check (eq_refl compute6 : -2 = -2). diff --git a/test-suite/primitive/sint63/ltb.v b/test-suite/primitive/sint63/ltb.v new file mode 100644 index 0000000000..aa72e1d377 --- /dev/null +++ b/test-suite/primitive/sint63/ltb.v @@ -0,0 +1,29 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 <? 1 = false). +Check (eq_refl false <: 1 <? 1 = false). +Check (eq_refl false <<: 1 <? 1 = false). +Definition compute1 := Eval compute in 1 <? 1. +Check (eq_refl compute1 : false = false). + +Check (eq_refl : 1 <? 2 = true). +Check (eq_refl true <: 1 <? 2 = true). +Check (eq_refl true <<: 1 <? 2 = true). +Definition compute2 := Eval compute in 1 <? 2. +Check (eq_refl compute2 : true = true). + +Check (eq_refl : 4611686018427387903 <? 0 = false). +Check (eq_refl false <: 4611686018427387903 <? 0 = false). +Check (eq_refl false <<: 4611686018427387903 <? 0 = false). +Definition compute3 := Eval compute in 4611686018427387903 <? 0. +Check (eq_refl compute3 : false = false). + +Check (eq_refl : 1 <? -1 = false). +Check (eq_refl false <: 1 <? -1 = false). +Check (eq_refl false <<: 1 <? -1 = false). +Definition compute4 := Eval compute in 1 <? -1. +Check (eq_refl compute4 : false = false). diff --git a/test-suite/primitive/sint63/mod.v b/test-suite/primitive/sint63/mod.v new file mode 100644 index 0000000000..a4872b45f3 --- /dev/null +++ b/test-suite/primitive/sint63/mod.v @@ -0,0 +1,53 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 6 mod 3 = 0). +Check (eq_refl 0 <: 6 mod 3 = 0). +Check (eq_refl 0 <<: 6 mod 3 = 0). +Definition compute1 := Eval compute in 6 mod 3. +Check (eq_refl compute1 : 0 = 0). + +Check (eq_refl : -6 mod 3 = 0). +Check (eq_refl 0 <: -6 mod 3 = 0). +Check (eq_refl 0 <<: -6 mod 3 = 0). +Definition compute2 := Eval compute in -6 mod 3. +Check (eq_refl compute2 : 0 = 0). + +Check (eq_refl : 6 mod -3 = 0). +Check (eq_refl 0 <: 6 mod -3 = 0). +Check (eq_refl 0 <<: 6 mod -3 = 0). +Definition compute3 := Eval compute in 6 mod -3. +Check (eq_refl compute3 : 0 = 0). + +Check (eq_refl : -6 mod -3 = 0). +Check (eq_refl 0 <: -6 mod -3 = 0). +Check (eq_refl 0 <<: -6 mod -3 = 0). +Definition compute4 := Eval compute in -6 mod -3. +Check (eq_refl compute4 : 0 = 0). + +Check (eq_refl : 5 mod 3 = 2). +Check (eq_refl 2 <: 5 mod 3 = 2). +Check (eq_refl 2 <<: 5 mod 3 = 2). +Definition compute5 := Eval compute in 5 mod 3. +Check (eq_refl compute5 : 2 = 2). + +Check (eq_refl : -5 mod 3 = -2). +Check (eq_refl (-2) <: -5 mod 3 = -2). +Check (eq_refl (-2) <<: -5 mod 3 = -2). +Definition compute6 := Eval compute in -5 mod 3. +Check (eq_refl compute6 : -2 = -2). + +Check (eq_refl : 5 mod -3 = 2). +Check (eq_refl 2 <: 5 mod -3 = 2). +Check (eq_refl 2 <<: 5 mod -3 = 2). +Definition compute7 := Eval compute in 5 mod -3. +Check (eq_refl compute7 : 2 = 2). + +Check (eq_refl : -5 mod -3 = -2). +Check (eq_refl (-2) <: -5 mod -3 = -2). +Check (eq_refl (-2) <<: -5 mod -3 = -2). +Definition compute8 := Eval compute in -5 mod -3. +Check (eq_refl compute8 : -2 = -2). diff --git a/test-suite/primitive/sint63/mul.v b/test-suite/primitive/sint63/mul.v new file mode 100644 index 0000000000..f72f643083 --- /dev/null +++ b/test-suite/primitive/sint63/mul.v @@ -0,0 +1,35 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 2 * 3 = 6). +Check (eq_refl 6 <: 2 * 3 = 6). +Check (eq_refl 6 <<: 2 * 3 = 6). +Definition compute1 := Eval compute in 2 * 3. +Check (eq_refl compute1 : 6 = 6). + +Check (eq_refl : -2 * 3 = -6). +Check (eq_refl (-6) <: -2 * 3 = -6). +Check (eq_refl (-6) <<: -2 * 3 = -6). +Definition compute2 := Eval compute in -2 * 3. +Check (eq_refl compute2 : -6 = -6). + +Check (eq_refl : 2 * -3 = -6). +Check (eq_refl (-6) <: 2 * -3 = -6). +Check (eq_refl (-6) <<: 2 * -3 = -6). +Definition compute3 := Eval compute in 2 * -3. +Check (eq_refl compute3 : -6 = -6). + +Check (eq_refl : -2 * -3 = 6). +Check (eq_refl 6 <: -2 * -3 = 6). +Check (eq_refl 6 <<: -2 * -3 = 6). +Definition compute4 := Eval compute in -2 * -3. +Check (eq_refl compute4 : 6 = 6). + +Check (eq_refl : 4611686018427387903 * 2 = -2). +Check (eq_refl (-2) <: 4611686018427387903 * 2 = -2). +Check (eq_refl (-2) <<: 4611686018427387903 * 2 = -2). +Definition compute5 := Eval compute in 4611686018427387903 * 2. +Check (eq_refl compute5 : -2 = -2). diff --git a/test-suite/primitive/sint63/signed.v b/test-suite/primitive/sint63/signed.v new file mode 100644 index 0000000000..d8333a8efb --- /dev/null +++ b/test-suite/primitive/sint63/signed.v @@ -0,0 +1,18 @@ +(* This file checks that operations over sint63 are signed. *) +Require Import Sint63. + +Open Scope sint63_scope. + +(* (0-1) must be negative 1 and not the maximum integer value *) + +Check (eq_refl : 1/(0-1) = -1). +Check (eq_refl (-1) <: 1/(0-1) = -1). +Check (eq_refl (-1) <<: 1/(0-1) = -1). +Definition compute1 := Eval compute in 1/(0-1). +Check (eq_refl compute1 : -1 = -1). + +Check (eq_refl : 3 mod (0-1) = 0). +Check (eq_refl 0 <: 3 mod (0-1) = 0). +Check (eq_refl 0 <<: 3 mod (0-1) = 0). +Definition compute2 := Eval compute in 3 mod (0-1). +Check (eq_refl compute2 : 0 = 0). diff --git a/test-suite/primitive/sint63/sub.v b/test-suite/primitive/sint63/sub.v new file mode 100644 index 0000000000..8504177286 --- /dev/null +++ b/test-suite/primitive/sint63/sub.v @@ -0,0 +1,25 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 3 - 2 = 1). +Check (eq_refl 1 <: 3 - 2 = 1). +Check (eq_refl 1 <<: 3 - 2 = 1). +Definition compute1 := Eval compute in 3 - 2. +Check (eq_refl compute1 : 1 = 1). + +Check (eq_refl : 0 - 1 = -1). +Check (eq_refl (-1) <: 0 - 1 = -1). +Check (eq_refl (-1) <<: 0 - 1 = -1). +Definition compute2 := Eval compute in 0 - 1. +Check (eq_refl compute2 : -1 = -1). + +Check (eq_refl : -4611686018427387904 - 1 = 4611686018427387903). +Check (eq_refl 4611686018427387903 <: + -4611686018427387904 - 1 = 4611686018427387903). +Check (eq_refl 4611686018427387903 <<: + -4611686018427387904 - 1 = 4611686018427387903). +Definition compute3 := Eval compute in -4611686018427387904 - 1. +Check (eq_refl compute3 : 4611686018427387903 = 4611686018427387903). diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 7bb725538b..a3ebe67325 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -205,6 +205,7 @@ Qed. Corollary to_Z_bounded : forall x, (0 <= φ x < wB)%Z. Proof. apply to_Z_rec_bounded. Qed. + (* =================================================== *) Local Open Scope Z_scope. (* General arithmetic results *) @@ -1904,6 +1905,22 @@ Qed. Lemma lxor0_r i : i lxor 0 = i. Proof. rewrite lxorC; exact (lxor0 i). Qed. +Lemma opp_to_Z_opp (x : int) : + φ x mod wB <> 0 -> + (- φ (- x)) mod wB = (φ x) mod wB. +Proof. + intros neqx0. + rewrite opp_spec. + rewrite (Z_mod_nz_opp_full (φ x%int63)) by assumption. + rewrite (Z.mod_small (φ x%int63)) by apply to_Z_bounded. + rewrite <- Z.add_opp_l. + rewrite Z.opp_add_distr, Z.opp_involutive. + replace (- wB) with (-1 * wB) by easy. + rewrite Z_mod_plus by easy. + now rewrite Z.mod_small by apply to_Z_bounded. +Qed. + + Module Export Int63Notations. Local Open Scope int63_scope. #[deprecated(since="8.13",note="use infix mod instead")] diff --git a/theories/Numbers/Cyclic/Int63/PrimInt63.v b/theories/Numbers/Cyclic/Int63/PrimInt63.v index 64c1b862c7..98127ef0ac 100644 --- a/theories/Numbers/Cyclic/Int63/PrimInt63.v +++ b/theories/Numbers/Cyclic/Int63/PrimInt63.v @@ -17,11 +17,21 @@ Register comparison as kernel.ind_cmp. Primitive int := #int63_type. Register int as num.int63.type. +Variant pos_neg_int63 := Pos (d:int) | Neg (d:int). +Register pos_neg_int63 as num.int63.pos_neg_int63. Declare Scope int63_scope. Definition id_int : int -> int := fun x => x. -Declare ML Module "int63_syntax_plugin". - -Module Export Int63NotationsInternalA. +Record int_wrapper := wrap_int {int_wrap : int}. +Register wrap_int as num.int63.wrap_int. +Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x). +Definition parser (x : pos_neg_int63) : option int := + match x with + | Pos p => Some p + | Neg _ => None + end. +Number Notation int parser printer : int63_scope. + +Module Import Int63NotationsInternalA. Delimit Scope int63_scope with int63. Bind Scope int63_scope with int. End Int63NotationsInternalA. @@ -37,6 +47,9 @@ Primitive lor := #int63_lor. Primitive lxor := #int63_lxor. + +Primitive asr := #int63_asr. + (* Arithmetic modulo operations *) Primitive add := #int63_add. @@ -50,6 +63,10 @@ Primitive div := #int63_div. Primitive mod := #int63_mod. +Primitive divs := #int63_divs. + +Primitive mods := #int63_mods. + (* Comparisons *) Primitive eqb := #int63_eq. @@ -57,6 +74,10 @@ Primitive ltb := #int63_lt. Primitive leb := #int63_le. +Primitive ltsb := #int63_lts. + +Primitive lesb := #int63_les. + (** Exact arithmetic operations *) Primitive addc := #int63_addc. @@ -76,7 +97,13 @@ Primitive addmuldiv := #int63_addmuldiv. (** Comparison *) Primitive compare := #int63_compare. +Primitive compares := #int63_compares. + (** Exotic operations *) Primitive head0 := #int63_head0. Primitive tail0 := #int63_tail0. + +Module Export PrimInt63Notations. + Export Int63NotationsInternalA. +End PrimInt63Notations. diff --git a/theories/Numbers/Cyclic/Int63/Sint63.v b/theories/Numbers/Cyclic/Int63/Sint63.v new file mode 100644 index 0000000000..c0239ae3db --- /dev/null +++ b/theories/Numbers/Cyclic/Int63/Sint63.v @@ -0,0 +1,407 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import ZArith. +Import Znumtheory. +Require Export Int63. +Require Import Lia. + +Declare Scope sint63_scope. +Definition printer (x : int_wrapper) : pos_neg_int63 := + if (int_wrap x <? 4611686018427387904)%int63 then (* 2^62 *) + Pos (int_wrap x) + else + Neg ((int_wrap x) lxor max_int + 1)%int63. +Definition parser (x : pos_neg_int63) : option int := + match x with + | Pos p => if (p <? 4611686018427387904)%int63 then Some p else None + | Neg n => if (n <=? 4611686018427387904)%int63 + then Some ((n - 1) lxor max_int)%int63 else None + end. +Number Notation int parser printer : sint63_scope. + + +Module Import Sint63NotationsInternalA. +Delimit Scope sint63_scope with sint63. +Bind Scope sint63_scope with int. +End Sint63NotationsInternalA. + + +Module Import Sint63NotationsInternalB. +Infix "<<" := Int63.lsl (at level 30, no associativity) : sint63_scope. +(* TODO do we want >> to be asr or lsr? And is there a notation for the other one? *) +Infix ">>" := asr (at level 30, no associativity) : sint63_scope. +Infix "land" := Int63.land (at level 40, left associativity) : sint63_scope. +Infix "lor" := Int63.lor (at level 40, left associativity) : sint63_scope. +Infix "lxor" := Int63.lxor (at level 40, left associativity) : sint63_scope. +Infix "+" := Int63.add : sint63_scope. +Infix "-" := Int63.sub : sint63_scope. +Infix "*" := Int63.mul : sint63_scope. +Infix "/" := divs : sint63_scope. +Infix "mod" := mods (at level 40, no associativity) : sint63_scope. +Infix "=?" := Int63.eqb (at level 70, no associativity) : sint63_scope. +Infix "<?" := ltsb (at level 70, no associativity) : sint63_scope. +Infix "<=?" := lesb (at level 70, no associativity) : sint63_scope. +Infix "≤?" := lesb (at level 70, no associativity) : sint63_scope. +Notation "- x" := (opp x) : sint63_scope. +Notation "n ?= m" := (compares n m) (at level 70, no associativity) : sint63_scope. +End Sint63NotationsInternalB. + +Definition min_int := Eval vm_compute in (lsl 1 62). +Definition max_int := Eval vm_compute in (min_int - 1)%sint63. + +(** Translation to and from Z *) +Definition to_Z (i:int) := + if (i <? min_int)%int63 then + φ i%int63 + else + (- φ (- i)%int63)%Z. + +Lemma to_Z_0 : to_Z 0 = 0. +Proof. easy. Qed. + +Lemma to_Z_min : to_Z min_int = - (wB / 2). +Proof. easy. Qed. + +Lemma to_Z_max : to_Z max_int = wB / 2 - 1. +Proof. easy. Qed. + +Lemma to_Z_bounded : forall x, (to_Z min_int <= to_Z x <= to_Z max_int)%Z. +Proof. + intros x; unfold to_Z. + case ltbP; [> lia | intros _]. + case (ltbP max_int); [> intros _ | now intros H; exfalso; apply H]. + rewrite opp_spec. + rewrite Z_mod_nz_opp_full by easy. + rewrite Z.mod_small by apply Int63.to_Z_bounded. + case ltbP. + - intros ltxmin; split. + + now transitivity 0%Z; [>| now apply Int63.to_Z_bounded]. + + replace (φ min_int%int63) with (φ max_int%int63 + 1)%Z in ltxmin. + * lia. + * now compute. + - rewrite Z.nlt_ge; intros leminx. + rewrite opp_spec. + rewrite Z_mod_nz_opp_full. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + split. + * rewrite <- Z.opp_le_mono. + now rewrite <- Z.sub_le_mono_l. + * transitivity 0%Z; [>| now apply Int63.to_Z_bounded]. + rewrite Z.opp_nonpos_nonneg. + apply Zle_minus_le_0. + apply Z.lt_le_incl. + now apply Int63.to_Z_bounded. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + now intros eqx0; rewrite eqx0 in leminx. +Qed. + +Lemma of_to_Z : forall x, of_Z (to_Z x) = x. +Proof. + unfold to_Z, of_Z. + intros x. + generalize (Int63.to_Z_bounded x). + case ltbP. + - intros ltxmin [leq0x _]. + generalize (Int63.of_to_Z x). + destruct (φ x%int63). + + now intros <-. + + now intros <-; unfold Int63.of_Z. + + now intros _. + - intros nltxmin leq0xltwB. + rewrite (opp_spec x). + rewrite Z_mod_nz_opp_full. + + rewrite Zmod_small by easy. + destruct (wB - φ x%int63) eqn: iswbmx. + * lia. + * simpl. + apply to_Z_inj. + rewrite opp_spec. + generalize (of_Z_spec (Z.pos p)). + simpl Int63.of_Z; intros ->. + rewrite <- iswbmx. + rewrite <- Z.sub_0_l. + rewrite <- (Zmod_0_l wB). + rewrite <- Zminus_mod. + replace (0 - _) with (φ x%int63 - wB) by ring. + rewrite <- Zminus_mod_idemp_r. + rewrite Z_mod_same_full. + rewrite Z.sub_0_r. + now rewrite Z.mod_small. + * lia. + + rewrite Z.mod_small by easy. + intros eqx0; revert nltxmin; rewrite eqx0. + now compute. +Qed. + +Lemma to_Z_inj (x y : int) : to_Z x = to_Z y -> x = y. +Proof. exact (fun e => can_inj of_to_Z e). Qed. + +Lemma to_Z_mod_Int63to_Z (x : int) : to_Z x mod wB = φ x%int63. +Proof. + unfold to_Z. + case ltbP; [> now rewrite Z.mod_small by now apply Int63.to_Z_bounded |]. + rewrite Z.nlt_ge; intros gexmin. + rewrite opp_to_Z_opp; rewrite Z.mod_small by now apply Int63.to_Z_bounded. + - easy. + - now intros neqx0; rewrite neqx0 in gexmin. +Qed. + + +(** Centered modulo *) +Definition cmod (x d : Z) : Z := + (x + d / 2) mod d - (d / 2). + +Lemma cmod_mod (x d : Z) : + cmod (x mod d) d = cmod x d. +Proof. + now unfold cmod; rewrite Zplus_mod_idemp_l. +Qed. + +Lemma cmod_small (x d : Z) : + - (d / 2) <= x < d / 2 -> cmod x d = x. +Proof. + intros bound. + unfold cmod. + rewrite Zmod_small; [> lia |]. + split; [> lia |]. + rewrite Z.lt_add_lt_sub_r. + apply (Z.lt_le_trans _ (d / 2)); [> easy |]. + now rewrite <- Z.le_add_le_sub_r, Z.add_diag, Z.mul_div_le. +Qed. + +Lemma to_Z_cmodwB (x : int) : + to_Z x = cmod (φ x%int63) wB. +Proof. + unfold to_Z, cmod. + case ltbP; change φ (min_int)%int63 with (wB / 2). + - intros ltxmin. + rewrite Z.mod_small; [> lia |]. + split. + + now apply Z.add_nonneg_nonneg; try apply Int63.to_Z_bounded. + + change wB with (wB / 2 + wB / 2) at 2; lia. + - rewrite Z.nlt_ge; intros gexmin. + rewrite Int63.opp_spec. + rewrite Z_mod_nz_opp_full. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + rewrite <- (Z_mod_plus_full _ (-1)). + change (-1 * wB) with (- (wB / 2) - wB / 2). + rewrite <- Z.add_assoc, Zplus_minus. + rewrite Z.mod_small. + * change wB with (wB / 2 + wB / 2) at 1; lia. + * split; [> lia |]. + apply Z.lt_sub_lt_add_r. + transitivity wB; [>| easy]. + now apply Int63.to_Z_bounded. + + rewrite Z.mod_small by now apply Int63.to_Z_bounded. + now intros not0; rewrite not0 in gexmin. +Qed. + +Lemma of_Z_spec (z : Z) : to_Z (of_Z z) = cmod z wB. +Proof. now rewrite to_Z_cmodwB, Int63.of_Z_spec, cmod_mod. Qed. + +Lemma of_Z_cmod (z : Z) : of_Z (cmod z wB) = of_Z z. +Proof. now rewrite <- of_Z_spec, of_to_Z. Qed. + +Lemma is_int (z : Z) : + to_Z min_int <= z <= to_Z max_int -> + z = to_Z (of_Z z). +Proof. + rewrite to_Z_min, to_Z_max. + intros bound; rewrite of_Z_spec, cmod_small; lia. +Qed. + +(** Specification of operations that differ on signed and unsigned ints *) + +Axiom asr_spec : forall x p, to_Z (x >> p) = (to_Z x) / 2 ^ (to_Z p). + +Axiom div_spec : forall x y, + to_Z x <> to_Z min_int \/ to_Z y <> (-1)%Z -> + to_Z (x / y) = Z.quot (to_Z x) (to_Z y). + +Axiom mod_spec : forall x y, to_Z (x mod y) = Z.rem (to_Z x) (to_Z y). + +Axiom ltb_spec : forall x y, (x <? y)%sint63 = true <-> to_Z x < to_Z y. + +Axiom leb_spec : forall x y, (x <=? y)%sint63 = true <-> to_Z x <= to_Z y. + +Axiom compare_spec : forall x y, (x ?= y)%sint63 = (to_Z x ?= to_Z y). + +(** Specification of operations that coincide on signed and unsigned ints *) + +Lemma add_spec (x y : int) : + to_Z (x + y)%sint63 = cmod (to_Z x + to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.add_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Z.add_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma sub_spec (x y : int) : + to_Z (x - y)%sint63 = cmod (to_Z x - to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.sub_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Zminus_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma mul_spec (x y : int) : + to_Z (x * y)%sint63 = cmod (to_Z x * to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.mul_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Zmult_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma succ_spec (x : int) : + to_Z (succ x)%sint63 = cmod (to_Z x + 1) wB. +Proof. now unfold succ; rewrite add_spec. Qed. + +Lemma pred_spec (x : int) : + to_Z (pred x)%sint63 = cmod (to_Z x - 1) wB. +Proof. now unfold pred; rewrite sub_spec. Qed. + +Lemma opp_spec (x : int) : + to_Z (- x)%sint63 = cmod (- to_Z x) wB. +Proof. + rewrite to_Z_cmodwB, Int63.opp_spec. + rewrite <- Z.sub_0_l, <- to_Z_mod_Int63to_Z, Zminus_mod_idemp_r. + now rewrite cmod_mod. +Qed. + +(** Behaviour when there is no under or overflow *) + +Lemma add_bounded (x y : int) : + to_Z min_int <= to_Z x + to_Z y <= to_Z max_int -> + to_Z (x + y) = to_Z x + to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite add_spec, cmod_small; [>| lia]. +Qed. + +Lemma sub_bounded (x y : int) : + to_Z min_int <= to_Z x - to_Z y <= to_Z max_int -> + to_Z (x - y) = to_Z x - to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite sub_spec, cmod_small; [>| lia]. +Qed. + +Lemma mul_bounded (x y : int) : + to_Z min_int <= to_Z x * to_Z y <= to_Z max_int -> + to_Z (x * y) = to_Z x * to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite mul_spec, cmod_small; [>| lia]. +Qed. + +Lemma succ_bounded (x : int) : + to_Z min_int <= to_Z x + 1 <= to_Z max_int -> + to_Z (succ x) = to_Z x + 1. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite succ_spec, cmod_small; [>| lia]. +Qed. + +Lemma pred_bounded (x : int) : + to_Z min_int <= to_Z x - 1 <= to_Z max_int -> + to_Z (pred x) = to_Z x - 1. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite pred_spec, cmod_small; [>| lia]. +Qed. + +Lemma opp_bounded (x : int) : + to_Z min_int <= - to_Z x <= to_Z max_int -> + to_Z (- x) = - to_Z x. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite opp_spec, cmod_small; [>| lia]. +Qed. + +(** Relationship with of_Z *) + +Lemma add_of_Z (x y : int) : + (x + y)%sint63 = of_Z (to_Z x + to_Z y). +Proof. now rewrite <- of_Z_cmod, <- add_spec, of_to_Z. Qed. + +Lemma sub_of_Z (x y : int) : + (x - y)%sint63 = of_Z (to_Z x - to_Z y). +Proof. now rewrite <- of_Z_cmod, <- sub_spec, of_to_Z. Qed. + +Lemma mul_of_Z (x y : int) : + (x * y)%sint63 = of_Z (to_Z x * to_Z y). +Proof. now rewrite <- of_Z_cmod, <- mul_spec, of_to_Z. Qed. + +Lemma succ_of_Z (x : int) : + (succ x)%sint63 = of_Z (to_Z x + 1). +Proof. now rewrite <- of_Z_cmod, <- succ_spec, of_to_Z. Qed. + +Lemma pred_of_Z (x : int) : + (pred x)%sint63 = of_Z (to_Z x - 1). +Proof. now rewrite <- of_Z_cmod, <- pred_spec, of_to_Z. Qed. + +Lemma opp_of_Z (x : int) : + (- x)%sint63 = of_Z (- to_Z x). +Proof. now rewrite <- of_Z_cmod, <- opp_spec, of_to_Z. Qed. + +(** Comparison *) +Import Bool. + +Lemma eqbP x y : reflect (to_Z x = to_Z y) (x =? y)%sint63. +Proof. + apply iff_reflect; rewrite Int63.eqb_spec. + now split; [> apply to_Z_inj | apply f_equal]. +Qed. + +Lemma ltbP x y : reflect (to_Z x < to_Z y) (x <? y)%sint63. +Proof. now apply iff_reflect; symmetry; apply ltb_spec. Qed. + +Lemma lebP x y : reflect (to_Z x <= to_Z y) (x ≤? y)%sint63. +Proof. now apply iff_reflect; symmetry; apply leb_spec. Qed. + +(** ASR *) +Lemma asr_0 (i : int) : (0 >> i)%sint63 = 0%sint63. +Proof. now apply to_Z_inj; rewrite asr_spec. Qed. + +Lemma asr_0_r (i : int) : (i >> 0)%sint63 = i. +Proof. now apply to_Z_inj; rewrite asr_spec, Zdiv_1_r. Qed. + +Lemma asr_neg_r (i n : int) : to_Z n < 0 -> (i >> n)%sint63 = 0%sint63. +Proof. + intros ltn0. + apply to_Z_inj. + rewrite asr_spec, Z.pow_neg_r by assumption. + now rewrite Zdiv_0_r. +Qed. + +Lemma asr_1 (n : int) : (1 >> n)%sint63 = (n =? 0)%sint63. +Proof. + apply to_Z_inj; rewrite asr_spec. + case eqbP; [> now intros -> | intros neqn0]. + case (lebP 0 n). + - intros le0n. + apply Z.div_1_l; apply Z.pow_gt_1; [> easy |]. + rewrite to_Z_0 in *; lia. + - rewrite Z.nle_gt; intros ltn0. + now rewrite Z.pow_neg_r. +Qed. + +Notation asr := asr (only parsing). +Notation div := divs (only parsing). +Notation rem := mods (only parsing). +Notation ltb := ltsb (only parsing). +Notation leb := lesb (only parsing). +Notation compare := compares (only parsing). + +Module Export Sint63Notations. + Export Sint63NotationsInternalA. + Export Sint63NotationsInternalB. +End Sint63Notations. diff --git a/theories/dune b/theories/dune index 18e000cfe1..90e9522b7b 100644 --- a/theories/dune +++ b/theories/dune @@ -15,7 +15,6 @@ coq.plugins.firstorder coq.plugins.number_string_notation - coq.plugins.int63_syntax coq.plugins.float_syntax coq.plugins.btauto diff --git a/theories/extraction/ExtrOCamlInt63.v b/theories/extraction/ExtrOCamlInt63.v index 7f7b4af98d..1949a1a9d8 100644 --- a/theories/extraction/ExtrOCamlInt63.v +++ b/theories/extraction/ExtrOCamlInt63.v @@ -10,7 +10,7 @@ (** Extraction to OCaml of native 63-bit machine integers. *) -From Coq Require Int63 Extraction. +From Coq Require Int63 Sint63 Extraction. (** Basic data types used by some primitive operators. *) @@ -26,6 +26,7 @@ Extraction Inline Int63.int. Extract Constant Int63.lsl => "Uint63.l_sl". Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Sint63.asr => "Uint63.a_sr". Extract Constant Int63.land => "Uint63.l_and". Extract Constant Int63.lor => "Uint63.l_or". Extract Constant Int63.lxor => "Uint63.l_xor". @@ -36,10 +37,15 @@ Extract Constant Int63.mul => "Uint63.mul". Extract Constant Int63.mulc => "Uint63.mulc". Extract Constant Int63.div => "Uint63.div". Extract Constant Int63.mod => "Uint63.rem". +Extract Constant Sint63.div => "Uint63.divs". +Extract Constant Sint63.rem => "Uint63.rems". + Extract Constant Int63.eqb => "Uint63.equal". Extract Constant Int63.ltb => "Uint63.lt". Extract Constant Int63.leb => "Uint63.le". +Extract Constant Sint63.ltb => "Uint63.lts". +Extract Constant Sint63.leb => "Uint63.les". Extract Constant Int63.addc => "Uint63.addc". Extract Constant Int63.addcarryc => "Uint63.addcarryc". @@ -51,6 +57,7 @@ Extract Constant Int63.diveucl_21 => "Uint63.div21". Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". Extract Constant Int63.compare => "Uint63.compare". +Extract Constant Sint63.compare => "Uint63.compares". Extract Constant Int63.head0 => "Uint63.head0". Extract Constant Int63.tail0 => "Uint63.tail0". |