From bbf2ded61869b8aa48e34424c15e795961820721 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 10 Jul 2019 16:07:09 +0200 Subject: [lemmas] Refactor code a bit, saving functions now to in the saving part. We localize functions for constant saving that were used before in the start hooks, but now they are called in the saving path in direct style. No functional change. --- vernac/lemmas.ml | 172 +++++++++++++++++++++++++++---------------------------- 1 file changed, 85 insertions(+), 87 deletions(-) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ecea9ae4c9..a8c95cad02 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -113,46 +113,6 @@ let by tac pf = (* Creating a lemma-like constant *) (************************************************************************) -(* Support for mutually proved theorems *) - -let retrieve_first_recthm uctx = function - | GlobRef.VarRef id -> - NamedDecl.get_value (Global.lookup_named id), - Decls.variable_opacity id - | GlobRef.ConstRef cst -> - let cb = Global.lookup_constant cst in - (* we get the right order somehow but surely it could be enforced in a better way *) - let uctx = UState.context uctx in - let inst = Univ.UContext.instance uctx in - let map (c, _, _) = Vars.subst_instance_constr inst c in - (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) - | _ -> assert false - -let adjust_guardness_conditions const = function - | [] -> const (* Not a recursive statement *) - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - let open Proof_global in - { const with proof_entry_body = - Future.chain const.proof_entry_body - (fun ((body, ctx), eff) -> - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> -(* let possible_indexes = - List.map2 (fun i c -> match i with Some i -> i | None -> - List.interval 0 (List.length ((lam_assum c)))) - lemma_guard (Array.to_list fixdefs) in -*) - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = - search_guard env - possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) } - -let default_thm_id = Id.of_string "Unnamed_thm" - let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || @@ -160,52 +120,6 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = then user_err ?loc (Id.print id ++ str " already exists.") -let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recthm.name; typ; impargs } = - let t_i = norm typ in - let kind = Decls.(IsAssumption Conjectural) in - match body with - | None -> - let open DeclareDef in - (match scope with - | Discharge -> - let impl = false in (* copy values from Vernacentries *) - let univs = match univs with - | Polymorphic_entry (_, univs) -> - (* What is going on here? *) - Univ.ContextSet.of_context univs - | Monomorphic_entry univs -> univs - in - let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in - let () = Declare.declare_variable ~name ~kind c in - (GlobRef.VarRef name,impargs) - | Global local -> - let kind = Decls.(IsAssumption Conjectural) in - let decl = Declare.ParameterEntry (None,(t_i,univs),None) in - let kn = Declare.declare_constant ~name ~local ~kind decl in - (GlobRef.ConstRef kn,impargs)) - | Some body -> - let body = norm body in - let rec body_i t = match Constr.kind t with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) - | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) - | App (t, args) -> mkApp (body_i t, args) - | _ -> - anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in - let body_i = body_i body in - let open DeclareDef in - match scope with - | Discharge -> - let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in - let c = Declare.SectionLocalDef const in - let () = Declare.declare_variable ~name ~kind c in - (GlobRef.VarRef name,impargs) - | Global local -> - let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in - let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in - (GlobRef.ConstRef kn,impargs) - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right @@ -315,9 +229,70 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?inference_hook ?hook thms start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl (************************************************************************) -(* Commom constant saving path *) +(* Commom constant saving path, for both Qed and Admitted *) (************************************************************************) +(* Helper for process_recthms *) +let retrieve_first_recthm uctx = function + | GlobRef.VarRef id -> + NamedDecl.get_value (Global.lookup_named id), + Decls.variable_opacity id + | GlobRef.ConstRef cst -> + let cb = Global.lookup_constant cst in + (* we get the right order somehow but surely it could be enforced in a better way *) + let uctx = UState.context uctx in + let inst = Univ.UContext.instance uctx in + let map (c, _, _) = Vars.subst_instance_constr inst c in + (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) + | _ -> assert false + +(* Helper for process_recthms *) +let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recthm.name; typ; impargs } = + let t_i = norm typ in + let kind = Decls.(IsAssumption Conjectural) in + match body with + | None -> + let open DeclareDef in + (match scope with + | Discharge -> + let impl = false in (* copy values from Vernacentries *) + let univs = match univs with + | Polymorphic_entry (_, univs) -> + (* What is going on here? *) + Univ.ContextSet.of_context univs + | Monomorphic_entry univs -> univs + in + let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in + let () = Declare.declare_variable ~name ~kind c in + GlobRef.VarRef name, impargs + | Global local -> + let kind = Decls.(IsAssumption Conjectural) in + let decl = Declare.ParameterEntry (None,(t_i,univs),None) in + let kn = Declare.declare_constant ~name ~local ~kind decl in + GlobRef.ConstRef kn, impargs) + | Some body -> + let body = norm body in + let rec body_i t = match Constr.kind t with + | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) + | CoFix (0,decls) -> mkCoFix (i,decls) + | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) + | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) + | App (t, args) -> mkApp (body_i t, args) + | _ -> + anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in + let body_i = body_i body in + let open DeclareDef in + match scope with + | Discharge -> + let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in + let c = Declare.SectionLocalDef const in + let () = Declare.declare_variable ~name ~kind c in + GlobRef.VarRef name, impargs + | Global local -> + let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in + let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in + GlobRef.ConstRef kn, impargs + (* This declares implicits and calls the hooks for all the theorems, including the main one *) let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps other_thms = @@ -395,10 +370,33 @@ let save_lemma_admitted ~(lemma : t) : unit = (* Saving a lemma-like constant *) (************************************************************************) +let default_thm_id = Id.of_string "Unnamed_thm" + let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then user_err Pp.(str "This command can only be used for unnamed theorem.") +(* Support for mutually proved theorems *) + +(* Helper for finish_proved *) +let adjust_guardness_conditions const = function + | [] -> const (* Not a recursive statement *) + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + let open Proof_global in + { const with + proof_entry_body = + Future.chain const.proof_entry_body + (fun ((body, ctx), eff) -> + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff) + } + let finish_proved env sigma idopt po info = let open Proof_global in let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in -- cgit v1.2.3 From b6000bd57f9dd20858678caee7e3962081243694 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 10 Jul 2019 16:13:22 +0200 Subject: [lemmas] save_remaining_recthms doesn't need a norm parameter. We make the interface to this function simpler, as a step towards trying to remove the duplication of this function with the code in `DeclareDef`. --- vernac/lemmas.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index a8c95cad02..6a754a0cde 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -247,7 +247,10 @@ let retrieve_first_recthm uctx = function | _ -> assert false (* Helper for process_recthms *) -let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recthm.name; typ; impargs } = +let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Recthm.name; typ; impargs } = + let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in + let body = Option.map EConstr.of_constr body in + let univs = UState.check_univ_decl ~poly uctx udecl in let t_i = norm typ in let kind = Decls.(IsAssumption Conjectural) in match body with @@ -300,10 +303,7 @@ let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) let body,opaq = retrieve_first_recthm uctx dref in - let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in - let body = Option.map EConstr.of_constr body in - let uctx = UState.check_univ_decl ~poly uctx udecl in - List.map_i (save_remaining_recthms env sigma ~poly ~scope norm uctx body opaq) 1 other_thms in + List.map_i (save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq) 1 other_thms in let thms_data = (dref,imps)::other_thms_data in List.iter (fun (dref,imps) -> maybe_declare_manual_implicits false dref imps; -- cgit v1.2.3 From ae5b8208ae77d36ead42b41b0a62bc19964bb90f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 23 Jul 2019 15:16:51 +0200 Subject: [obligations] Use already existing type alias. Simple cleanup: we make use of the `obligation_info` type alias in the function generating it. --- vernac/obligations.mli | 44 +++++++++++++++++++++++++------------------- 1 file changed, 25 insertions(+), 19 deletions(-) diff --git a/vernac/obligations.mli b/vernac/obligations.mli index f97bc784c3..3bffdb5f52 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -18,27 +18,33 @@ val check_evars : env -> evar_map -> unit val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list -(* env, id, evars, number of function prototypes to try to clear from - evars contexts, object and type *) -val eterm_obligations : env -> Id.t -> evar_map -> int -> - ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types -> - (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * - unit Proofview.tactic option) array - (* Existential key, obl. name, type as product, - location of the original evar, associated tactic, - status and dependencies as indexes into the array *) - * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * - constr * types - (* Translations from existential identifiers to obligation identifiers - and for terms with existentials to closed terms, given a - translation from obligation identifiers to constrs, new term, new type *) - +(* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) type obligation_info = (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array - (* ident, type, location, (opaque or transparent, expand or define), - dependencies, tactic to solve it *) + (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array + +(* env, id, evars, number of function prototypes to try to clear from + evars contexts, object and type *) +val eterm_obligations + : env + -> Id.t + -> evar_map + -> int + -> ?status:Evar_kinds.obligation_definition_status + -> EConstr.constr + -> EConstr.types + -> obligation_info * + + (* Existential key, obl. name, type as product, location of the + original evar, associated tactic, status and dependencies as + indexes into the array *) + ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * + + (* Translations from existential identifiers to obligation + identifiers and for terms with existentials to closed terms, + given a translation from obligation identifiers to constrs, + new term, new type *) + constr * types val default_tactic : unit Proofview.tactic ref -- cgit v1.2.3