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>

1 files changed, 55 insertions, 0 deletions

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 })
+    ()