From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/proof_global.ml | 662 +++++++++++++++++++++++++++++++++---------------- 1 file changed, 450 insertions(+), 212 deletions(-) (limited to 'proofs/proof_global.ml') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index a58fab0c..f55ab700 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - Util.error (Format.sprintf "No proof mode named \"%s\"." n) + Errors.error (Format.sprintf "No proof mode named \"%s\"." n) + +let register_proof_mode ({name = n} as m) = + Hashtbl.add proof_modes n (Ephemeron.create m) -let register_proof_mode ({ name = n } as m) = Hashtbl.add proof_modes n m (* initial mode: standard mode *) let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) } let _ = register_proof_mode standard (* Default proof mode, to be set at the beginning of proofs. *) -let default_proof_mode = ref standard +let default_proof_mode = ref (find_proof_mode "No") let _ = Goptions.declare_string_option {Goptions. @@ -48,48 +51,63 @@ let _ = optdepr = false; optname = "default proof mode" ; optkey = ["Default";"Proof";"Mode"] ; - optread = begin fun () -> - let { name = name } = !default_proof_mode in name - end; - optwrite = begin fun n -> - default_proof_mode := find_proof_mode n - end + optread = begin fun () -> + (Ephemeron.default !default_proof_mode standard).name + end; + optwrite = begin fun n -> + default_proof_mode := find_proof_mode n + end } (*** Proof Global Environment ***) -(* local shorthand *) -type nproof = identifier*Proof.proof - (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_info = { - strength : Decl_kinds.goal_kind ; - compute_guard : lemma_possible_guards; - hook :Tacexpr.declaration_hook ; - mode : proof_mode +type proof_universes = Evd.evar_universe_context + +type proof_object = { + id : Names.Id.t; + entries : Entries.definition_entry list; + persistence : Decl_kinds.goal_kind; + universes: proof_universes; + (* constraints : Univ.constraints; *) +} + +type proof_ending = + | Admitted + | Proved of Vernacexpr.opacity_flag * + (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * + proof_object +type proof_terminator = proof_ending -> unit +type closed_proof = proof_object * proof_terminator + +type pstate = { + pid : Id.t; + terminator : proof_terminator Ephemeron.key; + endline_tactic : Tacexpr.raw_tactic_expr option; + section_vars : Context.section_context option; + proof : Proof.proof; + strength : Decl_kinds.goal_kind; + mode : proof_mode Ephemeron.key; } -(* Invariant: the domain of proof_info is current_proof.*) -(* The head of [!current_proof] is the actual current proof, the other ones are +(* The head of [!pstates] is the actual current proof, the other ones are to be resumed when the current proof is closed or aborted. *) -let current_proof = ref ([]:nproof list) -let proof_info = ref (Idmap.empty : proof_info Idmap.t) +let pstates = ref ([] : pstate list) (* Current proof_mode, for bookkeeping *) let current_proof_mode = ref !default_proof_mode (* combinators for proof modes *) -let update_proof_mode () = - match !current_proof with - | (id,_)::_ -> - let { mode = m } = Idmap.find id !proof_info in - !current_proof_mode.reset (); +let update_proof_mode () = + match !pstates with + | { mode = m } :: _ -> + Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); current_proof_mode := m; - !current_proof_mode.set () - | _ -> - !current_proof_mode.reset (); - current_proof_mode := standard + Ephemeron.iter_opt !current_proof_mode (fun x -> x.set ()) + | _ -> + Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + current_proof_mode := find_proof_mode "No" (* combinators for the current_proof lists *) let push a l = l := a::!l; @@ -97,213 +115,271 @@ let push a l = l := a::!l; exception NoSuchProof let _ = Errors.register_handler begin function - | NoSuchProof -> Util.error "No such proof." + | NoSuchProof -> Errors.error "No such proof." | _ -> raise Errors.Unhandled end -let rec extract id l = - let rec aux = function - | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l) - | np::l -> let (np', l) = aux l in (np' , np::l) - | [] -> raise NoSuchProof - in - let (np,l') = aux !l in - l := l'; - update_proof_mode (); - np exception NoCurrentProof let _ = Errors.register_handler begin function - | NoCurrentProof -> Util.error "No focused proof (No proof-editing in progress)." + | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)." | _ -> raise Errors.Unhandled end -let extract_top l = - match !l with - | np::l' -> l := l' ; update_proof_mode (); np - | [] -> raise NoCurrentProof -let find_top l = - match !l with + +(*** Proof Global manipulation ***) + +let get_all_proof_names () = + List.map (function { pid = id } -> id) !pstates + +let cur_pstate () = + match !pstates with | np::_ -> np | [] -> raise NoCurrentProof -let rotate_top l1 l2 = - let np = extract_top l1 in - push np l2 +let give_me_the_proof () = (cur_pstate ()).proof +let get_current_proof_name () = (cur_pstate ()).pid -let rotate_find id l1 l2 = - let np = extract id l1 in - push np l2 - +let interp_tac = ref (fun _ -> assert false) +let set_interp_tac f = interp_tac := f -(* combinators for the proof_info map *) -let add id info m = - m := Idmap.add id info !m -let remove id m = - m := Idmap.remove id !m - -(*** Proof Global manipulation ***) +let with_current_proof f = + match !pstates with + | [] -> raise NoCurrentProof + | p :: rest -> + let et = + match p.endline_tactic with + | None -> Proofview.tclUNIT () + | Some tac -> !interp_tac tac in + let (newpr,ret) = f et p.proof in + let p = { p with proof = newpr } in + pstates := p :: rest; + ret +let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ()) -let get_all_proof_names () = - List.map fst !current_proof +let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact) -let give_me_the_proof () = - snd (find_top current_proof) -let get_current_proof_name () = - fst (find_top current_proof) +(* Sets the tactic to be used when a tactic line is closed with [...] *) +let set_endline_tactic tac = + match !pstates with + | [] -> raise NoCurrentProof + | p :: rest -> pstates := { p with endline_tactic = Some tac } :: rest (* spiwack: it might be considered to move error messages away. Or else to remove special exceptions from Proof_global. Arguments for the former: there is no reason Proof_global is only - accessed directly through vernacular commands. Error message should be + accessed directly through vernacular commands. Error message should be pushed to external layers, and so we should be able to have a finer control on error message on complex actions. *) let msg_proofs () = match get_all_proof_names () with | [] -> (spc () ++ str"(No proof-editing in progress).") | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++ - (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l)++ str ".") + (pr_sequence Nameops.pr_id l) ++ str".") -let there_is_a_proof () = !current_proof <> [] +let there_is_a_proof () = not (List.is_empty !pstates) let there_are_pending_proofs () = there_is_a_proof () let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - Util.error (Pp.string_of_ppcmds + Errors.error (Pp.string_of_ppcmds (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++ str"Use \"Abort All\" first or complete proof(s).")) end let discard_gen id = - ignore (extract id current_proof); - remove id proof_info - -let discard (loc,id) = - try - discard_gen id - with NoSuchProof -> - Util.user_err_loc + pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates + +let discard (loc,id) = + let n = List.length !pstates in + discard_gen id; + if Int.equal (List.length !pstates) n then + Errors.user_err_loc (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ()) let discard_current () = - let (id,_) = extract_top current_proof in - remove id proof_info - -let discard_all () = - current_proof := []; - proof_info := Idmap.empty + if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates + +let discard_all () = pstates := [] (* [set_proof_mode] sets the proof mode to be used after it's called. It is typically called by the Proof Mode command. *) -(* Core component. - No undo handling. - Applies to proof [id], and proof mode [m]. *) -let set_proof_mode m id = - let info = Idmap.find id !proof_info in - let info = { info with mode = m } in - proof_info := Idmap.add id info !proof_info; +let set_proof_mode m id = + pstates := + List.map (function { pid = id' } as p -> + if Id.equal id' id then { p with mode = m } else p) !pstates; update_proof_mode () -(* Complete function. - Handles undo. - Applies to current proof, and proof mode name [mn]. *) -let set_proof_mode mn = - let m = find_proof_mode mn in - let id = get_current_proof_name () in - let pr = give_me_the_proof () in - Proof.add_undo begin let curr = !current_proof_mode in fun () -> - set_proof_mode curr id ; update_proof_mode () - end pr ; - set_proof_mode m id - -exception AlreadyExists -let _ = Errors.register_handler begin function - | AlreadyExists -> Util.error "Already editing something of that name." - | _ -> raise Errors.Unhandled -end -(* [start_proof s str env t hook tac] starts a proof of name [s] and - conclusion [t]; [hook] is optionally a function to be applied at - proof end (e.g. to declare the built constructions as a coercion - or a setoid morphism); init_tac is possibly a tactic to - systematically apply at initialization time (e.g. to start the - proof of mutually dependent theorems). - It raises exception [ProofInProgress] if there is a proof being - currently edited. *) -let start_proof id str goals ?(compute_guard=[]) hook = - begin - List.iter begin fun (id_ex,_) -> - if Names.id_ord id id_ex = 0 then raise AlreadyExists - end !current_proof - end; - let p = Proof.start goals in - add id { strength=str ; - compute_guard=compute_guard ; - hook=hook ; - mode = ! default_proof_mode } proof_info ; - push (id,p) current_proof - -(* arnaud: à enlever *) -let run_tactic tac = - let p = give_me_the_proof () in - let env = Global.env () in - Proof.run_tactic env tac p -(* Sets the tactic to be used when a tactic line is closed with [...] *) -let set_endline_tactic tac = - let p = give_me_the_proof () in - Proof.set_endline_tactic tac p +let set_proof_mode mn = + set_proof_mode (find_proof_mode mn) (get_current_proof_name ()) + +let activate_proof_mode mode = + Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) +let disactivate_proof_mode mode = + Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ()) + +(** [start_proof sigma id str 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 + is (spiwack: for potential printing, I believe is used only by + closing commands and the xml plugin); [terminator] is used at the + end of the proof to close the proof. The proof is started in the + evar map [sigma] (which can typically contain universe + constraints). *) +let start_proof sigma id str goals terminator = + let initial_state = { + pid = id; + terminator = Ephemeron.create terminator; + proof = Proof.start sigma goals; + endline_tactic = None; + section_vars = None; + strength = str; + mode = find_proof_mode "No" } in + push initial_state pstates + +let start_dependent_proof id str goals terminator = + let initial_state = { + pid = id; + terminator = Ephemeron.create terminator; + proof = Proof.dependent_start goals; + endline_tactic = None; + section_vars = None; + strength = str; + mode = find_proof_mode "No" } in + push initial_state pstates + +let get_used_variables () = (cur_pstate ()).section_vars let set_used_variables l = - let p = give_me_the_proof () in let env = Global.env () in - let ids = List.fold_right Idset.add l Idset.empty in + let ids = List.fold_right Id.Set.add l Id.Set.empty in let ctx = Environ.keep_hyps env ids in - Proof.set_used_variables ctx p - -let get_used_variables () = - Proof.get_used_variables (give_me_the_proof ()) - -let with_end_tac tac = - let p = give_me_the_proof () in - Proof.with_end_tac p tac - -let close_proof () = - (* spiwack: for now close_proof doesn't actually discard the proof, it is done - by [Command.save]. *) - try - let id = get_current_proof_name () in - let p = give_me_the_proof () in - let proofs_and_types = Proof.return p in - let section_vars = Proof.get_used_variables p in - let entries = List.map - (fun (c,t) -> { Entries.const_entry_body = c; - const_entry_secctx = section_vars; - const_entry_type = Some t; - const_entry_opaque = true }) - proofs_and_types - in - let { compute_guard=cg ; strength=str ; hook=hook } = - Idmap.find id !proof_info - in - (id, (entries,cg,str,hook)) - with - | Proof.UnfinishedProof -> - Util.error "Attempt to save an incomplete proof" - | Proof.HasUnresolvedEvar -> - Util.error "Attempt to save a proof with existential variables still non-instantiated" - + match !pstates with + | [] -> raise NoCurrentProof + | p :: rest -> + if not (Option.is_empty p.section_vars) then + Errors.error "Used section variables can be declared only once"; + pstates := { p with section_vars = Some ctx} :: rest; + ctx + +let get_open_goals () = + let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in + List.length gl + + List.fold_left (+) 0 + (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + + List.length shelf + +let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = + let { pid; section_vars; strength; proof; terminator } = cur_pstate () in + let poly = pi2 strength (* Polymorphic *) in + let initial_goals = Proof.initial_goals proof in + let fpl, univs = Future.split2 fpl in + let universes = + if poly || now then Future.force univs + else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) + in + (* Because of dependent subgoals at the begining of proofs, we could + have existential variables in the initial types of goals, we need to + normalise them for the kernel. *) + let subst_evar k = + Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in + let nf = Universes.nf_evars_and_universes_opt_subst subst_evar + (Evd.evar_universe_context_subst universes) in + let make_body = + if poly || now then + let make_body t (c, eff) = + let open Universes in + let body = c and typ = nf t in + let used_univs_body = Universes.universes_of_constr body in + let used_univs_typ = Universes.universes_of_constr typ in + let ctx = Evd.evar_universe_context_set universes in + if keep_body_ucst_sepatate then + (* For vi2vo compilation proofs are computed now but we need to + * completent the univ constraints of the typ with the ones of + * the body. So we keep the two sets distinct. *) + let ctx_body = restrict_universe_context ctx used_univs_body in + let ctx_typ = restrict_universe_context ctx used_univs_typ in + let univs_typ = Univ.ContextSet.to_context ctx_typ in + (univs_typ, typ), ((body, ctx_body), eff) + else + (* Since the proof is computed now, we can simply have 1 set of + * constraints in which we merge the ones for the body and the ones + * for the typ *) + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let ctx = restrict_universe_context ctx used_univs in + let univs = Univ.ContextSet.to_context ctx in + (univs, typ), ((body, Univ.ContextSet.empty), eff) + in + fun t p -> + Future.split2 (Future.chain ~pure:true p (make_body t)) + else + fun t p -> + let initunivs = Evd.evar_context_universe_context universes in + Future.from_val (initunivs, nf t), + Future.chain ~pure:true p (fun (pt,eff) -> + (pt, Evd.evar_universe_context_set (Future.force univs)), eff) + in + let entries = + Future.map2 (fun p (_, t) -> + let univstyp, body = make_body t p in + let univs, typ = Future.force univstyp in + { Entries. + const_entry_body = body; + const_entry_secctx = section_vars; + const_entry_feedback = feedback_id; + const_entry_type = Some typ; + const_entry_inline_code = false; + const_entry_opaque = true; + const_entry_universes = univs; + const_entry_polymorphic = poly}) + fpl initial_goals in + { id = pid; entries = entries; persistence = strength; universes = universes }, + fun pr_ending -> Ephemeron.get terminator pr_ending + +type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context + +let return_proof () = + let { proof; strength = (_,poly,_) } = cur_pstate () in + let initial_goals = Proof.initial_goals proof in + let evd = + let error s = raise (Errors.UserError("last tactic before Qed",s)) in + try Proof.return proof with + | Proof.UnfinishedProof -> + error(str"Attempt to save an incomplete proof") + | Proof.HasShelvedGoals -> + error(str"Attempt to save a proof with shelved goals") + | Proof.HasGivenUpGoals -> + error(str"Attempt to save a proof with given up goals") + | Proof.HasUnresolvedEvar-> + error(str"Attempt to save a proof with existential " ++ + str"variables still non-instantiated") in + let eff = Evd.eval_side_effects evd in + let evd = + if poly || !Flags.compilation_mode = Flags.BuildVo + then Evd.nf_constraints evd + else evd in + (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) + let proofs = + List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in + proofs, Evd.evar_universe_context evd + +let close_future_proof ~feedback_id proof = + close_proof ~keep_body_ucst_sepatate:true ~feedback_id ~now:false proof +let close_proof ~keep_body_ucst_sepatate fix_exn = + close_proof ~keep_body_ucst_sepatate ~now:true + (Future.from_val ~fix_exn (return_proof ())) + +(** Gets the current terminator without checking that the proof has + been completed. Useful for the likes of [Admitted]. *) +let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator +let set_terminator hook = + match !pstates with + | [] -> raise NoCurrentProof + | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps -(**********************************************************) -(* *) -(* Utility functions *) -(* *) -(**********************************************************) -let maximal_unfocus k p = - begin try while Proof.no_focused_goal p do - Proof.unfocus k p - done - with Proof.FullyUnfocused | Proof.CannotUnfocusThisWay -> () - end (**********************************************************) @@ -314,14 +390,25 @@ let maximal_unfocus k p = module Bullet = struct - open Store.Field + type t = Vernacexpr.bullet + + let bullet_eq b1 b2 = match b1, b2 with + | Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2 + | Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2 + | Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2 + | _ -> false + let pr_bullet b = + match b with + | Vernacexpr.Dash n -> str (String.make n '-') + | Vernacexpr.Star n -> str (String.make n '*') + | Vernacexpr.Plus n -> str (String.make n '+') - type t = Vernacexpr.bullet type behavior = { name : string; - put : Proof.proof -> t -> unit + put : Proof.proof -> t -> Proof.proof; + suggest: Proof.proof -> string option } let behaviors = Hashtbl.create 4 @@ -330,11 +417,55 @@ module Bullet = struct (*** initial modes ***) let none = { name = "None"; - put = fun _ _ -> () + put = (fun x _ -> x); + suggest = (fun _ -> None) } let _ = register_behavior none module Strict = struct + type suggestion = + | Suggest of t (* this bullet is mandatory here *) + | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *) + | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending, + some focused goals exists. *) + | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *) + | ProofFinished (* No more goal anywhere *) + + (* give a message only if more informative than the standard coq message *) + let suggest_on_solved_goal sugg = + match sugg with + | NeedClosingBrace -> Some "Try unfocusing with \"}\"." + | NoBulletInUse -> None + | ProofFinished -> None + | Suggest b -> Some ("Focus next goal with bullet " + ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^".") + | Unfinished b -> Some ("The current bullet " + ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^ " is unfinished.") + + (* give always a message. *) + let suggest_on_error sugg = + match sugg with + | NeedClosingBrace -> "Try unfocusing with \"}\"." + | NoBulletInUse -> assert false (* This should never raise an error. *) + | ProofFinished -> "No more subgoals." + | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^ " is mandatory here.") + | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^ " is not finished.") + + exception FailedBullet of t * suggestion + + let _ = + Errors.register_handler + (function + | FailedBullet (b,sugg) -> + let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in + Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg)) + | _ -> raise Errors.Unhandled) + + (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind) let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind @@ -350,42 +481,88 @@ module Bullet = struct let has_bullet bul pr = let rec has_bullet = function - | b'::_ when bul=b' -> true + | b'::_ when bullet_eq bul b' -> true | _::l -> has_bullet l | [] -> false in has_bullet (get_bullets pr) - (* precondition: the stack is not empty *) + (* pop a bullet from proof [pr]. There should be at least one + bullet in use. If pop impossible (pending proofs on this level + of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *) let pop pr = match get_bullets pr with - | b::_ -> - Proof.unfocus bullet_kind pr; - (*returns*) b + | b::_ -> Proof.unfocus bullet_kind pr () , b | _ -> assert false - let push b pr = + let push (b:t) pr = Proof.focus bullet_cond (b::get_bullets pr) 1 pr + (* Used only in the next function. + TODO: use a recursive function instead? *) + exception SuggestFound of t + + let suggest_bullet (prf:Proof.proof): suggestion = + if Proof.is_done prf then ProofFinished + else if not (Proof.no_focused_goal prf) + then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *) + match get_bullets prf with + | b::_ -> Unfinished b + | _ -> NoBulletInUse + else (* There is no goal under focus but some are unfocussed, + let us look at the bullet needed. If no *) + let pcobaye = ref prf in + try + while true do + let pcobaye', b = pop !pcobaye in + (* pop went well, this means that there are no more goals + *under this* bullet b, see if a new b can be pushed. *) + (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *) + raise (SuggestFound b) + with SuggestFound _ as e -> raise e + | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *) + pcobaye := pcobaye' + done; + assert false + with SuggestFound b -> Suggest b + | _ -> NeedClosingBrace (* No push was possible, but there are still + subgoals somewhere: there must be a "}" to use. *) + + + let rec pop_until (prf:Proof.proof) bul: Proof.proof = + let prf', b = pop prf in + if bullet_eq bul b then prf' + else pop_until prf' bul + let put p bul = - if has_bullet bul p then - Proof.transaction p begin fun () -> - while bul <> pop p do () done; + try + if not (has_bullet bul p) then + (* bullet is not in use, so pushing it is always ok unless + no goal under focus. *) push bul p - end - else - push bul p + else + match suggest_bullet p with + | Suggest suggested_bullet when bullet_eq bul suggested_bullet + -> (* suggested_bullet is mandatory and you gave the right one *) + let p' = pop_until p bul in + push bul p' + (* the bullet you gave is in use but not the right one *) + | sugg -> raise (FailedBullet (bul,sugg)) + with Proof.NoSuchGoals _ -> (* push went bad *) + raise (FailedBullet (bul,suggest_bullet p)) let strict = { name = "Strict Subproofs"; - put = put + put = put; + suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf)) + } let _ = register_behavior strict end (* Current bullet behavior, controled by the option *) let current_behavior = ref Strict.strict - + let _ = Goptions.declare_string_option {Goptions. optsync = true; @@ -402,16 +579,77 @@ module Bullet = struct let put p b = (!current_behavior).put p b + + let suggest p = + (!current_behavior).suggest p end +let _ = + let hook n = + let prf = give_me_the_proof () in + (Bullet.suggest prf) in + Proofview.set_nosuchgoals_hook hook + + +(**********************************************************) +(* *) +(* Default goal selector *) +(* *) +(**********************************************************) + + +(* Default goal selector: selector chosen when a tactic is applied + without an explicit selector. *) +let default_goal_selector = ref (Vernacexpr.SelectNth 1) +let get_default_goal_selector () = !default_goal_selector + +let print_goal_selector = function + | Vernacexpr.SelectAll -> "all" + | Vernacexpr.SelectNth i -> string_of_int i + | Vernacexpr.SelectId id -> Id.to_string id + | Vernacexpr.SelectAllParallel -> "par" + +let parse_goal_selector = function + | "all" -> Vernacexpr.SelectAll + | i -> + let err_msg = "A selector must be \"all\" or a natural number." in + begin try + let i = int_of_string i in + if i < 0 then Errors.error err_msg; + Vernacexpr.SelectNth i + with Failure _ -> Errors.error err_msg + end + +let _ = + Goptions.declare_string_option {Goptions. + optsync = true ; + optdepr = false; + optname = "default goal selector" ; + optkey = ["Default";"Goal";"Selector"] ; + optread = begin fun () -> print_goal_selector !default_goal_selector end; + optwrite = begin fun n -> + default_goal_selector := parse_goal_selector n + end + } + + module V82 = struct let get_current_initial_conclusions () = - let p = give_me_the_proof () in - let id = get_current_proof_name () in - let { strength=str ; hook=hook } = - Idmap.find id !proof_info - in - (id,(Proof.V82.get_initial_conclusions p, str, hook)) + let { pid; strength; proof } = cur_pstate () in + let initial = Proof.initial_goals proof in + let goals = List.map (fun (o, c) -> c) initial in + pid, (goals, strength) end +type state = pstate list + +let freeze ~marshallable = + match marshallable with + | `Yes -> + Errors.anomaly (Pp.str"full marshalling of proof state not supported") + | `Shallow -> !pstates + | `No -> !pstates +let unfreeze s = pstates := s; update_proof_mode () +let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof + -- cgit v1.2.3