From e43b1768d0f8399f426b92f4dfe31955daceb1a4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 16 Feb 2018 01:02:17 +0100 Subject: 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 Co-authored-by: Benjamin Grégoire Co-authored-by: Vincent Laporte --- kernel/nativeconv.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'kernel/nativeconv.ml') diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index f5d7ab3c9d..baa290367f 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -34,6 +34,8 @@ let rec conv_val env pb lvl v1 v2 cu = conv_accu env pb lvl k1 k2 cu | Vconst i1, Vconst i2 -> if Int.equal i1 i2 then cu else raise NotConvertible + | Vint64 i1, Vint64 i2 -> + if Int64.equal i1 i2 then cu else raise NotConvertible | Vblock b1, Vblock b2 -> let n1 = block_size b1 in let n2 = block_size b2 in @@ -47,7 +49,7 @@ let rec conv_val env pb lvl v1 v2 cu = aux lvl max b1 b2 (i+1) cu in aux lvl (n1-1) b1 b2 0 cu - | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible + | Vaccu _, _ | Vconst _, _ | Vint64 _, _ | Vblock _, _ -> raise NotConvertible and conv_accu env pb lvl k1 k2 cu = let n1 = accu_nargs k1 in -- cgit v1.2.3