diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/decl_kinds.ml | 1 | ||||
| -rw-r--r-- | library/declaremods.ml | 4 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | library/global.ml | 8 | ||||
| -rw-r--r-- | library/global.mli | 6 | ||||
| -rw-r--r-- | library/keys.ml | 6 | ||||
| -rw-r--r-- | library/library.ml | 6 | ||||
| -rw-r--r-- | library/library.mli | 4 |
8 files changed, 20 insertions, 17 deletions
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/declaremods.ml b/library/declaremods.ml index 8699583cdf..5fd11e187a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -928,10 +928,10 @@ let append_end_library_hook f = let old_f = !end_library_hook in end_library_hook := fun () -> old_f(); f () -let end_library ?except dir = +let end_library ?except ~output_native_objects dir = !end_library_hook(); let oname = Lib.end_compilation_checks dir in - let mp,cenv,ast = Global.export ?except dir in + let mp,cenv,ast = Global.export ?except ~output_native_objects dir in let prefix, lib_stack = Lib.end_compilation oname in assert (ModPath.equal mp (MPfile dir)); let substitute, keep, _ = Lib.classify_segment lib_stack in diff --git a/library/declaremods.mli b/library/declaremods.mli index 7aa4bc30ce..2b28ba908e 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -99,7 +99,7 @@ val get_library_native_symbols : library_name -> Nativecode.symbols val start_library : library_name -> unit val end_library : - ?except:Future.UUIDSet.t -> library_name -> + ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name -> Safe_typing.compiled_library * library_objects * Safe_typing.native_library (** append a function to be executed at end_library *) diff --git a/library/global.ml b/library/global.ml index 84d2a37170..cf996ce644 100644 --- a/library/global.ml +++ b/library/global.ml @@ -143,7 +143,8 @@ let mind_of_delta_kn kn = (** Operations on libraries *) let start_library dir = globalize (Safe_typing.start_library dir) -let export ?except s = Safe_typing.export ?except (safe_env ()) s +let export ?except ~output_native_objects s = + Safe_typing.export ?except ~output_native_objects (safe_env ()) s let import c u d = globalize (Safe_typing.import c u d) @@ -175,11 +176,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..4e2ad92717 100644 --- a/library/global.mli +++ b/library/global.mli @@ -108,7 +108,7 @@ val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ. (** {6 Compiled libraries } *) val start_library : DirPath.t -> ModPath.t -val export : ?except:Future.UUIDSet.t -> DirPath.t -> +val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> DirPath.t -> ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library val import : Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest -> @@ -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) diff --git a/library/library.ml b/library/library.ml index 9b9bd07c93..37dadadb76 100644 --- a/library/library.ml +++ b/library/library.ml @@ -657,7 +657,7 @@ let error_recursively_dependent_library dir = (* Security weakness: file might have been changed on disk between writing the content and computing the checksum... *) -let save_library_to ?todo dir f otab = +let save_library_to ?todo ~output_native_objects dir f otab = let except = match todo with | None -> (* XXX *) @@ -668,7 +668,7 @@ let save_library_to ?todo dir f otab = assert(Filename.check_suffix f ".vio"); List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in - let cenv, seg, ast = Declaremods.end_library ~except dir in + let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in let tasks, utab, dtab = match todo with @@ -716,7 +716,7 @@ let save_library_to ?todo dir f otab = System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; (* Writing native code files *) - if !Flags.output_native_objects then + if output_native_objects then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Nativelib.compile_library dir ast fn) then user_err Pp.(str "Could not compile the library to native code.") diff --git a/library/library.mli b/library/library.mli index c016352808..a976be0184 100644 --- a/library/library.mli +++ b/library/library.mli @@ -38,9 +38,11 @@ type seg_proofs = Constr.constr Future.computation array an export otherwise just a simple import *) val import_module : bool -> qualid list -> unit -(** End the compilation of a library and save it to a ".vo" file *) +(** End the compilation of a library and save it to a ".vo" file. + [output_native_objects]: when producing vo objects, also compile the native-code version. *) val save_library_to : ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> + output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : |