diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 61 |
1 files changed, 29 insertions, 32 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index e4bab195..c48a90ac 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inv.ml,v 1.53.2.3 2005/09/08 12:28:00 herbelin Exp $ *) +(* $Id: inv.ml 7880 2006-01-16 13:59:08Z herbelin $ *) open Pp open Util @@ -46,13 +46,13 @@ let collect_meta_variables c = let check_no_metas clenv ccl = if occur_meta ccl then - let metas = List.map (fun n -> Metamap.find n clenv.namenv) - (collect_meta_variables ccl) in + let metas = List.filter (fun na -> na<>Anonymous) + (List.map (Evd.meta_name clenv.env) (collect_meta_variables ccl)) in errorlabstrm "inversion" (str ("Cannot find an instantiation for variable"^ (if List.length metas = 1 then " " else "s ")) ++ - prlist_with_sep pr_coma pr_id metas - (* ajouter "in " ++ prterm ccl mais il faut le bon contexte *)) + prlist_with_sep pr_coma pr_name metas + (* ajouter "in " ++ pr_lconstr ccl mais il faut le bon contexte *)) let var_occurs_in_pf gl id = let env = pf_env gl in @@ -88,8 +88,7 @@ let var_occurs_in_pf gl id = type inversion_status = Dep of constr option | NoDep let compute_eqn env sigma n i ai = - (ai,get_type_of env sigma ai), - (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) + (ai, (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))) let make_inv_predicate env sigma indf realargs id status concl = let nrealargs = List.length realargs in @@ -112,7 +111,7 @@ let make_inv_predicate env sigma indf realargs id status concl = | None -> let sort = get_sort_of env sigma concl in let p = make_arity env true indf sort in - abstract_list_all env sigma p concl (realargs@[mkVar id]) in + Unification.abstract_list_all env sigma p concl (realargs@[mkVar id]) in let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in (* We lift to make room for the equations *) (hyps,lift nrealargs bodypred) @@ -128,14 +127,13 @@ let make_inv_predicate env sigma indf realargs id status concl = In any case, we carry along the rest of pairs *) let rec build_concl eqns n = function | [] -> (prod_it concl eqns,n) - | ((ai,ati),(xi,ti))::restlist -> + | (ai,(xi,ti))::restlist -> let (lhs,eqnty,rhs) = if closed0 ti then (xi,ti,ai) else - make_iterated_tuple env' sigma (ai,ati) (xi,ti) + make_iterated_tuple env' sigma ai (xi,ti) in - let sort = get_sort_of env sigma concl in let eq_term = Coqlib.build_coq_eq () in let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist @@ -306,17 +304,16 @@ let remember_first_eq id x = if !x = None then x := Some id a rewrite rule. It erases the clause which is given as input *) let projectAndApply thin id eqname names depids gls = - let env = pf_env gls in - let clearer id = - if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC) in - let subst_hyp_LR id = tclTHEN (tclTRY(hypSubst_LR id onConcl)) (clearer id) in - let subst_hyp_RL id = tclTHEN (tclTRY(hypSubst_RL id onConcl)) (clearer id) in + let subst_hyp l2r id = + tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id))) + (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC)) + in let substHypIfVariable tac id gls = let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in match (kind_of_term t1, kind_of_term t2) with - | Var id1, _ -> generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls - | _, Var id2 -> generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls - | _ -> tac id gls + | Var id1, _ -> generalizeRewriteIntros (subst_hyp true id) depids id1 gls + | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2 gls + | _ -> tac id gls in let deq_trailer id neqns = tclTHENSEQ @@ -326,7 +323,7 @@ let projectAndApply thin id eqname names depids gls = (intro_move idopt None) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) - (tclTRY (onLastHyp (substHypIfVariable subst_hyp_RL)))) + (tclTRY (onLastHyp (substHypIfVariable (subst_hyp false))))) names); (if names = [] then clear [id] else tclIDTAC)] in @@ -380,6 +377,8 @@ let rewrite_equations_gene othin neqns ba gl = let rec get_names allow_conj = function | IntroWildcard -> error "Discarding pattern not allowed for inversion equations" + | IntroAnonymous -> + error "Anonymous pattern not allowed for inversion equations" | IntroOrAndPattern [l] -> if allow_conj then if l = [] then (None,[]) else @@ -401,7 +400,6 @@ let rewrite_equations othin neqns names ba gl = let (depids,nodepids) = split_dep_and_nodep ba.assums gl in let rewrite_eqns = let first_eq = ref None in - let update id = if !first_eq = None then first_eq := Some id in match othin with | Some thin -> tclTHENSEQ @@ -446,12 +444,11 @@ let rewrite_equations_tac (gene, othin) id neqns names ba = let raw_inversion inv_kind indbinding id status names gl = let env = pf_env gl and sigma = project gl in let c = mkVar id in - let (wc,kONT) = startWalk gl in let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in - let indclause = mk_clenv_from wc (c,t) in + let indclause = mk_clenv_from gl (c,t) in let indclause' = clenv_constrain_with_bindings indbinding indclause in - let newc = clenv_instance_template indclause' in - let ccl = clenv_instance_template_type indclause' in + let newc = clenv_value indclause' in + let ccl = clenv_type indclause' in check_no_metas indclause' ccl; let IndType (indf,realargs) = try find_rectype env sigma ccl @@ -477,7 +474,7 @@ let raw_inversion inv_kind indbinding id status names gl = (fun id -> (tclTHEN (apply_term (mkVar id) - (list_tabulate (fun _ -> mkMeta(Clenv.new_meta())) neqns)) + (list_tabulate (fun _ -> Evarutil.mk_new_meta()) neqns)) reflexivity))]) gl @@ -524,15 +521,15 @@ open Tacexpr let inv k = inv_gen false k NoDep -let half_inv_tac id = inv SimpleInversion None (NamedHyp id) -let inv_tac id = inv FullInversion None (NamedHyp id) -let inv_clear_tac id = inv FullInversionClear None (NamedHyp id) +let half_inv_tac id = inv SimpleInversion IntroAnonymous (NamedHyp id) +let inv_tac id = inv FullInversion IntroAnonymous (NamedHyp id) +let inv_clear_tac id = inv FullInversionClear IntroAnonymous (NamedHyp id) let dinv k c = inv_gen false k (Dep c) -let half_dinv_tac id = dinv SimpleInversion None None (NamedHyp id) -let dinv_tac id = dinv FullInversion None None (NamedHyp id) -let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) +let half_dinv_tac id = dinv SimpleInversion None IntroAnonymous (NamedHyp id) +let dinv_tac id = dinv FullInversion None IntroAnonymous (NamedHyp id) +let dinv_clear_tac id = dinv FullInversionClear None IntroAnonymous (NamedHyp id) (* InvIn will bring the specified clauses into the conclusion, and then * perform inversion on the named hypothesis. After, it will intro them |