diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 117 |
1 files changed, 54 insertions, 63 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index eddbf72a..5d137988 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.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) *) (************************************************************************) open Pp @@ -15,7 +17,7 @@ open Evd let use_unification_heuristics_ref = ref true let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Solve unification constraints at every \".\""; Goptions.optkey = ["Solve";"Unification";"Constraints"]; Goptions.optread = (fun () -> !use_unification_heuristics_ref); @@ -24,19 +26,6 @@ let _ = Goptions.declare_bool_option { let use_unification_heuristics () = !use_unification_heuristics_ref -let refining = Proof_global.there_are_pending_proofs -let check_no_pending_proofs = Proof_global.check_no_pending_proof - -let get_current_proof_name = Proof_global.get_current_proof_name -let get_all_proof_names = Proof_global.get_all_proof_names - -type lemma_possible_guards = Proof_global.lemma_possible_guards -type universe_binders = Proof_global.universe_binders - -let delete_proof = Proof_global.discard -let delete_current_proof = Proof_global.discard_current -let delete_all_proofs = Proof_global.discard_all - let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator = let goals = [ (Global.env_of_context hyps , c) ] in Proof_global.start_proof sigma id ?pl str goals terminator; @@ -55,44 +44,31 @@ let cook_this_proof p = let cook_proof () = cook_this_proof (fst (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x))) -let get_pftreestate () = - Proof_global.give_me_the_proof () - -let set_end_tac tac = - Proof_global.set_endline_tactic tac - -let set_used_variables l = - Proof_global.set_used_variables l -let get_used_variables () = - Proof_global.get_used_variables () - -let get_universe_binders () = - Proof_global.get_universe_binders () exception NoSuchGoal let _ = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.error "No such goal." + | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end + let get_nth_V82_goal i = let p = Proof_global.give_me_the_proof () in - let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in - try - { it=(List.nth goals (i-1)) ; sigma=sigma; } + let goals,_,_,_,sigma = Proof.proof p in + try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal - + let get_goal_context_gen i = let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context i = try get_goal_context_gen i - with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." - | NoSuchGoal -> CErrors.error "No such goal." + with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") + | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") let get_current_goal_context () = try get_goal_context_gen 1 - with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." + with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, there is no accessible evar either *) @@ -106,14 +82,14 @@ let get_current_context () = (Evd.from_env env, env) | NoSuchGoal -> (* No more focused goals ? *) - let p = get_pftreestate () in + let p = Proof_global.give_me_the_proof () in let evd = Proof.in_proof p (fun x -> x) in (evd, Global.env ()) let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with | (id,([concl],strength)) -> id,strength,concl - | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") + | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.") let solve ?with_end_tac gi info_lvl tac pr = try @@ -143,12 +119,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) with - | Proof_global.NoCurrentProof -> CErrors.error "No focused proof" - | CList.IndexOutOfRange -> - match gi with - | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in - CErrors.errorlabstrm "" msg - | _ -> assert false + Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof") let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) @@ -170,11 +141,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo try let status = by tac in let _,(const,univs,_) = cook_proof () in - delete_current_proof (); - const, status, fst univs + Proof_global.discard_current (); + let univs = UState.demote_seff_univs const univs in + const, status, univs with reraise -> let reraise = CErrors.push reraise in - delete_current_proof (); + Proof_global.discard_current (); iraise reraise let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = @@ -186,12 +158,11 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with - const_entry_body = Future.chain ~pure:true ce.const_entry_body - (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in - let (cb, ctx), se = Future.force ce.const_entry_body in - let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - assert(Safe_typing.empty_private_constants = se); - cb, status, Evd.evar_universe_context univs' + const_entry_body = Future.chain ce.const_entry_body + (fun (pt, _) -> pt, ()) } in + let (cb, ctx), () = Future.force ce.const_entry_body in + let univs = UState.merge side_eff Evd.univ_rigid univs ctx in + cb, status, univs let refine_by_tactic env sigma ty tac = (** Save the initial side-effects to restore them afterwards. We set the @@ -199,6 +170,8 @@ let refine_by_tactic env sigma ty tac = ones created during the tactic invocation easily. *) let eff = Evd.eval_side_effects sigma in let sigma = Evd.drop_side_effects sigma in + (** Save the existing goals *) + let prev_future_goals = save_future_goals sigma in (** Start a proof *) let prf = Proof.start sigma [env, ty] in let (prf, _) = @@ -209,17 +182,30 @@ let refine_by_tactic env sigma ty tac = iraise (e, info) in (** Plug back the retrieved sigma *) - let sigma = Proof.in_proof prf (fun sigma -> sigma) in + let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in + assert (stack = []); let ans = match Proof.initial_goals prf with | [c, _] -> c | _ -> assert false in let ans = Reductionops.nf_evar sigma ans in + let ans = EConstr.Unsafe.to_constr ans in (** [neff] contains the freshly generated side-effects *) let neff = Evd.eval_side_effects sigma in (** Reset the old side-effects *) let sigma = Evd.drop_side_effects sigma in let sigma = Evd.emit_side_effects eff sigma in + (** Restore former goals *) + let sigma = restore_future_goals sigma prev_future_goals in + (** Push remaining goals as future_goals which is the only way we + have to inform the caller that there are goals to collect while + not being encapsulated in the monad *) + (** Goals produced by tactic "shelve" *) + let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in + (** Goals produced by tactic "give_up" *) + let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in + (** Other goals *) + let sigma = List.fold_right Evd.declare_future_goal goals sigma in (** Get rid of the fresh side-effects by internalizing them in the term itself. Note that this is unsound, because the tactic may have solved other goals that were already present during its invocation, so that @@ -238,20 +224,25 @@ let declare_implicit_tactic tac = implicit_tactic := Some tac let clear_implicit_tactic () = implicit_tactic := None -let solve_by_implicit_tactic env sigma evk = +let apply_implicit_tactic tac = (); fun env sigma evk -> let evi = Evd.find_undefined sigma evk in - match (!implicit_tactic, snd (evar_source evk sigma)) with - | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) + match snd (evar_source evk sigma) with + | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) + Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> - let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in + let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in (try let c = Evarutil.nf_evars_universes sigma evi.evar_concl in + let c = EConstr.of_constr c in if Evarutil.has_undefined_evars sigma c then raise Exit; let (ans, _, ctx) = build_by_tactic env (Evd.evar_universe_context sigma) c tac in let sigma = Evd.set_universe_context sigma ctx in - sigma, ans + sigma, EConstr.of_constr ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit + +let solve_by_implicit_tactic () = match !implicit_tactic with +| None -> None +| Some tac -> Some (apply_implicit_tactic tac) |