diff options
| -rw-r--r-- | tactics/equality.ml | 73 | ||||
| -rw-r--r-- | tactics/tactics.ml | 11 | ||||
| -rw-r--r-- | tactics/tactics.mli | 9 |
3 files changed, 75 insertions, 18 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 99216a127d..0b3bf54bfa 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -54,23 +54,66 @@ open Evd -- Eduardo (19/8/97) *) +let rewrite_unif_flags = { + Unification.modulo_conv_on_closed_terms = None; + Unification.use_metas_eagerly = true; + Unification.modulo_delta = empty_transparent_state; + Unification.resolve_evars = true; +} + +let instantiate_lemma env sigma gl c ty l l2r concl = + let eqclause = Clenv.make_clenv_binding { gl with sigma = sigma } (c,ty) l in + let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in + let rec split_last_two = function + | [c1;c2] -> [],(c1, c2) + | x::y::z -> + let l,res = split_last_two (y::z) in x::l, res + | _ -> error "The term provided is not an applied relation." in + let others,(c1,c2) = split_last_two args in + let evd', c' = + Unification.w_unify_to_subterm ~flags:rewrite_unif_flags env + ((if l2r then c1 else c2),concl) eqclause.evd + in + let cl' = {eqclause with evd = evd'} in + let cl' = + let mvs = clenv_dependent false cl' in + clenv_pose_metas_as_evars cl' mvs + in cl' + +let instantiate_lemma env sigma gl c ty l l2r concl = + let gl = { gl with sigma = sigma } in + let ct = pf_type_of gl c in + let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in + let eqclause = Clenv.make_clenv_binding gl (c,t) l in + eqclause + +let rewrite_elim with_evars c e ?(allow_K=true) = + general_elim_clause_gen (elimination_clause_scheme with_evars allow_K) c e + +let rewrite_elim_in with_evars id c e = + general_elim_clause_gen (elimination_in_clause_scheme with_evars id) c e + (* Ad hoc asymmetric general_elim_clause *) -let general_elim_clause with_evars cls sigma c l elim = +let general_elim_clause with_evars cls rew elim = try (match cls with | None -> (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal and did not fail for useless conditional rewritings generating an extra condition *) - tclNOTSAMEGOAL (tclTHEN (Refiner.tclEVARS sigma) - (general_elim with_evars (c,l) elim ~allow_K:false)) - | Some id -> - tclTHEN (Refiner.tclEVARS sigma) (general_elim_in with_evars id (c,l) elim)) + tclNOTSAMEGOAL (rewrite_elim with_evars rew elim ~allow_K:false) + | Some id -> rewrite_elim_in with_evars id rew elim) with Pretype_errors.PretypeError (env, (Pretype_errors.NoOccurrenceFound (c', _))) -> raise (Pretype_errors.PretypeError (env, (Pretype_errors.NoOccurrenceFound (c', cls)))) - + +let general_elim_clause with_evars cls sigma c t l l2r elim gl = + let c = instantiate_lemma (pf_env gl) sigma gl c t l l2r + (match cls with None -> pf_concl gl | Some id -> pf_get_hyp_typ gl id) + in + tclTHEN (Refiner.tclEVARS c.evd) (general_elim_clause with_evars cls c elim) gl + (* The next function decides in particular whether to try a regular rewrite or a setoid rewrite. Approach is to break everything, if [eq] appears in head position @@ -94,9 +137,9 @@ let find_elim hdcncl lft2rgt cls gl = try pf_global gl (id_of_string rwr_thm) with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".") -let leibniz_rewrite_ebindings_clause cls lft2rgt sigma c l with_evars gl hdcncl = +let leibniz_rewrite_ebindings_clause cls lft2rgt sigma c t l with_evars gl hdcncl = let elim = find_elim hdcncl lft2rgt cls gl in - general_elim_clause with_evars cls sigma c l (elim,NoBindings) gl + general_elim_clause with_evars cls sigma c t l lft2rgt (elim,NoBindings) gl let adjust_rewriting_direction args lft2rgt = if List.length args = 1 then @@ -115,21 +158,23 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_ let sigma, c' = c in let sigma = Evd.merge sigma (project gl) in let ctype = get_type_of env sigma c' in - let rels, t = decompose_prod (whd_betaiotazeta sigma ctype) in + let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in match match_with_equality_type t with | Some (hdcncl,args) -> (* Fast path: direct leibniz rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in - leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl + leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' (it_mkProd_or_LetIn t rels) + l with_evars gl hdcncl | None -> - let env' = List.fold_left (fun env (n,t) -> push_rel (n, None, t) env) env rels in - let _,t' = splay_prod env' sigma t in (* Search for underlying eq *) + let env' = push_rel_context rels env in + let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) match match_with_equality_type t' with | Some (hdcncl,args) -> (* Maybe a setoid relation with eq inside *) let lft2rgt = adjust_rewriting_direction args lft2rgt in if l = NoBindings && !is_applied_setoid_relation t then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl else - (try leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl + (try leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' + (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars gl hdcncl with e -> try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl with _ -> raise e) @@ -886,7 +931,7 @@ let injEq ipats (eq,(t,t1,t2)) eq_clause = errorlabstrm "Equality.inj" (str"Nothing to do, it is an equality between convertible terms.") | Inr posns -> -(* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ? +(* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ? let t1 = try_delta_expand env sigma t1 in let t2 = try_delta_expand env sigma t2 in *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0452a9ed88..a87ea90ff9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -690,7 +690,7 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl = | _ -> errorlabstrm "elimination_clause" (str "The type of elimination clause is not well-formed.")) in - let elimclause' = clenv_fchain indmv elimclause indclause in + let elimclause' = clenv_fchain ~flags:elim_flags indmv elimclause indclause in res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags gl @@ -702,13 +702,16 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl = * matching I, lbindc are the expected terms for c arguments *) +let general_elim_clause_gen elimtac indclause (elimc,lbindelimc) gl = + let elimt = pf_type_of gl elimc in + let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in + elimtac elimclause indclause gl + let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl = let ct = pf_type_of gl c in let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in let indclause = make_clenv_binding gl (c,t) lbindc in - let elimt = pf_type_of gl elimc in - let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in - elimtac elimclause indclause gl + general_elim_clause_gen elimtac indclause (elimc,lbindelimc) gl let general_elim with_evars c e ?(allow_K=true) = general_elim_clause (elimination_clause_scheme with_evars allow_K) c e diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 136833ad78..355380a74c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -248,6 +248,15 @@ type elim_scheme = { val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme val rebuild_elimtype_from_scheme: elim_scheme -> types +val elimination_clause_scheme : evars_flag -> + bool -> clausenv -> clausenv -> tactic + +val elimination_in_clause_scheme : evars_flag -> identifier -> + clausenv -> clausenv -> tactic + +val general_elim_clause_gen : (Clenv.clausenv -> 'a -> tactic) -> + 'a -> constr * open_constr bindings -> tactic + val general_elim : evars_flag -> constr with_ebindings -> constr with_ebindings -> ?allow_K:bool -> tactic val general_elim_in : evars_flag -> |