diff options
| author | Maxime Dénès | 2018-02-16 01:02:17 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-04 13:12:40 +0000 |
| commit | e43b1768d0f8399f426b92f4dfe31955daceb1a4 (patch) | |
| tree | d46d10f8893205750e7238e69512736243315ef6 /kernel/vmvalues.mli | |
| parent | a1b7f53a68c9ccae637f2c357fbe50a09e211a4a (diff) | |
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>
Diffstat (limited to 'kernel/vmvalues.mli')
| -rw-r--r-- | kernel/vmvalues.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index ae1d416ed5..6d984d5f49 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -44,6 +44,7 @@ type structured_constant = | Const_b0 of tag | Const_univ_level of Univ.Level.t | Const_val of structured_values + | Const_uint of Uint63.t val pp_struct_const : structured_constant -> Pp.t @@ -125,6 +126,7 @@ type whd = | Vcofix of vcofix * to_update * arguments option | Vconstr_const of int | Vconstr_block of vblock + | Vint64 of int64 | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t @@ -145,6 +147,7 @@ val val_of_proj : Projection.Repr.t -> values -> values val val_of_atom : atom -> values val val_of_int : int -> structured_values val val_of_block : tag -> structured_values array -> structured_values +val val_of_uint : Uint63.t -> structured_values external val_of_annot_switch : annot_switch -> values = "%identity" external val_of_proj_name : Projection.Repr.t -> values = "%identity" |