From 398fe8ee23759a1c28d91204aa013beae1dc602b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 12 Oct 2018 18:25:18 +0200 Subject: Cleaning the status of Local Definition and similar. Formerly, knowing if a declaration was to be discharged, to be global but invisible at import, or to be global but visible at import was obtained by combining the parser-level information (i.e. use of Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use of Local vs Global) with the result of testing whether there were open sections. We change the meaning of the Discharge flag: it does not tell anymore that it was syntactically a Variable/Hypothesis/Let, but tells the expected semantics of the declaration (issuing a warning in the parser-to-interpreter step if the semantics is not the one suggested by the syntax). In particular, the interpretation/command engine becomes independent of the parser. The new "semantic" type is: type import_status = ImportDefaultBehavior | ImportNeedQualified type locality = Discharge | Global of import_status In the process, we found a couple of inconsistencies in the treatment of the locality status. See bug #8722 and test file LocalDefinition.v. --- plugins/derive/derive.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/indfun.ml | 4 ++-- plugins/funind/indfun_common.ml | 18 ++++++------------ plugins/funind/invfun.ml | 4 ++-- plugins/funind/recdef.ml | 6 +++--- plugins/ltac/rewrite.ml | 2 +- 8 files changed, 17 insertions(+), 23 deletions(-) (limited to 'plugins') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 9c1882dc9a..7c0f269481 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -26,7 +26,7 @@ let start_deriving f suchthat lemma = let env = Global.env () in let sigma = Evd.from_env env in - let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in + let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index e38ea992ab..b3a799fb6a 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -995,7 +995,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num Ensures by: obvious i*) (mk_equation_id f_id) - (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) + Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem) evd lemma_type in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 7b26cb0c74..965ce68811 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -311,7 +311,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let pstate = Lemmas.start_proof new_princ_name - (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) + Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) !evd (EConstr.of_constr new_principle_type) in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 241da053b7..7070f01c6f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -417,7 +417,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComDefinition.do_definition ~program_mode:false fname - (Decl_kinds.Global,false,Decl_kinds.Definition) pl + Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left @@ -434,7 +434,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in None, evd,List.rev rev_pconstants | _ -> - ComFixpoint.do_fixpoint Global false fixpoint_exprl; + ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 48cf040919..6d9690096f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -124,26 +124,20 @@ open Declare let definition_message = Declare.definition_message -let get_locality = function -| Discharge -> true -| Local -> true -| Global -> false - let save id const ?hook uctx (locality,_,kind) = 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 r = match locality with + | Discharge -> let k = Kindops.logical_kind_of_goal_kind kind in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Discharge | Local | Global -> - let local = get_locality locality in + VarRef id + | Global local -> let k = Kindops.logical_kind_of_goal_kind kind in let kn = declare_constant id ~local (DefinitionEntry const, k) in - (locality, ConstRef kn) + ConstRef kn in - Lemmas.call_hook ?hook ~fix_exn uctx [] l r; + Lemmas.call_hook ?hook ~fix_exn uctx [] locality r; definition_message id let with_full_print f a = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 03568fc6c7..8a16326ba3 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -805,7 +805,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let (typ,_) = lemmas_types_infos.(i) in let pstate = Lemmas.start_proof lem_id - (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) + Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) !evd typ in let pstate = fst @@ Pfedit.by @@ -866,7 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_complete_id f_id in let pstate = Lemmas.start_proof lem_id - (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma + Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma (fst lemmas_types_infos.(i)) in let pstate = fst (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e2321d233c..5bedb360d1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1371,7 +1371,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type in let pstate = Lemmas.start_proof na - (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) + Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) sigma gls_type ~hook:(Lemmas.mk_hook hook) in let pstate = if Indfun_common.is_strict_tcc () then @@ -1411,7 +1411,7 @@ let com_terminate hook = let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = let pstate = Lemmas.start_proof thm_name - (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) + (Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref @@ -1457,7 +1457,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let pstate = Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign evd + let pstate = Lemmas.start_proof eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd (EConstr.of_constr equation_lemma_type) in let pstate = fst @@ by (Proofview.V82.tactic (start_equation f_ref terminate_ref diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e0a31e7dba..b99e77ab2b 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1995,7 +1995,7 @@ let add_morphism_interactive atts m n : Proof_global.t = let env = Global.env () in let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in - let kind = Decl_kinds.Global, atts.polymorphic, + let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic, Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in -- cgit v1.2.3