diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/evar_tactics.ml | 1 | ||||
| -rw-r--r-- | tactics/extraargs.ml4 | 80 | ||||
| -rw-r--r-- | tactics/extraargs.mli | 16 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 13 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 12 |
6 files changed, 124 insertions, 6 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 7efa9299e..140deb3a9 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -25,6 +25,7 @@ let evars_of evc c = | _ -> fold_constr evrec acc c in evrec [] c + let instantiate n rawc ido gl = let wc = Refiner.project_with_focus gl in let evl = diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 4aace33dc..3fbd27c60 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -13,6 +13,9 @@ open Pp open Pcoq open Genarg +open Names +open Tacexpr +open Tacinterp (* Rewriting orientation *) @@ -23,9 +26,86 @@ let pr_orient _prc _prt = function | true -> Pp.mt () | false -> Pp.str " <-" + ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient | [ "->" ] -> [ true ] | [ "<-" ] -> [ false ] | [ ] -> [ true ] END + +let pr_gen prc _ c = prc c + +let pr_rawc _ _ raw = Ppconstr.pr_rawconstr raw + +let interp_raw _ _ (t,_) = t + +let glob_raw ist a = Tacinterp.intern_constr ist a + +let subst_raw subst arawc = Tacinterp.subst_rawconstr subst arawc + +ARGUMENT EXTEND raw + TYPED AS rawconstr + PRINTED BY pr_rawc + + INTERPRETED BY interp_raw + GLOBALIZED BY glob_raw + SUBSTITUTED BY subst_raw + + RAW_TYPED AS constr_expr + RAW_PRINTED BY pr_gen + + GLOB_TYPED AS rawconstr_and_expr + GLOB_PRINTED BY pr_gen + + [ constr(c) ] -> [ c ] + +END + +type 'id gen_place= ('id * hyp_location_flag,unit) location + +type loc_place = identifier Util.located gen_place +type place = identifier gen_place + +let pr_gen_place pr_id = function + ConclLocation () -> Pp.mt () + | HypLocation (id,InHyp) -> str "in " ++ pr_id id + | HypLocation (id,InHypTypeOnly) -> + str "in (Type of " ++ pr_id id ++ str ")" + | HypLocation (id,InHypValueOnly) -> + str "in (Value of " ++ pr_id id ++ str ")" + +let pr_loc_place _ _ = pr_gen_place (fun (_,id) -> Nameops.pr_id id) +let pr_place _ _ = pr_gen_place Nameops.pr_id + +let intern_place ist = function + ConclLocation () -> ConclLocation () + | HypLocation (id,hl) -> HypLocation (intern_hyp ist id,hl) + +let interp_place ist gl = function + ConclLocation () -> ConclLocation () + | HypLocation (id,hl) -> HypLocation (interp_hyp ist gl id,hl) + +let subst_place subst pl = pl + +ARGUMENT EXTEND hloc + TYPED AS place + PRINTED BY pr_place + INTERPRETED BY interp_place + GLOBALIZED BY intern_place + SUBSTITUTED BY subst_place + RAW_TYPED AS loc_place + RAW_PRINTED BY pr_loc_place + GLOB_TYPED AS loc_place + GLOB_PRINTED BY pr_loc_place + [ ] -> + [ ConclLocation () ] +| [ "in" ident(id) ] -> + [ HypLocation ((Util.dummy_loc,id),InHyp) ] +| [ "in" "(" "Type" "of" ident(id) ")" ] -> + [ HypLocation ((Util.dummy_loc,id),InHypTypeOnly) ] +| [ "in" "(" "Value" "of" ident(id) ")" ] -> + [ HypLocation ((Util.dummy_loc,id),InHypValueOnly) ] + + END + diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 3e0099010..a6ab2ed8b 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -10,9 +10,25 @@ open Tacexpr open Term +open Names open Proof_type open Topconstr +open Rawterm val rawwit_orient : bool raw_abstract_argument_type val wit_orient : bool closed_abstract_argument_type val orient : bool Pcoq.Gram.Entry.e + +val rawwit_raw : constr_expr raw_abstract_argument_type +val wit_raw : rawconstr closed_abstract_argument_type +val raw : constr_expr Pcoq.Gram.Entry.e + +type 'id gen_place= ('id * hyp_location_flag,unit) location + +type loc_place = identifier Util.located gen_place +type place = identifier gen_place + +val rawwit_hloc : loc_place raw_abstract_argument_type +val wit_hloc : place closed_abstract_argument_type +val hloc : loc_place Pcoq.Gram.Entry.e + diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e55df2bf1..65bed9007 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -242,6 +242,14 @@ TACTIC EXTEND Evar [ let_evar Names.Anonymous typ ] END +open Tacexpr + +TACTIC EXTEND Instantiate + [ "Instantiate" "(" integer(i) ":=" raw(c) ")" hloc(hl) ] -> + [ instantiate i c hl ] +END + + (** Nijmegen "step" tactic for setoid rewriting *) open Tacticals diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2b2f39e1e..4a395fa31 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -663,12 +663,13 @@ let rec intern_atomic lf ist x = let na = intern_name lf ist na in TacLetTac (na,intern_constr ist c, (clause_app (intern_hyp_location ist) cls)) - | TacInstantiate (n,c,idh) -> +(* | TacInstantiate (n,c,idh) -> TacInstantiate (n,intern_constr ist c, (match idh with ConclLocation () -> ConclLocation () | HypLocation (id,hloc) -> - HypLocation(intern_hyp_or_metaid ist id,hloc))) + HypLocation(intern_hyp_or_metaid ist id,hloc))) +*) (* Automation tactics *) | TacTrivial l -> TacTrivial l @@ -1717,13 +1718,13 @@ and interp_atomic ist gl = function | TacLetTac (na,c,clp) -> let clp = interp_clause ist gl clp in h_let_tac (interp_name ist na) (pf_interp_constr ist gl c) clp - | TacInstantiate (n,c,idh) -> h_instantiate n (fst c) +(* | TacInstantiate (n,c,idh) -> h_instantiate n (fst c) (* pf_interp_constr ist gl c *) (match idh with ConclLocation () -> ConclLocation () | HypLocation (id,hloc) -> HypLocation(interp_hyp ist gl id,hloc)) - +*) (* Automation tactics *) | TacTrivial l -> Auto.h_trivial l | TacAuto (n, l) -> Auto.h_auto n l @@ -1976,8 +1977,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl) | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c) | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp) - | TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido) - +(*| TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido) +*) (* Automation tactics *) | TacTrivial l -> TacTrivial l | TacAuto (n,l) -> TacAuto (n,l) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 49af044c5..88cdf43c5 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -87,9 +87,18 @@ val interp_genarg : val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument +val intern_constr : + glob_sign -> constr_expr -> rawconstr_and_expr + +val intern_hyp : + glob_sign -> identifier Util.located -> identifier Util.located + val subst_genarg : Names.substitution -> glob_generic_argument -> glob_generic_argument +val subst_rawconstr : + Names.substitution -> rawconstr_and_expr -> rawconstr_and_expr + (* Interprets any expression *) val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value @@ -101,6 +110,9 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr val interp_tac_gen : (identifier * value) list -> debug_info -> raw_tactic_expr -> tactic +val interp_hyp : interp_sign -> goal sigma -> + identifier Util.located -> identifier + (* Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr |