aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/elim.ml33
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/tacticals.ml6
-rw-r--r--tactics/tacticals.mli3
-rw-r--r--tactics/tactics.ml14
-rw-r--r--tactics/tactics.mli3
-rw-r--r--tactics/tauto.ml8
-rw-r--r--tactics/wcclausenv.ml8
-rw-r--r--tactics/wcclausenv.mli8
9 files changed, 53 insertions, 34 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml
index ff07f6c09..4e414b35e 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -42,7 +42,7 @@ Require Elim.
Require Le.
Goal (y:nat){x:nat | (le O x)/\(le x y)}->(le O y).
Intros y H.
- Decompose [sig and] H;EAuto.
+ Decompose [sig and] H;EAuto. [HUM HUM !! Y a peu de chance qu'ça marche !]
Qed.
Another example :
@@ -67,33 +67,46 @@ let rec general_decompose_clause recognizer =
cls)
(fun _ -> tclIDTAC)
+(* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste
+ pas si aucune élimination n'est possible *)
+
let rec general_decompose recognizer c gl =
let typc = pf_type_of gl c in
(tclTHENS (cut typc)
[(tclTHEN intro
(onLastHyp (general_decompose_clause recognizer)));
(exact c)]) gl
-
-let head_in l c = List.mem (List.hd (head_constr c)) l
-
+
+let head_in gls indl t =
+ try
+ let ity = fst (find_mrectype (pf_env gls) (project gls) t) in
+ List.mem ity indl
+ with Induc -> false
+
+let inductive_of_ident gls id =
+ try
+ fst (find_mrectype (pf_env gls) (project gls) (pf_global gls id))
+ with Induc ->
+ errorlabstrm "Decompose"
+ [< print_id id; 'sTR " is not an inductive type" >]
+
let decompose_these c l gls =
- let l = List.map (pf_global gls) l in
- general_decompose (fun (_,t) -> head_in l t) c gls
+ let indl = List.map (inductive_of_ident gls) l in
+ general_decompose (fun (_,t) -> head_in gls indl t) c gls
let decompose_nonrec c gls =
general_decompose
- (fun (_,t) ->
- (is_non_recursive_type (List.hd (head_constr t))))
+ (fun (_,t) -> is_non_recursive_type t)
c gls
let decompose_and c gls =
general_decompose
- (fun (_,t) -> (is_conjunction (List.hd (head_constr t))))
+ (fun (_,t) -> is_conjunction t)
c gls
let decompose_or c gls =
general_decompose
- (fun (_,t) -> (is_disjunction (List.hd (head_constr t))))
+ (fun (_,t) -> is_disjunction t)
c gls
let dyn_decompose args gl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 5ecf3a39a..b4cc547d1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -142,7 +142,7 @@ let h_replace c1 c2 = v_replace [(Constr c1);(Constr c2)]
let conditional_rewrite lft2rgt tac (c,bl) =
tclTHEN_i (general_rewrite_bindings lft2rgt (c,bl))
- (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac) 1
+ (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)
let dyn_conditional_rewrite lft2rgt = function
| [(Tacexp tac); (Command com);(Bindings binds)] ->
@@ -1470,7 +1470,7 @@ let rewriteRL_in_tac = hide_tactic "RewriteRLin" (dyn_rewrite_in false)
let conditional_rewrite_in lft2rgt id tac (c,bl) =
tclTHEN_i (general_rewrite_in lft2rgt id (c,bl))
- (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac) 1
+ (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac)
let dyn_conditional_rewrite_in lft2rgt = function
| [(Tacexp tac); Identifier id; (Command com);(Bindings binds)] ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 294a13c6d..c8f687698 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -48,8 +48,6 @@ let dyn_tclIDTAC = function [] -> tclIDTAC | _ -> anomaly "tclIDTAC"
let dyn_tclFAIL = function [] -> tclFAIL | _ -> anomaly "tclFAIL"
-let tclTHEN_i1 tac1 tac2 = tclTHEN_i tac1 tac2 1
-
(* apply a tactic to the nth element of the signature *)
let tclNTH_HYP m (tac : constr->tactic) gl =
@@ -344,14 +342,14 @@ let general_elim_then_using
largs = List.map (clenv_instance_term ce) largs;
pred = clenv_instance_term ce hd }
in
- tac ba gl
+ tac ba gl
in
let elimclause' =
match predicate with
| None -> elimclause'
| Some p -> clenv_assign pmv p elimclause'
in
- elim_res_pf_THEN_i kONT elimclause' after_tac 1 gl
+ elim_res_pf_THEN_i kONT elimclause' after_tac gl
let elimination_then_using tac predicate (indbindings,elimbindings) c gl =
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index de91973d6..7a0e3f9c5 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -18,7 +18,7 @@ open Wcclausenv
val tclIDTAC : tactic
val tclORELSE : tactic -> tactic -> tactic
val tclTHEN : tactic -> tactic -> tactic
-val tclTHEN_i : tactic -> (int -> tactic) -> int -> tactic
+val tclTHEN_i : tactic -> (int -> tactic) -> tactic
val tclTHENL : tactic -> tactic -> tactic
val tclTHENS : tactic -> tactic list -> tactic
val tclREPEAT : tactic -> tactic
@@ -44,7 +44,6 @@ val dyn_tclFAIL : tactic_arg list -> tactic
type clause = identifier option
-val tclTHEN_i1 : tactic -> (int -> tactic) -> tactic
val nth_clause : int -> goal sigma -> clause
val clause_type : clause -> goal sigma -> constr
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 860c98126..c35109e2c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -38,7 +38,16 @@ let get_pairs_from_bindings =
| _ -> error "not a binding list!"
in
List.map pair_from_binding
-
+
+let force_reference c =
+ match fst (decomp_app c) with
+ | DOPN (Const sp,ctxt) -> c
+ | DOPN (Evar ev,ctxt) -> c
+ | DOPN (MutConstruct (spi,j),ctxt) -> c
+ | DOPN (MutInd (sp,i),ctxt) -> c
+ | VAR id -> c
+ | _ -> error "Not an atomic type"
+
let rec string_head_bound = function
| DOPN(Const _,_) as x ->
string_of_id (basename (path_of_const x))
@@ -50,10 +59,11 @@ let rec string_head_bound = function
string_of_id (mib.mind_packets.(tyi).mind_consnames.(i-1))
| VAR id -> string_of_id id
| _ -> raise Bound
-
+
let string_head c =
try string_head_bound c with Bound -> error "Bound head variable"
+
let rec head_constr_bound t l =
let t = strip_outer_cast(collapse_appl t) in
match t with
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 751a77739..92e76fbd3 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -25,6 +25,9 @@ val make_clenv_binding_apply :
val type_clenv_binding : walking_constraints ->
constr * constr -> constr substitution -> constr
+(* [force_reference c] fails if [c] is not a reference *)
+val force_reference : constr -> constr
+
val string_head : constr -> string
val head_constr : constr -> constr list
val head_constr_bound : constr -> constr list -> constr list
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 2708bf01a..52b4e288c 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -1864,18 +1864,14 @@ let tautoOR ti gls =
(t_exacto := tt;
subbuts l thyp gls)
-let exact_Idtac = function
- | 0 -> exacto (!t_exacto)
- | _ -> tclIDTAC
-
let tautoOR_0 gl =
tclORELSE
- (tclTHEN_i (tautoOR false) exact_Idtac 0)
+ (tclTHENSI (tautoOR false) [exacto (!t_exacto)])
tAUTOFAIL gl
let intuitionOR =
tclTRY (tclTHEN
- (tclTHEN_i (tautoOR true) exact_Idtac 0)
+ (tclTHENSI (tautoOR true) [exacto (!t_exacto)])
default_full_auto)
(*--- Mixed code Chet-Cesar ---*)
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index b7fdd67a7..7cdd5c1fe 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -124,13 +124,13 @@ let res_pf_THEN kONT clenv tac gls =
let clenv' = (clenv_unique_resolver false clenv gls) in
(tclTHEN (clenv_refine kONT clenv') (tac clenv')) gls
-let res_pf_THEN_i kONT clenv tac i gls =
+let res_pf_THEN_i kONT clenv tac gls =
let clenv' = (clenv_unique_resolver false clenv gls) in
- tclTHEN_i (clenv_refine kONT clenv') (tac clenv') i gls
+ tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
-let elim_res_pf_THEN_i kONT clenv tac i gls =
+let elim_res_pf_THEN_i kONT clenv tac gls =
let clenv' = (clenv_unique_resolver true clenv gls) in
- tclTHEN_i (clenv_refine kONT clenv') (tac clenv') i gls
+ tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
let rec build_args acc ce p_0 p_1 =
match p_0,p_1 with
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 01d05a690..af96177b3 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -42,13 +42,13 @@ val add_prods_sign :
val res_pf_THEN :
(wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic) -> tactic
+(* This behaves as [res_pf_THEN] but the tactic applied then takes
+ also the subgoal number (starting from 1) as argument *)
val res_pf_THEN_i :
- (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) ->
- int -> tactic
+ (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
val elim_res_pf_THEN_i :
- (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) ->
- int -> tactic
+ (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
val mk_clenv_using : wc -> constr -> wc clausenv
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 02:48:35 +0000