diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 493 |
1 files changed, 131 insertions, 362 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e753e972..d6c0e334 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (***********************************************************************) @@ -18,6 +20,8 @@ open Util open Pp open Names +module NamedDecl = Context.Named.Declaration + (*** Proof Modes ***) (* Type of proof modes : @@ -34,7 +38,7 @@ let proof_modes = Hashtbl.create 6 let find_proof_mode n = try Hashtbl.find proof_modes n with Not_found -> - CErrors.error (Format.sprintf "No proof mode named \"%s\"." n) + CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n)) let register_proof_mode ({name = n} as m) = Hashtbl.add proof_modes n (CEphemeron.create m) @@ -50,8 +54,7 @@ let get_default_proof_mode_name () = (CEphemeron.default !default_proof_mode standard).name let _ = - Goptions.declare_string_option {Goptions. - optsync = true ; + Goptions.(declare_string_option { optdepr = false; optname = "default proof mode" ; optkey = ["Default";"Proof";"Mode"] ; @@ -61,41 +64,42 @@ let _ = optwrite = begin fun n -> default_proof_mode := find_proof_mode n end - } + }) (*** Proof Global Environment ***) (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_universes = Evd.evar_universe_context * Universes.universe_binders option -type universe_binders = Id.t Loc.located list type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of Vernacexpr.opacity_flag * - (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * + Misctypes.lident option * proof_object type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator type pstate = { - pid : Id.t; + pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; - endline_tactic : Tacexpr.raw_tactic_expr option; - section_vars : Context.section_context option; - proof : Proof.proof; + endline_tactic : Genarg.glob_generic_argument option; + section_vars : Context.Named.t option; + proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; - universe_binders: universe_binders option; + universe_decl: Univdecls.universe_decl; } +type t = pstate list +type state = t + let make_terminator f = f let apply_terminator f = f @@ -123,13 +127,13 @@ let push a l = l := a::!l; exception NoSuchProof let _ = CErrors.register_handler begin function - | NoSuchProof -> CErrors.error "No such proof." + | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.") | _ -> raise CErrors.Unhandled end exception NoCurrentProof let _ = CErrors.register_handler begin function - | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)." + | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end @@ -144,11 +148,9 @@ let cur_pstate () = | [] -> raise NoCurrentProof let give_me_the_proof () = (cur_pstate ()).proof +let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None let get_current_proof_name () = (cur_pstate ()).pid -let interp_tac = ref (fun _ -> assert false) -let set_interp_tac f = interp_tac := f - let with_current_proof f = match !pstates with | [] -> raise NoCurrentProof @@ -156,11 +158,18 @@ let with_current_proof f = let et = match p.endline_tactic with | None -> Proofview.tclUNIT () - | Some tac -> !interp_tac tac in + | Some tac -> + let open Geninterp in + let ist = { lfun = Id.Map.empty; extra = TacStore.empty } in + let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in + let tac = Geninterp.interp tag ist tac in + Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) + 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 compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact) @@ -182,7 +191,7 @@ let msg_proofs () = match get_all_proof_names () with | [] -> (spc () ++ str"(No proof-editing in progress).") | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++ - (pr_sequence Nameops.pr_id l) ++ str".") + (pr_sequence Id.print l) ++ str".") let there_is_a_proof () = not (List.is_empty !pstates) let there_are_pending_proofs () = there_is_a_proof () @@ -190,20 +199,20 @@ let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - CErrors.error (Pp.string_of_ppcmds + CErrors.user_err (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++ - str"Use \"Abort All\" first or complete proof(s).")) + str"Use \"Abort All\" first or complete proof(s).") end let discard_gen id = pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates -let discard (loc,id) = +let discard {CAst.loc;v=id} = let n = List.length !pstates in discard_gen id; if Int.equal (List.length !pstates) n then - CErrors.user_err_loc - (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ()) + CErrors.user_err ?loc + ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ()) let discard_current () = if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates @@ -226,15 +235,22 @@ let activate_proof_mode mode = let disactivate_current_proof_mode () = CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) -(** [start_proof sigma id str goals terminator] starts a proof of name +let default_universe_decl = + let open Misctypes in + { univdecl_instance = []; + univdecl_extensible_instance = true; + univdecl_constraints = Univ.Constraint.empty; + univdecl_extensible_constraints = true } + +(** [start_proof sigma id pl 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 ?pl str goals terminator = + constraints), and with universe bindings pl. *) +let start_proof sigma id ?(pl=default_universe_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -243,10 +259,10 @@ let start_proof sigma id ?pl str goals terminator = section_vars = None; strength = str; mode = find_proof_mode "No"; - universe_binders = pl } in + universe_decl = pl } in push initial_state pstates -let start_dependent_proof id ?pl str goals terminator = +let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -255,16 +271,15 @@ let start_dependent_proof id ?pl str goals terminator = section_vars = None; strength = str; mode = find_proof_mode "No"; - universe_binders = pl } in + universe_decl = pl } in push initial_state pstates let get_used_variables () = (cur_pstate ()).section_vars -let get_universe_binders () = (cur_pstate ()).universe_binders +let get_universe_decl () = (cur_pstate ()).universe_decl let proof_using_auto_clear = ref false let _ = Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = "Proof using Clear Unused"; Goptions.optkey = ["Proof";"Using";"Clear";"Unused"]; Goptions.optread = (fun () -> !proof_using_auto_clear); @@ -276,19 +291,19 @@ let set_used_variables l = let ids = List.fold_right Id.Set.add l Id.Set.empty in let ctx = Environ.keep_hyps env ids in let ctx_set = - List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in + List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in let vars_of = Environ.global_vars_set in let aux env entry (ctx, all_safe, to_clear as orig) = match entry with | LocalAssum (x,_) -> if Id.Set.mem x all_safe then orig - else (ctx, all_safe, (Loc.ghost,x)::to_clear) + else (ctx, all_safe, (CAst.make x)::to_clear) | LocalDef (x,bo, ty) as decl -> if Id.Set.mem x all_safe then orig else let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in if Id.Set.subset vars all_safe then (decl :: ctx, Id.Set.add x all_safe, to_clear) - else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in + else (ctx, all_safe, (CAst.make x) :: to_clear) in let ctx, _, to_clear = Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in let to_clear = if !proof_using_auto_clear then to_clear else [] in @@ -296,7 +311,7 @@ let set_used_variables l = | [] -> raise NoCurrentProof | p :: rest -> if not (Option.is_empty p.section_vars) then - CErrors.error "Used section variables can be declared only once"; + CErrors.user_err Pp.(str "Used section variables can be declared only once"); pstates := { p with section_vars = Some ctx} :: rest; ctx, to_clear @@ -307,17 +322,18 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf -let constrain_variables init uctx = - let levels = Univ.Instance.levels (Univ.UContext.instance init) in - let cstrs = UState.constrain_variables levels uctx in - Univ.ContextSet.add_constraints cstrs (UState.context_set uctx) +type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t -let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = - let { pid; section_vars; strength; proof; terminator; universe_binders } = +let close_proof ~keep_body_ucst_separate ?feedback_id ~now + (fpl : closed_proof_output Future.computation) = + let { pid; section_vars; strength; proof; terminator; universe_decl } = cur_pstate () in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in + let constrain_variables ctx = + UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx + in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in (* Because of dependent subgoals at the beginning of proofs, we could @@ -326,72 +342,73 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = 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 + (UState.subst universes) in let make_body = if poly || now then let make_body t (c, eff) = - let open Universes in let body = c in - let typ = - if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then - nf t - else t - in - let used_univs_body = Universes.universes_of_constr body in - let used_univs_typ = Universes.universes_of_constr typ in - if keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff) then - let initunivs = Evd.evar_context_universe_context initial_euctx in - let ctx = constrain_variables initunivs universes in + let allow_deferred = + not poly && (keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff)) + in + let typ = if allow_deferred then t else nf t in + let env = Global.env () in + let used_univs_body = Univops.universes_of_constr env body in + let used_univs_typ = Univops.universes_of_constr env typ in + if allow_deferred then + let initunivs = UState.const_univ_entry ~poly initial_euctx in + let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to - * complement the univ constraints of the typ with the ones of - * the body. So we keep the two sets distinct. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx_body = restrict_universe_context ctx used_univs in - (initunivs, typ), ((body, ctx_body), eff) + complement the univ constraints of the typ with the ones of + the body. So we keep the two sets distinct. *) + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let ctx_body = UState.restrict ctx used_univs in + let univs = UState.check_mono_univ_decl ctx_body universe_decl in + (initunivs, typ), ((body, univs), eff) else - let initunivs = Univ.UContext.empty in - let ctx = constrain_variables initunivs universes in (* 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 *) + constraints in which we merge the ones for the body and the ones + for the typ. We recheck the declaration after restricting with + the actually used universes. + TODO: check if restrict is really necessary now. *) 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 + let ctx = UState.restrict universes used_univs in + let univs = UState.check_univ_decl ~poly ctx universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in - fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t)) + fun t p -> Future.split2 (Future.chain p (make_body t)) else fun t p -> - let initunivs = Evd.evar_context_universe_context initial_euctx in - Future.from_val (initunivs, nf t), - Future.chain ~pure:true p (fun (pt,eff) -> - (pt,constrain_variables initunivs (Future.force univs)),eff) + (* Already checked the univ_decl for the type universes when starting the proof. *) + let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in + Future.from_val (univctx, nf t), + Future.chain p (fun (pt,eff) -> + (* Deferred proof, we already checked the universe declaration with + the initial universes, ensure that the final universes respect + the declaration as well. If the declaration is non-extensible, + this will prevent the body from adding universes and constraints. *) + let bodyunivs = constrain_variables (Future.force univs) in + let univs = UState.check_mono_univ_decl bodyunivs universe_decl in + (pt,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 - let binders = - Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes))) - universe_binders + let entry_fn p (_, t) = + let t = EConstr.Unsafe.to_constr t in + 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; } in + let entries = Future.map2 entry_fn fpl initial_goals in { id = pid; entries = entries; persistence = strength; - universes = (universes, binders) }, + universes }, fun pr_ending -> CEphemeron.get terminator pr_ending -type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context - let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in if allow_partial then begin @@ -401,14 +418,14 @@ let return_proof ?(allow_partial=false) () = (** 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 -> c, eff) proofs in + let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd end else let initial_goals = Proof.initial_goals proof in let evd = let error s = let prf = str " (in proof " ++ Id.print pid ++ str ")" in - raise (CErrors.UserError("last tactic before Qed",s ++ prf)) + raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf)) in try Proof.return proof with | Proof.UnfinishedProof -> @@ -420,12 +437,12 @@ let return_proof ?(allow_partial=false) () = | Proof.HasUnresolvedEvar-> error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes 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 + List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in proofs, Evd.evar_universe_context evd let close_future_proof ~feedback_id proof = @@ -442,263 +459,6 @@ let set_terminator hook = | [] -> raise NoCurrentProof | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps - - - -(**********************************************************) -(* *) -(* Bullets *) -(* *) -(**********************************************************) - -module Bullet = struct - - 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 behavior = { - name : string; - put : Proof.proof -> t -> Proof.proof; - suggest: Proof.proof -> std_ppcmds - } - - let behaviors = Hashtbl.create 4 - let register_behavior b = Hashtbl.add behaviors b.name b - - (*** initial modes ***) - let none = { - name = "None"; - put = (fun x _ -> x); - suggest = (fun _ -> mt ()) - } - 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 -> str"Try unfocusing with \"}\"." - | NoBulletInUse -> mt () - | ProofFinished -> mt () - | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"." - | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished." - - (* give always a message. *) - let suggest_on_error sugg = - match sugg with - | NeedClosingBrace -> str"Try unfocusing with \"}\"." - | NoBulletInUse -> assert false (* This should never raise an error. *) - | ProofFinished -> str"No more subgoals." - | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here." - | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished." - - exception FailedBullet of t * suggestion - - let _ = - CErrors.register_handler - (function - | FailedBullet (b,sugg) -> - let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in - CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg) - | _ -> raise CErrors.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 - - (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command - experience will tell if this is the right discipline of if we want to be finer and - reset them only for a choice of bullets. *) - let get_bullets pr = - if Proof.is_last_focus bullet_kind pr then - Proof.get_at_focus bullet_kind pr - else - [] - - let has_bullet bul pr = - let rec has_bullet = function - | b'::_ when bullet_eq bul b' -> true - | _::l -> has_bullet l - | [] -> false - in - has_bullet (get_bullets pr) - - (* 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 () , b - | _ -> assert false - - 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 = - 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 - 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; - suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf)) - - } - let _ = register_behavior strict - end - - (* Current bullet behavior, controlled by the option *) - let current_behavior = ref Strict.strict - - let _ = - Goptions.declare_string_option {Goptions. - optsync = true; - optdepr = false; - optname = "bullet behavior"; - optkey = ["Bullet";"Behavior"]; - optread = begin fun () -> - (!current_behavior).name - end; - optwrite = begin fun n -> - current_behavior := - try Hashtbl.find behaviors n - with Not_found -> - CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".") - end - } - - 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_range_selector (i, j) = - if i = j then string_of_int i - else string_of_int i ^ "-" ^ string_of_int j - -let print_goal_selector = function - | Vernacexpr.SelectAll -> "all" - | Vernacexpr.SelectNth i -> string_of_int i - | Vernacexpr.SelectList l -> "[" ^ - String.concat ", " (List.map print_range_selector l) ^ "]" - | Vernacexpr.SelectId id -> Id.to_string id - -let parse_goal_selector = function - | "all" -> Vernacexpr.SelectAll - | i -> - let err_msg = "The default selector must be \"all\" or a natural number." in - begin try - let i = int_of_string i in - if i < 0 then CErrors.error err_msg; - Vernacexpr.SelectNth i - with Failure _ -> CErrors.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 { pid; strength; proof } = cur_pstate () in @@ -707,12 +467,10 @@ module V82 = struct pid, (goals, strength) end -type state = pstate list - let freeze ~marshallable = match marshallable with | `Yes -> - CErrors.anomaly (Pp.str"full marshalling of proof state not supported") + CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") | `Shallow -> !pstates | `No -> !pstates let unfreeze s = pstates := s; update_proof_mode () @@ -727,3 +485,14 @@ let update_global_env () = 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 (p, ()))) + +(* XXX: Bullet hook, should be really moved elsewhere *) +let _ = + let hook n = + try + let prf = give_me_the_proof () in + (Proof_bullet.suggest prf) + with NoCurrentProof -> mt () + in + Proofview.set_nosuchgoals_hook hook + |