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 --- library/decl_kinds.ml | 1 + library/global.ml | 5 +---- library/global.mli | 4 +--- library/keys.ml | 6 +++++- 4 files changed, 8 insertions(+), 8 deletions(-) (limited to 'library') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 171d51800e..8d5c2fb687 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -70,6 +70,7 @@ type goal_kind = locality * polymorphic * goal_object_kind (** Kinds used in library *) type logical_kind = + | IsPrimitive | IsAssumption of assumption_object_kind | IsDefinition of definition_object_kind | IsProof of theorem_kind diff --git a/library/global.ml b/library/global.ml index 84d2a37170..784a02449c 100644 --- a/library/global.ml +++ b/library/global.ml @@ -175,11 +175,8 @@ let with_global f = let (a, ctx) = f (env ()) (current_dirpath ()) in push_context_set false ctx; a -(* spiwack: register/unregister functions for retroknowledge *) -let register field value = - globalize0 (Safe_typing.register field value) - let register_inline c = globalize0 (Safe_typing.register_inline c) +let register_inductive c r = globalize0 (Safe_typing.register_inductive c r) let set_strategy k l = globalize0 (Safe_typing.set_strategy k l) diff --git a/library/global.mli b/library/global.mli index 40962e21af..df18625a5f 100644 --- a/library/global.mli +++ b/library/global.mli @@ -142,10 +142,8 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t (** {6 Retroknowledge } *) -val register : - Retroknowledge.field -> GlobRef.t -> unit - val register_inline : Constant.t -> unit +val register_inductive : inductive -> CPrimitives.prim_ind -> unit (** {6 Oracle } *) diff --git a/library/keys.ml b/library/keys.ml index 58883ccc88..45b6fae2f0 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -25,13 +25,14 @@ type key = | KFix | KCoFix | KRel + | KInt module KeyOrdered = struct type t = key let hash gr = match gr with - | KGlob gr -> 8 + GlobRef.Ordered.hash gr + | KGlob gr -> 9 + GlobRef.Ordered.hash gr | KLam -> 0 | KLet -> 1 | KProd -> 2 @@ -40,6 +41,7 @@ module KeyOrdered = struct | KFix -> 5 | KCoFix -> 6 | KRel -> 7 + | KInt -> 8 let compare gr1 gr2 = match gr1, gr2 with @@ -133,6 +135,7 @@ let constr_key kind c = | Evar _ -> raise Not_found | Sort _ -> KSort | LetIn _ -> KLet + | Int _ -> KInt in Some (aux c) with Not_found -> None @@ -148,6 +151,7 @@ let pr_key pr_global = function | KFix -> str"Fix" | KCoFix -> str"CoFix" | KRel -> str"Rel" + | KInt -> str"Int" let pr_keyset pr_global v = prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) -- cgit v1.2.3