aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/inv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/inv.ml')
-rw-r--r--tactics/inv.ml185
1 files changed, 94 insertions, 91 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ec96a887d..c9d54f84f 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -28,6 +28,7 @@ open Elim
open Equality
open Misctypes
open Tacexpr
+open Proofview.Notations
let collect_meta_variables c =
let rec collrec acc c = match kind_of_term c with
@@ -272,19 +273,18 @@ Summary: nine useless hypotheses!
Nota: with Inversion_clear, only four useless hypotheses
*)
-let generalizeRewriteIntros tac depids id gls =
- let dids = dependent_hyps id depids gls in
- (tclTHENSEQ
- [bring_hyps dids; tac;
+let generalizeRewriteIntros tac depids id =
+ Tacmach.New.of_old (dependent_hyps id depids) >>- fun dids ->
+ (Tacticals.New.tclTHENLIST
+ [Proofview.V82.tactic (bring_hyps dids); tac;
(* may actually fail to replace if dependent in a previous eq *)
intros_replacing (ids_of_named_context dids)])
- gls
let rec tclMAP_i n tacfun = function
- | [] -> tclDO n (tacfun None)
+ | [] -> Tacticals.New.tclDO n (tacfun None)
| a::l ->
- if Int.equal n 0 then error "Too many names."
- else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
+ if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("", Pp.str"Too many names."))
+ else Tacticals.New.tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
@@ -296,29 +296,29 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
If it can discriminate then the goal is proved, if not tries to use it as
a rewrite rule. It erases the clause which is given as input *)
-let projectAndApply thin id eqname names depids gls =
+let projectAndApply thin id eqname names depids =
let subst_hyp l2r id =
tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id)))
(if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
in
- let substHypIfVariable tac id gls =
- let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in
+ let substHypIfVariable tac id =
+ Tacmach.New.of_old (fun gls -> Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id)) >>- fun (t,t1,t2) ->
match (kind_of_term t1, kind_of_term t2) with
- | Var id1, _ -> generalizeRewriteIntros (subst_hyp true id) depids id1 gls
- | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2 gls
- | _ -> tac id gls
+ | Var id1, _ -> generalizeRewriteIntros (Proofview.V82.tactic (subst_hyp true id)) depids id1
+ | _, Var id2 -> generalizeRewriteIntros (Proofview.V82.tactic (subst_hyp false id)) depids id2
+ | _ -> tac id
in
let deq_trailer id _ neqns =
- tclTHENSEQ
- [(if not (List.is_empty names) then clear [id] else tclIDTAC);
+ Tacticals.New.tclTHENLIST
+ [Proofview.V82.tactic (if not (List.is_empty names) then clear [id] else tclIDTAC);
(tclMAP_i neqns (fun idopt ->
- tclTRY (tclTHEN
+ Tacticals.New.tclTRY (Tacticals.New.tclTHEN
(intro_move idopt MoveLast)
(* try again to substitute and if still not a variable after *)
(* decomposition, arbitrarily try to rewrite RL !? *)
- (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false))))))
+ (Tacticals.New.tclTRY (Tacticals.New.onLastHypId (substHypIfVariable (fun id -> Proofview.V82.tactic (subst_hyp false id)))))))
names);
- (if List.is_empty names then clear [id] else tclIDTAC)]
+ Proofview.V82.tactic (if List.is_empty names then clear [id] else tclIDTAC)]
in
substHypIfVariable
(* If no immediate variable in the equation, try to decompose it *)
@@ -327,42 +327,40 @@ let projectAndApply thin id eqname names depids gls =
dEqThen false (deq_trailer id)
(Some (ElimOnConstr (mkVar id,NoBindings))))
id
- gls
(* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
soi-meme (proposition de Valerie). *)
-let rewrite_equations_gene othin neqns ba gl =
- let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
+let rewrite_equations_gene othin neqns ba =
+ Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) >>- fun (depids,nodepids) ->
let rewrite_eqns =
match othin with
| Some thin ->
- onLastHypId
+ Tacticals.New.onLastHypId
(fun last ->
- tclTHENSEQ
- [tclDO neqns
- (tclTHEN intro
- (onLastHypId
+ Tacticals.New.tclTHENLIST
+ [Tacticals.New.tclDO neqns
+ (Tacticals.New.tclTHEN intro
+ (Tacticals.New.onLastHypId
(fun id ->
- tclTRY
+ Tacticals.New.tclTRY
(projectAndApply thin id (ref MoveLast)
[] depids))));
- onHyps (compose List.rev (afterHyp last)) bring_hyps;
- onHyps (afterHyp last)
- (compose clear ids_of_named_context)])
- | None -> tclIDTAC
+ Proofview.V82.tactic (onHyps (compose List.rev (afterHyp last)) bring_hyps);
+ Proofview.V82.tactic (onHyps (afterHyp last)
+ (compose clear ids_of_named_context))])
+ | None -> Proofview.tclUNIT ()
in
- (tclTHENSEQ
- [tclDO neqns intro;
- bring_hyps nodepids;
- clear (ids_of_named_context nodepids);
- onHyps (compose List.rev (nLastDecls neqns)) bring_hyps;
- onHyps (nLastDecls neqns) (compose clear ids_of_named_context);
+ (Tacticals.New.tclTHENLIST
+ [Tacticals.New.tclDO neqns intro;
+ Proofview.V82.tactic (bring_hyps nodepids);
+ Proofview.V82.tactic (clear (ids_of_named_context nodepids));
+ Proofview.V82.tactic (onHyps (compose List.rev (nLastDecls neqns)) bring_hyps);
+ Proofview.V82.tactic (onHyps (nLastDecls neqns) (compose clear ids_of_named_context));
rewrite_eqns;
- tclMAP (fun (id,_,_ as d) ->
+ Proofview.V82.tactic (tclMAP (fun (id,_,_ as d) ->
(tclORELSE (clear [id])
(tclTHEN (bring_hyps [d]) (clear [id]))))
- depids])
- gl
+ depids)])
(* Introduction of the equations on arguments
othin: discriminates Simple Inversion, Inversion and Inversion_clear
@@ -398,35 +396,34 @@ let extract_eqn_names = function
| None -> None,[]
| Some x -> x
-let rewrite_equations othin neqns names ba gl =
+let rewrite_equations othin neqns names ba =
let names = List.map (get_names true) names in
- let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
+ Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) >>- fun (depids,nodepids) ->
let rewrite_eqns =
let first_eq = ref MoveLast in
match othin with
| Some thin ->
- tclTHENSEQ
- [onHyps (compose List.rev (nLastDecls neqns)) bring_hyps;
- onHyps (nLastDecls neqns) (compose clear ids_of_named_context);
+ Tacticals.New.tclTHENLIST
+ [Proofview.V82.tactic (onHyps (compose List.rev (nLastDecls neqns)) bring_hyps);
+ Proofview.V82.tactic (onHyps (nLastDecls neqns) (compose clear ids_of_named_context));
tclMAP_i neqns (fun o ->
let idopt,names = extract_eqn_names o in
- (tclTHEN
+ (Tacticals.New.tclTHEN
(intro_move idopt MoveLast)
- (onLastHypId (fun id ->
- tclTRY (projectAndApply thin id first_eq names depids)))))
+ (Tacticals.New.onLastHypId (fun id ->
+ Tacticals.New.tclTRY (projectAndApply thin id first_eq names depids)))))
names;
- tclMAP (fun (id,_,_) gl ->
- intro_move None (if thin then MoveLast else !first_eq) gl)
+ Tacticals.New.tclMAP (fun (id,_,_) -> Proofview.tclUNIT () >= fun () -> (* delay for [first_eq]. *)
+ intro_move None (if thin then MoveLast else !first_eq))
nodepids;
- tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids]
- | None -> tclIDTAC
+ Proofview.V82.tactic (tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids)]
+ | None -> Proofview.tclUNIT ()
in
- (tclTHENSEQ
- [tclDO neqns intro;
- bring_hyps nodepids;
- clear (ids_of_named_context nodepids);
+ (Tacticals.New.tclTHENLIST
+ [Tacticals.New.tclDO neqns intro;
+ Proofview.V82.tactic (bring_hyps nodepids);
+ Proofview.V82.tactic (clear (ids_of_named_context nodepids));
rewrite_eqns])
- gl
let interp_inversion_kind = function
| SimpleInversion -> None
@@ -440,61 +437,66 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
else rewrite_equations othin neqns names ba in
match othin with
| Some true (* if Inversion_clear, clear the hypothesis *) ->
- tclTHEN tac (tclTRY (clear [id]))
+ Tacticals.New.tclTHEN tac (Proofview.V82.tactic (tclTRY (clear [id])))
| _ ->
tac
-let raw_inversion inv_kind id status names gl =
- let env = pf_env gl and sigma = project gl in
+let raw_inversion inv_kind id status names =
+ Goal.env >>- fun env ->
+ Goal.defs >>- fun sigma ->
+ Goal.concl >>- fun concl ->
let c = mkVar id in
+ Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind >>- fun reduce_to_atomic_ind ->
+ Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
let (ind,t) =
- try pf_reduce_to_atomic_ind gl (pf_type_of gl c)
+ try
+ reduce_to_atomic_ind (type_of c)
with UserError _ ->
errorlabstrm "raw_inversion"
(str ("The type of "^(Id.to_string id)^" is not inductive.")) in
- let indclause = mk_clenv_from gl (c,t) in
+ Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>- fun indclause ->
let ccl = clenv_type indclause in
check_no_metas indclause ccl;
let IndType (indf,realargs) = find_rectype env sigma ccl in
let (elim_predicate,neqns) =
- make_inv_predicate env sigma indf realargs id status (pf_concl gl) in
+ make_inv_predicate env sigma indf realargs id status concl in
let (cut_concl,case_tac) =
- if status != NoDep && (dependent c (pf_concl gl)) then
+ if status != NoDep & (dependent c concl) then
Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
- case_then_using
+ Tacticals.New.case_then_using
else
Reduction.beta_appvect elim_predicate (Array.of_list realargs),
- case_nodep_then_using
+ Tacticals.New.case_nodep_then_using
in
- (tclTHENS
+ (Tacticals.New.tclTHENS
(assert_tac Anonymous cut_concl)
[case_tac names
(introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
(Some elim_predicate) ([],[]) ind indclause;
- onLastHypId
+ Tacticals.New.onLastHypId
(fun id ->
- (tclTHEN
- (apply_term (mkVar id)
- (List.init neqns (fun _ -> Evarutil.mk_new_meta())))
+ (Tacticals.New.tclTHEN
+ (Proofview.V82.tactic (apply_term (mkVar id)
+ (List.init neqns (fun _ -> Evarutil.mk_new_meta()))))
reflexivity))])
- gl
(* Error messages of the inversion tactics *)
let wrap_inv_error id = function
| Indrec.RecursionSchemeError
(Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) ->
- errorlabstrm ""
+ Proofview.tclZERO (Errors.UserError ("",
(strbrk "Inversion would require case analysis on sort " ++
pr_sort k ++
strbrk " which is not allowed for inductive definition " ++
- pr_inductive (Global.env()) i ++ str ".")
- | e -> raise e
+ pr_inductive (Global.env()) i ++ str ".")))
+ | e -> Proofview.tclZERO e
(* The most general inversion tactic *)
-let inversion inv_kind status names id gls =
- try (raw_inversion inv_kind id status names) gls
- with e when Errors.noncritical e -> wrap_inv_error id e
+let inversion inv_kind status names id =
+ Proofview.tclORELSE
+ (raw_inversion inv_kind id status names)
+ (wrap_inv_error id)
(* Specializing it... *)
@@ -519,25 +521,26 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
* perform inversion on the named hypothesis. After, it will intro them
* back to their places in the hyp-list. *)
-let invIn k names ids id gls =
- let hyps = List.map (pf_get_hyp gls) ids in
- let nb_prod_init = nb_prod (pf_concl gls) in
- let intros_replace_ids gls =
+let invIn k names ids id =
+ Goal.sensitive_list_map Tacmach.New.pf_get_hyp ids >>- fun hyps ->
+ Goal.concl >>- fun concl ->
+ let nb_prod_init = nb_prod concl in
+ let intros_replace_ids =
+ Goal.concl >>- fun concl ->
let nb_of_new_hyp =
- nb_prod (pf_concl gls) - (List.length hyps + nb_prod_init)
+ nb_prod concl - (List.length hyps + nb_prod_init)
in
if nb_of_new_hyp < 1 then
- intros_replacing ids gls
+ intros_replacing ids
else
- tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) gls
+ Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids)
in
- try
- (tclTHENSEQ
- [bring_hyps hyps;
+ Proofview.tclORELSE
+ (Tacticals.New.tclTHENLIST
+ [Proofview.V82.tactic (bring_hyps hyps);
inversion (false,k) NoDep names id;
intros_replace_ids])
- gls
- with e when Errors.noncritical e -> wrap_inv_error id e
+ (wrap_inv_error id)
let invIn_gen k names idl = try_intros_until (invIn k names idl)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 06:47:37 +0000