summaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/equality.ml32
-rw-r--r--tactics/extratactics.ml443
-rw-r--r--tactics/rewrite.ml414
-rw-r--r--tactics/tactics.ml8
4 files changed, 74 insertions, 23 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6b16adb4..7a774cc9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: equality.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: equality.ml 13586 2010-10-27 17:42:13Z jforest $ *)
open Pp
open Util
@@ -185,12 +185,30 @@ let find_elim hdcncl lft2rgt dep cls args gl =
pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep
|| Flags.version_less_or_equal Flags.V8_2
then
- (* use eq_rect, eq_rect_r, JMeq_rect, etc for compatibility *)
- let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
- let hdcncls = string_of_inductive hdcncl ^ suffix in
- let rwr_thm = if lft2rgt = Some (cls=None) then hdcncls^"_r" else hdcncls in
- try pf_global gl (id_of_string rwr_thm)
- with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".")
+ match kind_of_term hdcncl with
+ | Ind ind_sp ->
+ let pr1 =
+ lookup_eliminator ind_sp (elimination_sort_of_clause cls gl)
+ in
+ if lft2rgt = Some (cls=None)
+ then
+ let c1 = destConst pr1 in
+ let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in
+ let l' = label_of_id (add_suffix (id_of_label l) "_r") in
+ let c1' = Global.constant_of_delta (make_con mp dp l') in
+ begin
+ try
+ let _ = Global.lookup_constant c1' in
+ mkConst c1'
+ with Not_found ->
+ let rwr_thm = string_of_label l' in
+ error ("Cannot find rewrite principle "^rwr_thm^".")
+ end
+ else pr1
+ | _ ->
+ (* cannot occur since we checked that we are in presence of
+ Logic.eq or Jmeq just before *)
+ assert false
else
let scheme_name = match dep, lft2rgt, inccl with
(* Non dependent case with symmetric equality *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 3f069ab2..dfc8b6bf 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: extratactics.ml4 13434 2010-09-18 20:11:37Z msozeau $ *)
+(* $Id: extratactics.ml4 13658 2010-11-29 11:09:05Z glondu $ *)
open Pp
open Pcoq
@@ -545,7 +545,7 @@ let subst_var_with_hole occ tid t =
| RVar (_,id) as x ->
if id = tid
then (decr occref; if !occref = 0 then x
- else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true))))
+ else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))))
else x
| c -> map_rawconstr_left_to_right substrec c in
let t' = substrec t
@@ -558,7 +558,7 @@ let subst_hole_with_term occ tc t =
let rec substrec = function
| RHole (_,Evd.QuestionMark(Evd.Define true)) ->
decr occref; if !occref = 0 then tc
- else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true)))
+ else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))
| c -> map_rawconstr_left_to_right substrec c
in
substrec t
@@ -580,8 +580,8 @@ let hResolve id c occ t gl =
try
Pretyping.Default.understand sigma env t_hole
with
- | Ploc.Exc (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
- resolve_hole (subst_hole_with_term (Ploc.line_nb loc) c_raw t_hole)
+ | Stdpp.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
+ resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
in
let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
let t_constr_type = Retyping.get_type_of env sigma t_constr in
@@ -629,3 +629,36 @@ TACTIC EXTEND constr_eq
| [ "constr_eq" constr(x) constr(y) ] -> [
if eq_constr x y then tclIDTAC else tclFAIL 0 (str "Not equal") ]
END
+
+TACTIC EXTEND is_evar
+| [ "is_evar" constr(x) ] ->
+ [ match kind_of_term x with
+ | Evar _ -> tclIDTAC
+ | _ -> tclFAIL 0 (str "Not an evar")
+ ]
+END
+
+let rec has_evar x =
+ match kind_of_term x with
+ | Evar _ -> true
+ | Rel _ | Var _ | Meta _ | Sort _ | Const _ | Ind _ | Construct _ ->
+ false
+ | Cast (t1, _, t2) | Prod (_, t1, t2) | Lambda (_, t1, t2) ->
+ has_evar t1 || has_evar t2
+ | LetIn (_, t1, t2, t3) ->
+ has_evar t1 || has_evar t2 || has_evar t3
+ | App (t1, ts) ->
+ has_evar t1 || has_evar_array ts
+ | Case (_, t1, t2, ts) ->
+ has_evar t1 || has_evar t2 || has_evar_array ts
+ | Fix ((_, tr)) | CoFix ((_, tr)) ->
+ has_evar_prec tr
+and has_evar_array x =
+ array_exists has_evar x
+and has_evar_prec (_, ts1, ts2) =
+ array_exists has_evar ts1 || array_exists has_evar ts2
+
+TACTIC EXTEND has_evar
+| [ "has_evar" constr(x) ] ->
+ [ if has_evar x then tclIDTAC else tclFAIL 0 (str "No evars") ]
+END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index d8497a7d..360be9ef 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -596,13 +596,13 @@ let make_leibniz_proof c ty r =
let prf =
mkApp (Lazy.force coq_f_equal,
[| r.rew_car; ty;
- mkLambda (Anonymous, r.rew_car, c (mkRel 1));
+ mkLambda (Anonymous, r.rew_car, c);
r.rew_from; r.rew_to; prf |])
in RewPrf (rel, prf)
| RewCast k -> r.rew_prf
in
{ r with rew_car = ty;
- rew_from = c r.rew_from; rew_to = c r.rew_to; rew_prf = prf }
+ rew_from = subst1 r.rew_from c; rew_to = subst1 r.rew_to c; rew_prf = prf }
open Elimschemes
@@ -772,21 +772,21 @@ let subterm all flags (s : strategy) : strategy =
let c' = s env sigma c cty cstr' evars in
(match c' with
| Some (Some r) ->
- Some (Some (make_leibniz_proof (fun x -> mkCase (ci, p, x, brs)) ty r))
+ Some (Some (make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r))
| x ->
if array_for_all ((=) 0) ci.ci_cstr_nargs then
let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in
let found, brs' = Array.fold_left (fun (found, acc) br ->
- if found <> None then (found, fun x -> br :: acc x)
+ if found <> None then (found, fun x -> lift 1 br :: acc x)
else
match s env sigma br ty cstr evars with
- | Some (Some r) -> (Some r, fun x -> x :: acc x)
- | _ -> (None, fun x -> br :: acc x))
+ | Some (Some r) -> (Some r, fun x -> mkRel 1 :: acc x)
+ | _ -> (None, fun x -> lift 1 br :: acc x))
(None, fun x -> []) brs
in
match found with
| Some r ->
- let ctxc x = mkCase (ci, p, c, Array.of_list (List.rev (brs' x))) in
+ let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' x))) in
Some (Some (make_leibniz_proof ctxc ty r))
| None -> x
else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4ecc4739..569cf356 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tactics.ml 13464 2010-09-24 22:23:02Z herbelin $ *)
+(* $Id: tactics.ml 13693 2010-12-08 15:32:25Z msozeau $ *)
open Pp
open Util
@@ -2365,8 +2365,8 @@ let abstract_args gl generalize_vars dep id defined f args =
in
let f', args' = decompose_indapp f args in
let parvars = ids_of_constr ~all:true Idset.empty f' in
+ let seen = ref parvars in
let dogen, f', args' =
- let seen = ref parvars in
let find i x = not (isVar x) ||
let v = destVar x in
if is_defined_variable env v || Idset.mem v !seen then true
@@ -2379,8 +2379,8 @@ let abstract_args gl generalize_vars dep id defined f args =
true, mkApp (f', before), after
in
if dogen then
- let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
- Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],parvars,Idset.empty,env) args'
+ let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
+ Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],!seen,Idset.empty,env) args'
in
let args, refls = List.rev args, List.rev refls in
let vars =
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-28 05:53:44 +0000