aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacticals.ml')
-rw-r--r--tactics/tacticals.ml212
1 files changed, 115 insertions, 97 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 66da9ee18..90b7d6581 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -11,12 +11,15 @@ open CErrors
open Util
open Names
open Term
+open EConstr
open Termops
open Declarations
open Tacmach
open Clenv
+open Tactypes
open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
(************************************************************************)
(* Tacticals re-exported from the Refiner module *)
@@ -70,7 +73,7 @@ let nthDecl m gl =
try List.nth (pf_hyps gl) (m-1)
with Failure _ -> error "No such assumption."
-let nthHypId m gl = nthDecl m gl |> get_id
+let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id
let nthHyp m gl = mkVar (nthHypId m gl)
let lastDecl gl = nthDecl 1 gl
@@ -81,7 +84,7 @@ let nLastDecls n gl =
try List.firstn n (pf_hyps gl)
with Failure _ -> error "Not enough hypotheses in the goal."
-let nLastHypsId n gl = List.map get_id (nLastDecls n gl)
+let nLastHypsId n gl = List.map (NamedDecl.get_id) (nLastDecls n gl)
let nLastHyps n gl = List.map mkVar (nLastHypsId n gl)
let onNthDecl m tac gl = tac (nthDecl m gl) gl
@@ -99,7 +102,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac
let onNLastHyps n tac = onHyps (nLastHyps n) tac
let afterHyp id gl =
- fst (List.split_when (Id.equal id % get_id) (pf_hyps gl))
+ fst (List.split_when (NamedDecl.get_id %> Id.equal id) (pf_hyps gl))
(***************************************)
(* Clause Tacticals *)
@@ -151,11 +154,11 @@ type branch_args = {
nassums : int; (* number of assumptions/letin to be introduced *)
branchsign : bool list; (* the signature of the branch.
true=assumption, false=let-in *)
- branchnames : Tacexpr.intro_patterns}
+ branchnames : intro_patterns}
type branch_assumptions = {
ba : branch_args; (* the branch args *)
- assums : Context.Named.t} (* the list of assumptions introduced *)
+ assums : named_context} (* the list of assumptions introduced *)
open Misctypes
@@ -172,14 +175,14 @@ let check_or_and_pattern_size check_and loc names branchsigns =
let n = Array.length branchsigns in
let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in
let err1 p1 p2 =
- user_err_loc (loc,"",str "Expects " ++ msg p1 p2 ++ str ".") in
+ user_err ~loc (str "Expects " ++ msg p1 p2 ++ str ".") in
let errn n =
- user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n
+ user_err ~loc (str "Expects a disjunctive pattern with " ++ int n
++ str " branches.") in
let err1' p1 p2 =
- user_err_loc (loc,"",strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
+ user_err ~loc (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
let errforthcoming loc =
- user_err_loc (loc,"",strbrk "Unexpected non atomic pattern.") in
+ user_err ~loc (strbrk "Unexpected non atomic pattern.") in
match names with
| IntroAndPattern l ->
if not (Int.equal n 1) then errn n;
@@ -224,6 +227,7 @@ let compute_induction_names = compute_induction_names_gen true
(* Compute the let-in signature of case analysis or standard induction scheme *)
let compute_constructor_signatures isrec ((_,k as ity),u) =
+ let open Term in
let rec analrec c recargs =
match kind_of_term c, recargs with
| Prod (_,_,c), recarg::rest ->
@@ -261,40 +265,7 @@ let pf_with_evars glsev k gls =
tclTHEN (Refiner.tclEVARS evd) (k a) gls
let pf_constr_of_global gr k =
- pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k
-
-(* computing the case/elim combinators *)
-
-let gl_make_elim ind gl =
- let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
- pf_apply Evd.fresh_global gl gr
-
-let gl_make_case_dep ind gl =
- let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
- let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
- (elimination_sort_of_goal gl)
- in
- (Sigma.to_evar_map sigma, r)
-
-let gl_make_case_nodep ind gl =
- let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
- let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
- (elimination_sort_of_goal gl)
- in
- (Sigma.to_evar_map sigma, r)
-
-let make_elim_branch_assumptions ba gl =
- let assums =
- try List.rev (List.firstn ba.nassums (pf_hyps gl))
- with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
- { ba = ba; assums = assums }
-
-let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
-
-let make_case_branch_assumptions = make_elim_branch_assumptions
-
-let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
-
+ pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k
(** Tacticals of Ltac defined directly in term of Proofview *)
module New = struct
@@ -311,7 +282,7 @@ module New = struct
tclZERO (Refiner.FailError (lvl,lazy msg))
let tclZEROMSG ?loc msg =
- let err = UserError ("", msg) in
+ let err = UserError (None, msg) in
let info = match loc with
| None -> Exninfo.null
| Some loc -> Loc.add_loc Exninfo.null loc
@@ -366,6 +337,16 @@ module New = struct
catch_failerror e <*> t2
end
end
+
+ let tclORELSE0L t1 t2 =
+ tclINDEPENDENTL begin
+ tclORELSE
+ t1
+ begin fun e ->
+ catch_failerror e <*> t2
+ end
+ end
+
let tclORELSE t1 t2 =
tclORELSE0 (tclPROGRESS t1) t2
@@ -417,6 +398,9 @@ module New = struct
let tclTRY t =
tclORELSE0 t (tclUNIT ())
+
+ let tclTRYb t =
+ tclORELSE0L (t <*> tclUNIT true) (tclUNIT false)
let tclIFTHENELSE t1 t2 t3 =
tclINDEPENDENT begin
@@ -478,10 +462,10 @@ module New = struct
(* Select a subset of the goals *)
let tclSELECT = function
- | Tacexpr.SelectNth i -> Proofview.tclFOCUS i i
- | Tacexpr.SelectList l -> Proofview.tclFOCUSLIST l
- | Tacexpr.SelectId id -> Proofview.tclFOCUSID id
- | Tacexpr.SelectAll -> fun tac -> tac
+ | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
+ | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
+ | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
+ | Vernacexpr.SelectAll -> fun tac -> tac
(* Check that holes in arguments have been resolved *)
@@ -508,7 +492,7 @@ module New = struct
| [] -> ()
| (evk,evi) :: _ ->
let (loc,_) = evi.Evd.evar_source in
- Pretype_errors.error_unsolvable_implicit loc env sigma evk None
+ Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None
let tclWITHHOLES accept_unresolved_holes tac sigma =
tclEVARMAP >>= fun sigma_initial ->
@@ -529,10 +513,10 @@ module New = struct
Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
let tclDELAYEDWITHHOLES check x tac =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let Sigma (x, sigma, _) = x.Tacexpr.delayed env sigma in
+ let Sigma (x, sigma, _) = x.delayed env sigma in
tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma)
end }
@@ -560,7 +544,7 @@ module New = struct
let nthHypId m gl =
(** We only use [id] *)
let gl = Proofview.Goal.assume gl in
- nthDecl m gl |> get_id
+ nthDecl m gl |> NamedDecl.get_id
let nthHyp m gl =
mkVar (nthHypId m gl)
@@ -573,13 +557,13 @@ module New = struct
let onLastHyp = onNthHyp 1
let onNthDecl m tac =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
Proofview.tclUNIT (nthDecl m gl) >>= tac
end }
let onLastDecl = onNthDecl 1
let ifOnHyp pred tac1 tac2 id =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let typ = Tacmach.New.pf_get_hyp_typ id gl in
if pred (id,typ) then
tac1 id
@@ -587,12 +571,12 @@ module New = struct
tac2 id
end }
- let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end }
+ let onHyps find tac = Proofview.Goal.enter { enter = begin fun gl -> tac (find.enter gl) end }
let afterHyp id tac =
Proofview.Goal.enter { enter = begin fun gl ->
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
- let rem, _ = List.split_when (Id.equal id % get_id) hyps in
+ let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in
tac rem
end }
@@ -620,30 +604,31 @@ module New = struct
(* c should be of type A1->.. An->B with B an inductive definition *)
let general_elim_then_using mk_elim
isrec allnames tac predicate ind (c, t) =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let sigma, elim = (mk_elim ind).enter gl in
+ let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Proofview.Goal.nf_enter { enter = begin fun gl ->
- let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
+ (Proofview.Goal.enter { enter = begin fun gl ->
+ let indclause = mk_clenv_from gl (c, t) in
(* applying elimination_scheme just a little modified *)
- let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
+ let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim) in
let indmv =
- match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
+ match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
| Meta mv -> mv
| _ -> anomaly (str"elimination")
in
let pmv =
- let p, _ = decompose_app elimclause.templtyp.Evd.rebus in
- match kind_of_term p with
+ let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in
+ match EConstr.kind elimclause.evd p with
| Meta p -> p
| _ ->
let name_elim =
- match kind_of_term elim with
+ match EConstr.kind sigma elim with
| Const (kn, _) -> string_of_con kn
| Var id -> string_of_id id
| _ -> "\b"
in
- errorlabstrm "Tacticals.general_elim_then_using"
+ user_err ~hdr:"Tacticals.general_elim_then_using"
(str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
in
let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
@@ -655,9 +640,9 @@ module New = struct
| None -> elimclause'
| Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
in
- let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in
+ let clenv' = clenv_unique_resolver ~flags elimclause' gl in
let after_tac i =
- let (hd,largs) = decompose_app clenv'.templtyp.Evd.rebus in
+ let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in
let ba = { branchsign = branchsigns.(i);
branchnames = brnames.(i);
nassums = List.length branchsigns.(i);
@@ -674,8 +659,66 @@ module New = struct
(Proofview.tclEXTEND [] tclIDTAC branchtacs)
end }) end }
+ let elimination_sort_of_goal gl =
+ (** Retyping will expand evars anyway. *)
+ let c = Proofview.Goal.concl (Goal.assume gl) in
+ pf_apply Retyping.get_sort_family_of gl c
+
+ let elimination_sort_of_hyp id gl =
+ (** Retyping will expand evars anyway. *)
+ let c = pf_get_hyp_typ id (Goal.assume gl) in
+ pf_apply Retyping.get_sort_family_of gl c
+
+ let elimination_sort_of_clause id gl = match id with
+ | None -> elimination_sort_of_goal gl
+ | Some id -> elimination_sort_of_hyp id gl
+
+ (* computing the case/elim combinators *)
+
+ let gl_make_elim ind = { enter = begin fun gl ->
+ let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
+ let (sigma, c) = pf_apply Evd.fresh_global gl gr in
+ (sigma, EConstr.of_constr c)
+ end }
+
+ let gl_make_case_dep (ind, u) = { enter = begin fun gl ->
+ let sigma = Sigma.Unsafe.of_evar_map (project gl) in
+ let u = EInstance.kind (project gl) u in
+ let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true
+ (elimination_sort_of_goal gl)
+ in
+ (Sigma.to_evar_map sigma, EConstr.of_constr r)
+ end }
+
+ let gl_make_case_nodep (ind, u) = { enter = begin fun gl ->
+ let sigma = Sigma.Unsafe.of_evar_map (project gl) in
+ let u = EInstance.kind (project gl) u in
+ let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false
+ (elimination_sort_of_goal gl)
+ in
+ (Sigma.to_evar_map sigma, EConstr.of_constr r)
+ end }
+
+ let make_elim_branch_assumptions ba hyps =
+ let assums =
+ try List.rev (List.firstn ba.nassums hyps)
+ with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
+ { ba = ba; assums = assums }
+
+ let elim_on_ba tac ba =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+ tac branches
+ end }
+
+ let case_on_ba tac ba =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+ tac branches
+ end }
+
let elimination_then tac c =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
let isrec,mkelim =
match (Global.lookup_mind (fst (fst ind))).mind_record with
@@ -691,37 +734,12 @@ module New = struct
let case_nodep_then_using =
general_elim_then_using gl_make_case_nodep false
- let elim_on_ba tac ba =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in
- tac branches
- end }
-
- let case_on_ba tac ba =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in
- tac branches
- end }
-
- let elimination_sort_of_goal gl =
- (** Retyping will expand evars anyway. *)
- let c = Proofview.Goal.concl (Goal.assume gl) in
- pf_apply Retyping.get_sort_family_of gl c
-
- let elimination_sort_of_hyp id gl =
- (** Retyping will expand evars anyway. *)
- let c = pf_get_hyp_typ id (Goal.assume gl) in
- pf_apply Retyping.get_sort_family_of gl c
-
- let elimination_sort_of_clause id gl = match id with
- | None -> elimination_sort_of_goal gl
- | Some id -> elimination_sort_of_hyp id gl
-
let pf_constr_of_global ref tac =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let (sigma, c) = Evd.fresh_global env sigma ref in
+ let c = EConstr.of_constr c in
Proofview.Unsafe.tclEVARS sigma <*> (tac c)
end }
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-18 14:04:39 +0000