From d050094c578bdf5fc0611b808949fee28ae2a641 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 26 Oct 2019 01:13:24 +0200 Subject: [proof] Remove duplication in the proof save path. We move towards more unification in the proof save path of interactive and non-interactive proofs. --- vernac/declareDef.ml | 46 +++++++++++++++++++++++++++++++++------------- 1 file changed, 33 insertions(+), 13 deletions(-) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 2b6f987fa6..ba4b42c4e0 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -43,35 +43,55 @@ module Hook = struct end (* Locality stuff *) -let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = +let declare_definition ~name ~scope ~kind ?hook_data ?(should_suggest=false) udecl ce imps = let fix_exn = Declare.Internal.get_fix_exn ce in - let gr = match scope with + let dref = match scope with | Discharge -> - let () = - declare_variable ~name ~kind (SectionLocalDef ce) - in - Names.GlobRef.VarRef name + let () = declare_variable ~name ~kind (SectionLocalDef ce) in + if should_suggest then Proof_using.suggest_variable (Global.env ()) name; + Names.GlobRef.VarRef name | Global local -> - let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in - let gr = Names.GlobRef.ConstRef kn in - let () = DeclareUniv.declare_univ_binders gr udecl in - gr + let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in + let gr = Names.GlobRef.ConstRef kn in + if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; + let () = DeclareUniv.declare_univ_binders gr udecl in + gr in - let () = maybe_declare_manual_implicits false gr imps in + let () = maybe_declare_manual_implicits false dref imps in let () = definition_message name in begin match hook_data with | None -> () | Some (hook, uctx, obls) -> - Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref = gr } + Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref } end; - gr + dref let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in let kind = Decls.IsDefinition kind in declare_definition ~name ~scope ~kind ?hook_data udecl ce imps +let warn_let_as_axiom = + CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" + Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ + spc () ++ strbrk "declared as an axiom.") + +let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = + let local = match scope with + | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified + | Global local -> local + in + let kind = Decls.(IsAssumption Conjectural) in + let decl = Declare.ParameterEntry pe in + let kn = Declare.declare_constant ~name ~local ~kind decl in + let dref = Names.GlobRef.ConstRef kn in + let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in + dref + +(* Preparing proof entries *) + let check_definition_evars ~allow_evars sigma = let env = Global.env () in if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma -- cgit v1.2.3 From c9f7a31ef67ce638ec591f9e5760941706bc12bc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 21 Feb 2020 19:08:22 -0500 Subject: [save proof] Declare universe_binders unconditionally for mutual assumptions. As suggested by Gaëtan in review, we move declaration of universe binders to the common code in `DeclareDef`; this changes the semantics for the assumption case when Recthms is not empty. --- vernac/declareDef.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index ba4b42c4e0..bd857a6e38 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -87,6 +87,8 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = let kn = Declare.declare_constant ~name ~local ~kind decl in let dref = Names.GlobRef.ConstRef kn in let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = Declare.assumption_message name in + let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in dref -- cgit v1.2.3 From 79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 29 Feb 2020 15:25:42 -0500 Subject: [lemmas] Handle mutual lemmas more uniformly. We split the paths for mutual / non-mutual constants, and we enforce some further invariants, in particular we avoid messing around with the body of saved constants, and using the indirect accessor. This should be almost semantically equivalent to the previous code, including some questionable choices present there. In further cleanups we will move this code to Declare, which should hopefully help clarify some of the semantics. --- vernac/declareDef.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index bd857a6e38..dea2ccb9af 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -43,8 +43,10 @@ module Hook = struct end (* Locality stuff *) -let declare_definition ~name ~scope ~kind ?hook_data ?(should_suggest=false) udecl ce imps = +let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let fix_exn = Declare.Internal.get_fix_exn ce in + let should_suggest = ce.Declare.proof_entry_opaque && + Option.is_empty ce.Declare.proof_entry_secctx in let dref = match scope with | Discharge -> let () = declare_variable ~name ~kind (SectionLocalDef ce) in -- cgit v1.2.3 From b35dae7a6a9cc08c4bcdce7409e0ef45382b7ee1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Mar 2020 00:46:23 -0500 Subject: [declare] Remove trivial wrapper In preparation for the introduction of an opaque mutual definition type at the `Declare` level we remove the not very useful wrapper `declare_fix`. Now we should be ready to profit from `DeclareDef` and its handling of common stuff such as `restrict_universe_context` and `check_univ_decl` etc... --- vernac/declareDef.ml | 5 ----- 1 file changed, 5 deletions(-) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index dea2ccb9af..39fd332184 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,11 +69,6 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = end; dref -let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - let kind = Decls.IsDefinition kind in - declare_definition ~name ~scope ~kind ?hook_data udecl ce imps - let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ -- cgit v1.2.3