diff options
33 files changed, 232 insertions, 252 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index aedd09560..6415a1a78 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -58,7 +58,7 @@ Copcodes Cemitcodes Nativevalues Future -Lazyconstr +Opaqueproof Declareops Retroknowledge Conv_oracle diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 82155a305..eefd07e60 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -58,7 +58,7 @@ let ppevar evk = pp (str (Evd.string_of_existential evk)) let ppconstr x = pp (Termops.print_constr x) let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) let ppterm = ppconstr -let ppsconstr x = ppconstr (Lazyconstr.force x) +let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index af6992252..58465849c 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -719,7 +719,7 @@ let compile env c = let compile_constant_body env = function | Undef _ | OpaqueDef _ -> BCconstant | Def sb -> - let body = Lazyconstr.force sb in + let body = Mod_subst.force_constr sb in match kind_of_term body with | Const kn' -> (* we use the canonical name of the constant*) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 75642648d..f81bcceb3 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -109,7 +109,7 @@ let abstract_constant_type = let abstract_constant_body = List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c) -type recipe = { from : constant_body; info : Lazyconstr.cooking_info } +type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool type result = @@ -118,21 +118,22 @@ type result = let on_body ml hy f = function | Undef _ as x -> x - | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs))) - | OpaqueDef lc -> - OpaqueDef (Lazyconstr.discharge_direct_lazy_constr ml hy f lc) + | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs))) + | OpaqueDef o -> + OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f + { Opaqueproof.modlist = ml; abstract = hy } o) let constr_of_def = function | Undef _ -> assert false - | Def cs -> Lazyconstr.force cs - | OpaqueDef lc -> Lazyconstr.force_opaque lc + | Def cs -> Mod_subst.force_constr cs + | OpaqueDef lc -> Opaqueproof.force_proof lc -let cook_constr { Lazyconstr.modlist ; abstract } c = +let cook_constr { Opaqueproof.modlist ; abstract } c = let cache = Hashtbl.create 13 in let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in abstract_constant_body (expmod_constr cache modlist c) hyps -let cook_constant env { from = cb; info = { Lazyconstr.modlist; abstract } } = +let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = let cache = Hashtbl.create 13 in let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in let body = on_body modlist hyps diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 05c7a2040..8493b81d8 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -14,7 +14,7 @@ open Univ (** {6 Cooking the constants. } *) -type recipe = { from : constant_body; info : Lazyconstr.cooking_info } +type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool @@ -23,9 +23,9 @@ type result = * Context.section_context option val cook_constant : env -> recipe -> result -val cook_constr : Lazyconstr.cooking_info -> Term.constr -> Term.constr +val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr (** {6 Utility functions used in module [Discharge]. } *) -val expmod_constr : Lazyconstr.work_list -> constr -> constr +val expmod_constr : Opaqueproof.work_list -> constr -> constr diff --git a/kernel/declarations.mli b/kernel/declarations.mli index ef56ae512..e6025790a 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -37,8 +37,8 @@ type inline = int option type constant_def = | Undef of inline - | Def of Lazyconstr.constr_substituted - | OpaqueDef of Lazyconstr.lazy_constr + | Def of constr Mod_subst.substituted + | OpaqueDef of Opaqueproof.opaque (* some contraints are in constant_constraints, some other may be in * the OpaueDef *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 21a961fc3..7c852a755 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -8,7 +8,6 @@ open Declarations open Mod_subst -open Lazyconstr open Util (** Operations concernings types in [Declarations] : @@ -18,14 +17,14 @@ open Util let body_of_constant cb = match cb.const_body with | Undef _ -> None - | Def c -> Some (Lazyconstr.force c) - | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc) + | Def c -> Some (force_constr c) + | OpaqueDef o -> Some (Opaqueproof.force_proof o) let constraints_of_constant cb = Univ.union_constraints cb.const_constraints (match cb.const_body with | Undef _ -> Univ.empty_constraint | Def c -> Univ.empty_constraint - | OpaqueDef lc -> snd (Lazyconstr.force_opaque_w_constraints lc)) + | OpaqueDef o -> Opaqueproof.force_constraints o) let constant_has_body cb = match cb.const_body with | Undef _ -> false @@ -57,8 +56,8 @@ let subst_const_type sub arity = match arity with let subst_const_def sub def = match def with | Undef _ -> def - | Def c -> Def (subst_constr_subst sub c) - | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) + | Def c -> Def (subst_constr sub c) + | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o) let subst_const_body sub cb = assert (List.is_empty cb.const_hyps); (* we're outside sections *) @@ -104,7 +103,7 @@ let hcons_const_type = function let hcons_const_def = function | Undef inl -> Undef inl | Def l_constr -> - let constr = force l_constr in + let constr = force_constr l_constr in Def (from_val (Term.hcons_constr constr)) | OpaqueDef _ as x -> x (* hashconsed when turned indirect *) @@ -238,7 +237,7 @@ let hcons_mind mib = let join_constant_body cb = match cb.const_body with - | OpaqueDef d -> Lazyconstr.join_lazy_constr d + | OpaqueDef o -> Opaqueproof.join_opaque o | _ -> () let string_of_side_effect = function diff --git a/kernel/environ.ml b/kernel/environ.ml index 93677e5a9..15db39328 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -189,7 +189,7 @@ exception NotEvaluableConst of const_evaluation_result let constant_value env kn = let cb = lookup_constant kn env in match cb.const_body with - | Def l_body -> Lazyconstr.force l_body + | Def l_body -> Mod_subst.force_constr l_body | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 7d318add5..bcd366f1a 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -12,7 +12,7 @@ Cbytecodes Copcodes Cemitcodes Nativevalues -Lazyconstr +Opaqueproof Declareops Retroknowledge Conv_oracle diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml deleted file mode 100644 index 23d6d559d..000000000 --- a/kernel/lazyconstr.ml +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Term -open Mod_subst - -type work_list = Id.t array Cmap.t * Id.t array Mindmap.t -type cooking_info = { modlist : work_list; abstract : Context.named_context } - -(** [constr_substituted] are [constr] with possibly pending - substitutions of kernel names. *) - -type constr_substituted = constr substituted - -let from_val = from_val - -let force = force subst_mps - -let subst_constr_subst = subst_substituted - -(** Opaque proof terms might be in some external tables. - The [force_opaque] function below allows to access these tables, - this might trigger the read of some extra parts of .vo files. - In the [Indirect] case, we accumulate "manually" a substitution - list, the younger one coming first. Nota: no [Direct] constructor - should end in a .vo, this is checked by coqchk. -*) - -type proofterm = (constr * Univ.constraints) Future.computation -type lazy_constr = - (* subst, lib, index *) - | Indirect of substitution list * DirPath.t * int - (* opaque in section or interactive session *) - | Direct of cooking_info list * (constr_substituted * Univ.constraints) Future.computation - -(* TODO : this hcons function could probably be improved (for instance - hash the dir_path in the Indirect case) *) - -let subst_lazy_constr sub = function - | Direct ([],cu) -> - Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c, u) -> - subst_constr_subst sub c, u)) - | Direct _ -> Errors.anomaly (Pp.str"still direct but not discharged") - | Indirect (l,dp,i) -> Indirect (sub::l,dp,i) - -let iter_direct_lazy_constr f = function - | Indirect _ -> Errors.anomaly (Pp.str "iter_direct_lazy_constr") - | Direct (d,cu) -> - Direct (d, Future.chain ~greedy:true ~pure:true cu (fun (c, u) -> f (force c); c, u)) - -let discharge_direct_lazy_constr modlist abstract f = function - | Indirect _ -> Errors.anomaly (Pp.str "discharge_direct_lazy_constr") - | Direct (d,cu) -> - Direct ({ modlist; abstract }::d, - Future.chain ~greedy:true ~pure:true cu (fun (c, u) -> - from_val (f (force c)), u)) - -let default_get_opaque dp _ = - Errors.error - ("Cannot access opaque proofs in library " ^ DirPath.to_string dp) -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 - -let force_lazy_constr = function - | Direct (_,c) -> Future.force c - | Indirect (l,dp,i) -> - let c = Future.force (!get_opaque dp i) in - List.fold_right subst_constr_subst l (from_val c), - Future.force - (Option.default - (Future.from_val Univ.empty_constraint) - (!get_univ dp i)) - -let join_lazy_constr = function - | Direct (_,c) -> ignore(Future.force c) - | Indirect (_,dp,i) -> - !join_indirect_local_opaque dp i; - !join_indirect_local_univ dp i - -let turn_indirect lc = match lc with - | Indirect _ -> - Errors.anomaly (Pp.str "Indirecting an already indirect opaque") - | Direct (d,cu) -> - let cu = Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> - (* this constr_substituted shouldn't have been substituted yet *) - assert (fst (Mod_subst.repr_substituted c) == None); - hcons_constr (force c),u) in - match !mk_indirect (d,cu) with - | None -> lc - | Some (dp,i) -> Indirect ([],dp,i) - -let force_opaque lc = - let c, _u = force_lazy_constr lc in force c -let force_opaque_w_constraints lc = - let c, u = force_lazy_constr lc in force c, u -let get_opaque_future_constraints lc = match lc with - | Indirect (_,dp,i) -> !get_univ dp i - | Direct (_,cu) -> Some(snd (Future.split2 ~greedy:true cu)) -let get_opaque_futures lc = match lc with - | Indirect _ -> assert false - | Direct (_,cu) -> - let cu = - Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> force c, u) in - Future.split2 ~greedy:true cu - -let opaque_from_val cu = - Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> from_val c, u)) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 009bcb770..f0d1aca4d 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -546,6 +546,9 @@ let force fsubst r = match r.subst_subst with let subst_substituted s r = { r with subst_subst = s :: r.subst_subst; } +let force_constr = force subst_mps +let subst_constr = subst_substituted + (* debug *) let repr_substituted r = match r.subst_subst with | [] -> None, r.subst_value diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index ddc05380a..34f10b31a 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -152,3 +152,7 @@ val occur_mbid : MBId.t -> substitution -> bool - [Some s, a] when r is a delayed substitution [s] applied to [a] *) val repr_substituted : 'a substituted -> substitution list option * 'a + +val force_constr : Term.constr substituted -> Term.constr +val subst_constr : + substitution -> Term.constr substituted -> Term.constr substituted diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 6e656fad9..6c0f1b060 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -80,11 +80,11 @@ let rec check_with_def env struc (idl,c) mp equiv = let cst = cb.const_constraints +++ cst1 +++ cst2 in j.uj_val, cst | Def cs -> - let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in + let cst1 = Reduction.conv env' c (Mod_subst.force_constr cs) in let cst = cb.const_constraints +++ cst1 in c, cst in - let def = Def (Lazyconstr.from_val c') in + let def = Def (Mod_subst.from_val c') in let cb' = { cb with const_body = def; diff --git a/kernel/modops.ml b/kernel/modops.ml index 2942412f0..2bd421bb3 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -345,7 +345,7 @@ let strengthen_const mp_from l cb resolver = let kn = KerName.make2 mp_from l in let con = constant_of_delta_kn resolver kn in { cb with - const_body = Def (Lazyconstr.from_val (mkConst con)); + const_body = Def (Mod_subst.from_val (mkConst con)); const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) } let rec strengthen_mod mp_from mp_to mb = @@ -407,7 +407,7 @@ let inline_delta_resolver env inl mp mbid mtb delta = match constant.const_body with | Undef _ | OpaqueDef _ -> l | Def body -> - let constr = Lazyconstr.force body in + let constr = Mod_subst.force_constr body in add_inline_delta_resolver kn (lev, Some constr) l with Not_found -> error_no_such_label_sub (con_label con) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 7d542c107..99513319b 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1523,7 +1523,7 @@ and compile_named env sigma auxdefs id = let compile_constant env sigma prefix ~interactive con body = match body with | Def t -> - let t = Lazyconstr.force t in + let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in let is_lazy = is_lazy t in let code = if is_lazy then mk_lazy code else code in @@ -1628,7 +1628,7 @@ let rec compile_deps env sigma prefix ~interactive init t = else let comp_stack, (mind_updates, const_updates) = match cb.const_body with | Def t -> - compile_deps env sigma prefix ~interactive init (Lazyconstr.force t) + compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) | _ -> init in let code, name = diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 258f03efd..e6a579c5b 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -639,11 +639,11 @@ and lambda_of_app env sigma f args = begin match cb.const_body with | Def csubst -> if cb.const_inline_code then - lambda_of_app env sigma (Lazyconstr.force csubst) args + lambda_of_app env sigma (Mod_subst.force_constr csubst) args else let prefix = get_const_prefix !global_env kn in let t = - if is_lazy (Lazyconstr.force csubst) then + if is_lazy (Mod_subst.force_constr csubst) then mkLapp Lforce [|Lconst (prefix, kn)|] else Lconst (prefix, kn) in diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml new file mode 100644 index 000000000..50208e28a --- /dev/null +++ b/kernel/opaqueproof.ml @@ -0,0 +1,112 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Term +open Mod_subst + +type work_list = Id.t array Cmap.t * Id.t array Mindmap.t +type cooking_info = { modlist : work_list; abstract : Context.named_context } +type proofterm = (constr * Univ.constraints) 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 + +(* hooks *) +let default_get_opaque dp _ = + Errors.error + ("Cannot access opaque proofs in library " ^ DirPath.to_string dp) +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") + | 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 -> NoIndirect([],cu) + | Some (dp,i) -> Indirect ([],dp,i) + +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") + | 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") + | Direct (d,cu) -> + Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u)) + +let join_opaque = 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 + +let force_proof = 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 + force_constr (List.fold_right subst_substituted l (from_val c)) + +let force_constraints = function + | Direct (_,cu) + | NoIndirect(_,cu) -> snd(Future.force cu) + | Indirect (_,dp,i) -> + match !get_univ dp i with + | None -> Univ.empty_constraint + | 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 + +let get_proof = 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 -> + force_constr (List.fold_right subst_substituted l (from_val c))) diff --git a/kernel/lazyconstr.mli b/kernel/opaqueproof.mli index db4d8fb72..957889aa9 100644 --- a/kernel/lazyconstr.mli +++ b/kernel/opaqueproof.mli @@ -10,52 +10,45 @@ open Names open Term open Mod_subst -type work_list = Id.t array Cmap.t * Id.t array Mindmap.t -type cooking_info = { modlist : work_list; abstract : Context.named_context } - -(** [constr_substituted] are [constr] with possibly pending - substitutions of kernel names. *) - -type constr_substituted +(** This module implements the handling of opaque proof terms. + Opauqe proof terms are special since: + - they can be lazily computed and substituted + - they are stoked in an optionally loaded segment of .vo files + An [opaque] proof terms holds the real data until fully discharged. + In this case it is called [direct]. + When it is [turn_indirect] the data is relocated to an opaque table + and the [opaque] is turned into an index. *) -val from_val : constr -> constr_substituted -val force : constr_substituted -> constr -val subst_constr_subst : - substitution -> constr_substituted -> constr_substituted - -(** Opaque proof terms might be in some external tables. The - [force_opaque] function below allows to access these tables, - this might trigger the read of some extra parts of .vo files *) - -type lazy_constr type proofterm = (constr * Univ.constraints) Future.computation +type opaque -(** From a [constr] to some (immediate) [lazy_constr]. *) -val opaque_from_val : proofterm -> lazy_constr +(** From a [proofterm] to some [opaque]. *) +val create : proofterm -> opaque -(** Turn an immediate [lazy_constr] into an indirect one, thanks - to the indirect opaque creator configured below. *) -val turn_indirect : lazy_constr -> lazy_constr +(** Turn a direct [opaque] into an indirect one, also hashconses constr *) +val turn_indirect : opaque -> opaque -(** From a [lazy_constr] back to a [constr]. This might use the +(** From a [opaque] back to a [constr]. This might use the indirect opaque accessor configured below. *) -val force_opaque : lazy_constr -> constr -val force_opaque_w_constraints : lazy_constr -> constr * Univ.constraints -val get_opaque_future_constraints : - lazy_constr -> Univ.constraints Future.computation option -val get_opaque_futures : - lazy_constr -> - Term.constr Future.computation * Univ.constraints Future.computation +val force_proof : opaque -> constr +val force_constraints : opaque -> Univ.constraints +val get_proof : opaque -> Term.constr Future.computation +val get_constraints : opaque -> Univ.constraints Future.computation option -val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr +val subst_opaque : substitution -> opaque -> opaque +val iter_direct_opaque : (constr -> unit) -> opaque -> opaque -(* val hcons_lazy_constr : lazy_constr -> lazy_constr *) +type work_list = Id.t array Cmap.t * Id.t array Mindmap.t +type cooking_info = { modlist : work_list; abstract : Context.named_context } -(* Used to discharge the proof term. *) -val iter_direct_lazy_constr : (constr -> unit) -> lazy_constr -> lazy_constr -val discharge_direct_lazy_constr : work_list -> Context.named_context -> (constr -> constr) -> lazy_constr -> lazy_constr +(* The type has two caveats: + 1) cook_constr is defined after + 2) we have to store the input in the [opaque] in order to be able to + discharge it when turning a .vi into a .vo *) +val discharge_direct_opaque : + cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque -val join_lazy_constr : lazy_constr -> unit +val join_opaque : opaque -> unit (** When stored indirectly, opaque terms are indexed by their library dirpath and an integer index. The following two functions activate diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a93415f92..241e9d565 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -283,8 +283,8 @@ let safe_push_named (id,_,_ as d) env = let push_named_def (id,de) senv = let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in let c,cst' = match c with - | Def c -> Lazyconstr.force c, Univ.empty_constraint - | OpaqueDef c -> Lazyconstr.force_opaque_w_constraints c + | Def c -> Mod_subst.force_constr c, Univ.empty_constraint + | OpaqueDef o -> Opaqueproof.force_proof o, Opaqueproof.force_constraints o | _ -> assert false in let senv = add_constraints (Now cst') senv in let senv' = add_constraints (Now cst) senv in @@ -321,7 +321,7 @@ let constraints_of_sfb = function match cb.const_body with | (Undef _ | Def _) -> [] | OpaqueDef lc -> - match Lazyconstr.get_opaque_future_constraints lc with + match Opaqueproof.get_constraints lc with | None -> [] | Some fc -> match Future.peek_val fc with @@ -383,7 +383,7 @@ let add_constant dir l decl senv = | 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 (Lazyconstr.turn_indirect lc) } + { cb with const_body = OpaqueDef (Opaqueproof.turn_indirect lc) } | _ -> cb in let senv' = add_field (l,SFBconst cb) (C kn) senv in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 6cedb6ad2..af4468981 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -290,8 +290,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = | Def lc1 -> (* NB: cb1 might have been strengthened and appear as transparent. Anyway [check_conv] will handle that afterwards. *) - let c1 = Lazyconstr.force lc1 in - let c2 = Lazyconstr.force lc2 in + let c1 = Mod_subst.force_constr lc1 in + let c2 = Mod_subst.force_constr lc2 in check_conv NotConvertibleBodyField cst conv env c1 c2)) | IndType ((kn,i),mind1) -> ignore (Errors.error ( diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f059ea1ae..c86c13e04 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -69,12 +69,12 @@ let handle_side_effects env body side_eff = match cb.const_body with | Undef _ -> assert false | Def b -> - let b = Lazyconstr.force b in + let b = Mod_subst.force_constr b in let b_ty = Typeops.type_of_constant_type env cb.const_type in let t = sub c 1 (Vars.lift 1 t) in mkLetIn (cname c, b, b_ty, t) | OpaqueDef b -> - let b = Lazyconstr.force_opaque b in + let b = Opaqueproof.force_proof b in let b_ty = Typeops.type_of_constant_type env cb.const_type in let t = sub c 1 (Vars.lift 1 t) in mkApp (mkLambda (cname c, b_ty, t), [|b|]) in @@ -108,7 +108,7 @@ let infer_declaration env dcl = let _typ, cst = constrain_type env j cst (`SomeWJ (typ,tyj,tycst)) in feedback_completion_typecheck feedback_id; j.uj_val, cst) in - let def = OpaqueDef (Lazyconstr.opaque_from_val proofterm) in + let def = OpaqueDef (Opaqueproof.create proofterm) in let typ = NonPolymorphicType typ in def, typ, tycst, c.const_entry_inline_code, c.const_entry_secctx | DefinitionEntry c -> @@ -120,7 +120,7 @@ let infer_declaration env dcl = let j = hcons_j j in let typ, cst = constrain_type env j cst (map_option_typ typ) in feedback_completion_typecheck feedback_id; - let def = Def (Lazyconstr.from_val j.uj_val) in + let def = Def (Mod_subst.from_val j.uj_val) in def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx let global_vars_set_constant_type env = function @@ -159,9 +159,9 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) = let ids_typ = global_vars_set_constant_type env typ in let ids_def = match def with | Undef _ -> Idset.empty - | Def cs -> global_vars_set env (Lazyconstr.force cs) + | Def cs -> global_vars_set env (Mod_subst.force_constr cs) | OpaqueDef lc -> - let vars = global_vars_set env (Lazyconstr.force_opaque lc) in + let vars = global_vars_set env (Opaqueproof.force_proof lc) in !suggest_proof_using kn env vars ids_typ context_ids; if !Flags.compilation_mode = Flags.BuildVo then record_aux env ids_typ vars; @@ -179,12 +179,12 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) = | Undef _ as x -> x (* nothing to check *) | Def cs as x -> let ids_typ = global_vars_set_constant_type env typ in - let ids_def = global_vars_set env (Lazyconstr.force cs) in + let ids_def = global_vars_set env (Mod_subst.force_constr cs) in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) - OpaqueDef (Lazyconstr.iter_direct_lazy_constr (fun c -> + OpaqueDef (Opaqueproof.iter_direct_opaque (fun c -> let ids_typ = global_vars_set_constant_type env typ in let ids_def = global_vars_set env c in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in diff --git a/library/declare.ml b/library/declare.ml index 477e96bd8..c0c4dd571 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -121,7 +121,7 @@ let open_constant i ((sp,kn), obj) = match (Global.lookup_constant con).const_body with | (Def _ | Undef _) -> () | OpaqueDef lc -> - match Lazyconstr.get_opaque_future_constraints lc with + match Opaqueproof.get_constraints lc with | Some f when Future.is_val f -> Global.add_constraints (Future.force f) | _ -> () @@ -155,7 +155,7 @@ let discharge_constant ((sp, kn), obj) = let hyps = section_segment_of_constant con in let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in let abstract = named_of_variable_context hyps in - let new_decl = GlobalRecipe{ from; info = { Lazyconstr.modlist; abstract }} in + let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) @@ -197,8 +197,8 @@ let declare_sideff se = let id_of c = Names.Label.to_id (Names.Constant.label c) in let pt_opaque_of cb = match cb with - | { const_body = Def sc } -> Lazyconstr.force sc, false - | { const_body = OpaqueDef fc } -> Lazyconstr.force_opaque fc, true + | { const_body = Def sc } -> Mod_subst.force_constr sc, false + | { const_body = OpaqueDef fc } -> Opaqueproof.force_proof fc, true | { const_body = Undef _ } -> anomaly(str"Undefined side effect") in let ty_of cb = diff --git a/library/lib.ml b/library/lib.ml index ee89bb997..331196565 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -385,7 +385,7 @@ type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap let sectab = Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list * - Lazyconstr.work_list * abstr_list) list) + Opaqueproof.work_list * abstr_list) list) ~name:"section-context" let add_section () = diff --git a/library/lib.mli b/library/lib.mli index 787dc969e..8975acd9a 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -187,7 +187,7 @@ val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive (* discharging a constant in one go *) -val full_replacement_context : unit -> Lazyconstr.work_list list +val full_replacement_context : unit -> Opaqueproof.work_list list val full_section_segment_of_constant : Names.constant -> (Context.named_context -> Context.named_context) list diff --git a/library/library.ml b/library/library.ml index c40f9d204..ccf282175 100644 --- a/library/library.ml +++ b/library/library.ml @@ -361,7 +361,7 @@ module OpaqueTables = struct let a_constr = Future.from_val (Term.mkRel 1) let a_univ = Future.from_val Univ.empty_constraint - let a_discharge : Lazyconstr.cooking_info list = [] + 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) @@ -424,17 +424,18 @@ module OpaqueTables = struct end -let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque -let _ = Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ -let _ = Lazyconstr.set_join_indirect_local_opaque OpaqueTables.join_local_opaque -let _ = Lazyconstr.set_join_indirect_local_univ OpaqueTables.join_local_univ +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 (************************************************************************) (* Internalise libraries *) type seg_lib = library_disk type seg_univ = Univ.constraints Future.computation array -type seg_discharge = Lazyconstr.cooking_info list array +type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Term.constr Future.computation array let mk_library md digest = @@ -658,7 +659,7 @@ let start_library f = let id = Id.of_string (Filename.basename f) in check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in - Lazyconstr.set_indirect_creator OpaqueTables.store; + Opaqueproof.set_indirect_creator OpaqueTables.store; Declaremods.start_library ldir; ldir,longf @@ -714,12 +715,12 @@ let save_library_to ?todo dir f = | Some d -> assert(!Flags.compilation_mode = Flags.BuildVi); f ^ "i", (fun x -> Some (d x)), (fun x -> Some x), (fun x -> Some x) in - Lazyconstr.reset_indirect_creator (); + Opaqueproof.reset_indirect_creator (); (* HACK: end_library resets Lib and then joins the safe env. To join the * env one needs to access the futures stored in the tables. Standard * accessors use Lib. Hence *) - Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque_nolib; - Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ_nolib; + Opaqueproof.set_indirect_opaque_accessor OpaqueTables.get_opaque_nolib; + Opaqueproof.set_indirect_univ_accessor OpaqueTables.get_univ_nolib; let cenv, seg, ast = Declaremods.end_library dir in let opaque_table, univ_table, disch_table, f2t_map = OpaqueTables.dump () in diff --git a/library/library.mli b/library/library.mli index ec39059e9..69fd5e940 100644 --- a/library/library.mli +++ b/library/library.mli @@ -33,7 +33,7 @@ val require_library_from_file : (** Segments of a library *) type seg_lib type seg_univ = Univ.constraints Future.computation array -type seg_discharge = Lazyconstr.cooking_info list array +type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Term.constr Future.computation array (** Open a module (or a library); if the boolean is true then it's also diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 5f17e0997..791294902 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -137,7 +137,7 @@ let check_arity env cb = let check_fix env cb i = match cb.const_body with | Def lbody -> - (match kind_of_term (Lazyconstr.force lbody) with + (match kind_of_term (Mod_subst.force_constr lbody) with | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd) | _ -> raise Impossible) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6fc1973d0..134e01ee1 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -285,7 +285,7 @@ let rec extract_type env db j c args = | Undef _ | OpaqueDef _ -> mlt | Def _ when is_custom r -> mlt | Def lbody -> - let newc = applist (Lazyconstr.force lbody, args) in + let newc = applist (Mod_subst.force_constr lbody, args) in let mlt' = extract_type env db j newc [] in (* ML type abbreviations interact badly with Coq *) (* reduction, so [mlt] and [mlt'] might be different: *) @@ -299,7 +299,7 @@ let rec extract_type env db j c args = | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *) | Def lbody -> (* We try to reduce. *) - let newc = applist (Lazyconstr.force lbody, args) in + let newc = applist (Mod_subst.force_constr lbody, args) in extract_type env db j newc [])) | Ind (kn,i) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in @@ -523,7 +523,7 @@ and mlt_env env r = match r with | Def l_body -> (match flag_of_type env typ with | Info,TypeScheme -> - let body = Lazyconstr.force l_body in + let body = Mod_subst.force_constr l_body in let s,vl = type_sign_vl env typ in let db = db_from_sign s in let t = extract_type_scheme env db body (List.length s) @@ -995,20 +995,20 @@ let extract_constant env kn cb = | (Info,TypeScheme) -> (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () - | Def c -> mk_typ (Lazyconstr.force c) + | Def c -> mk_typ (Mod_subst.force_constr c) | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_typ (Lazyconstr.force_opaque c) + mk_typ (Opaqueproof.force_proof c) else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () - | Def c -> mk_def (Lazyconstr.force c) + | Def c -> mk_def (Mod_subst.force_constr c) | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_def (Lazyconstr.force_opaque c) + mk_def (Opaqueproof.force_proof c) else mk_ax ()) let extract_constant_spec env kn cb = @@ -1023,7 +1023,7 @@ let extract_constant_spec env kn cb = | Undef _ | OpaqueDef _ -> Stype (r, vl, None) | Def body -> let db = db_from_sign s in - let body = Lazyconstr.force body in + let body = Mod_subst.force_constr body in let t = extract_type_scheme env db body (List.length s) in Stype (r, vl, Some t)) | (Info, Default) -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index da230ee0d..031db5b0c 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -531,11 +531,11 @@ let print_full_pure_context () = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr (Lazyconstr.force_opaque lc) + str "Proof " ++ pr_lconstr (Opaqueproof.force_proof lc) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ - pr_lconstr (Lazyconstr.force c)) + pr_lconstr (Mod_subst.force_constr c)) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in diff --git a/printing/printmod.ml b/printing/printmod.ml index b5f84c79e..34224d7b5 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -153,7 +153,7 @@ let print_body is_impl env mp (l,body) = | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env (Lazyconstr.force l)) + Printer.pr_lconstr_env env (Mod_subst.force_constr l)) | _ -> mt ()) ++ str ".") | SFBmind mib -> diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 07c91c8d5..f0ea69533 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -135,8 +135,8 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac let constr_of_def = function | Declarations.Undef _ -> assert false - | Declarations.Def cs -> Lazyconstr.force cs - | Declarations.OpaqueDef lc -> Lazyconstr.force_opaque lc + | Declarations.Def cs -> Mod_subst.force_constr cs + | Declarations.OpaqueDef lc -> Opaqueproof.force_proof lc let build_by_tactic env typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index aa64e3f22..6f696f27a 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -10,7 +10,7 @@ open Context open Cooking open Declarations open Entries -open Lazyconstr +open Opaqueproof val process_inductive : named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 9b07b4fcd..9a86d7ea0 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -830,7 +830,7 @@ end = struct (* {{{ *) List.iter (fun (_,se) -> Declareops.iter_side_effects (function | Declarations.SEsubproof(_, { Declarations.const_body = Declarations.OpaqueDef f } ) -> - Lazyconstr.join_lazy_constr f + Opaqueproof.join_opaque f | _ -> ()) se) l; l) in @@ -888,7 +888,8 @@ end = struct (* {{{ *) let c = Global.lookup_constant con in match c.Declarations.const_body with | Declarations.OpaqueDef lc -> - let pr, uc = Lazyconstr.get_opaque_futures lc in + let uc = Option.get (Opaqueproof.get_constraints lc) 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 ignore(Future.join pr); |