summaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
commit72b9a7df489ea47b3e5470741fd39f6100d31676 (patch)
tree60108a573d2a80d2dd4e3833649890e32427ff8d /tactics/tactics.ml
parent55ce117e8083477593cf1ff2e51a3641c7973830 (diff)
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r--tactics/tactics.ml71
1 files changed, 50 insertions, 21 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cb98ec18..c863a453 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tactics.ml 9605 2007-02-07 12:19:19Z notin $ *)
+(* $Id: tactics.ml 9853 2007-05-23 14:25:47Z letouzey $ *)
open Pp
open Util
@@ -503,6 +503,20 @@ let cut_in_parallel l =
in
prec (List.rev l)
+let error_uninstantiated_metas t clenv =
+ let na = meta_name clenv.env (List.hd (Metaset.elements (metavars_of t))) in
+ let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
+ in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id)
+
+let clenv_refine_in id clenv gl =
+ let new_hyp_typ = clenv_type clenv in
+ if occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv;
+ let new_hyp_prf = clenv_value clenv in
+ tclTHEN
+ (tclEVARS (evars_of clenv.env))
+ (cut_replacing id new_hyp_typ
+ (fun x gl -> refine_no_check new_hyp_prf gl)) gl
+
(****************************************************)
(* Resolution tactics *)
(****************************************************)
@@ -575,12 +589,7 @@ let apply_in id lemmas gls =
let t' = pf_get_hyp_typ gls id in
let innermostclause = mk_clenv_from_n gls (Some 0) (mkVar id,t') in
let clause = List.fold_left (apply_in_once gls) innermostclause lemmas in
- let new_hyp_prf = clenv_value clause in
- let new_hyp_typ = clenv_type clause in
- tclTHEN
- (tclEVARS (evars_of clause.env))
- (cut_replacing id new_hyp_typ
- (fun x gls -> refine_no_check new_hyp_prf gls)) gls
+ clenv_refine_in id clause gls
(* A useful resolution tactic which, if c:A->B, transforms |- C into
|- B -> C and |- A
@@ -839,15 +848,11 @@ let elimination_in_clause_scheme id elimclause indclause gl =
let hyp_typ = pf_type_of gl hyp in
let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
let elimclause'' = clenv_fchain hypmv elimclause' hypclause in
- let new_hyp_prf = clenv_value elimclause'' in
let new_hyp_typ = clenv_type elimclause'' in
if eq_constr hyp_typ new_hyp_typ then
errorlabstrm "general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id);
- tclTHEN
- (tclEVARS (evars_of elimclause''.env))
- (cut_replacing id new_hyp_typ
- (fun x gls -> refine_no_check new_hyp_prf gls)) gl
+ clenv_refine_in id elimclause'' gl
let general_elim_in id =
general_elim_clause (elimination_in_clause_scheme id)
@@ -2328,10 +2333,18 @@ let dImp cls =
let setoid_reflexivity = ref (fun _ -> assert false)
let register_setoid_reflexivity f = setoid_reflexivity := f
-let reflexivity gl =
- match match_with_equation (pf_concl gl) with
+let reflexivity_red allowred gl =
+ (* PL: usual reflexivity don't perform any reduction when searching
+ for an equality, but we may need to do some when called back from
+ inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+ let concl = if not allowred then pf_concl gl
+ else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl)
+ in
+ match match_with_equation concl with
| None -> !setoid_reflexivity gl
- | Some (hdcncl,args) -> one_constructor 1 NoBindings gl
+ | Some _ -> one_constructor 1 NoBindings gl
+
+let reflexivity gl = reflexivity_red false gl
let intros_reflexivity = (tclTHEN intros reflexivity)
@@ -2345,8 +2358,14 @@ let intros_reflexivity = (tclTHEN intros reflexivity)
let setoid_symmetry = ref (fun _ -> assert false)
let register_setoid_symmetry f = setoid_symmetry := f
-let symmetry gl =
- match match_with_equation (pf_concl gl) with
+let symmetry_red allowred gl =
+ (* PL: usual symmetry don't perform any reduction when searching
+ for an equality, but we may need to do some when called back from
+ inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+ let concl = if not allowred then pf_concl gl
+ else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl)
+ in
+ match match_with_equation concl with
| None -> !setoid_symmetry gl
| Some (hdcncl,args) ->
let hdcncls = string_of_inductive hdcncl in
@@ -2360,7 +2379,7 @@ let symmetry gl =
| [c1;c2] -> mkApp (hdcncl, [| c2; c1 |])
| _ -> assert false
in
- tclTHENLAST (cut symc)
+ tclTHENFIRST (cut symc)
(tclTHENLIST
[ intro;
tclLAST_HYP simplest_case;
@@ -2368,6 +2387,8 @@ let symmetry gl =
gl
end
+let symmetry gl = symmetry_red false gl
+
let setoid_symmetry_in = ref (fun _ _ -> assert false)
let register_setoid_symmetry_in f = setoid_symmetry_in := f
@@ -2408,8 +2429,14 @@ let intros_symmetry =
let setoid_transitivity = ref (fun _ _ -> assert false)
let register_setoid_transitivity f = setoid_transitivity := f
-let transitivity t gl =
- match match_with_equation (pf_concl gl) with
+let transitivity_red allowred t gl =
+ (* PL: usual transitivity don't perform any reduction when searching
+ for an equality, but we may need to do some when called back from
+ inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+ let concl = if not allowred then pf_concl gl
+ else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl)
+ in
+ match match_with_equation concl with
| None -> !setoid_transitivity t gl
| Some (hdcncl,args) ->
let hdcncls = string_of_inductive hdcncl in
@@ -2436,7 +2463,9 @@ let transitivity t gl =
tclLAST_HYP simplest_case;
assumption ])) gl
end
-
+
+let transitivity t gl = transitivity_red false t gl
+
let intros_transitivity n = tclTHEN intros (transitivity n)
(* tactical to save as name a subproof such that the generalisation of