summaryrefslogtreecommitdiff
path: root/tactics/tacticals.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacticals.ml')
-rw-r--r--tactics/tacticals.ml257
1 files changed, 140 insertions, 117 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f5922411..66da9ee1 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -7,15 +7,16 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
open Termops
-open Context
open Declarations
open Tacmach
open Clenv
+open Sigma.Notations
+open Context.Named.Declaration
(************************************************************************)
(* Tacticals re-exported from the Refiner module *)
@@ -69,7 +70,7 @@ let nthDecl m gl =
try List.nth (pf_hyps gl) (m-1)
with Failure _ -> error "No such assumption."
-let nthHypId m gl = pi1 (nthDecl m gl)
+let nthHypId m gl = nthDecl m gl |> get_id
let nthHyp m gl = mkVar (nthHypId m gl)
let lastDecl gl = nthDecl 1 gl
@@ -80,7 +81,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 pi1 (nLastDecls n gl)
+let nLastHypsId n gl = List.map 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
@@ -98,7 +99,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 (fun (hyp,_,_) -> Id.equal hyp id) (pf_hyps gl))
+ fst (List.split_when (Id.equal id % get_id) (pf_hyps gl))
(***************************************)
(* Clause Tacticals *)
@@ -147,14 +148,16 @@ type branch_args = {
largs : constr list; (* its arguments *)
branchnum : int; (* the branch number *)
pred : constr; (* the predicate we used *)
- nassums : int; (* the number of assumptions to be introduced *)
+ nassums : int; (* number of assumptions/letin to be introduced *)
branchsign : bool list; (* the signature of the branch.
- true=recursive argument, false=constant *)
+ true=assumption, false=let-in *)
branchnames : Tacexpr.intro_patterns}
type branch_assumptions = {
- ba : branch_args; (* the branch args *)
- assums : named_context} (* the list of assumptions introduced *)
+ ba : branch_args; (* the branch args *)
+ assums : Context.Named.t} (* the list of assumptions introduced *)
+
+open Misctypes
let fix_empty_or_and_pattern nv l =
(* 1- The syntax does not distinguish between "[ ]" for one clause with no
@@ -162,36 +165,78 @@ let fix_empty_or_and_pattern nv l =
(* 2- More generally, we admit "[ ]" for any disjunctive pattern of
arbitrary length *)
match l with
- | [[]] -> List.make nv []
+ | IntroOrPattern [[]] -> IntroOrPattern (List.make nv [])
| _ -> l
-let check_or_and_pattern_size loc names n =
- if not (Int.equal (List.length names) n) then
- if Int.equal n 1 then
- user_err_loc (loc,"",str "Expects a conjunctive pattern.")
- else
- user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n
- ++ str " branches.")
-
-let compute_induction_names n = function
+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
+ let errn n =
+ user_err_loc (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
+ let errforthcoming loc =
+ user_err_loc (loc,"",strbrk "Unexpected non atomic pattern.") in
+ match names with
+ | IntroAndPattern l ->
+ if not (Int.equal n 1) then errn n;
+ let l' = List.filter (function _,IntroForthcoming _ -> true | _,IntroNaming _ | _,IntroAction _ -> false) l in
+ if l' != [] then errforthcoming (fst (List.hd l'));
+ if check_and then
+ let p1 = List.count (fun x -> x) branchsigns.(0) in
+ let p2 = List.length branchsigns.(0) in
+ let p = List.length l in
+ if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2;
+ if Int.equal p p1 then
+ IntroAndPattern
+ (List.extend branchsigns.(0) (Loc.ghost,IntroNaming IntroAnonymous) l)
+ else
+ names
+ else
+ names
+ | IntroOrPattern ll ->
+ if not (Int.equal n (List.length ll)) then
+ if Int.equal n 1 then
+ let p1 = List.count (fun x -> x) branchsigns.(0) in
+ let p2 = List.length branchsigns.(0) in
+ err1' p1 p2 else errn n;
+ names
+
+let get_and_check_or_and_pattern_gen check_and loc names branchsigns =
+ let names = check_or_and_pattern_size check_and loc names branchsigns in
+ match names with
+ | IntroAndPattern l -> [|l|]
+ | IntroOrPattern l -> Array.of_list l
+
+let get_and_check_or_and_pattern = get_and_check_or_and_pattern_gen true
+
+let compute_induction_names_gen check_and branchletsigns = function
| None ->
- Array.make n []
+ Array.make (Array.length branchletsigns) []
| Some (loc,names) ->
- let names = fix_empty_or_and_pattern n names in
- check_or_and_pattern_size loc names n;
- Array.of_list names
+ let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in
+ get_and_check_or_and_pattern_gen check_and loc names branchletsigns
-let compute_construtor_signatures isrec ((_,k as ity),u) =
+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 rec analrec c recargs =
match kind_of_term c, recargs with
| Prod (_,_,c), recarg::rest ->
- let b = match Declareops.dest_recarg recarg with
- | Norec | Imbr _ -> false
- | Mrec (_,j) -> isrec && Int.equal j k
- in b :: (analrec c rest)
- | LetIn (_,_,_,c), rest -> false :: (analrec c rest)
+ let rest = analrec c rest in
+ begin match Declareops.dest_recarg recarg with
+ | Norec | Imbr _ -> true :: rest
+ | Mrec (_,j) ->
+ if isrec && Int.equal j k then true :: true :: rest
+ else true :: rest
+ end
+ | LetIn (_,_,_,c), rest -> false :: analrec c rest
| _, [] -> []
- | _ -> anomaly (Pp.str "compute_construtor_signatures")
+ | _ -> anomaly (Pp.str "compute_constructor_signatures")
in
let (mib,mip) = Global.lookup_inductive ity in
let n = mib.mind_nparams in
@@ -225,60 +270,28 @@ let gl_make_elim ind gl =
pf_apply Evd.fresh_global gl gr
let gl_make_case_dep ind gl =
- pf_apply Indrec.build_case_analysis_scheme gl ind true
+ 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 =
- pf_apply Indrec.build_case_analysis_scheme gl ind false
+ 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 rec makerec (assums,cargs,constargs,recargs,indargs) lb lc =
- match lb,lc with
- | ([], _) ->
- { ba = ba;
- assums = assums}
- | ((true::tl), ((idrec,_,_ as recarg)::(idind,_,_ as indarg)::idtl)) ->
- makerec (recarg::indarg::assums,
- idrec::cargs,
- idrec::recargs,
- constargs,
- idind::indargs) tl idtl
- | ((false::tl), ((id,_,_ as constarg)::idtl)) ->
- makerec (constarg::assums,
- id::cargs,
- id::constargs,
- recargs,
- indargs) tl idtl
- | (_, _) -> anomaly (Pp.str "make_elim_branch_assumptions")
- in
- makerec ([],[],[],[],[]) ba.branchsign
- (try List.firstn ba.nassums (pf_hyps gl)
- with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions"))
+ 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 ba gl =
- let rec makerec (assums,cargs,constargs,recargs) p_0 p_1 =
- match p_0,p_1 with
- | ([], _) ->
- { ba = ba;
- assums = assums}
- | ((true::tl), ((idrec,_,_ as recarg)::idtl)) ->
- makerec (recarg::assums,
- idrec::cargs,
- idrec::recargs,
- constargs) tl idtl
- | ((false::tl), ((id,_,_ as constarg)::idtl)) ->
- makerec (constarg::assums,
- id::cargs,
- recargs,
- id::constargs) tl idtl
- | (_, _) -> anomaly (Pp.str "make_case_branch_assumptions")
- in
- makerec ([],[],[],[]) ba.branchsign
- (try List.firstn ba.nassums (pf_hyps gl)
- with Failure _ -> anomaly (Pp.str "make_case_branch_assumptions"))
+let make_case_branch_assumptions = make_elim_branch_assumptions
let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
@@ -309,7 +322,7 @@ module New = struct
try
Refiner.catch_failerror e;
tclUNIT ()
- with e -> tclZERO e
+ with e when CErrors.noncritical e -> tclZERO e
(* spiwack: I chose to give the Ltac + the same semantics as
[Proofview.tclOR], however, for consistency with the or-else
@@ -463,6 +476,13 @@ module New = struct
let tclPROGRESS t =
Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
+ (* 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
+
(* Check that holes in arguments have been resolved *)
let check_evars env sigma extsigma origsigma =
@@ -501,18 +521,26 @@ module New = struct
try
let () = check_evars env sigma_final sigma sigma_initial in
tclUNIT x
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
tclZERO e
else
tclUNIT x
in
Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
+ let tclDELAYEDWITHHOLES check x tac =
+ Proofview.Goal.nf_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
+ tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma)
+ end }
+
let tclTIMEOUT n t =
Proofview.tclOR
(Proofview.tclTIMEOUT n t)
begin function (e, info) -> match e with
- | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e)))
+ | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e)))
| e -> Proofview.tclZERO ~info e
end
@@ -523,7 +551,7 @@ module New = struct
let hyps = Proofview.Goal.hyps gl in
try
List.nth hyps (m-1)
- with Failure _ -> Errors.error "No such assumption."
+ with Failure _ -> CErrors.error "No such assumption."
let nLastDecls gl n =
try List.firstn n (Proofview.Goal.hyps gl)
@@ -532,72 +560,70 @@ module New = struct
let nthHypId m gl =
(** We only use [id] *)
let gl = Proofview.Goal.assume gl in
- let (id,_,_) = nthDecl m gl in
- id
+ nthDecl m gl |> get_id
let nthHyp m gl =
mkVar (nthHypId m gl)
let onNthHypId m tac =
- Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end
+ Proofview.Goal.enter { enter = begin fun gl -> tac (nthHypId m gl) end }
let onNthHyp m tac =
- Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end
+ Proofview.Goal.enter { enter = begin fun gl -> tac (nthHyp m gl) end }
let onLastHypId = onNthHypId 1
let onLastHyp = onNthHyp 1
let onNthDecl m tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
Proofview.tclUNIT (nthDecl m gl) >>= tac
- end
+ end }
let onLastDecl = onNthDecl 1
let ifOnHyp pred tac1 tac2 id =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let typ = Tacmach.New.pf_get_hyp_typ id gl in
if pred (id,typ) then
tac1 id
else
tac2 id
- end
+ end }
- let onHyps find tac = Proofview.Goal.nf_enter (fun gl -> tac (find gl))
+ let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end }
let afterHyp id tac =
- Proofview.Goal.nf_enter begin fun gl ->
- let hyps = Proofview.Goal.hyps gl in
- let rem, _ = List.split_when (fun (hyp,_,_) -> Id.equal hyp id) hyps in
+ 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
tac rem
- end
+ end }
let fullGoal gl =
let hyps = Tacmach.New.pf_ids_of_hyps gl in
None :: List.map Option.make hyps
let tryAllHyps tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let hyps = Tacmach.New.pf_ids_of_hyps gl in
tclFIRST_PROGRESS_ON tac hyps
- end
+ end }
let tryAllHypsAndConcl tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
tclFIRST_PROGRESS_ON tac (fullGoal gl)
- end
+ end }
let onClause tac cl =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let hyps = Tacmach.New.pf_ids_of_hyps gl in
tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
- end
+ end }
(* Find the right elimination suffix corresponding to the sort of the goal *)
(* 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
- begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Proofview.Goal.nf_enter begin fun gl ->
+ (Proofview.Goal.nf_enter { enter = begin fun gl ->
let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl 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
@@ -621,8 +647,8 @@ module New = struct
(str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
in
let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
- let branchsigns = compute_construtor_signatures isrec ind in
- let brnames = compute_induction_names (Array.length branchsigns) allnames in
+ let branchsigns = compute_constructor_signatures isrec ind in
+ let brnames = compute_induction_names_gen false branchsigns allnames in
let flags = Unification.elim_flags () in
let elimclause' =
match predicate with
@@ -634,10 +660,7 @@ module New = struct
let (hd,largs) = decompose_app clenv'.templtyp.Evd.rebus in
let ba = { branchsign = branchsigns.(i);
branchnames = brnames.(i);
- nassums =
- List.fold_left
- (fun acc b -> if b then acc+2 else acc+1)
- 0 branchsigns.(i);
+ nassums = List.length branchsigns.(i);
branchnum = i+1;
ity = ind;
largs = List.map (clenv_nf_meta clenv') largs;
@@ -649,10 +672,10 @@ module New = struct
Proofview.tclTHEN
(Clenvtac.clenv_refine false clenv')
(Proofview.tclEXTEND [] tclIDTAC branchtacs)
- end) end
+ end }) end }
let elimination_then tac c =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_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
@@ -660,7 +683,7 @@ module New = struct
| Some _ -> false,gl_make_case_dep
in
general_elim_then_using mkelim isrec None tac None ind (c, t)
- end
+ end }
let case_then_using =
general_elim_then_using gl_make_case_dep false
@@ -669,16 +692,16 @@ module New = struct
general_elim_then_using gl_make_case_nodep false
let elim_on_ba tac ba =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in
tac branches
- end
+ end }
let case_on_ba tac ba =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in
tac branches
- end
+ end }
let elimination_sort_of_goal gl =
(** Retyping will expand evars anyway. *)
@@ -695,11 +718,11 @@ module New = struct
| Some id -> elimination_sort_of_hyp id gl
let pf_constr_of_global ref tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let (sigma, c) = Evd.fresh_global env sigma ref in
Proofview.Unsafe.tclEVARS sigma <*> (tac c)
- end
+ end }
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 07:27:17 +0000