diff options
34 files changed, 286 insertions, 250 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 5f6aebc4e..412742611 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -161,10 +161,10 @@ let on_body ml hy f = function OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f { Opaqueproof.modlist = ml; abstract = hy } o) -let constr_of_def = function +let constr_of_def otab = function | Undef _ -> assert false | Def cs -> Mod_subst.force_constr cs - | OpaqueDef lc -> Opaqueproof.force_proof lc + | OpaqueDef lc -> Opaqueproof.force_proof otab lc let expmod_constr_subst cache modlist subst c = let c = expmod_constr cache modlist c in @@ -189,7 +189,8 @@ let lift_univs cb subst = subst, Univ.UContext.make (inst,cstrs') else subst, cb.const_universes -let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = +let cook_constant env { from = cb; info } = + let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in let usubst, univs = lift_univs cb usubst in @@ -211,7 +212,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = | TemplateArity (ctx,s) -> let t = mkArity (ctx,Type s.template_level) in let typ = abstract_constant_type (expmod t) hyps in - let j = make_judge (constr_of_def body) typ in + let j = make_judge (constr_of_def (opaque_tables env) body) typ in Typeops.make_polymorphic_if_constant_for_ind env j in let projection pb = diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 51e435d79..d99382129 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -42,10 +42,10 @@ let instantiate cb c = Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c else c -let body_of_constant cb = match cb.const_body with +let body_of_constant otab cb = match cb.const_body with | Undef _ -> None | Def c -> Some (instantiate cb (force_constr c)) - | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof o)) + | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o)) let type_of_constant cb = match cb.const_type with @@ -54,23 +54,24 @@ let type_of_constant cb = if t' == t then x else RegularArity t' | TemplateArity _ as x -> x -let constraints_of_constant cb = Univ.Constraint.union +let constraints_of_constant otab cb = Univ.Constraint.union (Univ.UContext.constraints cb.const_universes) (match cb.const_body with | Undef _ -> Univ.empty_constraint | Def c -> Univ.empty_constraint - | OpaqueDef o -> Univ.ContextSet.constraints (Opaqueproof.force_constraints o)) + | OpaqueDef o -> + Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) -let universes_of_constant cb = +let universes_of_constant otab cb = match cb.const_body with | Undef _ | Def _ -> cb.const_universes | OpaqueDef o -> Univ.UContext.union cb.const_universes - (Univ.ContextSet.to_context (Opaqueproof.force_constraints o)) + (Univ.ContextSet.to_context (Opaqueproof.force_constraints otab o)) -let universes_of_polymorphic_constant cb = +let universes_of_polymorphic_constant otab cb = if cb.const_polymorphic then - let univs = universes_of_constant cb in + let univs = universes_of_constant otab cb in Univ.instantiate_univ_context univs else Univ.UContext.empty @@ -291,9 +292,9 @@ let hcons_mind mib = (** {6 Stm machinery } *) -let join_constant_body cb = +let join_constant_body otab cb = match cb.const_body with - | OpaqueDef o -> Opaqueproof.join_opaque o + | OpaqueDef o -> Opaqueproof.join_opaque otab o | _ -> () let string_of_side_effect = function diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 04a067aff..497856676 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -28,15 +28,19 @@ val constant_has_body : constant_body -> bool (** Accessing const_body, forcing access to opaque proof term if needed. Only use this function if you know what you're doing. *) -val body_of_constant : constant_body -> Term.constr option +val body_of_constant : + Opaqueproof.opaquetab -> constant_body -> Term.constr option val type_of_constant : constant_body -> constant_type -val constraints_of_constant : constant_body -> Univ.constraints -val universes_of_constant : constant_body -> Univ.universe_context +val constraints_of_constant : + Opaqueproof.opaquetab -> constant_body -> Univ.constraints +val universes_of_constant : + Opaqueproof.opaquetab -> constant_body -> Univ.universe_context (** Return the universe context, in case the definition is polymorphic, otherwise the context is empty. *) -val universes_of_polymorphic_constant : constant_body -> Univ.universe_context +val universes_of_polymorphic_constant : + Opaqueproof.opaquetab -> constant_body -> Univ.universe_context val is_opaque : constant_body -> bool @@ -71,7 +75,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body -val join_constant_body : constant_body -> unit +val join_constant_body : Opaqueproof.opaquetab -> constant_body -> unit (** {6 Hash-consing} *) diff --git a/kernel/environ.ml b/kernel/environ.ml index b331d8da7..c3e59487c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -57,6 +57,8 @@ let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context let named_context_val env = env.env_named_context,env.env_named_vals let rel_context env = env.env_rel_context +let opaque_tables env = env.indirect_pterms +let set_opaque_tables env indirect_pterms = { env with indirect_pterms } let empty_context env = match env.env_rel_context, env.env_named_context with diff --git a/kernel/environ.mli b/kernel/environ.mli index 5e9e5264d..a20944758 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,6 +46,9 @@ val rel_context : env -> rel_context val named_context : env -> named_context val named_context_val : env -> named_context_val +val opaque_tables : env -> Opaqueproof.opaquetab +val set_opaque_tables : env -> Opaqueproof.opaquetab -> env + val engagement : env -> engagement option val is_impredicative_set : env -> bool diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index cab3276c3..7a9b12c43 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -72,7 +72,7 @@ let rec check_with_def env struc (idl,c) mp equiv = (* In the spirit of subtyping.check_constant, we accept any implementations of parameters and opaques terms, as long as they have the right type *) - let ccst = Declareops.constraints_of_constant cb in + let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in let env' = Environ.add_constraints ccst env' in let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> diff --git a/kernel/modops.ml b/kernel/modops.ml index 859f83e05..585b38a08 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -612,19 +612,20 @@ let clean_bounded_mod_expr sign = (** {6 Stm machinery } *) -let rec join_module mb = - implem_iter join_signature join_expression mb.mod_expr; - Option.iter join_expression mb.mod_type_alg; - join_signature mb.mod_type -and join_modtype mt = - Option.iter join_expression mt.typ_expr_alg; - join_signature mt.typ_expr -and join_field (l,body) = match body with - |SFBconst sb -> join_constant_body sb +let rec join_module otab mb = + implem_iter (join_signature otab) (join_expression otab) mb.mod_expr; + Option.iter (join_expression otab) mb.mod_type_alg; + join_signature otab mb.mod_type +and join_modtype otab mt = + Option.iter (join_expression otab) mt.typ_expr_alg; + join_signature otab mt.typ_expr +and join_field otab (l,body) = match body with + |SFBconst sb -> join_constant_body otab sb |SFBmind _ -> () - |SFBmodule m -> join_module m - |SFBmodtype m -> join_modtype m -and join_structure struc = List.iter join_field struc -and join_signature sign = functor_iter join_modtype join_structure sign -and join_expression me = functor_iter join_modtype (fun _ -> ()) me + |SFBmodule m -> join_module otab m + |SFBmodtype m -> join_modtype otab m +and join_structure otab struc = List.iter (join_field otab) struc +and join_signature otab sign = + functor_iter (join_modtype otab) (join_structure otab) sign +and join_expression otab me = functor_iter (join_modtype otab) (fun _ -> ()) me diff --git a/kernel/modops.mli b/kernel/modops.mli index 63d71a566..0009b859c 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -80,8 +80,7 @@ val clean_bounded_mod_expr : module_signature -> module_signature (** {6 Stm machinery } *) -val join_module : module_body -> unit -val join_structure : structure_body -> unit +val join_structure : Opaqueproof.opaquetab -> structure_body -> unit (** {6 Errors } *) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index a5def3dc8..52e6eb95d 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -21,7 +21,8 @@ type proofterm = (constr * Univ.universe_context_set) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) | Direct of cooking_info list * proofterm - | NoIndirect of substitution list * proofterm +type opaquetab = (cooking_info list * proofterm) Int.Map.t * DirPath.t +let empty_opaquetab = Int.Map.empty, DirPath.initial (* hooks *) let default_get_opaque dp _ = @@ -31,87 +32,113 @@ let default_get_univ dp _ = Errors.error ("Cannot access universe constraints of opaque proofs in library " ^ DirPath.to_string dp) -let default_mk_indirect _ = None -let default_join_indirect_local_opaque _ _ = () -let default_join_indirect_local_univ _ _ = () let get_opaque = ref default_get_opaque let get_univ = ref default_get_univ -let join_indirect_local_opaque = ref default_join_indirect_local_opaque -let join_indirect_local_univ = ref default_join_indirect_local_univ -let mk_indirect = ref default_mk_indirect let set_indirect_opaque_accessor f = (get_opaque := f) let set_indirect_univ_accessor f = (get_univ := f) -let set_indirect_creator f = (mk_indirect := f) -let set_join_indirect_local_opaque f = join_indirect_local_opaque := f -let set_join_indirect_local_univ f = join_indirect_local_univ := f -let reset_indirect_creator () = mk_indirect := default_mk_indirect (* /hooks *) let create cu = Direct ([],cu) -let turn_indirect o = match o with - | Indirect _ - | NoIndirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque") +let turn_indirect dp o (prfs,odp) = match o with + | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque") | Direct (d,cu) -> let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in - match !mk_indirect (d,cu) with - | None -> Future.sink cu; NoIndirect([],cu) - | Some (dp,i) -> Indirect ([],dp,i) + let id = Int.Map.cardinal prfs in + let prfs = Int.Map.add id (d,cu) prfs in + let ndp = + if DirPath.equal dp odp then odp + else if DirPath.equal odp DirPath.initial then dp + else Errors.anomaly + (Pp.str "Using the same opaque table for multiple dirpaths") in + Indirect ([],dp,id), (prfs, ndp) let subst_opaque sub = function | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) - | NoIndirect (s,uc) -> NoIndirect (sub::s,uc) | Direct _ -> Errors.anomaly (Pp.str "Substituting a Direct opaque") let iter_direct_opaque f = function - | Indirect _ - | NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque") + | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque") | Direct (d,cu) -> Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u)) let discharge_direct_opaque ~cook_constr ci = function - | Indirect _ - | NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque") + | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque") | Direct (d,cu) -> Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u)) -let join_opaque = function +let join_opaque (prfs,odp) = function | Direct (_,cu) -> ignore(Future.join cu) - | NoIndirect (_,cu) -> ignore(Future.join cu) | Indirect (_,dp,i) -> - !join_indirect_local_opaque dp i; - !join_indirect_local_univ dp i + if DirPath.equal dp odp then + let fp = snd (Int.Map.find i prfs) in + ignore(Future.join fp) -let force_proof = function +let uuid_opaque (prfs,odp) = function + | Direct (_,cu) -> Some (Future.uuid cu) + | Indirect (_,dp,i) -> + if DirPath.equal dp odp + then Some (Future.uuid (snd (Int.Map.find i prfs))) + else None + +let force_proof (prfs,odp) = function | Direct (_,cu) -> fst(Future.force cu) - | NoIndirect (l,cu) -> - let c, _ = Future.force cu in - force_constr (List.fold_right subst_substituted l (from_val c)) | Indirect (l,dp,i) -> - let c = Future.force (!get_opaque dp i) in + let pt = + if DirPath.equal dp odp + then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst + else !get_opaque dp i in + let c = Future.force pt in force_constr (List.fold_right subst_substituted l (from_val c)) -let force_constraints = function - | Direct (_,cu) - | NoIndirect(_,cu) -> snd(Future.force cu) +let force_constraints (prfs,odp) = function + | Direct (_,cu) -> snd(Future.force cu) | Indirect (_,dp,i) -> - match !get_univ dp i with - | None -> Univ.ContextSet.empty - | Some u -> Future.force u - -let get_constraints = function - | Direct (_,cu) - | NoIndirect(_,cu) -> Some(Future.chain ~pure:true cu snd) - | Indirect (_,dp,i) -> !get_univ dp i + if DirPath.equal dp odp + then snd (Future.force (snd (Int.Map.find i prfs))) + else match !get_univ dp i with + | None -> Univ.ContextSet.empty + | Some u -> Future.force u + +let get_constraints (prfs,odp) = function + | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd) + | Indirect (_,dp,i) -> + if DirPath.equal dp odp + then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd) + else !get_univ dp i -let get_proof = function +let get_proof (prfs,odp) = function | Direct (_,cu) -> Future.chain ~pure:true cu fst - | NoIndirect(l,cu) -> - Future.chain ~pure:true cu (fun (c,_) -> - force_constr (List.fold_right subst_substituted l (from_val c))) | Indirect (l,dp,i) -> - Future.chain ~pure:true (!get_opaque dp i) (fun c -> + let pt = + if DirPath.equal dp odp + then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst + else !get_opaque dp i in + Future.chain ~pure:true pt (fun c -> force_constr (List.fold_right subst_substituted l (from_val c))) + +module FMap = Future.UUIDMap + +let a_constr = Future.from_val (Term.mkRel 1) +let a_univ = Future.from_val Univ.ContextSet.empty +let a_discharge : cooking_info list = [] + +let dump (otab,_) = + let n = Int.Map.cardinal otab in + let opaque_table = Array.make n a_constr in + let univ_table = Array.make n a_univ in + let disch_table = Array.make n a_discharge in + let f2t_map = ref FMap.empty in + Int.Map.iter (fun n (d,cu) -> + let c, u = Future.split2 ~greedy:true cu in + Future.sink u; + Future.sink c; + opaque_table.(n) <- c; + univ_table.(n) <- u; + disch_table.(n) <- d; + f2t_map := FMap.add (Future.uuid cu) n !f2t_map) + otab; + opaque_table, univ_table, disch_table, !f2t_map diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 092f0aeb1..5f1c28292 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -9,6 +9,7 @@ open Names open Term open Mod_subst +open Int (** This module implements the handling of opaque proof terms. Opauqe proof terms are special since: @@ -20,20 +21,25 @@ open Mod_subst and the [opaque] is turned into an index. *) type proofterm = (constr * Univ.universe_context_set) Future.computation +type opaquetab type opaque +val empty_opaquetab : opaquetab + (** From a [proofterm] to some [opaque]. *) val create : proofterm -> opaque -(** Turn a direct [opaque] into an indirect one, also hashconses constr *) -val turn_indirect : opaque -> opaque +(** Turn a direct [opaque] into an indirect one, also hashconses constr. + * The integer is an hint of the maximum id used so far *) +val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab (** From a [opaque] back to a [constr]. This might use the indirect opaque accessor configured below. *) -val force_proof : opaque -> constr -val force_constraints : opaque -> Univ.universe_context_set -val get_proof : opaque -> Term.constr Future.computation -val get_constraints : opaque -> Univ.universe_context_set Future.computation option +val force_proof : opaquetab -> opaque -> constr +val force_constraints : opaquetab -> opaque -> Univ.universe_context_set +val get_proof : opaquetab -> opaque -> Term.constr Future.computation +val get_constraints : + opaquetab -> opaque -> Univ.universe_context_set Future.computation option val subst_opaque : substitution -> opaque -> opaque val iter_direct_opaque : (constr -> unit) -> opaque -> opaque @@ -52,7 +58,14 @@ type cooking_info = { val discharge_direct_opaque : cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque -val join_opaque : opaque -> unit +val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option +val join_opaque : opaquetab -> opaque -> unit + +val dump : opaquetab -> + Constr.t Future.computation array * + Univ.universe_context_set Future.computation array * + cooking_info list array * + int Future.UUIDMap.t (** When stored indirectly, opaque terms are indexed by their library dirpath and an integer index. The following two functions activate @@ -61,12 +74,8 @@ val join_opaque : opaque -> unit any indirect link, and default accessor always raises an error. *) -val set_indirect_creator : - (cooking_info list * proofterm -> (DirPath.t * int) option) -> unit val set_indirect_opaque_accessor : (DirPath.t -> int -> Term.constr Future.computation) -> unit val set_indirect_univ_accessor : (DirPath.t -> int -> Univ.universe_context_set Future.computation option) -> unit -val set_join_indirect_local_opaque : (DirPath.t -> int -> unit) -> unit -val set_join_indirect_local_univ : (DirPath.t -> int -> unit) -> unit -val reset_indirect_creator : unit -> unit + diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index a5221c779..48043f116 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -74,7 +74,9 @@ type env = { env_nb_rel : int; env_stratification : stratification; env_conv_oracle : Conv_oracle.oracle; - retroknowledge : Retroknowledge.retroknowledge } + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} type named_context_val = named_context * named_vals @@ -96,7 +98,8 @@ let empty_env = { env_engagement = None; env_type_in_type = false}; env_conv_oracle = Conv_oracle.empty; - retroknowledge = Retroknowledge.initial_retroknowledge } + retroknowledge = Retroknowledge.initial_retroknowledge; + indirect_pterms = Opaqueproof.empty_opaquetab } (* Rel context *) @@ -141,7 +144,9 @@ let push_named d env = env_nb_rel = env.env_nb_rel; env_stratification = env.env_stratification; env_conv_oracle = env.env_conv_oracle; - retroknowledge = env.retroknowledge; } + retroknowledge = env.retroknowledge; + indirect_pterms = env.indirect_pterms; + } let lookup_named_val id env = snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals) diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 9561333c8..7ef2ab009 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -54,7 +54,9 @@ type env = { env_nb_rel : int; env_stratification : stratification; env_conv_oracle : Conv_oracle.oracle; - retroknowledge : Retroknowledge.retroknowledge } + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} type named_context_val = named_context * named_vals diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f7464013f..9aca7727b 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -125,7 +125,7 @@ type safe_environment = type_in_type : bool; imports : vodigest DPMap.t; loads : (module_path * module_body) list; - local_retroknowledge : Retroknowledge.action list} + local_retroknowledge : Retroknowledge.action list } and modvariant = | NONE @@ -133,6 +133,12 @@ and modvariant = | SIG of module_parameters * safe_environment (** saved env *) | STRUCT of module_parameters * safe_environment (** saved env *) +let rec library_dp_of_senv senv = + match senv.modvariant with + | NONE | LIBRARY -> ModPath.dp senv.modpath + | SIG(_,senv) -> library_dp_of_senv senv + | STRUCT(_,senv) -> library_dp_of_senv senv + let empty_environment = { env = Environ.empty_env; modpath = initial_path; @@ -219,7 +225,7 @@ let is_curmod_library senv = match senv.modvariant with LIBRARY -> true | _ -> false let join_safe_environment e = - Modops.join_structure e.revstruct; + Modops.join_structure (Environ.opaque_tables e.env) e.revstruct; List.fold_left (fun e fc -> add_constraints (Now (Future.join fc)) e) {e with future_cst = []} e.future_cst @@ -312,9 +318,12 @@ let push_named_def (id,de) senv = let c,typ,univs = Term_typing.translate_local_def senv.env id de in let senv' = push_context univs senv in let c, senv' = match c with - | Def c -> Mod_subst.force_constr c, senv' - | OpaqueDef o -> Opaqueproof.force_proof o, - push_context_set (Opaqueproof.force_constraints o) senv' + | Def c -> Mod_subst.force_constr c, senv' + | OpaqueDef o -> + Opaqueproof.force_proof (Environ.opaque_tables senv'.env) o, + push_context_set + (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o) + senv' | _ -> assert false in let env'' = safe_push_named (id,Some c,typ) senv'.env in {senv' with env=env''} @@ -341,7 +350,7 @@ let labels_of_mib mib = Array.iter visit_mip mib.mind_packets; get () -let globalize_constant_universes cb = +let globalize_constant_universes env cb = if cb.const_polymorphic then [Now Univ.Constraint.empty] else @@ -350,7 +359,7 @@ let globalize_constant_universes cb = (match cb.const_body with | (Undef _ | Def _) -> [] | OpaqueDef lc -> - match Opaqueproof.get_constraints lc with + match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with | None -> [] | Some fc -> match Future.peek_val fc with @@ -363,9 +372,9 @@ let globalize_mind_universes mb = else [Now (Univ.UContext.constraints mb.mind_universes)] -let constraints_of_sfb sfb = +let constraints_of_sfb env sfb = match sfb with - | SFBconst cb -> globalize_constant_universes cb + | SFBconst cb -> globalize_constant_universes env cb | SFBmind mib -> globalize_mind_universes mib | SFBmodtype mtb -> [Now mtb.typ_constraints] | SFBmodule mb -> [Now mb.mod_constraints] @@ -389,7 +398,7 @@ let add_field ((l,sfb) as field) gn senv = | SFBmodule _ | SFBmodtype _ -> check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty) in - let cst = constraints_of_sfb sfb in + let cst = constraints_of_sfb senv.env sfb in let senv = add_constraints_list cst senv in let env' = match sfb, gn with | SFBconst cb, C con -> Environ.add_constant con cb senv.env @@ -421,13 +430,17 @@ let add_constant dir l decl senv = let cb = Term_typing.translate_recipe senv.env kn r in if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb in - let cb = match cb.const_body with + let cb, otab = match cb.const_body with | OpaqueDef lc when DirPath.is_empty dir -> (* In coqc, opaque constants outside sections will be stored indirectly in a specific table *) - { cb with const_body = OpaqueDef (Opaqueproof.turn_indirect lc) } - | _ -> cb + let od, otab = + Opaqueproof.turn_indirect + (library_dp_of_senv senv) lc (Environ.opaque_tables senv.env) in + { cb with const_body = OpaqueDef od }, otab + | _ -> cb, (Environ.opaque_tables senv.env) in + let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with | Undef (Some lev) -> @@ -588,7 +601,7 @@ let propagate_senv newdef newenv newresolver senv oldsenv = imports = senv.imports; loads = senv.loads@oldsenv.loads; local_retroknowledge = - senv.local_retroknowledge@oldsenv.local_retroknowledge } + senv.local_retroknowledge@oldsenv.local_retroknowledge } let end_module l restype senv = let mp = senv.modpath in @@ -597,7 +610,7 @@ let end_module l restype senv = let () = check_empty_context senv in let mbids = List.rev_map fst params in let mb = build_module_body params restype senv in - let newenv = oldsenv.env in + let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in let newenv = set_engagement_opt newenv senv.engagement in let senv'= propagate_loads { senv with @@ -619,7 +632,7 @@ let end_modtype l senv = let () = check_empty_context senv in let mbids = List.rev_map fst params in let auto_tb = NoFunctor (List.rev senv.revstruct) in - let newenv = oldsenv.env in + let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in let newenv = Environ.add_constraints senv.univ newenv in let newenv = set_engagement_opt newenv senv.engagement in let senv' = propagate_loads {senv with env=newenv} in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 4f54220e7..857f577a8 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -352,7 +352,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let u1 = inductive_instance mind1 in let arity1,cst1 = constrained_type_of_inductive env ((mind1,mind1.mind_packets.(i)),u1) in - let cst2 = Declareops.constraints_of_constant cb2 in + let cst2 = + Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in let typ2 = Typeops.type_of_constant_type env cb2.const_type in let cst = Constraint.union cst (Constraint.union cst1 cst2) in let error = NotConvertibleTypeField (env, arity1, typ2) in @@ -367,7 +368,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; let u1 = inductive_instance mind1 in let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in - let cst2 = Declareops.constraints_of_constant cb2 in + let cst2 = + Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in let ty2 = Typeops.type_of_constant_type env cb2.const_type in let cst = Constraint.union cst (Constraint.union cst1 cst2) in let error = NotConvertibleTypeField (env, ty1, ty2) in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 232508bc8..415e91f70 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -86,7 +86,7 @@ let handle_side_effects env body side_eff = let univs = cb.const_universes in sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t) | OpaqueDef b -> - let b = Opaqueproof.force_proof b in + let b = Opaqueproof.force_proof (opaque_tables env) b in let poly = cb.const_polymorphic in if not poly then let b_ty = Typeops.type_of_constant_type env cb.const_type in @@ -217,9 +217,11 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) | Undef _ -> Idset.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) | OpaqueDef lc -> - let vars = global_vars_set env (Opaqueproof.force_proof lc) in + let vars = + global_vars_set env + (Opaqueproof.force_proof (opaque_tables env) lc) in (* we force so that cst are added to the env immediately after *) - ignore(Opaqueproof.force_constraints lc); + ignore(Opaqueproof.force_constraints (opaque_tables env) lc); !suggest_proof_using kn env vars ids_typ context_ids; if !Flags.compilation_mode = Flags.BuildVo then record_aux env ids_typ vars; diff --git a/lib/future.ml b/lib/future.ml index 77386a1a9..6ebbd4b1d 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -40,6 +40,8 @@ module UUID = struct let equal = (==) end +module UUIDMap = Map.Make(UUID) + type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] (* Val is not necessarily a final state, so the diff --git a/lib/future.mli b/lib/future.mli index c4b55db25..18b014132 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -60,6 +60,8 @@ module UUID : sig val equal : t -> t -> bool end +module UUIDMap : Map.S with type key = UUID.t + exception NotReady type 'a computation diff --git a/library/assumptions.ml b/library/assumptions.ml index e4638f5e4..b01e24196 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -236,7 +236,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = else (s, acc) else (s, acc) in - match Declareops.body_of_constant cb with + match Global.body_of_constant_body cb with | None -> do_type (Axiom kn) | Some body -> do_constr body s acc diff --git a/library/declare.ml b/library/declare.ml index 1c9e10a19..4ec81c49f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -116,7 +116,7 @@ let open_constant i ((sp,kn), obj) = match (Global.lookup_constant con).const_body with | (Def _ | Undef _) -> () | OpaqueDef lc -> - match Opaqueproof.get_constraints lc with + match Opaqueproof.get_constraints (Global.opaque_tables ())lc with | Some f when Future.is_val f -> Global.push_context_set (Future.force f) | _ -> () @@ -208,7 +208,8 @@ let declare_sideff env fix_exn se = match cb with | { const_body = Def sc } -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false | { const_body = OpaqueDef fc } -> - (Opaqueproof.force_proof fc, Opaqueproof.force_constraints fc), true + (Opaqueproof.force_proof (Environ.opaque_tables env) fc, + Opaqueproof.force_constraints (Environ.opaque_tables env) fc), true | { const_body = Undef _ } -> anomaly(str"Undefined side effect") in let ty_of cb = diff --git a/library/global.ml b/library/global.ml index 80238d8e2..49f78e495 100644 --- a/library/global.ml +++ b/library/global.ml @@ -113,6 +113,14 @@ let lookup_modtype kn = lookup_modtype kn (env()) let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) +let opaque_tables () = Environ.opaque_tables (env ()) +let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb +let body_of_constant cst = body_of_constant_body (lookup_constant cst) +let constraints_of_constant_body cb = + Declareops.constraints_of_constant (opaque_tables ()) cb +let universes_of_constant_body cb = + Declareops.universes_of_constant (opaque_tables ()) cb + (** Operations on kernel names *) let constant_of_delta_kn kn = @@ -153,7 +161,9 @@ let type_of_global_unsafe r = | VarRef id -> Environ.named_type id env | ConstRef c -> let cb = Environ.lookup_constant c env in - let univs = Declareops.universes_of_polymorphic_constant cb in + let univs = + Declareops.universes_of_polymorphic_constant + (Environ.opaque_tables env) cb in let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in Vars.subst_instance_constr (Univ.UContext.instance univs) ty | IndRef ind -> @@ -175,7 +185,9 @@ let type_of_global_in_context env r = | VarRef id -> Environ.named_type id env, Univ.UContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - let univs = Declareops.universes_of_polymorphic_constant cb in + let univs = + Declareops.universes_of_polymorphic_constant + (Environ.opaque_tables env) cb in Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in @@ -198,7 +210,8 @@ let universes_of_global env r = | VarRef id -> Univ.UContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - Declareops.universes_of_polymorphic_constant cb + Declareops.universes_of_polymorphic_constant + (Environ.opaque_tables env) cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in Univ.instantiate_univ_context mib.mind_universes diff --git a/library/global.mli b/library/global.mli index 7dcfdbd3a..8ae77a9e4 100644 --- a/library/global.mli +++ b/library/global.mli @@ -87,6 +87,14 @@ val exists_objlabel : Label.t -> bool val constant_of_delta_kn : kernel_name -> constant val mind_of_delta_kn : kernel_name -> mutual_inductive +val opaque_tables : unit -> Opaqueproof.opaquetab +val body_of_constant : constant -> Term.constr option +val body_of_constant_body : Declarations.constant_body -> Term.constr option +val constraints_of_constant_body : + Declarations.constant_body -> Univ.constraints +val universes_of_constant_body : + Declarations.constant_body -> Univ.universe_context + (** {6 Compiled libraries } *) val start_library : DirPath.t -> module_path diff --git a/library/heads.ml b/library/heads.ml index 8b28f0500..94ce11731 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -123,7 +123,7 @@ let compute_head = function let is_Def = function Declarations.Def _ -> true | _ -> false in let body = if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body - then Declareops.body_of_constant cb else None + then Declareops.body_of_constant (Environ.opaque_tables env) cb else None in (match body with | None -> RigidHead (RigidParameter cst) diff --git a/library/library.ml b/library/library.ml index 7bff05cda..7f5ca5af6 100644 --- a/library/library.ml +++ b/library/library.ml @@ -351,87 +351,15 @@ let access_opaque_table dp i = (fetch_table "opaque proofs") add_opaque_table !opaque_tables dp i let access_univ_table dp i = - access_table - (fetch_table "universe contexts of opaque proofs") - add_univ_table !univ_tables dp i - -(** Table of opaque terms from the library currently being compiled *) - -module OpaqueTables = struct - - let a_constr = Future.from_val (Term.mkRel 1) - let a_univ = Future.from_val Univ.ContextSet.empty - let a_discharge : Opaqueproof.cooking_info list = [] - - let local_opaque_table = ref (Array.make 100 a_constr) - let local_univ_table = ref (Array.make 100 a_univ) - let local_discharge_table = ref (Array.make 100 a_discharge) - let local_index = ref 0 - - module FMap = Map.Make(Future.UUID) - let f2t = ref FMap.empty - - let get_opaque dp i = - if DirPath.equal dp (Lib.library_dp ()) - then (!local_opaque_table).(i) - else access_opaque_table dp i - - let join_local_opaque dp i = - if DirPath.equal dp (Lib.library_dp ()) then - ignore(Future.force (!local_opaque_table).(i)) - - let join_local_univ dp i = - if DirPath.equal dp (Lib.library_dp ()) then - ignore(Future.join (!local_univ_table).(i)) - - let get_univ dp i = - if DirPath.equal dp (Lib.library_dp ()) - then Some (!local_univ_table).(i) - else try Some (access_univ_table dp i) with Not_found -> None - - let store (d,cu) = - let n = !local_index in - incr local_index; - if Int.equal n (Array.length !local_opaque_table) then begin - let t = Array.make (2*n) a_constr in - Array.blit !local_opaque_table 0 t 0 n; - local_opaque_table := t; - let t = Array.make (2*n) a_univ in - Array.blit !local_univ_table 0 t 0 n; - local_univ_table := t; - let t = Array.make (2*n) a_discharge in - Array.blit !local_discharge_table 0 t 0 n; - local_discharge_table := t - end; - let c, u = Future.split2 ~greedy:true cu in - Future.sink u; - Future.sink c; - (!local_opaque_table).(n) <- c; - (!local_univ_table).(n) <- u; - (!local_discharge_table).(n) <- d; - f2t := FMap.add (Future.uuid cu) n !f2t; - Some (Lib.library_dp (), n) - - let dump () = - Array.sub !local_opaque_table 0 !local_index, - Array.sub !local_univ_table 0 !local_index, - Array.sub !local_discharge_table 0 !local_index, - FMap.bindings !f2t - - let reset () = - local_discharge_table := Array.make 100 a_discharge; - local_univ_table := Array.make 100 a_univ; - local_opaque_table := Array.make 100 a_constr; - f2t := FMap.empty; - local_index := 0 - -end + try + Some (access_table + (fetch_table "universe contexts of opaque proofs") + add_univ_table !univ_tables dp i) + with Not_found -> None let () = - Opaqueproof.set_indirect_opaque_accessor OpaqueTables.get_opaque; - Opaqueproof.set_indirect_univ_accessor OpaqueTables.get_univ; - Opaqueproof.set_join_indirect_local_opaque OpaqueTables.join_local_opaque; - Opaqueproof.set_join_indirect_local_univ OpaqueTables.join_local_univ + Opaqueproof.set_indirect_opaque_accessor access_opaque_table; + Opaqueproof.set_indirect_univ_accessor access_univ_table (************************************************************************) (* Internalise libraries *) @@ -694,8 +622,6 @@ let start_library f = check_module_name file; check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in - OpaqueTables.reset (); - Opaqueproof.set_indirect_creator OpaqueTables.store; Declaremods.start_library ldir; ldir,longf @@ -743,7 +669,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 = +let save_library_to ?todo dir f otab = let f, todo, utab, dtab = match todo with | None -> @@ -753,10 +679,8 @@ let save_library_to ?todo dir f = assert(!Flags.compilation_mode = Flags.BuildVi); f ^ "i", (fun x -> Some (d x)), (fun x -> Some (x,Univ.ContextSet.empty,false)), (fun x -> Some x) in - Opaqueproof.reset_indirect_creator (); let cenv, seg, ast = Declaremods.end_library dir in - let opaque_table, univ_table, disch_table, f2t_map = - OpaqueTables.dump () in + let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in assert(!Flags.compilation_mode = Flags.BuildVi || Array.for_all Future.is_val opaque_table); let md = { diff --git a/library/library.mli b/library/library.mli index 5154c25e4..c92b9d623 100644 --- a/library/library.mli +++ b/library/library.mli @@ -43,8 +43,8 @@ val import_module : bool -> qualid located -> unit val start_library : string -> DirPath.t * string (** {6 End the compilation of a library and save it to a ".vo" file } *) -val save_library_to : ?todo:((Future.UUID.t * int) list -> 'tasks) -> - DirPath.t -> string -> unit +val save_library_to : ?todo:(int Future.UUIDMap.t -> 'tasks) -> + DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs diff --git a/library/universes.ml b/library/universes.ml index cc0153311..708324aed 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -310,7 +310,10 @@ let unsafe_instance_from ctx = let fresh_constant_instance env c inst = let cb = lookup_constant c env in if cb.Declarations.const_polymorphic then - let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) inst in + let inst, ctx = + fresh_instance_from + (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst + in ((c, inst), ctx) else ((c,Instance.empty), ContextSet.empty) @@ -331,7 +334,8 @@ let fresh_constructor_instance env (ind,i) inst = let unsafe_constant_instance env c = let cb = lookup_constant c env in if cb.Declarations.const_polymorphic then - let inst, ctx = unsafe_instance_from (Declareops.universes_of_constant cb) in + let inst, ctx = unsafe_instance_from + (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in ((c, inst), ctx) else ((c,Instance.empty), UContext.empty) @@ -441,7 +445,7 @@ let type_of_reference env r = let cb = Environ.lookup_constant c env in let ty = Typeops.type_of_constant_type env cb.const_type in if cb.const_polymorphic then - let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) None in + let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in Vars.subst_instance_constr inst ty, ctx else ty, ContextSet.empty diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index ea2239673..cae7f0999 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1013,7 +1013,7 @@ let extract_constant env kn cb = | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_typ (Opaqueproof.force_proof c) + mk_typ (Opaqueproof.force_proof (Environ.opaque_tables env) c) else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with @@ -1022,7 +1022,7 @@ let extract_constant env kn cb = | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_def (Opaqueproof.force_proof c) + mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c) else mk_ax ()) let extract_constant_spec env kn cb = diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index cd3f1a5d4..b740e192a 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -948,8 +948,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) let f_def = Global.lookup_constant (fst (destConst f)) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in - let f_body = Option.get (body_of_constant f_def) - in + let f_body = Option.get (Global.body_of_constant_body f_def)in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in let fnames_with_params = @@ -1065,7 +1064,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : } in let get_body const = - match body_of_constant (Global.lookup_constant const) with + match Global.body_of_constant const with | Some body -> Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c4a340880..41f3a5a8b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -384,7 +384,7 @@ let get_funs_constant mp dp = in function const -> let find_constant_body const = - match body_of_constant (Global.lookup_constant const) with + match Global.body_of_constant const with | Some body -> let body = Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index b613a4b13..71ebf4923 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -763,7 +763,7 @@ let make_graph (f_ref:global_reference) = | _ -> raise (UserError ("", str "Not a function reference") ) in Dumpglob.pause (); - (match body_of_constant c_body with + (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom !" | Some body -> let env = Global.env () in diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e0f6ef25c..efdbb0dc4 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -470,10 +470,10 @@ let ungeneralized_type_of_constant_type t = let print_constant with_values sep sp = let cb = Global.lookup_constant sp in - let val_0 = Declareops.body_of_constant cb in + let val_0 = Global.body_of_constant_body cb in let typ = Declareops.type_of_constant cb in let typ = ungeneralized_type_of_constant_type typ in - let univs = Univ.instantiate_univ_context (Declareops.universes_of_constant cb) in + let univs = Univ.instantiate_univ_context (Global.universes_of_constant_body cb) in hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> @@ -626,7 +626,7 @@ let print_full_pure_context () = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr (Opaqueproof.force_proof lc) + str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 36f2b14cb..b0fea5916 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -47,7 +47,7 @@ let retrieve_first_recthm = function (pi2 (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - (body_of_constant cb, is_opaque cb) + (Global.body_of_constant_body cb, is_opaque cb) | _ -> assert false let adjust_guardness_conditions const = function diff --git a/stm/stm.ml b/stm/stm.ml index 3e8181fe9..b68ef9496 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -805,8 +805,9 @@ module Task = struct List.iter (fun (_,se) -> Declareops.iter_side_effects (function | Declarations.SEsubproof(_, { Declarations.const_body = Declarations.OpaqueDef f; - const_universes = univs } ) -> - Opaqueproof.join_opaque f + const_universes = univs } ) -> + (* They are Direct *) + Opaqueproof.join_opaque Opaqueproof.empty_opaquetab f | _ -> ()) se) (fst l); l, Unix.gettimeofday () -. wall_clock in @@ -885,7 +886,8 @@ module Slaves : sig val slave_init_stdout : unit -> unit type tasks - val dump : (Future.UUID.t * int) list -> tasks + val dump_final : int Future.UUIDMap.t -> tasks + val dump_snapshot : int Future.UUIDMap.t -> tasks val check_task : string -> tasks -> int -> bool val info_tasks : tasks -> (string * float * int) list val finish_task : @@ -953,21 +955,24 @@ end = struct Nametab.locate_constant (Libnames.qualid_of_ident po.Proof_global.id) in let c = Global.lookup_constant con in - match c.Declarations.const_body with - | Declarations.OpaqueDef lc -> - let uc = Option.get (Opaqueproof.get_constraints lc) in - let uc = - Future.chain - ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in - let pr = Opaqueproof.get_proof lc in - let pr = Future.chain ~greedy:true ~pure:true pr discharge in - let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in - Future.sink pr; - let extra = Future.join uc in - u.(bucket) <- uc; - p.(bucket) <- pr; - u, Univ.ContextSet.union cst extra, false - | _ -> assert false + let o = match c.Declarations.const_body with + | Declarations.OpaqueDef o -> o + | _ -> assert false in + let uc = + Option.get + (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in + let pr = + Future.from_val (Option.get (Global.body_of_constant_body c)) in + let uc = + Future.chain + ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in + let pr = Future.chain ~greedy:true ~pure:true pr discharge in + let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in + Future.sink pr; + let extra = Future.join uc in + u.(bucket) <- uc; + p.(bucket) <- pr; + u, Univ.ContextSet.union cst extra, false let check_task name l i = match check_task_aux "" name l i with @@ -1031,7 +1036,12 @@ end = struct let dump f2t_map = let tasks = TaskQueue.dump () in prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks)); - List.map (function r -> { r with r_uuid = List.assoc r.r_uuid f2t_map }) + List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map }) + (CList.map_filter (Task.request_of_task `Fresh) tasks) + let dump_snapshot f2t_map = + let tasks = TaskQueue.snapshot () in + prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks)); + List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map }) (CList.map_filter (Task.request_of_task `Fresh) tasks) end diff --git a/stm/stm.mli b/stm/stm.mli index 75aa08e7b..d77c19cfb 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -48,7 +48,8 @@ val stop_worker : string -> unit val join : unit -> unit (* To save to disk an incomplete document *) type tasks -val dump : (Future.UUID.t * int) list -> tasks +val dump_final : int Future.UUIDMap.t -> tasks +val dump_snapshot : int Future.UUIDMap.t -> tasks val check_task : string -> tasks -> int -> bool val info_tasks : tasks -> (string * float * int) list diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 248a6b513..dcce58199 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -321,7 +321,7 @@ let compile verbosely f = Stm.join (); let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); - Library.save_library_to ldir long_f_dot_v; + Library.save_library_to ldir long_f_dot_v (Global.opaque_tables ()); Aux_file.record_in_aux_at Loc.ghost "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); @@ -333,7 +333,8 @@ let compile verbosely f = let _ = load_vernac verbosely long_f_dot_v in Stm.finish (); check_pending_proofs (); - Library.save_library_to ~todo:Stm.dump ldir long_f_dot_v + Library.save_library_to ~todo:Stm.dump_final ldir long_f_dot_v + (Global.opaque_tables ()) | Vi2Vo -> let open Filename in let open Library in |