Merge PR #13275: Put all Int63 primitives in a separate file

Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl

15 files changed, 163 insertions, 93 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 8ab4265b15..cbe526be68 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -278,11 +278,13 @@ through the <tt>Require Import</tt> command.</p>
     <dd>
     theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
     theories/Numbers/Cyclic/Abstract/NZCyclic.v
+    theories/Numbers/Cyclic/Abstract/CarryType.v
     theories/Numbers/Cyclic/Abstract/DoubleType.v
     theories/Numbers/Cyclic/Int31/Cyclic31.v
     theories/Numbers/Cyclic/Int31/Ring31.v
     theories/Numbers/Cyclic/Int31/Int31.v
     theories/Numbers/Cyclic/Int63/Cyclic63.v
+    theories/Numbers/Cyclic/Int63/PrimInt63.v
     theories/Numbers/Cyclic/Int63/Int63.v
     theories/Numbers/Cyclic/Int63/Ring63.v
     theories/Numbers/Cyclic/ZModulo/ZModulo.v
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
index b14b02f3bb..110b26581f 100644
--- a/plugins/syntax/int63_syntax.ml
+++ b/plugins/syntax/int63_syntax.ml
@@ -20,14 +20,14 @@ open Libnames
 
 (*** Constants for locating int63 constructors ***)
 
-let q_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.Int63.int"
-let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.Int63.id_int"
+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"; "Int63"]
+let int63_module = ["Coq"; "Numbers"; "Cyclic"; "Int63"; "PrimInt63"]
 let int63_path = make_path int63_module "int"
 let int63_scope = "int63_scope"
 
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index eefa338f0d..ca8e1b58a8 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -1,7 +1,5 @@
 2%int63
      : int
-(2 + 2)%int63
-     : int
 2
      : int
 9223372036854775807
@@ -17,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.Int63.int
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
 0
      : int
 0
@@ -32,13 +30,7 @@ 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
-2 + 2
-     : int
-     = 4
-     : int
-     = 37151199385380486
+add 2 2
      : int
 The command has indeed failed with message:
 int63 are only non-negative numbers.
@@ -56,3 +48,11 @@ t = 2%i63
      : nat
 2
      : int
+(2 + 2)%int63
+     : int
+2 + 2
+     : int
+     = 4
+     : int
+     = 37151199385380486
+     : int
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index c49616d918..6f1046f7a5 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -1,7 +1,6 @@
-Require Import Int63 Cyclic63.
+Require Import PrimInt63.
 
 Check 2%int63.
-Check (2 + 2)%int63.
 Open Scope int63_scope.
 Check 2.
 Check 9223372036854775807.
@@ -18,10 +17,7 @@ Fail Check 0xg.
 Fail Check 0xG.
 Fail Check 00x1.
 Fail Check 0x.
-Check (Int63.add 2 2).
-Check (2+2).
-Eval vm_compute in 2+2.
-Eval vm_compute in 65675757 * 565675998.
+Check (PrimInt63.add 2 2).
 Fail Check -1.
 Fail Check 9223372036854775808.
 Open Scope nat_scope.
@@ -36,3 +32,11 @@ Check 2.
 Close Scope nat_scope.
 Check 2.
 Close Scope int63_scope.
+
+Require Import Int63.
+
+Check (2 + 2)%int63.
+Open Scope int63_scope.
+Check (2+2).
+Eval vm_compute in 2+2.
+Eval vm_compute in 65675757 * 565675998.
diff --git a/test-suite/primitive/uint63/addcarryc.v b/test-suite/primitive/uint63/addcarryc.v
index a4430769ca..7ab3af51d8 100644
--- a/test-suite/primitive/uint63/addcarryc.v
+++ b/test-suite/primitive/uint63/addcarryc.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/addmuldiv.v b/test-suite/primitive/uint63/addmuldiv.v
index 72b0164b49..e3aded6c96 100644
--- a/test-suite/primitive/uint63/addmuldiv.v
+++ b/test-suite/primitive/uint63/addmuldiv.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/diveucl.v b/test-suite/primitive/uint63/diveucl.v
index 8f88a0f356..43a0741ffe 100644
--- a/test-suite/primitive/uint63/diveucl.v
+++ b/test-suite/primitive/uint63/diveucl.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/head0.v b/test-suite/primitive/uint63/head0.v
index f4234d2605..30cbce4537 100644
--- a/test-suite/primitive/uint63/head0.v
+++ b/test-suite/primitive/uint63/head0.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/subcarryc.v b/test-suite/primitive/uint63/subcarryc.v
index e81b6536b2..6a773dde5d 100644
--- a/test-suite/primitive/uint63/subcarryc.v
+++ b/test-suite/primitive/uint63/subcarryc.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/tail0.v b/test-suite/primitive/uint63/tail0.v
index c9d426087a..1f91e4106c 100644
--- a/test-suite/primitive/uint63/tail0.v
+++ b/test-suite/primitive/uint63/tail0.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v
index ed7947aa63..4c818a7e52 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Int63 FloatClass.
+Require Import PrimInt63 FloatClass.
 
 (** * Definition of the interface for primitive floating-point arithmetic
 
diff --git a/theories/Numbers/Cyclic/Abstract/CarryType.v b/theories/Numbers/Cyclic/Abstract/CarryType.v
new file mode 100644
index 0000000000..a21a1c8022
--- /dev/null
+++ b/theories/Numbers/Cyclic/Abstract/CarryType.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+Set Implicit Arguments.
+
+#[universes(template)]
+Variant carry (A : Type) :=
+| C0 : A -> carry A
+| C1 : A -> carry A.
diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v
index 165f9893ca..e399bcfc0f 100644
--- a/theories/Numbers/Cyclic/Abstract/DoubleType.v
+++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v
@@ -13,15 +13,15 @@
 Set Implicit Arguments.
 
 Require Import BinInt.
+Require Import CarryType.
 Local Open Scope Z_scope.
 
 Definition base digits := Z.pow 2 (Zpos digits).
 Arguments base digits: simpl never.
 
-#[universes(template)]
-Variant carry (A : Type) :=
-| C0 : A -> carry A
-| C1 : A -> carry A.
+Notation carry := carry (only parsing).
+Notation C0 := C0 (only parsing).
+Notation C1 := C1 (only parsing).
 
 Definition interp_carry {A} (sign:Z)(B:Z)(interp:A -> Z) c :=
   match c with
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index dbca2f0947..c469a49903 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -17,55 +17,25 @@ Require Import Zpow_facts.
 Require Import Zgcd_alt.
 Require ZArith.
 Import Znumtheory.
-
-Register bool as kernel.ind_bool.
-Register prod as kernel.ind_pair.
-Register carry as kernel.ind_carry.
-Register comparison as kernel.ind_cmp.
+Require Export PrimInt63.
 
 Definition size := 63%nat.
 
-Primitive int := #int63_type.
-Register int as num.int63.type.
-Declare Scope int63_scope.
-Definition id_int : int -> int := fun x => x.
-Declare ML Module "int63_syntax_plugin".
-
-Module Import Int63NotationsInternalA.
-Delimit Scope int63_scope with int63.
-Bind Scope int63_scope with int.
-End Int63NotationsInternalA.
-
-(* Logical operations *)
-Primitive lsl := #int63_lsl.
-
-Primitive lsr := #int63_lsr.
-
-Primitive land := #int63_land.
-
-Primitive lor := #int63_lor.
-
-Primitive lxor := #int63_lxor.
-
-(* Arithmetic modulo operations *)
-Primitive add := #int63_add.
-
-Primitive sub := #int63_sub.
-
-Primitive mul := #int63_mul.
-
-Primitive mulc := #int63_mulc.
-
-Primitive div := #int63_div.
-
-Primitive mod := #int63_mod.
-
-(* Comparisons *)
-Primitive eqb := #int63_eq.
-
-Primitive ltb := #int63_lt.
-
-Primitive leb := #int63_le.
+Notation int := int (only parsing).
+Notation lsl := lsl (only parsing).
+Notation lsr := lsr (only parsing).
+Notation land := land (only parsing).
+Notation lor := lor (only parsing).
+Notation lxor := lxor (only parsing).
+Notation add := add (only parsing).
+Notation sub := sub (only parsing).
+Notation mul := mul (only parsing).
+Notation mulc := mulc (only parsing).
+Notation div := div (only parsing).
+Notation mod := mod (only parsing).
+Notation eqb := eqb (only parsing).
+Notation ltb := ltb (only parsing).
+Notation leb := leb (only parsing).
 
 Local Open Scope int63_scope.
 
@@ -139,34 +109,29 @@ Register Inline subcarry.
 Definition addc_def x y :=
   let r := x + y in
   if r <? x then C1 r else C0 r.
-(* the same but direct implementation for efficiency *)
-Primitive addc := #int63_addc.
+Notation addc := addc (only parsing).
 
 Definition addcarryc_def x y :=
   let r := addcarry x y in
   if r <=? x then C1 r else C0 r.
-(* the same but direct implementation for efficiency *)
-Primitive addcarryc := #int63_addcarryc.
+Notation addcarryc := addcarryc (only parsing).
 
 Definition subc_def x y :=
   if y <=? x then C0 (x - y) else C1 (x - y).
-(* the same but direct implementation for efficiency *)
-Primitive subc := #int63_subc.
+Notation subc := subc (only parsing).
 
 Definition subcarryc_def x y :=
   if y <? x then C0 (x - y - 1) else C1 (x - y - 1).
-(* the same but direct implementation for efficiency *)
-Primitive subcarryc := #int63_subcarryc.
+Notation subcarryc := subcarryc (only parsing).
 
 Definition diveucl_def x y := (x/y, x mod y).
-(* the same but direct implementation for efficiency *)
-Primitive diveucl := #int63_diveucl.
+Notation diveucl := diveucl (only parsing).
 
-Primitive diveucl_21 := #int63_div21.
+Notation diveucl_21 := diveucl_21 (only parsing).
 
 Definition addmuldiv_def p x y :=
   (x << p) lor (y >> (digits - p)).
-Primitive addmuldiv := #int63_addmuldiv.
+Notation addmuldiv := addmuldiv (only parsing).
 
 Module Import Int63NotationsInternalC.
 Notation "- x" := (opp x) : int63_scope.
@@ -188,7 +153,7 @@ Definition compare_def x y :=
   if x <? y then Lt
   else if (x =? y) then Eq else Gt.
 
-Primitive compare := #int63_compare.
+Notation compare := compare (only parsing).
 
 Import Bool ZArith.
 (** Translation to Z *)
@@ -371,8 +336,8 @@ Axiom leb_spec : forall x y, (x <=? y)%int63 = true <-> φ x <= φ y.
 (** Exotic operations *)
 
 (** I should add the definition (like for compare) *)
-Primitive head0 := #int63_head0.
-Primitive tail0 := #int63_tail0.
+Notation head0 := head0 (only parsing).
+Notation tail0 := tail0 (only parsing).
 
 (** Axioms on operations which are just short cut *)
 
@@ -1950,7 +1915,6 @@ Module Export Int63Notations.
    Notation "m <= n" := (m <=? n) : int63_scope.
   #[deprecated(since="8.13",note="use infix ≤? instead")]
    Notation "m ≤ n" := (m <=? n) (at level 70, no associativity) : int63_scope.
-  Export Int63NotationsInternalA.
   Export Int63NotationsInternalB.
   Export Int63NotationsInternalC.
   Export Int63NotationsInternalD.
diff --git a/theories/Numbers/Cyclic/Int63/PrimInt63.v b/theories/Numbers/Cyclic/Int63/PrimInt63.v
new file mode 100644
index 0000000000..64c1b862c7
--- /dev/null
+++ b/theories/Numbers/Cyclic/Int63/PrimInt63.v
@@ -0,0 +1,82 @@
+(************************************************************************)
+(*         *   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 Export CarryType.
+
+Register bool as kernel.ind_bool.
+Register prod as kernel.ind_pair.
+Register carry as kernel.ind_carry.
+Register comparison as kernel.ind_cmp.
+
+Primitive int := #int63_type.
+Register int as num.int63.type.
+Declare Scope int63_scope.
+Definition id_int : int -> int := fun x => x.
+Declare ML Module "int63_syntax_plugin".
+
+Module Export Int63NotationsInternalA.
+Delimit Scope int63_scope with int63.
+Bind Scope int63_scope with int.
+End Int63NotationsInternalA.
+
+(* Logical operations *)
+Primitive lsl := #int63_lsl.
+
+Primitive lsr := #int63_lsr.
+
+Primitive land := #int63_land.
+
+Primitive lor := #int63_lor.
+
+Primitive lxor := #int63_lxor.
+
+(* Arithmetic modulo operations *)
+Primitive add := #int63_add.
+
+Primitive sub := #int63_sub.
+
+Primitive mul := #int63_mul.
+
+Primitive mulc := #int63_mulc.
+
+Primitive div := #int63_div.
+
+Primitive mod := #int63_mod.
+
+(* Comparisons *)
+Primitive eqb := #int63_eq.
+
+Primitive ltb := #int63_lt.
+
+Primitive leb := #int63_le.
+
+(** Exact arithmetic operations *)
+
+Primitive addc := #int63_addc.
+
+Primitive addcarryc := #int63_addcarryc.
+
+Primitive subc := #int63_subc.
+
+Primitive subcarryc := #int63_subcarryc.
+
+Primitive diveucl := #int63_diveucl.
+
+Primitive diveucl_21 := #int63_div21.
+
+Primitive addmuldiv := #int63_addmuldiv.
+
+(** Comparison *)
+Primitive compare := #int63_compare.
+
+(** Exotic operations *)
+
+Primitive head0 := #int63_head0.
+Primitive tail0 := #int63_tail0.