From 1235c6c3cfc6770920f46de30b1c4b0f5cb44b19 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 28 Oct 2015 12:49:03 +0100 Subject: Do not pause globing in funind. (Fix bug #4382) Since the functions of this plugin exit by raising exceptions, globing was never restarted. This prevented coqdoc from generating a proper output whenever some feature of this plugin was used. There does not seem to be any parsing of dynamic expressions, so pausing globing does not make much sense in the first place. --- plugins/funind/functional_principles_types.ml | 7 +------ plugins/funind/indfun.ml | 9 ++------- 2 files changed, 3 insertions(+), 13 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 64284c6fe7..9e27ddf2e9 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -594,9 +594,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr in const::other_result - let build_scheme fas = - Dumpglob.pause (); let evd = (ref (Evd.from_env (Global.env ()))) in let pconstants = (List.map (fun (_,f,sort) -> @@ -626,10 +624,7 @@ let build_scheme fas = Declare.definition_message princ_id ) fas - bodies_types; - Dumpglob.continue () - - + bodies_types let build_case_scheme fa = let env = Global.env () diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index eadeebd38e..47c67ed2aa 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -27,7 +27,6 @@ let choose_dest_or_ind scheme_info = Tactics.induction_destruct (is_rec_info scheme_info) false let functional_induction with_clean c princl pat = - Dumpglob.pause (); let res = let f,args = decompose_app c in fun g -> @@ -123,9 +122,7 @@ let functional_induction with_clean c princl pat = (args_as_induction_constr,princ'))) subst_and_reduce g' - in - Dumpglob.continue (); - res + in res let rec abstract_glob_constr c = function | [] -> c @@ -831,7 +828,6 @@ let make_graph (f_ref:global_reference) = end | _ -> raise (UserError ("", str "Not a function reference") ) in - Dumpglob.pause (); (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom !" | Some body -> @@ -883,8 +879,7 @@ let make_graph (f_ref:global_reference) = (* We register the infos *) List.iter (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id))) - expr_list); - Dumpglob.continue () + expr_list) let do_generate_principle = do_generate_principle [] warning_error true -- cgit v1.2.3 From b5a0e384b405f64fd0854d5e88b55e8c2a159c02 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 11:02:09 -0400 Subject: Univs: fix bug #4375, accept universe binders on (co)-fixpoints --- plugins/funind/indfun.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 47c67ed2aa..3dbd438061 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -592,7 +592,7 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in + let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in let fixpoint_exprl_with_new_bl = -- cgit v1.2.3 From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- plugins/derive/derive.ml | 4 ++-- plugins/funind/functional_principles_types.ml | 14 +++++++------- plugins/funind/functional_principles_types.mli | 10 +++++++++- plugins/funind/indfun_common.ml | 2 +- plugins/funind/indfun_common.mli | 4 ++-- 5 files changed, 21 insertions(+), 13 deletions(-) (limited to 'plugins') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index c232ae31ad..d6c29283f1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let map_const_entry_body (f:Term.constr->Term.constr) (x:Entries.const_entry_body) - : Entries.const_entry_body = +let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) + : Safe_typing.private_constants Entries.const_entry_body = Future.chain ~pure:true x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9e27ddf2e9..c439323243 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -334,7 +334,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) ignore( Declare.declare_constant name - (Entries.DefinitionEntry ce, + (DefinitionEntry ce, Decl_kinds.IsDefinition (Decl_kinds.Scheme)) ); Declare.definition_message name; @@ -447,7 +447,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list = +let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr let sorts = Array.of_list sorts in List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in - let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in + let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = @@ -585,9 +585,9 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with - Entries.const_entry_body = - (Future.from_val (Term_typing.mk_pure_proof princ_body)); - Entries.const_entry_type = Some scheme_type + const_entry_body = + (Future.from_val (Safe_typing.mk_pure_proof princ_body)); + const_entry_type = Some scheme_type } ) other_fun_princ_types @@ -620,7 +620,7 @@ let build_scheme fas = ignore (Declare.declare_constant princ_id - (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); Declare.definition_message princ_id ) fas diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index f6e5578d2e..bc082f0730 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* sorts array -> exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*glob_sort) list -> Entries.definition_entry list + (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list val build_scheme : (Id.t*Libnames.reference*glob_sort) list -> unit val build_case_scheme : (Id.t*Libnames.reference*glob_sort) -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 35bd1c36da..aa47e26192 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -149,7 +149,7 @@ let get_locality = function | Global -> false let save with_clean id const (locality,_,kind) hook = - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in + let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 10daf6e848..23f1da1ba7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -46,7 +46,7 @@ val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr -val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> +val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> unit Lemmas.declaration_hook Ephemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and @@ -54,7 +54,7 @@ val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> *) val get_proof_clean : bool -> Names.Id.t * - (Entries.definition_entry * Decl_kinds.goal_kind) + (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind) -- cgit v1.2.3 From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 12:36:20 -0400 Subject: Univs: local names handling. Keep user-side information on the names used in instances of universe polymorphic references and use them for printing. --- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/merge.ml | 4 ++-- plugins/funind/recdef.ml | 2 +- plugins/setoid_ring/newring.ml4 | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c439323243..c47602bda0 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -330,7 +330,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in + let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in ignore( Declare.declare_constant name diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 60c58730a3..e3455e7702 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -884,10 +884,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,impls = Command.interp_mutual_inductive indl [] + let mie,pl,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie impls) + ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ca0b9c5feb..5d41ec7237 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1509,7 +1509,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(Evd.universe_context evm) res in + let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = fst (*FIXME*)(interp_constr diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 1c4ba88237..c7185ff25e 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd + Array.map (fun x -> nf (constr_of x)) !res, snd (Evd.universe_context evd) let stdlib_modules = [["Coq";"Setoids";"Setoid"]; -- cgit v1.2.3