aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/goal.ml3
-rw-r--r--proofs/goal.mli3
-rw-r--r--proofs/proofview.ml11
-rw-r--r--proofs/proofview.mli4
-rw-r--r--tactics/tacinterp.ml248
5 files changed, 142 insertions, 127 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml
index e590e7763..46f002cb3 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -352,6 +352,9 @@ let env env _ _ _ = env
let defs _ rdefs _ _ =
!rdefs
+let enter f = (); fun env rdefs _ info ->
+ f env !rdefs (Evd.evar_hyps info) (Evd.evar_concl info)
+
(*** Conversion in goals ***)
let convert_hyp check (id,b,bt as d) env rdefs gl info =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 216e12f3a..6a19e0d69 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -147,6 +147,9 @@ val env : Environ.env sensitive
(* [defs] is the [Evd.evar_map] at the current evaluation point *)
val defs : Evd.evar_map sensitive
+(* [enter] combines [env], [defs], [hyps] and [concl] in a single
+ primitive. *)
+val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> 'a) -> 'a sensitive
(*** Additional functions ***)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index fb8796dbd..dace158ac 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -691,8 +691,19 @@ module Goal = struct
let concl = lift Goal.concl
let hyps = lift Goal.hyps
let env = lift Goal.env
+
+ let enter f =
+ lift (Goal.enter f) >= fun ts ->
+ tclDISPATCH ts
+ let enterl f =
+ lift (Goal.enter f) >= fun ts ->
+ tclDISPATCHL ts >= fun res ->
+ tclUNIT (List.flatten res)
+
end
module NonLogical = Proofview_monad.NonLogical
let tclLIFT = Proofview_monad.Logical.lift
+
+
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 3f80768d8..fa1a8d56f 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -290,7 +290,9 @@ module Goal : sig
(* [lift (Goal.return x)] *)
val return : 'a -> 'a glist tactic
- (* [lift Goal.concl] *)
+ val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> unit tactic) -> unit tactic
+ val enterl : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> 'a glist tactic) -> 'a glist tactic
+ (* [lift Goal.concl] *)
val concl : Term.constr glist tactic
(* [lift Goal.hyps] *)
val hyps : Environ.named_context_val glist tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index aec8e27f8..0e54ed84c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1341,11 +1341,9 @@ and interp_letin ist llc u =
(* Interprets the Match Context expressions *)
and interp_match_goal ist lz lr lmr =
- Proofview.Goal.hyps >>== fun hyps ->
+ Proofview.Goal.enterl begin fun env sigma hyps concl ->
let hyps = Environ.named_context_of_val hyps in
let hyps = if lr then List.rev hyps else hyps in
- Proofview.Goal.concl >>== fun concl ->
- Proofview.Goal.env >>== fun env ->
let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps =
let rec match_next_pattern next = match IStream.peek next with
| None -> Proofview.tclZERO PatternMatchingFailure
@@ -1421,10 +1419,10 @@ and interp_match_goal ist lz lr lmr =
else mt()) ++ str"."))
))
end in
- Proofview.tclEVARMAP >= fun sigma ->
apply_match_goal ist env 0 lmr
(read_match_rule (extract_ltac_constr_values ist env)
ist env sigma lmr)
+ end
(* Tries to match the hypotheses in a Match Context *)
and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
@@ -1635,19 +1633,19 @@ and interp_match ist lz constr lmr =
Proofview.tclZERO e
end
end >>== fun csr ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>== fun env ->
- let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
- Proofview.tclORELSE
- (apply_match ist csr ilr)
- begin function
- | e ->
- Proofview.tclLIFT (debugging_exception_step ist true e (fun () -> str "match expression")) <*>
- Proofview.tclZERO e
- end >>== fun res ->
- Proofview.tclLIFT (debugging_step ist (fun () ->
- str "match expression returns " ++ pr_value (Some env) res)) <*>
- (Proofview.Goal.return res)
+ Proofview.Goal.enterl begin fun env sigma _ _ ->
+ let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
+ Proofview.tclORELSE
+ (apply_match ist csr ilr)
+ begin function
+ | e ->
+ Proofview.tclLIFT (debugging_exception_step ist true e (fun () -> str "match expression")) <*>
+ Proofview.tclZERO e
+ end >>== fun res ->
+ Proofview.tclLIFT (debugging_step ist (fun () ->
+ str "match expression returns " ++ pr_value (Some env) res)) <*>
+ (Proofview.Goal.return res)
+ end
(* Interprets tactic expressions : returns a "constr" *)
and interp_ltac_constr ist e =
@@ -1730,28 +1728,26 @@ and interp_atomic ist tac =
gl
end
| TacApply (a,ev,cb,cl) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- begin try (* interp_open_constr_with_bindings_loc can raise exceptions *)
- let sigma, l =
- List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
- in
- let tac = match cl with
- | None -> fun l -> Proofview.V82.tactic (h_apply a ev l)
- | Some cl ->
- (fun l ->
- Tacmach.New.of_old (fun gl -> interp_in_hyp_as ist gl cl) >>= fun cl ->
- h_apply_in a ev l cl) in
- Tacticals.New.tclWITHHOLES ev tac sigma l
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ try (* interp_open_constr_with_bindings_loc can raise exceptions *)
+ let sigma, l =
+ List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
+ in
+ let tac = match cl with
+ | None -> fun l -> Proofview.V82.tactic (h_apply a ev l)
+ | Some cl ->
+ (fun l ->
+ Tacmach.New.of_old (fun gl -> interp_in_hyp_as ist gl cl) >>= fun cl ->
+ h_apply_in a ev l cl) in
+ Tacticals.New.tclWITHHOLES ev tac sigma l
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
| TacElim (ev,cb,cbo) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- begin try (* interpretation functions may raise exceptions *)
- let sigma, cb = interp_constr_with_bindings ist env sigma cb in
- let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
- Tacticals.New.tclWITHHOLES ev (h_elim ev cb) sigma cbo
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ try (* interpretation functions may raise exceptions *)
+ let sigma, cb = interp_constr_with_bindings ist env sigma cb in
+ let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
+ Tacticals.New.tclWITHHOLES ev (h_elim ev cb) sigma cbo
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
| TacElimType c ->
@@ -1763,10 +1759,10 @@ and interp_atomic ist tac =
gl
end
| TacCase (ev,cb) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- let sigma, cb = interp_constr_with_bindings ist env sigma cb in
- Tacticals.New.tclWITHHOLES ev (h_case ev) sigma cb
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ let sigma, cb = interp_constr_with_bindings ist env sigma cb in
+ Tacticals.New.tclWITHHOLES ev (h_case ev) sigma cb
+ end
| TacCaseType c ->
Proofview.V82.tactic begin fun gl ->
let (sigma,c_interp) = pf_interp_type ist gl c in
@@ -1824,23 +1820,22 @@ and interp_atomic ist tac =
gl
end
| TacAssert (t,ipat,c) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- begin try (* intrerpreation function may raise exceptions *)
- let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in
- Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>= fun patt ->
- Tacticals.New.tclTHEN
- (Proofview.V82.tclEVARS sigma)
- (Tactics.forward (Option.map (interp_tactic ist) t)
- (Option.map patt ipat) c)
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ try (* intrerpreation function may raise exceptions *)
+ let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in
+ Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>= fun patt ->
+ Tacticals.New.tclTHEN
+ (Proofview.V82.tclEVARS sigma)
+ (Tactics.forward (Option.map (interp_tactic ist) t)
+ (Option.map patt ipat) c)
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
| TacGeneralize cl ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- Proofview.V82.tactic begin fun gl ->
- let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
- tclWITHHOLES false (h_generalize_gen) sigma cl gl
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.V82.tactic begin fun gl ->
+ let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
+ tclWITHHOLES false (h_generalize_gen) sigma cl gl
+ end
end
| TacGeneralizeDep c ->
Proofview.V82.tactic begin fun gl ->
@@ -1851,36 +1846,37 @@ and interp_atomic ist tac =
gl
end
| TacLetTac (na,c,clp,b,eqpat) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) >>= fun clp ->Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) >>= fun eqpat ->
- if Locusops.is_nowhere clp then
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) >>= fun clp ->
+ Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) >>= fun eqpat ->
+ if Locusops.is_nowhere clp then
(* We try to fully-typecheck the term *)
- Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
+ Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
Tacticals.New.tclTHEN
(Proofview.V82.tclEVARS sigma)
(h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
- else
+ else
(* We try to keep the pattern structure as much as possible *)
- begin try
- h_let_pat_tac b (interp_fresh_name ist env na)
- (interp_pure_open_constr ist env sigma c) clp eqpat
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
- end
+ begin try
+ h_let_pat_tac b (interp_fresh_name ist env na)
+ (interp_pure_open_constr ist env sigma c) clp eqpat
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
+ end
(* Automation tactics *)
| TacTrivial (debug,lems,l) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- Auto.h_trivial ~debug
- (interp_auto_lemmas ist env sigma lems)
- (Option.map (List.map (interp_hint_base ist)) l)
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ Auto.h_trivial ~debug
+ (interp_auto_lemmas ist env sigma lems)
+ (Option.map (List.map (interp_hint_base ist)) l)
+ end
| TacAuto (debug,n,lems,l) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
- (interp_auto_lemmas ist env sigma lems)
- (Option.map (List.map (interp_hint_base ist)) l)
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
+ (interp_auto_lemmas ist env sigma lems)
+ (Option.map (List.map (interp_hint_base ist)) l)
+ end
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
@@ -1926,11 +1922,11 @@ and interp_atomic ist tac =
(Proofview.V82.tclEVARS sigma)
(Elim.h_decompose l c_interp)
| TacSpecialize (n,cb) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- Proofview.V82.tactic begin fun gl ->
- let sigma, cb = interp_constr_with_bindings ist env sigma cb in
- tclWITHHOLES false (h_specialize n) sigma cb gl
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.V82.tactic begin fun gl ->
+ let sigma, cb = interp_constr_with_bindings ist env sigma cb in
+ tclWITHHOLES false (h_specialize n) sigma cb gl
+ end
end
| TacLApply c ->
Proofview.V82.tactic begin fun gl ->
@@ -1969,27 +1965,27 @@ and interp_atomic ist tac =
(* Constructors *)
| TacLeft (ev,bl) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- let sigma, bl = interp_bindings ist env sigma bl in
- Tacticals.New.tclWITHHOLES ev (h_left ev) sigma bl
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ let sigma, bl = interp_bindings ist env sigma bl in
+ Tacticals.New.tclWITHHOLES ev (h_left ev) sigma bl
+ end
| TacRight (ev,bl) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- let sigma, bl = interp_bindings ist env sigma bl in
- Tacticals.New.tclWITHHOLES ev (h_right ev) sigma bl
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ let sigma, bl = interp_bindings ist env sigma bl in
+ Tacticals.New.tclWITHHOLES ev (h_right ev) sigma bl
+ end
| TacSplit (ev,_,bll) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
- Tacticals.New.tclWITHHOLES ev (h_split ev) sigma bll
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
+ Tacticals.New.tclWITHHOLES ev (h_split ev) sigma bll
+ end
| TacAnyConstructor (ev,t) ->
Tactics.any_constructor ev (Option.map (interp_tactic ist) t)
| TacConstructor (ev,n,bl) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- let sigma, bl = interp_bindings ist env sigma bl in
- Tacticals.New.tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ let sigma, bl = interp_bindings ist env sigma bl in
+ Tacticals.New.tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl
+ end
(* Conversion *)
| TacReduce (r,cl) ->
@@ -2021,24 +2017,24 @@ and interp_atomic ist tac =
gl
end
| TacChange (Some op,c,cl) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- Proofview.V82.tactic begin fun gl ->
- let sign,op = interp_typed_pattern ist env sigma op in
- (* spiwack: (2012/04/18) the evar_map output by pf_interp_constr
- is dropped as the evar_map taken as input (from
- extend_gl_hyps) is incorrect. This means that evar
- instantiated by pf_interp_constr may be lost, there. *)
- let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
- let (_,c_interp) =
- try pf_interp_constr ist (extend_gl_hyps gl sign) c
- with e when to_catch e (* Hack *) ->
- errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
- in
- tclTHEN
- (tclEVARS sigma)
- (h_change (Some op) c_interp (interp_clause ist { gl with sigma=sigma } cl))
- gl
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.V82.tactic begin fun gl ->
+ let sign,op = interp_typed_pattern ist env sigma op in
+ (* spiwack: (2012/04/18) the evar_map output by pf_interp_constr
+ is dropped as the evar_map taken as input (from
+ extend_gl_hyps) is incorrect. This means that evar
+ instantiated by pf_interp_constr may be lost, there. *)
+ let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
+ let (_,c_interp) =
+ try pf_interp_constr ist (extend_gl_hyps gl sign) c
+ with e when to_catch e (* Hack *) ->
+ errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+ in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_change (Some op) c_interp (interp_clause ist { gl with sigma=sigma } cl))
+ gl
+ end
end
(* Equivalence relations *)
@@ -2213,8 +2209,7 @@ let eval_tactic t =
let interp_tac_gen lfun avoid_ids debug t =
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
+ Proofview.Goal.enter begin fun env sigma _ _ ->
let extra = TacStore.set TacStore.empty f_debug debug in
let extra = TacStore.set extra f_avoid_ids avoid_ids in
let ist = { lfun = lfun; extra = extra } in
@@ -2223,6 +2218,7 @@ let interp_tac_gen lfun avoid_ids debug t =
(intern_pure_tactic {
ltacvars; ltacrecvars = Id.Map.empty;
gsigma = sigma; genv = env } t)
+ end
let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
let _ = Proof_global.set_interp_tac interp
@@ -2234,15 +2230,15 @@ let eval_ltac_constr t =
(* Used to hide interpretation for pretty-print, now just launch tactics *)
let hide_interp t ot =
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
- gsigma = sigma; genv = env } in
- let te = intern_pure_tactic ist t in
- let t = eval_tactic te in
- match ot with
- | None -> t
- | Some t' -> Tacticals.New.tclTHEN t t'
+ Proofview.Goal.enter begin fun env sigma _ _ ->
+ let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
+ gsigma = sigma; genv = env } in
+ let te = intern_pure_tactic ist t in
+ let t = eval_tactic te in
+ match ot with
+ | None -> t
+ | Some t' -> Tacticals.New.tclTHEN t t'
+ end
(***************************************************************************)
(** Register standard arguments *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 18:20:30 +0000