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, 0 insertions, 52 deletions

diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
deleted file mode 100644
index dca1757b7d..0000000000
--- a/kernel/cinstr.mli
+++ /dev/null
@@ -1,52 +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)         *)
-(************************************************************************)
-open Names
-open Constr
-open Vmvalues
-open Cbytecodes
-
-(** This file defines the lambda code for the bytecode compiler. It has been
-extracted from Clambda.ml because of the retroknowledge architecture. *)
-
-type uint =
-  | UintVal of Uint31.t
-  | UintDigits of lambda array
-  | UintDecomp of lambda
-
-and lambda =
-  | Lrel          of Name.t * int
-  | Lvar          of Id.t
-  | Levar         of Evar.t * lambda array
-  | Lprod         of lambda * lambda
-  | Llam          of Name.t array * lambda
-  | Llet          of Name.t * lambda * lambda
-  | Lapp          of lambda * lambda array
-  | Lconst        of pconstant
-  | Lprim         of pconstant * int (* arity *) * instruction * lambda array
-  | Lcase         of case_info * reloc_table * lambda * lambda * lam_branches
-  | Lfix          of (int array * int) * fix_decl
-  | Lcofix        of int * fix_decl (* must be in eta-expanded form *)
-  | Lmakeblock    of int * lambda array
-  | Lval          of structured_values
-  | Lsort         of Sorts.t
-  | Lind          of pinductive
-  | Lproj         of Projection.Repr.t * lambda
-  | Lint          of int
-  | Luint         of uint
-
-(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation
-to be correct. Otherwise, memoization of previous evaluations will be applied
-again to extra arguments (see #7333). *)
-
-and lam_branches =
-  { constant_branches : lambda array;
-    nonconstant_branches : (Name.t array * lambda) array }
-
-and fix_decl =  Name.t array * lambda array * lambda array