diff options
| -rw-r--r-- | plugins/derive/derive.ml | 78 | ||||
| -rw-r--r-- | vernac/declareObl.ml | 37 | ||||
| -rw-r--r-- | vernac/declareObl.mli | 21 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 165 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 42 | ||||
| -rw-r--r-- | vernac/obligations.ml | 9 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 2 |
7 files changed, 165 insertions, 189 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 0f0bec0129..0447b79dcd 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -8,16 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Constr open Context open Context.Named.Declaration -let map_const_entry_body (f:constr->constr) (x: Evd.side_effects Entries.const_entry_body) - : Evd.side_effects Entries.const_entry_body = - Future.chain x begin fun ((b,ctx),fx) -> - (f b , ctx) , fx - end - (** [start_deriving f suchthat lemma] starts a proof of [suchthat] (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] @@ -36,71 +29,18 @@ let start_deriving f suchthat name : Lemmas.t = (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) let goals = let open Proofview in - TCons ( env , sigma , f_type_type , (fun sigma f_type -> + TCons ( env , sigma , f_type_type , (fun sigma f_type -> TCons ( env , sigma , f_type , (fun sigma ef -> - let f_type = EConstr.Unsafe.to_constr f_type in - let ef = EConstr.Unsafe.to_constr ef in - let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in - let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in - TCons ( env' , sigma , suchthat , (fun sigma _ -> - TNil sigma)))))) - in - - (* The terminator handles the registering of constants when the proof is closed. *) - let terminator com = - (* Extracts the relevant information from the proof. [Admitted] - and [Save] result in user errors. [opaque] is [true] if the - proof was concluded by [Qed], and [false] if [Defined]. [f_def] - and [lemma_def] correspond to the proof of [f] and of - [suchthat], respectively. *) - let (opaque,f_def,lemma_def) = - match com with - | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Lemmas.Proved (_,Some _,_,_,_) -> - CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Lemmas.Proved (opaque, None, obj,_,_) -> - match Proof_global.(obj.entries) with - | [_;f_def;lemma_def] -> - opaque <> Proof_global.Transparent , f_def , lemma_def - | _ -> assert false - in - (* The opacity of [f_def] is adjusted to be [false], as it - must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Entries.const_entry_opaque = false } in - let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in - let f_kn = Declare.declare_constant f f_def in - let f_kn_term = mkConst f_kn in - (* In the type and body of the proof of [suchthat] there can be - references to the variable [f]. It needs to be replaced by - references to the constant [f] declared above. This substitution - performs this precise action. *) - let substf c = Vars.replace_vars [f,f_kn_term] c in - (* Extracts the type of the proof of [suchthat]. *) - let lemma_pretype = - match Entries.(lemma_def.const_entry_type) with - | Some t -> t - | None -> assert false (* Proof_global always sets type here. *) - in - (* The references of [f] are subsituted appropriately. *) - let lemma_type = substf lemma_pretype in - (* The same is done in the body of the proof. *) - let lemma_body = - map_const_entry_body substf Entries.(lemma_def.const_entry_body) - in - let lemma_def = let open Entries in { lemma_def with - const_entry_body = lemma_body ; - const_entry_type = Some lemma_type ; - const_entry_opaque = opaque ; } - in - let lemma_def = - Entries.DefinitionEntry lemma_def , - Decl_kinds.(IsProof Proposition) - in - ignore (Declare.declare_constant name lemma_def) + let f_type = EConstr.Unsafe.to_constr f_type in + let ef = EConstr.Unsafe.to_constr ef in + let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in + let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in + TCons ( env' , sigma , suchthat , (fun sigma _ -> + TNil sigma)))))) in - let terminator = Lemmas.Internal.make_terminator terminator in - let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in + let proof_ending = Lemmas.Proof_ending.(End_derive {f; name}) in + let lemma = Lemmas.start_dependent_lemma name kind goals ~proof_ending in Lemmas.pf_map (Proof_global.map_proof begin fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p end) lemma diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index b269f69ece..71215d2a3e 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -486,13 +486,16 @@ let dependencies obls n = obls; !res -let obligation_terminator name num auto pf = +type obligation_qed_info = + { name : Id.t + ; num : int + ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress + } + +let obligation_terminator opq entries uctx { name; num; auto } = let open Proof_global in - let open Lemmas in - let term = Lemmas.standard_proof_terminator in - match pf with - | Admitted _ -> Internal.apply_terminator term pf - | Proved (opq, id, { entries=[entry]; universes=uctx }, hook, compute_guard ) -> begin + match entries with + | [entry] -> let env = Global.env () in let ty = entry.Entries.const_entry_type in let body, eff = Future.force entry.const_entry_body in @@ -539,18 +542,20 @@ let obligation_terminator name num auto pf = if defined then UState.make (Global.universes ()) else ctx in - let prg = { prg with prg_ctx } in - try + let prg = {prg with prg_ctx} in + begin try ignore (update_obls prg obls (pred rem)); if pred rem > 0 then - begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some name) None deps) - end + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + ignore (auto (Some name) deps None) with e when CErrors.noncritical e -> let e = CErrors.push e in pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) - end - | Proved (_, _, _,_,_) -> - CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") + end + | _ -> + CErrors.anomaly + Pp.( + str + "[obligation_terminator] close_proof returned more than one proof \ + term") diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 5d02639245..70a4601ac6 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -61,14 +61,6 @@ module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set val declare_definition : program_info -> Names.GlobRef.t -val obligation_terminator : - Id.t - -> int - -> (ProgMap.key option -> 'a option -> Int.Set.t -> 'b) - -> Lemmas.proof_ending - -> unit -(** [obligation_terminator] part 2 of saving an obligation *) - type progress = (* Resolution status of a program *) | Remain of int @@ -78,6 +70,19 @@ type progress = | Defined of GlobRef.t (* Defined as id *) +type obligation_qed_info = + { name : Id.t + ; num : int + ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress + } + +val obligation_terminator + : Proof_global.opacity_flag + -> Evd.side_effects Entries.definition_entry list + -> UState.t + -> obligation_qed_info -> unit +(** [obligation_terminator] part 2 of saving an obligation *) + val update_obls : program_info -> obligation array diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 98c7c0d077..686f52565c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -38,29 +38,22 @@ module NamedDecl = Context.Named.Declaration type lemma_possible_guards = int list list -type proof_ending = - | Admitted of - Names.Id.t * - Decl_kinds.goal_kind * - Entries.parameter_entry * - UState.t * - DeclareDef.Hook.t option - - | Proved of - Proof_global.opacity_flag * - lident option * - Proof_global.proof_object * - DeclareDef.Hook.t option * - lemma_possible_guards - -type proof_terminator = (proof_ending -> unit) CEphemeron.key +module Proof_ending = struct + + type t = + | Regular + | End_obligation of DeclareObl.obligation_qed_info + | End_derive of { f : Id.t; name : Id.t } + +end (* Proofs with a save constant function *) type t = { proof : Proof_global.t - ; terminator : proof_terminator ; hook : DeclareDef.Hook.t option ; compute_guard : lemma_possible_guards + ; proof_ending : Proof_ending.t CEphemeron.key + (* This could be improved and the CEphemeron removed *) } let pf_map f pf = { pf with proof = f pf.proof } @@ -71,12 +64,9 @@ let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t) (* To be removed *) module Internal = struct -let make_terminator f = CEphemeron.create f -let apply_terminator f = CEphemeron.get f - (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) -let get_info ps = ps.terminator, ps.hook, ps.compute_guard +let get_info ps = ps.hook, ps.compute_guard, ps.proof_ending end (* Internal *) @@ -209,7 +199,6 @@ let look_for_possibly_mutual_statements sigma = function | [] -> anomaly (Pp.str "Empty list of theorems.") (* Saving a goal *) - let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes = let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in try @@ -316,15 +305,14 @@ let admit ?hook ctx (id,k,e) pl () = Declare.declare_univ_binders (ConstRef kn) pl; DeclareDef.Hook.call ?hook ctx [] (Global local) (ConstRef kn) -(* Starting a goal *) +let finish_admitted id k pe ctx hook = + let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in + Feedback.feedback Feedback.AddedAxiom -let standard_proof_terminator = +let finish_proved opaque idopt po hook compute_guard = let open Proof_global in - Internal.make_terminator begin function - | Admitted (id,k,pe,ctx,hook) -> - let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in - Feedback.feedback Feedback.AddedAxiom - | Proved (opaque,idopt, { id; entries=[const]; persistence; universes }, hook, compute_guard ) -> + match po with + | { id; entries=[const]; persistence; universes } -> let is_opaque, export_seff = match opaque with | Transparent -> false, true | Opaque -> true, false @@ -335,9 +323,8 @@ let standard_proof_terminator = | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in let () = save ~export_seff id const universes compute_guard persistence hook universes in () - | Proved (opaque,idopt, _, hook,_) -> - CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") - end + | _ -> + CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term") let initialize_named_context_for_proof () = let sign = Global.named_context () in @@ -382,14 +369,17 @@ module Stack = struct end -let start_lemma id ?pl kind sigma ?(terminator=standard_proof_terminator) ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c = +(* Starting a goal *) +let start_lemma id ?pl kind sigma ?(proof_ending = Proof_ending.Regular) + ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c = let goals = [ Global.env_of_context sign , c ] in let proof = Proof_global.start_proof sigma id ?pl kind goals in - { proof ; terminator; hook; compute_guard } + { proof ; hook; compute_guard; proof_ending = CEphemeron.create proof_ending } -let start_dependent_lemma id ?pl kind ?(terminator=standard_proof_terminator) ?sign ?(compute_guard=[]) ?hook telescope = +let start_dependent_lemma id ?pl kind ?(proof_ending = Proof_ending.Regular) + ?(compute_guard=[]) ?hook telescope = let proof = Proof_global.start_dependent_proof id ?pl kind telescope in - { proof; terminator; hook; compute_guard } + { proof; hook; compute_guard; proof_ending = CEphemeron.create proof_ending } let rec_tac_initializer finite guard thms snl = if finite then @@ -480,23 +470,17 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms = start_lemma_with_initialization ?hook kind evd decl recguard thms snl (* Saving a proof *) - -let keep_admitted_vars = ref true - -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "keep section variables in admitted proofs"; - optkey = ["Keep"; "Admitted"; "Variables"]; - optread = (fun () -> !keep_admitted_vars); - optwrite = (fun b -> keep_admitted_vars := b) } +let get_keep_admitted_vars = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"keep section variables in admitted proofs" + ~key:["Keep"; "Admitted"; "Variables"] + ~value:true let save_lemma_admitted ?proof ~(lemma : t) = - let pe = let open Proof_global in match proof with - | Some ({ id; entries; persistence = k; universes }, (_, hook, _)) -> + | Some ({ id; entries; persistence = k; universes }, (hook, _, _)) -> if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); let { const_entry_secctx; const_entry_type } = List.hd entries in @@ -504,8 +488,8 @@ let save_lemma_admitted ?proof ~(lemma : t) = user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in let ctx = UState.univ_entry ~poly:(pi2 k) universes in - let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, (typ, ctx), None), universes, hook) + let sec_vars = if get_keep_admitted_vars () then const_entry_secctx else None in + finish_admitted id k (sec_vars, (typ, ctx), None) universes hook | None -> let pftree = Proof_global.get_proof lemma.proof in let gk = Proof_global.get_persistence lemma.proof in @@ -522,7 +506,7 @@ let save_lemma_admitted ?proof ~(lemma : t) = let pproofs, _univs = Proof_global.return_proof ~allow_partial:true lemma.proof in let sec_vars = - if not !keep_admitted_vars then None + if not (get_keep_admitted_vars ()) then None else match Proof_global.get_used_variables lemma.proof, pproofs with | Some _ as x, _ -> x | None, (pproof, _) :: _ -> @@ -533,13 +517,64 @@ let save_lemma_admitted ?proof ~(lemma : t) = | _ -> None in let decl = Proof_global.get_universe_decl lemma.proof in let ctx = UState.check_univ_decl ~poly universes decl in - Admitted(name,gk,(sec_vars, (typ, ctx), None), universes, lemma.hook) - in - CEphemeron.get lemma.terminator pe + finish_admitted name gk (sec_vars, (typ, ctx), None) universes lemma.hook + +(************************************************************************) +(* Saving a lemma-like constant *) +(************************************************************************) + +type proof_info = DeclareDef.Hook.t option * lemma_possible_guards * Proof_ending.t CEphemeron.key -type proof_info = proof_terminator * DeclareDef.Hook.t option * lemma_possible_guards +let default_info = None, [], CEphemeron.create Proof_ending.Regular -let default_info = standard_proof_terminator, None, [] +let finish_derive ~f ~name ~idopt ~opaque ~entries = + (* Extracts the relevant information from the proof. [Admitted] and + [Save] result in user errors. [opaque] is [true] if the proof was + concluded by [Qed], and [false] if [Defined]. [f_def] and + [lemma_def] correspond to the proof of [f] and of [suchthat], + respectively. *) + + if Option.has_some idopt then + CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name."); + + let opaque, f_def, lemma_def = + match entries with + | [_;f_def;lemma_def] -> + opaque <> Proof_global.Transparent , f_def , lemma_def + | _ -> assert false + in + (* The opacity of [f_def] is adjusted to be [false], as it + must. Then [f] is declared in the global environment. *) + let f_def = { f_def with Entries.const_entry_opaque = false } in + let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in + let f_kn = Declare.declare_constant f f_def in + let f_kn_term = mkConst f_kn in + (* In the type and body of the proof of [suchthat] there can be + references to the variable [f]. It needs to be replaced by + references to the constant [f] declared above. This substitution + performs this precise action. *) + let substf c = Vars.replace_vars [f,f_kn_term] c in + (* Extracts the type of the proof of [suchthat]. *) + let lemma_pretype = + match Entries.(lemma_def.const_entry_type) with + | Some t -> t + | None -> assert false (* Proof_global always sets type here. *) + in + (* The references of [f] are subsituted appropriately. *) + let lemma_type = substf lemma_pretype in + (* The same is done in the body of the proof. *) + let lemma_body = Future.chain Entries.(lemma_def.const_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in + let lemma_def = let open Entries in + { lemma_def with + const_entry_body = lemma_body ; + const_entry_type = Some lemma_type ; + const_entry_opaque = opaque ; } + in + let lemma_def = + Entries.DefinitionEntry lemma_def , + Decl_kinds.(IsProof Proposition) + in + ignore (Declare.declare_constant name lemma_def) let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) @@ -550,10 +585,18 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt = | None -> (* XXX: The close_proof and proof state API should be refactored so it is possible to insert proofs properly into the state *) - let { proof; terminator; hook; compute_guard } = Option.get lemma in - Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (terminator, hook, compute_guard) + let { proof; hook; compute_guard; proof_ending } = Option.get lemma in + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (hook, compute_guard, proof_ending) | Some (proof, info) -> proof, info in - let terminator, hook, compute_guard = proof_info in - CEphemeron.get terminator (Proved (opaque,idopt,proof_obj,hook,compute_guard)) + let hook, compute_guard, proof_ending = proof_info in + let open Proof_global in + let open Proof_ending in + match CEphemeron.default proof_ending Regular with + | Regular -> + finish_proved opaque idopt proof_obj hook compute_guard + | End_obligation oinfo -> + DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo + | End_derive { f ; name } -> + finish_derive ~f ~name ~idopt ~opaque ~entries:proof_obj.entries diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 961c1e41ef..51eada978a 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -11,9 +11,8 @@ open Names open Decl_kinds -(* Proofs that define a constant + terminators *) +(* Proofs that define a constant *) type t -type proof_terminator type lemma_possible_guards = int list list module Stack : sig @@ -38,8 +37,6 @@ module Stack : sig end -val standard_proof_terminator : proof_terminator - val set_endline_tactic : Genarg.glob_generic_argument -> t -> t val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t val pf_fold : (Proof_global.t -> 'a) -> t -> 'a @@ -48,12 +45,21 @@ val by : unit Proofview.tactic -> t -> t * bool (* Start of high-level proofs with an associated constant *) +module Proof_ending : sig + + type t = + | Regular + | End_obligation of DeclareObl.obligation_qed_info + | End_derive of { f : Id.t; name : Id.t } + +end + val start_lemma : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map - -> ?terminator:proof_terminator + -> ?proof_ending:Proof_ending.t -> ?sign:Environ.named_context_val -> ?compute_guard:lemma_possible_guards -> ?hook:DeclareDef.Hook.t @@ -64,8 +70,7 @@ val start_dependent_lemma : Id.t -> ?pl:UState.universe_decl -> goal_kind - -> ?terminator:proof_terminator - -> ?sign:Environ.named_context_val + -> ?proof_ending:Proof_ending.t -> ?compute_guard:lemma_possible_guards -> ?hook:DeclareDef.Hook.t -> Proofview.telescope @@ -112,29 +117,8 @@ val save_lemma_proved -> idopt:Names.lident option -> unit -(* API to build a terminator, should go away *) -type proof_ending = - | Admitted of - Names.Id.t * - Decl_kinds.goal_kind * - Entries.parameter_entry * - UState.t * - DeclareDef.Hook.t option - | Proved of - Proof_global.opacity_flag * - lident option * - Proof_global.proof_object * - DeclareDef.Hook.t option * - lemma_possible_guards - -(** This stuff is internal and will be removed in the future. *) +(* To be removed *) module Internal : sig - (** Only needed due to the Proof_global compatibility layer. *) val get_info : t -> proof_info - - (** Only needed by obligations, should be reified soon *) - val make_terminator : (proof_ending -> unit) -> proof_terminator - val apply_terminator : proof_terminator -> proof_ending -> unit - end diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 9a34bda423..cd8d22ac9a 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -471,7 +471,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr = if pred rem > 0 then begin let deps = dependencies obls num in if not (Int.Set.is_empty deps) then - ignore (auto (Some prg.prg_name) None deps) + ignore (auto (Some prg.prg_name) deps None) end let rec solve_obligation prg num tac = @@ -490,11 +490,10 @@ let rec solve_obligation prg num tac = let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in - let auto n tac oblset = auto_solve_obligations n ~oblset tac in - let terminator = Lemmas.Internal.make_terminator - (obligation_terminator prg.prg_name num auto) in + let auto n oblset tac = auto_solve_obligations n ~oblset tac in + let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in - let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in + let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~proof_ending ~hook in let lemma = fst @@ Lemmas.by !default_tactic lemma in let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in lemma diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 0749314301..d28eeb341d 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -14,9 +14,9 @@ Proof_using Egramcoq Metasyntax DeclareDef -Lemmas DeclareObl Canonical +Lemmas Class Auto_ind_decl Search |