Primitive integers

This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.

Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.

This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.

Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

6 files changed, 79 insertions, 121 deletions

diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
deleted file mode 100644
index e34a401c2c..0000000000
--- a/plugins/syntax/int31_syntax.ml
+++ /dev/null
@@ -1,114 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \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 = "int31_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-(* digit-based syntax for int31 *)
-
-open Bigint
-open Names
-open Globnames
-open Glob_term
-
-(*** Constants for locating int31 constructors ***)
-
-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)
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-let make_mind mp id = Names.MutInd.make2 mp (Label.make id)
-let make_mind_mpfile dir id = make_mind (ModPath.MPfile (make_dir dir)) id
-let make_mind_mpdot dir modname id =
-  let mp = ModPath.MPdot (ModPath.MPfile (make_dir dir), Label.make modname)
-  in make_mind mp id
-
-
-(* int31 stuff *)
-let int31_module = ["Coq"; "Numbers"; "Cyclic"; "Int31"; "Int31"]
-let int31_path = make_path int31_module "int31"
-let int31_id = make_mind_mpfile int31_module
-let int31_scope = "int31_scope"
-
-let int31_construct = ConstructRef ((int31_id "int31",0),1)
-
-let int31_0 = ConstructRef ((int31_id "digits",0),1)
-let int31_1 = ConstructRef ((int31_id "digits",0),2)
-
-(*** Definition of the Non_closed exception, used in the pretty printing ***)
-exception Non_closed
-
-(*** Parsing for int31 in digital notation ***)
-
-(* parses a *non-negative* integer (from bigint.ml) into an int31
-   wraps modulo 2^31 *)
-let int31_of_pos_bigint ?loc n =
-  let ref_construct = DAst.make ?loc (GRef (int31_construct, None)) in
-  let ref_0 = DAst.make ?loc (GRef (int31_0, None)) in
-  let ref_1 = DAst.make ?loc (GRef (int31_1, None)) in
-  let rec args counter n =
-    if counter <= 0 then
-      []
-    else
-      let (q,r) = div2_with_rest n in
-	(if r then ref_1 else ref_0)::(args (counter-1) q)
-  in
-  DAst.make ?loc (GApp (ref_construct, List.rev (args 31 n)))
-
-let error_negative ?loc =
-  CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
-
-let interp_int31 ?loc n =
-  if is_pos_or_zero n then
-    int31_of_pos_bigint ?loc n
-  else
-    error_negative ?loc
-
-(* Pretty prints an int31 *)
-
-let bigint_of_int31 =
-  let rec args_parsing args cur =
-    match args with
-      | [] -> cur
-      | r::l when is_gr r int31_0 -> args_parsing l (mult_2 cur)
-      | r::l when is_gr r int31_1 -> args_parsing l (add_1 (mult_2 cur))
-      | _ -> raise Non_closed
-  in
-  fun c -> match DAst.get c with
-  | GApp (r, args) when is_gr r int31_construct -> args_parsing args zero
-  | _ -> raise Non_closed
-
-let uninterp_int31 (AnyGlobConstr i) =
-  try
-    Some (bigint_of_int31 i)
-  with Non_closed ->
-    None
-
-open Notation
-
-let at_declare_ml_module f x =
-  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-(* Actually declares the interpreter for int31 *)
-
-let _ =
-  register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31);
-  at_declare_ml_module enable_prim_token_interpretation
-    { pt_local = false;
-      pt_scope = int31_scope;
-      pt_interp_info = Uid int31_scope;
-      pt_required = (int31_path,int31_module);
-      pt_refs = [int31_construct];
-      pt_in_match = true }
diff --git a/plugins/syntax/int31_syntax_plugin.mlpack b/plugins/syntax/int31_syntax_plugin.mlpack
deleted file mode 100644
index 54a5bc0cd1..0000000000
--- a/plugins/syntax/int31_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Int31_syntax
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
new file mode 100644
index 0000000000..992b7a986b
--- /dev/null
+++ b/plugins/syntax/int63_syntax.ml
@@ -0,0 +1,55 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+
+(* 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.Int63.int"
+let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.Int63.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_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;
+                 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 = NumeralNotation o;
+           pt_required = (int63_path, int63_module);
+           pt_refs = [];
+           pt_in_match = false })
+    ()
diff --git a/plugins/syntax/int63_syntax_plugin.mlpack b/plugins/syntax/int63_syntax_plugin.mlpack
new file mode 100644
index 0000000000..d83d554fe6
--- /dev/null
+++ b/plugins/syntax/int63_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Int63_syntax
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index ea564ae2ba..0c6d2ac0d1 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -69,6 +69,14 @@ let locate_int () =
     }, mkRefC q_int, mkRefC q_uint)
   else None
 
+let locate_int63 () =
+  let int63n = "num.int63.type" in
+  if Coqlib.has_ref int63n
+  then
+    let q_int63 = qualid_of_ref int63n in
+    Some (mkRefC q_int63)
+  else None
+
 let has_type f ty =
   let (sigma, env) = Pfedit.get_current_context () in
   let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
@@ -79,17 +87,18 @@ let type_error_to f ty =
   CErrors.user_err
     (pr_qualid f ++ str " should go from Decimal.int to " ++
      pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
-     fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).")
+     fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
 
 let type_error_of g ty =
   CErrors.user_err
     (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
      str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
-     str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).")
+     str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
 
 let vernac_numeral_notation local ty f g scope opts =
   let int_ty = locate_int () in
   let z_pos_ty = locate_z () in
+  let int63_ty = locate_int63 () in
   let tyc = Smartlocate.global_inductive_with_alias ty in
   let to_ty = Smartlocate.global_with_alias f in
   let of_ty = Smartlocate.global_with_alias g in
@@ -111,6 +120,10 @@ let vernac_numeral_notation local ty f g scope opts =
     match z_pos_ty with
     | Some (z_pos_ty, cZ) when has_type f (arrow cZ cty) -> Z z_pos_ty, Direct
     | Some (z_pos_ty, cZ) when has_type f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
+    | _ ->
+    match int63_ty with
+    | Some cint63 when has_type f (arrow cint63 cty) -> Int63, Direct
+    | Some cint63 when has_type f (arrow cint63 (opt cty)) -> Int63, Option
     | _ -> type_error_to f ty
   in
   (* Check the type of g *)
@@ -124,6 +137,10 @@ let vernac_numeral_notation local ty f g scope opts =
     match z_pos_ty with
     | Some (z_pos_ty, cZ) when has_type g (arrow cty cZ) -> Z z_pos_ty, Direct
     | Some (z_pos_ty, cZ) when has_type g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
+    | _ ->
+    match int63_ty with
+    | Some cint63 when has_type g (arrow cty cint63) -> Int63, Direct
+    | Some cint63 when has_type g (arrow cty (opt cint63)) -> Int63, Option
     | _ -> type_error_of g ty
   in
   let o = { to_kind; to_ty; of_kind; of_ty;
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
index 1ab16c700d..aac46338ea 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/plugin_base.dune
@@ -20,8 +20,8 @@
  (libraries coq.vernac))
 
 (library
- (name int31_syntax_plugin)
- (public_name coq.plugins.int31_syntax)
- (synopsis "Coq syntax plugin: int31")
- (modules int31_syntax)
+ (name int63_syntax_plugin)
+ (public_name coq.plugins.int63_syntax)
+ (synopsis "Coq syntax plugin: int63")
+ (modules int63_syntax)
  (libraries coq.vernac))