From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- proofs/clenv.mli | 1 - proofs/clenvtac.mli | 1 - proofs/goal.ml | 2 -- proofs/logic.ml | 12 --------- proofs/pfedit.ml | 35 ++++++++++++++++++++++++ proofs/pfedit.mli | 8 ++++++ proofs/proof.mli | 2 +- proofs/proof_global.ml | 32 ++++++++++++++++------ proofs/proof_global.mli | 6 +++-- proofs/proof_type.ml | 1 - proofs/proof_type.mli | 1 - proofs/proofview.ml | 72 +++++++++++++++++++++++++++++++++++++++++-------- proofs/proofview.mli | 10 +++---- proofs/redexpr.ml | 2 +- 14 files changed, 139 insertions(+), 46 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 9b671bcf..eb108170 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -10,7 +10,6 @@ open Names open Term open Environ open Evd -open Mod_subst open Unification open Misctypes diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index da40427c..ea204361 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -8,7 +8,6 @@ open Term open Clenv -open Proof_type open Tacexpr open Unification diff --git a/proofs/goal.ml b/proofs/goal.ml index e3570242..107ce7f8 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -9,8 +9,6 @@ open Util open Pp open Term -open Vars -open Context (* This module implements the abstract interface to goals *) (* A general invariant of the module, is that a goal whose associated diff --git a/proofs/logic.ml b/proofs/logic.ml index 53f8093e..b8206ca1 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Environ open Reductionops @@ -83,12 +82,6 @@ let apply_to_hyp sign id f = if !check then error_no_such_hypothesis id else sign -let apply_to_hyp_and_dependent_on sign id f g = - try apply_to_hyp_and_dependent_on sign id f g - with Hyp_not_found -> - if !check then error_no_such_hypothesis id - else sign - let check_typability env sigma c = if !check then let _ = type_of env sigma c in () @@ -277,11 +270,6 @@ let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let rename_hyp id1 id2 sign = - apply_to_hyp_and_dependent_on sign id1 - (fun (_,b,t) _ -> (id2,b,t)) - (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) - (**********************************************************************) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index fdc93bcb..d1b6afe2 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -156,6 +156,41 @@ let build_by_tactic env ctx ?(poly=false) typ tac = assert(Univ.ContextSet.is_empty ctx); cb, status, univs +let refine_by_tactic env sigma ty tac = + (** Save the initial side-effects to restore them afterwards. We set the + current set of side-effects to be empty so that we can retrieve the + ones created during the tactic invocation easily. *) + let eff = Evd.eval_side_effects sigma in + let sigma = Evd.drop_side_effects sigma in + (** Start a proof *) + let prf = Proof.start sigma [env, ty] in + let (prf, _) = + try Proof.run_tactic env tac prf + with Logic_monad.TacticFailure e as src -> + (** Catch the inner error of the monad tactic *) + let (_, info) = Errors.push src in + iraise (e, info) + in + (** Plug back the retrieved sigma *) + let sigma = Proof.in_proof prf (fun sigma -> sigma) in + let ans = match Proof.initial_goals prf with + | [c, _] -> c + | _ -> assert false + in + let ans = Reductionops.nf_evar sigma 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 + (** 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 + those goals rely on effects that are not present anymore. Hopefully, + this hack will work in most cases. *) + let ans = Term_typing.handle_side_effects env ans neff in + ans, sigma + (**********************************************************************) (* Support for resolution of evars in tactic interpretation, including resolution by application of tactics *) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index edbc18a3..5e0fb4dd 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -157,6 +157,14 @@ val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context +val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic -> + constr * Evd.evar_map +(** A variant of the above function that handles open terms as well. + Caveat: all effects are purged in the returned term at the end, but other + evars solved by side-effects are NOT purged, so that unexpected failures may + occur. Ideally all code using this function should be rewritten in the + monad. *) + (** Declare the default tactic to fill implicit arguments *) val declare_implicit_tactic : unit Proofview.tactic -> unit diff --git a/proofs/proof.mli b/proofs/proof.mli index 4ae64ae6..2b85ec87 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -134,7 +134,7 @@ exception FullyUnfocused exception CannotUnfocusThisWay (* This is raised when trying to focus on non-existing subgoals. It is - handled by an error message but one may need to catched it and + handled by an error message but one may need to catch it and settle a better error message in some case (suggesting a better bullet for example), see proof_global.ml function Bullet.pop and Bullet.push. *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f55ab700..5bff3c81 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -74,7 +74,7 @@ type proof_object = { } type proof_ending = - | Admitted + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object @@ -295,7 +295,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = 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 + * complement 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 @@ -338,21 +338,37 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = 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 return_proof ?(allow_partial=false) () = + let { pid; proof; strength = (_,poly,_) } = cur_pstate () in + if allow_partial then begin + if Proof.is_done proof then begin + msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++ + str" is complete, no need to end it with Admitted"); + end; + let proofs = Proof.partial_proof proof in + let _,_,_,_, evd = Proof.proof proof in + let eff = Evd.eval_side_effects 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 -> 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 = raise (Errors.UserError("last tactic before Qed",s)) in + let error s = + let prf = str " (in proof " ++ Id.print pid ++ str ")" in + raise (Errors.UserError("last tactic before Qed",s ++ prf)) + 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") + error(strbrk"Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed.") | Proof.HasUnresolvedEvar-> - error(str"Attempt to save a proof with existential " ++ - str"variables still non-instantiated") in + error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in let evd = if poly || !Flags.compilation_mode = Flags.BuildVo diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 2700e901..9d5038a3 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -66,7 +66,7 @@ type proof_object = { } type proof_ending = - | Admitted + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object @@ -99,7 +99,9 @@ val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context -val return_proof : unit -> closed_proof_output +(* 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 -> unit -> closed_proof_output val close_future_proof : feedback_id:Stateid.t -> closed_proof_output Future.computation -> closed_proof diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 26bb78df..47b2b255 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -10,7 +10,6 @@ open Evd open Names open Term -open Context open Tacexpr open Glob_term open Nametab diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index e709be5b..f5e2bad2 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -9,7 +9,6 @@ open Evd open Names open Term -open Context open Tacexpr open Glob_term open Nametab diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a25683bf..6f626341 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -192,8 +192,8 @@ let unfocus c sp = succeed). Another benefit is that it is possible to write tactics that can be executed even if there are no focused goals. - Tactics form a monad ['a tactic], in a sense a tactic can be - seens as a function (without argument) which returns a value of - type 'a and modifies the environement (in our case: the view). + seen as a function (without argument) which returns a value of + type 'a and modifies the environment (in our case: the view). Tactics of course have arguments, but these are given at the meta-level as OCaml functions. Most tactics in the sense we are used to return [()], that is no really interesting values. But @@ -719,22 +719,72 @@ let give_up = (** {7 Control primitives} *) -(** Equality function on goals *) -let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in - Evd.eq_evar_info evars2 evi1 evi2 + +module Progress = struct + + (** equality function up to evar instantiation in heterogeneous + contexts. *) + (* spiwack (2015-02-19): In the previous version of progress an + equality which considers two universes equal when it is consistent + tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this + behaviour has to be restored as well. This has to be established by + practice. *) + + let rec eq_constr sigma1 sigma2 t1 t2 = + Constr.equal_with + (fun t -> Evarutil.kind_of_term_upto sigma1 t) + (fun t -> Evarutil.kind_of_term_upto sigma2 t) + t1 t2 + + (** equality function on hypothesis contexts *) + let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = + let open Environ in + let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in + let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = + Names.Id.equal i1 i2 && Option.equal (eq_constr sigma1 sigma2) c1 c2 + && (eq_constr sigma1 sigma2) t1 t2 + in List.equal eq_named_declaration c1 c2 + + let eq_evar_body sigma1 sigma2 b1 b2 = + let open Evd in + match b1, b2 with + | Evar_empty, Evar_empty -> true + | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2 + | _ -> false + + let eq_evar_info sigma1 sigma2 ei1 ei2 = + let open Evd in + eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl && + eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) && + eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body + + (** Equality function on goals *) + let goal_equal evars1 gl1 evars2 gl2 = + let evi1 = Evd.find evars1 gl1 in + let evi2 = Evd.find evars2 gl2 in + eq_evar_info evars1 evars2 evi1 evi2 + +end let tclPROGRESS t = let open Proof in Pv.get >>= fun initial -> t >>= fun res -> Pv.get >>= fun final -> + (* [*_test] test absence of progress. [quick_test] is approximate + whereas [exhaustive_test] is complete. *) + let quick_test = + initial.solution == final.solution && initial.comb == final.comb + in + let exhaustive_test = + Util.List.for_all2eq begin fun i f -> + Progress.goal_equal initial.solution i final.solution f + end initial.comb final.comb + in let test = - Evd.progress_evar_map initial.solution final.solution && - not (Util.List.for_all2eq (fun i f -> goal_equal initial.solution i final.solution f) initial.comb final.comb) + quick_test || exhaustive_test in - if test then + if not test then tclUNIT res else tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) @@ -1126,7 +1176,7 @@ module V82 = struct (* Returns the open goals of the proofview together with the evar_map to - interprete them. *) + interpret them. *) let goals { comb = comb ; solution = solution; } = { Evd.it = comb ; sigma = solution } diff --git a/proofs/proofview.mli b/proofs/proofview.mli index ec255f6a..5a9e7f39 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -37,7 +37,7 @@ type entry val compact : entry -> proofview -> entry * proofview (** Initialises a proofview, the main argument is a list of - environements (including a [named_context] which are used as + environments (including a [named_context] which are used as hypotheses) pair with conclusion types, creating accordingly many initial goals. Because a proof does not necessarily starts in an empty [evar_map] (indeed a proof can be triggered by an incomplete @@ -114,8 +114,8 @@ val unfocus : focus_context -> proofview -> proofview succeed). Another benefit is that it is possible to write tactics that can be executed even if there are no focused goals. - Tactics form a monad ['a tactic], in a sense a tactic can be - seens as a function (without argument) which returns a value of - type 'a and modifies the environement (in our case: the view). + seen as a function (without argument) which returns a value of + type 'a and modifies the environment (in our case: the view). Tactics of course have arguments, but these are given at the meta-level as OCaml functions. Most tactics in the sense we are used to return [()], that is no really interesting values. But @@ -230,7 +230,7 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic [i] to [j] (see {!focus}). The rest of the goals is restored after the tactic action. If the specified range doesn't correspond to existing goals, fails with [NoSuchGoals] (a user error). this - exception is catched at toplevel with a default message + a hook + exception is caught at toplevel with a default message + a hook message that can be customized by [set_nosuchgoals_hook] below. This hook is used to add a suggestion about bullets when applicable. *) @@ -547,7 +547,7 @@ module V82 : sig val grab : proofview -> proofview (* Returns the open goals of the proofview together with the evar_map to - interprete them. *) + interpret them. *) val goals : proofview -> Evar.t list Evd.sigma val top_goals : entry -> proofview -> Evar.t list Evd.sigma diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 18588867..1383d755 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -234,7 +234,7 @@ let reduction_of_red_expr env = with Not_found -> error("unknown user-defined reduction \""^s^"\""))) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) - | CbvNative o -> (contextualize cbv_native cbv_native o, VMcast) + | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) in reduction_of_red_expr -- cgit v1.2.3