From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Dec 2010 11:53:29 +0100 Subject: Imported Upstream version 8.3pl1 --- tactics/equality.ml | 32 +++++++++++++++++++++++++------- tactics/extratactics.ml4 | 43 ++++++++++++++++++++++++++++++++++++++----- tactics/rewrite.ml4 | 14 +++++++------- tactics/tactics.ml | 8 ++++---- 4 files changed, 74 insertions(+), 23 deletions(-) (limited to 'tactics') 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 = -- cgit v1.2.3