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>

9 files changed, 63 insertions, 3 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 13078840ef..8e49800982 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -967,6 +967,8 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
   | GCast (c, c') ->
       CCast (sub_extern true scopes vars c,
              map_cast_type (extern_typ scopes vars) c')
+  | GInt i ->
+     CPrim(Numeral (Uint63.to_string i,true))
 
   in insert_coercion coercion (CAst.make ?loc c)
 
@@ -1312,6 +1314,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
           Array.map (fun (_,_,ty) -> ty) v,
           Array.map (fun (_,bd,_) -> bd) v)
   | PSort s -> GSort s
+  | PInt i -> GInt i
 
 let extern_constr_pattern env sigma pat =
   extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
diff --git a/interp/declare.ml b/interp/declare.ml
index 6778fa1e7a..ea6ed8321d 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -442,6 +442,9 @@ let assumption_message id =
   discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
   Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
 
+let register_message id =
+  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is registered")
+
 (** Monomorphic universes need to survive sections. *)
 
 let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
diff --git a/interp/declare.mli b/interp/declare.mli
index 468e056909..669657af6f 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -74,6 +74,7 @@ val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool
 
 val definition_message : Id.t -> unit
 val assumption_message : Id.t -> unit
+val register_message : Id.t -> unit
 val fixpoint_message : int array option -> Id.t list -> unit
 val cofixpoint_message : Id.t list -> unit
 val recursive_message : bool (** true = fixpoint *) ->
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index f5be0ddbae..a537b4848c 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -101,6 +101,7 @@ let type_of_logical_kind = function
       | Property
       | Proposition
       | Corollary -> "thm")
+  | IsPrimitive -> "prim"
 
 let type_of_global_ref gr =
   if Typeclasses.is_class gr then
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 8a89bcdf26..959455dfd2 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -225,7 +225,7 @@ let rec is_rigid_head sigma t = match kind sigma t with
         | Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i)))
         | _ -> is_rigid_head sigma f)
   | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
-  | Prod _ | Meta _ | Cast _ -> assert false
+  | Prod _ | Meta _ | Cast _ | Int _ -> assert false
 
 let is_rigid env sigma t =
   let open Context.Rel.Declaration in
diff --git a/interp/notation.ml b/interp/notation.ml
index ca27d439fb..bc68d97bb8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -574,6 +574,7 @@ type target_kind =
   | Int of int_ty (* Coq.Init.Decimal.int + uint *)
   | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
+  | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
 
 type string_target_kind =
   | ListByte
@@ -637,6 +638,7 @@ let rec constr_of_glob env sigma g = match DAst.get g with
       let sigma,c = constr_of_glob env sigma gc in
       let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
       sigma,mkApp (c, Array.of_list cl)
+  | Glob_term.GInt i -> sigma, mkInt i
   | _ ->
       raise NotAValidPrimToken
 
@@ -649,6 +651,7 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
   | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
   | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
   | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
+  | Int i -> DAst.make ?loc (Glob_term.GInt i)
   | _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c))
 
 let no_such_prim_token uninterpreted_token_kind ?loc ty =
@@ -683,6 +686,16 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) =
 
 end
 
+(** Conversion from bigint to int63 *)
+let rec int63_of_pos_bigint i =
+  let open Bigint in
+  if equal i zero then Uint63.of_int 0
+  else
+    let (quo,rem) = div2_with_rest i in
+    if rem then Uint63.add (Uint63.of_int 1)
+      (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo))
+    else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)
+
 module Numeral = struct
 (** * Numeral notation *)
 open PrimTokenNotation
@@ -838,6 +851,32 @@ let bigint_of_z z = match Constr.kind z with
       end
   | _ -> raise NotAValidPrimToken
 
+(** Now, [Int63] from/to bigint *)
+
+let int63_of_pos_bigint ?loc n =
+  let i = int63_of_pos_bigint n in
+  mkInt i
+
+let error_negative ?loc =
+  CErrors.user_err ?loc ~hdr:"interp_int63" (Pp.str "int63 are only non-negative numbers.")
+
+let error_overflow ?loc n =
+  CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Bigint.to_string n))
+
+let interp_int63 ?loc n =
+  let open Bigint in
+  if is_pos_or_zero n
+  then
+    if less_than n (pow two 63)
+    then int63_of_pos_bigint ?loc n
+    else error_overflow ?loc n
+  else error_negative ?loc
+
+let bigint_of_int63 c =
+  match Constr.kind c with
+  | Int i -> Bigint.of_string (Uint63.to_string i)
+  | _ -> raise NotAValidPrimToken
+
 let big2raw n =
   if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
   else (Bigint.to_string (Bigint.neg n), false)
@@ -856,6 +895,7 @@ let interp o ?loc n =
     | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n)
     | UInt _ (* n <= 0 *) -> no_such_prim_token "number" ?loc o.ty_name
     | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n)
+    | Int63 -> interp_int63 ?loc (raw2big n)
   in
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -877,6 +917,7 @@ let uninterp o n =
       | (Int _, c) -> rawnum_of_coqint c
       | (UInt _, c) -> (rawnum_of_coquint c, true)
       | (Z _, c) -> big2raw (bigint_of_z c)
+      | (Int63, c) -> big2raw (bigint_of_int63 c)
     end o n
 end
 
diff --git a/interp/notation.mli b/interp/notation.mli
index a482e00e81..5dcc96dc29 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -127,6 +127,7 @@ type target_kind =
   | Int of int_ty (* Coq.Init.Decimal.int + uint *)
   | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
+  | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
 
 type string_target_kind =
   | ListByte
@@ -320,3 +321,6 @@ val entry_has_ident : notation_entry_level -> bool
 (** Rem: printing rules for primitive token are canonical *)
 
 val with_notation_protection : ('a -> 'b) -> 'a -> 'b
+
+(** Conversion from bigint to int63 *)
+val int63_of_pos_bigint : Bigint.bigint -> Uint63.t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 8d225fe683..890c24e633 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -89,9 +89,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
   glob_sort_eq s1 s2
 | NCast (t1, c1), NCast (t2, c2) ->
   (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
+| NInt i1, NInt i2 ->
+   Uint63.equal i1 i2
 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
   | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
-  | NRec _ | NSort _ | NCast _ ), _ -> false
+  | NRec _ | NSort _ | NCast _ | NInt _), _ -> false
 
 (**********************************************************************)
 (* Re-interpret a notation as a glob_constr, taking care of binders   *)
@@ -220,6 +222,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
   | NSort x -> GSort x
   | NHole (x, naming, arg)  -> GHole (x, naming, arg)
   | NRef x -> GRef (x,None)
+  | NInt i -> GInt i
 
 let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
@@ -435,6 +438,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
       NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
   | GCast (c,k) -> NCast (aux c,map_cast_type aux k)
   | GSort s -> NSort s
+  | GInt i -> NInt i
   | GHole (w,naming,arg) ->
      if arg != None then has_ltac := true;
      NHole (w, naming, arg)
@@ -623,6 +627,7 @@ let rec subst_notation_constr subst bound raw =
 	  NRec (fk,idl,dll',tl',bl')
 
   | NSort _ -> raw
+  | NInt _ -> raw
 
   | NHole (knd, naming, solve) ->
     let nknd = match knd with
@@ -1189,6 +1194,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
     match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
   | GSort (GType _), NSort (GType _) when not u -> sigma
   | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
+  | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma
   | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, NHole _ -> sigma
 
@@ -1216,7 +1222,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
 
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
      | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
-     | GCast _ ), _ -> raise No_match
+     | GCast _ | GInt _ ), _ -> raise No_match
 
 and match_in u = match_ true u
 
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 0ef1f267f6..6fe20486dc 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -43,6 +43,7 @@ type notation_constr =
       notation_constr array * notation_constr array
   | NSort of glob_sort
   | NCast of notation_constr * notation_constr cast_type
+  | NInt of Uint63.t
 
 (** Note concerning NList: first constr is iterator, second is terminator;
     first id is where each argument of the list has to be substituted