summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.mli1
-rw-r--r--proofs/clenvtac.mli1
-rw-r--r--proofs/goal.ml2
-rw-r--r--proofs/logic.ml12
-rw-r--r--proofs/pfedit.ml35
-rw-r--r--proofs/pfedit.mli8
-rw-r--r--proofs/proof.mli2
-rw-r--r--proofs/proof_global.ml32
-rw-r--r--proofs/proof_global.mli6
-rw-r--r--proofs/proof_type.ml1
-rw-r--r--proofs/proof_type.mli1
-rw-r--r--proofs/proofview.ml72
-rw-r--r--proofs/proofview.mli10
-rw-r--r--proofs/redexpr.ml2
14 files changed, 139 insertions, 46 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-27 10:30:36 +0000