diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 102 |
1 files changed, 52 insertions, 50 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index af204e77..86641114 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inv.ml 12410 2009-10-24 17:23:39Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -14,6 +14,7 @@ open Names open Nameops open Term open Termops +open Namegen open Global open Sign open Environ @@ -37,21 +38,22 @@ open Rawterm open Genarg open Tacexpr -let collect_meta_variables c = +let collect_meta_variables c = let rec collrec acc c = match kind_of_term c with | Meta mv -> mv::acc | _ -> fold_constr collrec acc c - in + in collrec [] c let check_no_metas clenv ccl = if occur_meta ccl then - let metas = List.filter (fun na -> na<>Anonymous) - (List.map (Evd.meta_name clenv.evd) (collect_meta_variables ccl)) in - errorlabstrm "inversion" + let metas = List.filter (fun m -> not (Evd.meta_defined clenv.evd m)) + (collect_meta_variables ccl) in + let metas = List.map (Evd.meta_name clenv.evd) metas in + errorlabstrm "inversion" (str ("Cannot find an instantiation for variable"^ (if List.length metas = 1 then " " else "s ")) ++ - prlist_with_sep pr_coma pr_name metas + prlist_with_sep pr_comma pr_name metas (* ajouter "in " ++ pr_lconstr ccl mais il faut le bon contexte *)) let var_occurs_in_pf gl id = @@ -60,7 +62,7 @@ let var_occurs_in_pf gl id = List.exists (occur_var_in_decl env id) (pf_hyps gl) (* [make_inv_predicate (ity,args) C] - + is given the inductive type, its arguments, both the global parameters and its local arguments, and is expected to produce a predicate P such that if largs is the "local" part of the @@ -127,16 +129,16 @@ let make_inv_predicate env sigma indf realargs id status concl = push <Ai>(mkRel k)=ai (when Ai is closed). In any case, we carry along the rest of pairs *) let rec build_concl eqns n = function - | [] -> (prod_it concl eqns,n) + | [] -> (it_mkProd concl eqns,n) | (ai,(xi,ti))::restlist -> let (lhs,eqnty,rhs) = - if closed0 ti then + if closed0 ti then (xi,ti,ai) - else + else make_iterated_tuple env' sigma ai (xi,ti) in let eq_term = Coqlib.build_coq_eq () in - let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in + let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist in let (newconcl,neqns) = build_concl [] 0 pairs in @@ -188,21 +190,21 @@ let make_inv_predicate env sigma indf realargs id status concl = it generalizes them, applies tac to rewrite all occurrencies of t, and introduces generalized hypotheis. Precondition: t=(mkVar id) *) - -let rec dependent_hyps id idlist gl = + +let rec dependent_hyps id idlist gl = let rec dep_rec =function | [] -> [] - | (id1,_,_)::l -> + | (id1,_,_)::l -> (* Update the type of id1: it may have been subject to rewriting *) let d = pf_get_hyp gl id1 in if occur_var_in_decl (Global.env()) id d then d :: dep_rec l else dep_rec l - in - dep_rec idlist + in + dep_rec idlist let split_dep_and_nodep hyps gl = - List.fold_right + List.fold_right (fun (id,_,_ as d) (l1,l2) -> if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2)) hyps ([],[]) @@ -280,17 +282,17 @@ Summary: nine useless hypotheses! Nota: with Inversion_clear, only four useless hypotheses *) -let generalizeRewriteIntros tac depids id gls = +let generalizeRewriteIntros tac depids id gls = let dids = dependent_hyps id depids gls in (tclTHENSEQ - [bring_hyps dids; tac; + [bring_hyps dids; tac; (* may actually fail to replace if dependent in a previous eq *) intros_replacing (ids_of_named_context dids)]) gls let rec tclMAP_i n tacfun = function | [] -> tclDO n (tacfun None) - | a::l -> + | a::l -> if n=0 then error "Too many names." else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l) @@ -317,14 +319,14 @@ let projectAndApply thin id eqname names depids gls = | _ -> tac id gls in let deq_trailer id neqns = - tclTHENSEQ + tclTHENSEQ [(if names <> [] then clear [id] else tclIDTAC); (tclMAP_i neqns (fun idopt -> - tclTHEN + tclTRY (tclTHEN (intro_move idopt no_move) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) - (tclTRY (onLastHyp (substHypIfVariable (subst_hyp false))))) + (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false)))))) names); (if names = [] then clear [id] else tclIDTAC)] in @@ -342,14 +344,14 @@ let rewrite_equations_gene othin neqns ba gl = let rewrite_eqns = match othin with | Some thin -> - onLastHyp + onLastHypId (fun last -> tclTHENSEQ [tclDO neqns (tclTHEN intro - (onLastHyp + (onLastHypId (fun id -> - tclTRY + tclTRY (projectAndApply thin id (ref no_move) [] depids)))); onHyps (compose List.rev (afterHyp last)) bring_hyps; @@ -361,8 +363,8 @@ let rewrite_equations_gene othin neqns ba gl = [tclDO neqns intro; bring_hyps nodepids; clear (ids_of_named_context nodepids); - onHyps (compose List.rev (nLastHyps neqns)) bring_hyps; - onHyps (nLastHyps neqns) (compose clear ids_of_named_context); + onHyps (compose List.rev (nLastDecls neqns)) bring_hyps; + onHyps (nLastDecls neqns) (compose clear ids_of_named_context); rewrite_eqns; tclMAP (fun (id,_,_ as d) -> (tclORELSE (clear [id]) @@ -378,13 +380,13 @@ let rewrite_equations_gene othin neqns ba gl = let rec get_names allow_conj (loc,pat) = match pat with | IntroWildcard -> error "Discarding pattern not allowed for inversion equations." - | IntroAnonymous -> + | IntroAnonymous | IntroForthcoming _ -> error "Anonymous pattern not allowed for inversion equations." | IntroFresh _ -> error "Fresh pattern not allowed for inversion equations." | IntroRewrite _-> error "Rewriting pattern not allowed for inversion equations." - | IntroOrAndPattern [l] -> + | IntroOrAndPattern [l] -> if allow_conj then if l = [] then (None,[]) else let l = List.map (fun id -> Option.get (fst (get_names false id))) l in @@ -408,13 +410,13 @@ let rewrite_equations othin neqns names ba gl = match othin with | Some thin -> tclTHENSEQ - [onHyps (compose List.rev (nLastHyps neqns)) bring_hyps; - onHyps (nLastHyps neqns) (compose clear ids_of_named_context); + [onHyps (compose List.rev (nLastDecls neqns)) bring_hyps; + onHyps (nLastDecls neqns) (compose clear ids_of_named_context); tclMAP_i neqns (fun o -> let idopt,names = extract_eqn_names o in (tclTHEN (intro_move idopt no_move) - (onLastHyp (fun id -> + (onLastHypId (fun id -> tclTRY (projectAndApply thin id first_eq names depids))))) names; tclMAP (fun (id,_,_) gl -> @@ -440,18 +442,18 @@ let rewrite_equations_tac (gene, othin) id neqns names ba = let tac = if gene then rewrite_equations_gene othin neqns ba else rewrite_equations othin neqns names ba in - if othin = Some true (* if Inversion_clear, clear the hypothesis *) then + if othin = Some true (* if Inversion_clear, clear the hypothesis *) then tclTHEN tac (tclTRY (clear [id])) - else + else tac let raw_inversion inv_kind id status names gl = let env = pf_env gl and sigma = project gl in let c = mkVar id in - let (ind,t) = + let (ind,t) = try pf_reduce_to_atomic_ind gl (pf_type_of gl c) - with UserError _ -> + with UserError _ -> errorlabstrm "raw_inversion" (str ("The type of "^(string_of_id id)^" is not inductive.")) in let indclause = mk_clenv_from gl (c,t) in @@ -461,19 +463,19 @@ let raw_inversion inv_kind id status names gl = let (elim_predicate,neqns) = make_inv_predicate env sigma indf realargs id status (pf_concl gl) in let (cut_concl,case_tac) = - if status <> NoDep & (dependent c (pf_concl gl)) then + if status <> NoDep & (dependent c (pf_concl gl)) then Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])), - case_then_using - else + case_then_using + else Reduction.beta_appvect elim_predicate (Array.of_list realargs), - case_nodep_then_using + case_nodep_then_using in (tclTHENS (assert_tac Anonymous cut_concl) - [case_tac names + [case_tac names (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) (Some elim_predicate) ([],[]) ind indclause; - onLastHyp + onLastHypId (fun id -> (tclTHEN (apply_term (mkVar id) @@ -487,7 +489,7 @@ let wrap_inv_error id = function (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> errorlabstrm "" (strbrk "Inversion would require case analysis on sort " ++ - pr_sort k ++ + pr_sort k ++ strbrk " which is not allowed for inductive definition " ++ pr_inductive (Global.env()) i ++ str ".") | e -> raise e @@ -526,16 +528,16 @@ let invIn k names ids id gls = let intros_replace_ids gls = let nb_of_new_hyp = nb_prod (pf_concl gls) - (List.length hyps + nb_prod_init) - in - if nb_of_new_hyp < 1 then + in + if nb_of_new_hyp < 1 then intros_replacing ids gls - else + else tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) gls in - try + try (tclTHENSEQ [bring_hyps hyps; - inversion (false,k) NoDep names id; + inversion (false,k) NoDep names id; intros_replace_ids]) gls with e -> wrap_inv_error id e |