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>

7 files changed, 97 insertions, 11 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index d9787bc73c..868a6ed3e9 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -245,6 +245,7 @@ let build_beq_scheme mode kn =
         | Fix _   -> raise (EqUnknown "fix")
         | Meta _  -> raise (EqUnknown "meta-variable")
         | Evar _  -> raise (EqUnknown "existential variable")
+        | Int _ -> raise (EqUnknown "int")
     in
       aux t
   in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 4b8371f5c3..7301e1fff7 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -178,3 +178,29 @@ let do_assumptions kind nl l =
       in
       subst'@subst, status' && status, next_uctx uctx)
     ([], true, uctx) l)
+
+let do_primitive id prim typopt =
+  if Lib.sections_are_opened () then
+    CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections.");
+  if Dumpglob.dump () then Dumpglob.dump_definition id false "ax";
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let evd, typopt = Option.fold_left_map
+      (interp_type_evars_impls ~impls:empty_internalization_env env)
+      evd typopt
+  in
+  let evd = Evd.minimize_universes evd in
+  let uvars, impls, typopt = match typopt with
+    | None -> Univ.LSet.empty, [], None
+    | Some (ty,impls) ->
+      EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty)
+  in
+  let evd = Evd.restrict_universe_context evd uvars in
+  let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in
+  let entry = { prim_entry_type = typopt;
+                prim_entry_univs = uctx;
+                prim_entry_content = prim;
+              }
+  in
+  let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in
+  register_message id.CAst.v
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 56932360a9..c5bf3725a9 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -33,3 +33,5 @@ val declare_assumption : coercion_flag -> assumption_kind ->
   UnivNames.universe_binders -> Impargs.manual_implicits ->
   bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
   GlobRef.t * Univ.Instance.t * bool
+
+val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 79adefdcf7..0664e18130 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -219,12 +219,51 @@ GRAMMAR EXTEND Gram
           { VernacRegister(g, RegisterCoqlib quid) }
       | IDENT "Register"; IDENT "Inline"; g = global ->
           { VernacRegister(g, RegisterInline) }
+      | IDENT "Primitive"; id = identref; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token ->
+          { VernacPrimitive(id, r, typopt) }
       | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
       | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
       | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l }
   ] ]
   ;
 
+   register_token:
+     [ [ r = register_prim_token -> { CPrimitives.OT_op r }
+       | r = register_type_token -> { CPrimitives.OT_type r } ] ]
+   ;
+
+   register_type_token:
+     [ [ "#int63_type" -> { CPrimitives.PT_int63 } ] ]
+   ;
+
+   register_prim_token:
+     [ [ "#int63_head0" -> { CPrimitives.Int63head0 }
+       | "#int63_tail0" -> { CPrimitives.Int63tail0 }
+       | "#int63_add" -> { CPrimitives.Int63add }
+       | "#int63_sub" -> { CPrimitives.Int63sub }
+       | "#int63_mul" -> { CPrimitives.Int63mul }
+       | "#int63_div" -> { CPrimitives.Int63div }
+       | "#int63_mod" -> { CPrimitives.Int63mod }
+       | "#int63_lsr" -> { CPrimitives.Int63lsr }
+       | "#int63_lsl" -> { CPrimitives.Int63lsl }
+       | "#int63_land" -> { CPrimitives.Int63land }
+       | "#int63_lor" -> { CPrimitives.Int63lor }
+       | "#int63_lxor" -> { CPrimitives.Int63lxor }
+       | "#int63_addc" -> { CPrimitives.Int63addc }
+       | "#int63_subc" -> { CPrimitives.Int63subc }
+       | "#int63_addcarryc" -> { CPrimitives.Int63addCarryC }
+       | "#int63_subcarryc" -> { CPrimitives.Int63subCarryC }
+       | "#int63_mulc" -> { CPrimitives.Int63mulc }
+       | "#int63_diveucl" -> { CPrimitives.Int63diveucl }
+       | "#int63_div21" -> { CPrimitives.Int63div21 }
+       | "#int63_addmuldiv" -> { CPrimitives.Int63addMulDiv }
+       | "#int63_eq" -> { CPrimitives.Int63eq }
+       | "#int63_lt" -> { CPrimitives.Int63lt }
+       | "#int63_le" -> { CPrimitives.Int63le }
+       | "#int63_compare" -> { CPrimitives.Int63compare }
+       ] ]
+    ;
+
   thm_token:
     [ [ "Theorem" -> { Theorem }
       | IDENT "Lemma" -> { Lemma }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5eeeaada2d..d22e52e960 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1182,6 +1182,12 @@ open Pputils
           hov 2
             (keyword "Register Inline" ++ spc() ++ pr_qualid qid)
         )
+      | VernacPrimitive(id,r,typopt) ->
+         hov 2
+             (keyword "Primitive" ++ spc() ++ pr_lident id ++
+                (Option.cata (fun ty -> spc() ++ str":" ++ pr_spc_lconstr ty) (mt()) typopt) ++ spc() ++
+                str ":=" ++ spc() ++
+                str (CPrimitives.op_or_type_to_string r))
       | VernacComments l ->
         return (
           hov 2
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 996fe320f9..7611355100 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2032,21 +2032,31 @@ let vernac_locate = function
 
 let vernac_register qid r =
   let gr = Smartlocate.global_with_alias qid in
- if Proof_global.there_are_pending_proofs () then
+  if Proof_global.there_are_pending_proofs () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
   match r with
   | RegisterInline ->
-    if not (isConstRef gr) then
-      user_err Pp.(str "Register inline: a constant is expected");
-    Global.register_inline (destConstRef gr)
+    begin match gr with
+    | ConstRef c -> Global.register_inline c
+    | _ -> CErrors.user_err (Pp.str "Register Inline: expecting a constant")
+    end
   | RegisterCoqlib n ->
-    let path, id = Libnames.repr_qualid n in
-    if DirPath.equal path Retroknowledge.int31_path
-    then
-      let f = Retroknowledge.(KInt31 (int31_field_of_string (Id.to_string id))) in
-      Global.register f gr
-    else
-      Coqlib.register_ref (Libnames.string_of_qualid n) gr
+    let ns, id = Libnames.repr_qualid n in
+    if DirPath.equal (dirpath_of_string "kernel") ns then begin
+      if Lib.sections_are_opened () then
+        user_err Pp.(str "Registering a kernel type is not allowed in sections");
+      let pind = match Id.to_string id with
+        | "ind_bool" -> CPrimitives.PIT_bool
+        | "ind_carry" -> CPrimitives.PIT_carry
+        | "ind_pair" -> CPrimitives.PIT_pair
+        | "ind_cmp" -> CPrimitives.PIT_cmp
+        | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace")
+      in
+      match gr with
+      | IndRef ind -> Global.register_inductive ind pind
+      | _ -> CErrors.user_err (Pp.str "Register in kernel: expecting an inductive type")
+    end
+    else Coqlib.register_ref (Libnames.string_of_qualid n) gr
 
 (********************)
 (* Proof management *)
@@ -2316,6 +2326,7 @@ let interp ?proof ~atts ~st c =
   | VernacLocate l -> unsupported_attributes atts;
     Feedback.msg_notice @@ vernac_locate l
   | VernacRegister (qid, r) -> unsupported_attributes atts; vernac_register qid r
+  | VernacPrimitive (id, prim, typopt) -> unsupported_attributes atts; ComAssumption.do_primitive id prim typopt
   | VernacComments l -> unsupported_attributes atts;
     Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
 
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 68a17e316e..2eb901890b 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -378,6 +378,7 @@ type nonrec vernac_expr =
   | VernacSearch of searchable * Goal_select.t option * search_restriction
   | VernacLocate of locatable
   | VernacRegister of qualid * register_kind
+  | VernacPrimitive of lident * CPrimitives.op_or_type * constr_expr option
   | VernacComments of comment list
 
   (* Proof management *)