Merge PR #13559: Signed primitive integers

Reviewed-by: SkySkimmer
Reviewed-by: silene
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: proux01

3 files changed, 44 insertions, 84 deletions

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