aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-04-03 15:55:27 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-04-22 11:21:02 +0200
commit4c6a5f56ef5ab248d9e816b4d7bee3001cab9a2e (patch)
tree0876edb671c9d9351eaa99c6a83c714eb6eda8b8 /tactics
parent72f29c3052c580eac9c6030d3f9d3c3964322c55 (diff)
Removing tactic compatibility layer from Elim.
Diffstat (limited to 'tactics')
-rw-r--r--tactics/elim.ml84
-rw-r--r--tactics/inv.ml3
-rw-r--r--tactics/tacticals.ml11
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tactics.ml4
5 files changed, 50 insertions, 54 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 5eb3dcfe6..845c4eee1 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -12,8 +12,8 @@ open Term
open Termops
open Inductiveops
open Hipattern
-open Tacmach
-open Tacticals
+open Tacmach.New
+open Tacticals.New
open Tactics
open Misctypes
open Proofview.Notations
@@ -22,27 +22,27 @@ let introElimAssumsThen tac ba =
let nassums =
List.fold_left
(fun acc b -> if b then acc+2 else acc+1)
- 0 ba.branchsign
+ 0 ba.Tacticals.branchsign
in
- let introElimAssums = Tacticals.New.tclDO nassums intro in
- (Tacticals.New.tclTHEN introElimAssums (Tacticals.New.elim_on_ba tac ba))
+ let introElimAssums = tclDO nassums intro in
+ (tclTHEN introElimAssums (elim_on_ba tac ba))
let introCaseAssumsThen tac ba =
let case_thin_sign =
List.flatten
(List.map (function b -> if b then [false;true] else [false])
- ba.branchsign)
+ ba.Tacticals.branchsign)
in
let n1 = List.length case_thin_sign in
- let n2 = List.length ba.branchnames in
+ let n2 = List.length ba.Tacticals.branchnames in
let (l1,l2),l3 =
- if n1 < n2 then List.chop n1 ba.branchnames, []
+ if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, []
else
- (ba.branchnames, []),
+ (ba.Tacticals.branchnames, []),
if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in
let introCaseAssums =
- Tacticals.New.tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in
- (Tacticals.New.tclTHEN introCaseAssums (Tacticals.New.case_on_ba (tac l2) ba))
+ tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in
+ (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
(* The following tactic Decompose repeatedly applies the
elimination(s) rule(s) of the types satisfying the predicate
@@ -63,18 +63,18 @@ Another example :
*)
let elimHypThen tac id =
- Tacticals.New.elimination_then tac (mkVar id)
+ elimination_then tac (mkVar id)
let rec general_decompose_on_hyp recognizer =
- Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT())
+ ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT())
and general_decompose_aux recognizer id =
elimHypThen
(introElimAssumsThen
(fun bas ->
- Tacticals.New.tclTHEN (Proofview.V82.tactic (clear [id]))
- (Tacticals.New.tclMAP (general_decompose_on_hyp recognizer)
- (ids_of_named_context bas.assums))))
+ tclTHEN (Proofview.V82.tactic (clear [id]))
+ (tclMAP (general_decompose_on_hyp recognizer)
+ (ids_of_named_context bas.Tacticals.assums))))
id
(* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste
@@ -85,17 +85,15 @@ let tmphyp_name = Id.of_string "_TmpHyp"
let up_to_delta = ref false (* true *)
let general_decompose recognizer c =
- Proofview.Goal.enter begin fun gl ->
- let type_of = Tacmach.New.pf_type_of gl in
- try (* type_of can raise exceptions *)
+ Proofview.Goal.raw_enter begin fun gl ->
+ let type_of = pf_type_of gl in
let typc = type_of c in
- Tacticals.New.tclTHENS (cut typc)
- [ Tacticals.New.tclTHEN (intro_using tmphyp_name)
- (Tacticals.New.onLastHypId
- (Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer)
+ tclTHENS (cut typc)
+ [ tclTHEN (intro_using tmphyp_name)
+ (onLastHypId
+ (ifOnHyp recognizer (general_decompose_aux recognizer)
(fun id -> Proofview.V82.tactic (clear [id]))));
Proofview.V82.tactic (exact_no_check c) ]
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
let head_in indl t gl =
@@ -110,7 +108,7 @@ let head_in indl t gl =
with Not_found -> false
let decompose_these c l =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.raw_enter begin fun gl ->
let indl = (*List.map inductive_of*) l in
general_decompose (fun (_,t) -> head_in indl t gl) c
end
@@ -139,47 +137,47 @@ let h_decompose_and = decompose_and
(* The tactic Double performs a double induction *)
let simple_elimination c =
- Tacticals.New.elimination_then (fun _ -> Tacticals.New.tclIDTAC) c
+ elimination_then (fun _ -> tclIDTAC) c
let induction_trailer abs_i abs_j bargs =
- Tacticals.New.tclTHEN
- (Tacticals.New.tclDO (abs_j - abs_i) intro)
- (Tacticals.New.onLastHypId
+ tclTHEN
+ (tclDO (abs_j - abs_i) intro)
+ (onLastHypId
(fun id ->
- Proofview.V82.tactic begin fun gls ->
- let idty = pf_type_of gls (mkVar id) in
- let fvty = global_vars (pf_env gls) idty in
+ Proofview.Goal.enter begin fun gl ->
+ let idty = pf_type_of gl (mkVar id) in
+ let fvty = global_vars (pf_env gl) idty in
let possible_bring_hyps =
- (List.tl (nLastDecls (abs_j - abs_i) gls)) @ bargs.assums
+ (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
in
let (hyps,_) =
List.fold_left
- (fun (bring_ids,leave_ids) (cid,_,cidty as d) ->
+ (fun (bring_ids,leave_ids) (cid,_,_ as d) ->
if not (List.mem cid leave_ids)
then (d::bring_ids,leave_ids)
else (bring_ids,cid::leave_ids))
([],fvty) possible_bring_hyps
in
let ids = List.rev (ids_of_named_context hyps) in
- (tclTHENSEQ
- [Proofview.V82.of_tactic (bring_hyps hyps); tclTRY (clear ids);
- Proofview.V82.of_tactic (simple_elimination (mkVar id))]) gls
+ (tclTHENLIST
+ [bring_hyps hyps; tclTRY (Proofview.V82.tactic (clear ids));
+ simple_elimination (mkVar id)])
end
))
let double_ind h1 h2 =
Proofview.Goal.enter begin fun gl ->
- let abs_i = Tacmach.New.of_old (depth_of_quantified_hypothesis true h1) gl in
- let abs_j = Tacmach.New.of_old (depth_of_quantified_hypothesis true h2) gl in
+ let abs_i = of_old (depth_of_quantified_hypothesis true h1) gl in
+ let abs_j = of_old (depth_of_quantified_hypothesis true h2) gl in
let abs =
if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else
- Proofview.tclZERO (Errors.UserError ("", Pp.str"Both hypotheses are the same.")) in
+ tclZEROMSG (Pp.str "Both hypotheses are the same.") in
abs >>= fun (abs_i,abs_j) ->
- (Tacticals.New.tclTHEN (Tacticals.New.tclDO abs_i intro)
- (Tacticals.New.onLastHypId
+ (tclTHEN (tclDO abs_i intro)
+ (onLastHypId
(fun id ->
- Tacticals.New.elimination_then
+ elimination_then
(introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id))))
end
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 0bc96c19d..0811e229e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -336,6 +336,9 @@ let projectAndApply thin id eqname names depids =
(Some (ElimOnConstr (mkVar id,NoBindings))))
id
+let nLastDecls i tac =
+ Proofview.Goal.enter (fun gl -> tac (nLastDecls gl i))
+
(* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
soi-meme (proposition de Valerie). *)
let rewrite_equations_gene othin neqns ba =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 926578e0e..967b6d544 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -475,14 +475,9 @@ module New = struct
List.nth hyps (m-1)
with Failure _ -> Errors.error "No such assumption."
- let nLastDecls n tac =
- Proofview.Goal.enter begin fun gl ->
- let hyps =
- try List.firstn n (Proofview.Goal.hyps gl)
- with Failure _ -> error "Not enough hypotheses in the goal."
- in
- tac hyps
- end
+ let nLastDecls gl n =
+ try List.firstn n (Proofview.Goal.hyps gl)
+ with Failure _ -> error "Not enough hypotheses in the goal."
let nthHypId m gl =
(** We only use [id] *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index d6c9e87f9..857ced838 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -216,7 +216,7 @@ module New : sig
val tclTIMEOUT : int -> unit tactic -> unit tactic
- val nLastDecls : int -> (named_context -> unit tactic) -> unit tactic
+ val nLastDecls : [ `NF ] Proofview.Goal.t -> int -> named_context
val ifOnHyp : (identifier * types -> bool) ->
(identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 74661b836..be5b0de3a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -665,9 +665,9 @@ let apply_term hdc argl gl =
let bring_hyps hyps =
if List.is_empty hyps then Tacticals.New.tclIDTAC
else
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let concl = Proofview.Goal.concl gl in
+ let concl = Tacmach.New.pf_nf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
let args = Array.of_list (instance_from_named_context hyps) in
Proofview.Refine.refine begin fun h ->