diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 4 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 8 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 90 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 55 |
4 files changed, 97 insertions, 60 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7333114eae..66b47a64a7 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) -let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) +let by tac = Proof_global.with_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) (**********************************************************************) (* Shortcut to build a term using tactics *) @@ -121,7 +121,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let evd = Evd.from_ctx ctx in let terminator = Proof_global.make_terminator (fun _ -> ()) in let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof ~ontop:None evd id goal_kind goals terminator in + let pf = Proof_global.start_proof evd id goal_kind goals terminator in try let pf, status = by tac pf in let open Proof_global in diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 77d701b41f..ec52d2d5cf 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -23,17 +23,17 @@ exception NoSuchGoal the current focused proof or raises a [UserError] if there is no focused proof or if there is no more subgoals *) -val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env +val get_goal_context : Proof_global.pstate -> int -> Evd.evar_map * env (** [get_current_goal_context ()] works as [get_goal_context 1] *) -val get_current_goal_context : Proof_global.t -> Evd.evar_map * env +val get_current_goal_context : Proof_global.pstate -> Evd.evar_map * env (** [get_current_context ()] returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. If there is no pending proof then it returns the current global environment and empty evar_map. *) -val get_current_context : Proof_global.t -> Evd.evar_map * env +val get_current_context : Proof_global.pstate -> Evd.evar_map * env (** {6 ... } *) @@ -49,7 +49,7 @@ val solve : ?with_end_tac:unit Proofview.tactic -> focused proof. Returns [false] if an unsafe tactic has been used. *) -val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool +val by : unit Proofview.tactic -> Proof_global.pstate -> Proof_global.pstate * bool (** Option telling if unification heuristics should be used. *) val use_unification_heuristics : unit -> bool diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 40ae4acc88..8d7960829b 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -63,23 +63,40 @@ let pstate_map f (pf, pfl) = (f pf, List.map f pfl) let make_terminator f = f let apply_terminator f = f +let get_current_pstate (ps,_) = ps + (* combinators for the current_proof lists *) let push ~ontop a = match ontop with | None -> a , [] | Some (l,ls) -> a, (l :: ls) +let maybe_push ~ontop = function + | Some pstate -> Some (push ~ontop pstate) + | None -> ontop + (*** Proof Global manipulation ***) let get_all_proof_names (pf : t) = let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in pn :: pns -let give_me_the_proof (ps,_) = ps.proof -let get_current_proof_name (ps,_) = (Proof.data ps.proof).Proof.name -let get_current_persistence (ps,_) = ps.strength +let give_me_the_proof ps = ps.proof +let get_current_proof_name ps = (Proof.data ps.proof).Proof.name +let get_current_persistence ps = ps.strength + +let with_current_pstate f (ps,psl) = + let ps, ret = f ps in + (ps, psl), ret + +let modify_current_pstate f (ps,psl) = + f ps, psl + +let modify_proof f ps = + let proof = f ps.proof in + {ps with proof} -let with_current_proof f (ps, psl) = +let with_proof f ps = let et = match ps.endline_tactic with | None -> Proofview.tclUNIT () @@ -92,16 +109,23 @@ let with_current_proof f (ps, psl) = in let (newpr,ret) = f et ps.proof in let ps = { ps with proof = newpr } in - (ps, psl), ret + ps, ret + +let with_current_proof f (ps,rest) = + let ps, ret = with_proof f ps in + (ps, rest), ret let simple_with_current_proof f pf = let p, () = with_current_proof (fun t p -> f t p , ()) pf in p -let compact_the_proof pf = simple_with_current_proof (fun _ -> Proof.compact) pf +let simple_with_proof f ps = + let ps, () = with_proof (fun t ps -> f t ps, ()) ps in ps + +let compact_the_proof pf = simple_with_proof (fun _ -> Proof.compact) pf (* Sets the tactic to be used when a tactic line is closed with [...] *) -let set_endline_tactic tac (ps, psl) = - { ps with endline_tactic = Some tac }, psl +let set_endline_tactic tac ps = + { ps with endline_tactic = Some tac } let pf_name_eq id ps = let Proof.{ name } = Proof.data ps.proof in @@ -112,8 +136,10 @@ let discard {CAst.loc;v=id} (ps, psl) = | [] -> None | ps :: psl -> Some (ps, psl) -let discard_current (ps, psl) = - if List.is_empty psl then None else Some List.(hd psl, tl psl) +let discard_current (_, psl) = + match psl with + | [] -> None + | ps :: psl -> Some (ps, psl) (** [start_proof sigma id pl str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and @@ -123,30 +149,26 @@ let discard_current (ps, psl) = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof ~ontop sigma name ?(pl=UState.default_univ_decl) kind goals terminator = - let initial_state = { - terminator = CEphemeron.create terminator; +let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator = + { terminator = CEphemeron.create terminator; proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; endline_tactic = None; section_vars = None; universe_decl = pl; - strength = kind } in - push ~ontop initial_state + strength = kind } -let start_dependent_proof ~ontop name ?(pl=UState.default_univ_decl) kind goals terminator = - let initial_state = { - terminator = CEphemeron.create terminator; +let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = + { terminator = CEphemeron.create terminator; proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; endline_tactic = None; section_vars = None; universe_decl = pl; - strength = kind } in - push ~ontop initial_state + strength = kind } -let get_used_variables (pf,_) = pf.section_vars -let get_universe_decl (pf,_) = pf.universe_decl +let get_used_variables pf = pf.section_vars +let get_universe_decl pf = pf.universe_decl -let set_used_variables (ps,psl) l = +let set_used_variables ps l = let open Context.Named.Declaration in let env = Global.env () in let ids = List.fold_right Id.Set.add l Id.Set.empty in @@ -170,9 +192,9 @@ let set_used_variables (ps,psl) l = if not (Option.is_empty ps.section_vars) then CErrors.user_err Pp.(str "Used section variables can be declared only once"); (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), ({ ps with section_vars = Some ctx}, psl) + (ctx, []), { ps with section_vars = Some ctx} -let get_open_goals (ps, _) = +let get_open_goals ps = let Proof.{ goals; stack; shelf } = Proof.data ps.proof in List.length goals + List.fold_left (+) 0 @@ -293,7 +315,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now universes }, fun pr_ending -> CEphemeron.get terminator pr_ending -let return_proof ?(allow_partial=false) (ps,_) = +let return_proof ?(allow_partial=false) ps = let { proof } = ps in if allow_partial then begin let proofs = Proof.partial_proof proof in @@ -322,27 +344,27 @@ let return_proof ?(allow_partial=false) (ps,_) = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in proofs, Evd.evar_universe_context evd -let close_future_proof ~opaque ~feedback_id (ps, psl) proof = +let close_future_proof ~opaque ~feedback_id ps proof = close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps -let close_proof ~opaque ~keep_body_ucst_separate fix_exn (ps, psl) = +let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = close_proof ~opaque ~keep_body_ucst_separate ~now:true - (Future.from_val ~fix_exn (return_proof (ps,psl))) ps + (Future.from_val ~fix_exn (return_proof ps)) ps (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) -let get_terminator (ps, _) = CEphemeron.get ps.terminator -let set_terminator hook (ps, psl) = - { ps with terminator = CEphemeron.create hook }, psl +let get_terminator ps = CEphemeron.get ps.terminator +let set_terminator hook ps = + { ps with terminator = CEphemeron.create hook } let copy_terminators ~src ~tgt = let (ps, psl), (ts,tsl) = src, tgt in assert(List.length psl = List.length tsl); {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl -let update_global_env (pf : t) = +let update_global_env pf = let res, () = - with_current_proof (fun _ p -> + with_proof (fun _ p -> Proof.in_proof p (fun sigma -> let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e2e457483b..6984fff63a 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -12,16 +12,20 @@ toplevel. In particular it defines the global proof environment. *) +type pstate type t -val get_current_proof_name : t -> Names.Id.t -val get_current_persistence : t -> Decl_kinds.goal_kind + +val get_current_pstate : t -> pstate + +val get_current_proof_name : pstate -> Names.Id.t +val get_current_persistence : pstate -> Decl_kinds.goal_kind val get_all_proof_names : t -> Names.Id.t list val discard : Names.lident -> t -> t option val discard_current : t -> t option -val give_me_the_proof : t -> Proof.t -val compact_the_proof : t -> t +val give_me_the_proof : pstate -> Proof.t +val compact_the_proof : pstate -> pstate (** When a proof is closed, it is reified into a [proof_object], where [id] is the name of the proof, [entries] the list of the proof terms @@ -52,6 +56,10 @@ type closed_proof = proof_object * proof_terminator val make_terminator : (proof_ending -> unit) -> proof_terminator val apply_terminator : proof_terminator -> proof_ending -> unit +val push : ontop:t option -> pstate -> t + +val maybe_push : ontop:t option -> pstate option -> t option + (** [start_proof ~ontop id str pl goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -60,25 +68,26 @@ val apply_terminator : proof_terminator -> proof_ending -> unit morphism). The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -val start_proof : ontop:t option -> +val start_proof : Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> - proof_terminator -> t + proof_terminator -> pstate (** Like [start_proof] except that there may be dependencies between initial goals. *) -val start_dependent_proof : ontop:t option -> +val start_dependent_proof : Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> - Proofview.telescope -> proof_terminator -> t + Proofview.telescope -> proof_terminator -> pstate (** Update the proofs global environment after a side-effecting command (e.g. a sublemma definition) has been run inside it. Assumes there_are_pending_proofs. *) -val update_global_env : t -> t +val update_global_env : pstate -> pstate (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> closed_proof +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> + pstate -> closed_proof (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be @@ -88,15 +97,15 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) -val return_proof : ?allow_partial:bool -> t -> closed_proof_output -val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> +val return_proof : ?allow_partial:bool -> pstate -> closed_proof_output +val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> pstate -> closed_proof_output Future.computation -> closed_proof (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) -val get_terminator : t -> proof_terminator -val set_terminator : proof_terminator -> t -> t -val get_open_goals : t -> int +val get_terminator : pstate -> proof_terminator +val set_terminator : proof_terminator -> pstate -> pstate +val get_open_goals : pstate -> int (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is no current proof. @@ -106,18 +115,24 @@ val with_current_proof : val simple_with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t +val with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> pstate -> pstate * 'a +val modify_proof : (Proof.t -> Proof.t) -> pstate -> pstate + +val with_current_pstate : (pstate -> pstate * 'a) -> t -> t * 'a +val modify_current_pstate : (pstate -> pstate) -> t -> t + (** Sets the tactic to be used when a tactic line is closed with [...] *) -val set_endline_tactic : Genarg.glob_generic_argument -> t -> t +val set_endline_tactic : Genarg.glob_generic_argument -> pstate -> pstate (** Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) -val set_used_variables : t -> - Names.Id.t list -> (Constr.named_context * Names.lident list) * t +val set_used_variables : pstate -> + Names.Id.t list -> (Constr.named_context * Names.lident list) * pstate -val get_used_variables : t -> Constr.named_context option +val get_used_variables : pstate -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) -val get_universe_decl : t -> UState.universe_decl +val get_universe_decl : pstate -> UState.universe_decl val copy_terminators : src:t -> tgt:t -> t |