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/subtyping.ml | |
| 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/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 347c30dd64..2fc3aa99b5 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -257,10 +257,10 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 = anything of the right type can implement it, even if bodies differ. *) (match cb2.const_body with - | Undef _ | OpaqueDef _ -> cst + | Primitive _ | Undef _ | OpaqueDef _ -> cst | Def lc2 -> (match cb1.const_body with - | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField + | Primitive _ | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField | Def lc1 -> (* NB: cb1 might have been strengthened and appear as transparent. Anyway [check_conv] will handle that afterwards. *) |