diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hiddentac.ml | 3 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 55 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 |
5 files changed, 46 insertions, 21 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index f5c54a5336..60f1ccf0ca 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -83,7 +83,7 @@ let h_new_induction ev c e idl = let h_new_destruct ev c e idl = abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) (new_destruct ev c e idl) -let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d) +let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d) let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) (* Context management *) @@ -94,6 +94,7 @@ let h_move dep id1 id2 = abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2) let h_rename l = abstract_tactic (TacRename l) (rename_hyp l) +let h_revert l = abstract_tactic (TacRevert l) (revert l) (* Constructors *) let h_left l = abstract_tactic (TacLeft l) (left_with_ebindings l) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 87232988b8..909d294cf6 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -76,7 +76,7 @@ val h_clear : bool -> identifier list -> tactic val h_clear_body : identifier list -> tactic val h_move : bool -> identifier -> identifier -> tactic val h_rename : (identifier*identifier) list -> tactic - +val h_revert : identifier list -> tactic (* Constructors *) val h_constructor : int -> open_constr bindings -> tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3245c31c7e..821586e7f0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -718,6 +718,7 @@ let rec intern_atomic lf ist x = TacRename (List.map (fun (id1,id2) -> intern_hyp_or_metaid ist id1, intern_hyp_or_metaid ist id2) l) + | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l) (* Constructors *) | TacLeft bl -> TacLeft (intern_bindings ist bl) @@ -2079,6 +2080,7 @@ and interp_atomic ist gl = function h_rename (List.map (fun (id1,id2) -> interp_hyp ist gl id1, interp_fresh_ident ist gl (snd id2)) l) + | TacRevert l -> h_revert (interp_hyp_list ist gl l) (* Constructors *) | TacLeft bl -> h_left (interp_bindings ist gl bl) @@ -2386,6 +2388,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacClearBody l as x -> x | TacMove (dep,id1,id2) as x -> x | TacRename l as x -> x + | TacRevert _ as x -> x (* Constructors *) | TacLeft bl -> TacLeft (subst_bindings subst bl) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6119185438..5f919a4dbe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -725,25 +725,41 @@ let rec intros_clearing = function tclTHENLIST [ intro; onLastHyp (fun id -> clear [id]); intros_clearing tl] -(* Adding new hypotheses *) - -let new_hyp mopt (c,lbind) g = - let clause = make_clenv_binding g (c,pf_type_of g c) lbind in - let clause = clenv_unify_meta_types clause in - let (thd,tstack) = whd_stack (clenv_value clause) in - let nargs = List.length tstack in - let cut_pf = - applist(thd, - match mopt with - | Some m -> if m < nargs then list_firstn m tstack else tstack - | None -> tstack) +(* Modifying/Adding an hypothesis *) + +let specialize mopt (c,lbind) g = + let evars, term = + if lbind = NoBindings then None, c + else + let clause = make_clenv_binding g (c,pf_type_of g c) lbind in + let clause = clenv_unify_meta_types clause in + let (thd,tstack) = whd_stack (clenv_value clause) in + let nargs = List.length tstack in + let tstack = match mopt with + | Some m -> + if m < nargs then list_firstn m tstack else tstack + | None -> + let rec chk = function + | [] -> [] + | t::l -> if occur_meta t then [] else t :: chk l + in chk tstack + in + let term = applist(thd,tstack) in + if occur_meta term then + errorlabstrm "" (str "Cannot infer an instance for " ++ + pr_name (meta_name clause.evd (List.hd (collect_metas term)))); + Some (evars_of clause.evd), term in - if occur_meta cut_pf then - errorlabstrm "" (str "Cannot infer an instance for " ++ - pr_name (meta_name clause.evd (List.hd (collect_metas cut_pf)))); - (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.evd)) - (cut (pf_type_of g cut_pf))) - ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g + tclTHEN + (match evars with Some e -> tclEVARS e | _ -> tclIDTAC) + (match kind_of_term (fst (decompose_app c)) with + | Var id when List.exists (fun (i,_,_)-> i=id) (pf_hyps g) -> + let id' = fresh_id [] id g in + tclTHENS (internal_cut id' (pf_type_of g term)) + [ exact_no_check term; + tclTHEN (clear [id]) (rename_hyp [id',id]) ] + | _ -> tclTHENLAST (cut (pf_type_of g term)) (exact_no_check term)) + g (* Keeping only a few hypotheses *) @@ -1084,6 +1100,9 @@ let generalize lconstr gl = let newcl = List.fold_right (generalize_goal gl) lconstr (pf_concl gl) in apply_type newcl lconstr gl +let revert hyps gl = + tclTHEN (generalize (List.map mkVar hyps)) (clear hyps) gl + (* Faudra-t-il une version avec plusieurs args de generalize_dep ? Cela peut-être troublant de faire "Generalize Dependent H n" dans "n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la diff --git a/tactics/tactics.mli b/tactics/tactics.mli index eb62f602aa..3a3bf6de51 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -156,11 +156,13 @@ val clear : identifier list -> tactic val clear_body : identifier list -> tactic val keep : identifier list -> tactic -val new_hyp : int option -> constr with_ebindings -> tactic +val specialize : int option -> constr with_ebindings -> tactic val move_hyp : bool -> identifier -> identifier -> tactic val rename_hyp : (identifier * identifier) list -> tactic +val revert : identifier list -> tactic + (*s Resolution tactics. *) val apply_type : constr -> constr list -> tactic |