diff options
author | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-02 02:21:53 +0000 |
---|---|---|
committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-02 02:21:53 +0000 |
commit | 413dfbee3dba16c3d2653b61f7372349a0d3c078 (patch) | |
tree | e7c9621cc500cd9a537380ed3c3881cb1d7fdebf | |
parent | 03cf2f56231587f98ced95091930696635ef6b50 (diff) |
Portage d'AutoRewrite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1043 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend | 70 | ||||
-rw-r--r-- | CHANGES | 3 | ||||
-rw-r--r-- | Makefile | 4 | ||||
-rw-r--r-- | TODO | 5 | ||||
-rw-r--r-- | proofs/proof_trees.ml | 2 | ||||
-rw-r--r-- | proofs/proof_type.ml | 2 | ||||
-rw-r--r-- | proofs/proof_type.mli | 2 | ||||
-rw-r--r-- | proofs/refiner.ml | 13 | ||||
-rw-r--r-- | proofs/refiner.mli | 8 | ||||
-rw-r--r-- | proofs/tacinterp.ml | 2 | ||||
-rw-r--r-- | proofs/tacmach.ml | 2 | ||||
-rw-r--r-- | proofs/tacmach.mli | 2 | ||||
-rw-r--r-- | states/MakeInitial.v | 2 | ||||
-rw-r--r-- | tactics/AutoRewrite.v | 25 | ||||
-rw-r--r-- | tactics/Equality.v | 89 | ||||
-rw-r--r-- | tactics/autorewrite.ml | 120 | ||||
-rw-r--r-- | tactics/autorewrite.mli | 11 | ||||
-rw-r--r-- | tactics/equality.ml | 4 | ||||
-rw-r--r-- | tactics/tactics.ml | 4 |
19 files changed, 246 insertions, 124 deletions
@@ -779,6 +779,22 @@ proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx parsing/printer.cmx \ proofs/proof_trees.cmx proofs/tacmach.cmx proofs/tactic_debug.cmi +proofs/toto.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \ + parsing/coqast.cmi library/declare.cmi lib/dyn.cmi kernel/environ.cmi \ + kernel/evd.cmi lib/gmap.cmi library/lib.cmi library/libobject.cmi \ + kernel/names.cmi library/nametab.cmi lib/options.cmi parsing/pattern.cmi \ + lib/pp.cmi pretyping/pretype_errors.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi kernel/sign.cmi library/summary.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \ + kernel/term.cmi pretyping/typing.cmi lib/util.cmi +proofs/toto.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \ + parsing/coqast.cmx library/declare.cmx lib/dyn.cmx kernel/environ.cmx \ + kernel/evd.cmx lib/gmap.cmx library/lib.cmx library/libobject.cmx \ + kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pattern.cmx \ + lib/pp.cmx pretyping/pretype_errors.cmx proofs/proof_type.cmx \ + pretyping/rawterm.cmx kernel/sign.cmx library/summary.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \ + kernel/term.cmx pretyping/typing.cmx lib/util.cmx scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo @@ -805,6 +821,20 @@ tactics/auto.cmx: parsing/astterm.cmx tactics/btermdn.cmx proofs/clenv.cmx \ pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \ kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx tactics/auto.cmi +tactics/autorewrite.cmo: parsing/ast.cmi toplevel/command.cmi \ + parsing/coqast.cmi tactics/equality.cmi tactics/hipattern.cmi \ + library/lib.cmi library/libobject.cmi kernel/names.cmi lib/pp.cmi \ + proofs/proof_type.cmi library/summary.cmi proofs/tacinterp.cmi \ + proofs/tacmach.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \ + kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + tactics/autorewrite.cmi +tactics/autorewrite.cmx: parsing/ast.cmx toplevel/command.cmx \ + parsing/coqast.cmx tactics/equality.cmx tactics/hipattern.cmx \ + library/lib.cmx library/libobject.cmx kernel/names.cmx lib/pp.cmx \ + proofs/proof_type.cmx library/summary.cmx proofs/tacinterp.cmx \ + proofs/tacmach.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \ + kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + tactics/autorewrite.cmi tactics/btermdn.cmo: tactics/dn.cmi parsing/pattern.cmi kernel/term.cmi \ tactics/termdn.cmi tactics/btermdn.cmi tactics/btermdn.cmx: tactics/dn.cmx parsing/pattern.cmx kernel/term.cmx \ @@ -853,22 +883,20 @@ tactics/equality.cmo: parsing/astterm.cmi parsing/coqast.cmi \ kernel/instantiate.cmi library/lib.cmi library/libobject.cmi \ proofs/logic.cmi kernel/names.cmi parsing/pattern.cmi lib/pp.cmi \ proofs/proof_type.cmi kernel/reduction.cmi pretyping/retyping.cmi \ - library/summary.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ - pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi kernel/typeops.cmi pretyping/typing.cmi kernel/univ.cmi \ - lib/util.cmi toplevel/vernacinterp.cmi tactics/wcclausenv.cmi \ - tactics/equality.cmi + proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ + kernel/typeops.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi tactics/wcclausenv.cmi tactics/equality.cmi tactics/equality.cmx: parsing/astterm.cmx parsing/coqast.cmx \ library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \ lib/gmapl.cmx tactics/hipattern.cmx kernel/inductive.cmx \ kernel/instantiate.cmx library/lib.cmx library/libobject.cmx \ proofs/logic.cmx kernel/names.cmx parsing/pattern.cmx lib/pp.cmx \ proofs/proof_type.cmx kernel/reduction.cmx pretyping/retyping.cmx \ - library/summary.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ - pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx \ - lib/util.cmx toplevel/vernacinterp.cmx tactics/wcclausenv.cmx \ - tactics/equality.cmi + proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ + kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx tactics/wcclausenv.cmx tactics/equality.cmi tactics/hiddentac.cmo: proofs/proof_type.cmi tactics/tacentries.cmi \ proofs/tacmach.cmi kernel/term.cmi tactics/hiddentac.cmi tactics/hiddentac.cmx: proofs/proof_type.cmx tactics/tacentries.cmx \ @@ -994,13 +1022,15 @@ tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \ library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \ kernel/inductive.cmi kernel/instantiate.cmi library/lib.cmi \ - kernel/names.cmi lib/pp.cmi pretyping/retyping.cmi kernel/sign.cmi \ - kernel/term.cmi pretyping/typing.cmi lib/util.cmi toplevel/class.cmi + kernel/names.cmi lib/pp.cmi kernel/reduction.cmi pretyping/retyping.cmi \ + kernel/sign.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/class.cmi toplevel/class.cmx: pretyping/classops.cmx kernel/declarations.cmx \ library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \ kernel/inductive.cmx kernel/instantiate.cmx library/lib.cmx \ - kernel/names.cmx lib/pp.cmx pretyping/retyping.cmx kernel/sign.cmx \ - kernel/term.cmx pretyping/typing.cmx lib/util.cmx toplevel/class.cmi + kernel/names.cmx lib/pp.cmx kernel/reduction.cmx pretyping/retyping.cmx \ + kernel/sign.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/class.cmi toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ kernel/evd.cmi library/global.cmi library/indrec.cmi kernel/inductive.cmi \ @@ -1021,7 +1051,7 @@ toplevel/coqinit.cmo: config/coq_config.cmi library/library.cmi \ toplevel/mltop.cmi lib/options.cmi lib/pp.cmi lib/system.cmi \ toplevel/toplevel.cmi toplevel/vernac.cmi toplevel/coqinit.cmi toplevel/coqinit.cmx: config/coq_config.cmx library/library.cmx \ - toplevel/mltop.cmi lib/options.cmx lib/pp.cmx lib/system.cmx \ + toplevel/mltop.cmx lib/options.cmx lib/pp.cmx lib/system.cmx \ toplevel/toplevel.cmx toplevel/vernac.cmx toplevel/coqinit.cmi toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \ toplevel/errors.cmi library/lib.cmi library/library.cmi \ @@ -1030,7 +1060,7 @@ toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \ toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmi toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \ toplevel/errors.cmx library/lib.cmx library/library.cmx \ - toplevel/mltop.cmi kernel/names.cmx lib/options.cmx lib/pp.cmx \ + toplevel/mltop.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ lib/profile.cmx library/states.cmx lib/system.cmx toplevel/toplevel.cmx \ toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx toplevel/coqtop.cmi toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \ @@ -1097,6 +1127,12 @@ toplevel/minicoq.cmx: kernel/declarations.cmx toplevel/fhimsg.cmx \ parsing/g_minicoq.cmi kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \ kernel/safe_typing.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx lib/util.cmx +toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \ + lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi toplevel/mltop.cmi +toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \ + lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx toplevel/mltop.cmi toplevel/protectedtoplevel.cmo: toplevel/errors.cmi \ toplevel/line_oriented_parser.cmi parsing/pcoq.cmi lib/pp.cmi \ toplevel/vernac.cmi toplevel/vernacinterp.cmi \ @@ -1121,7 +1157,7 @@ toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi toplevel/mltop.cmi \ kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ lib/pp.cmi toplevel/protectedtoplevel.cmi lib/util.cmi \ toplevel/vernac.cmi toplevel/vernacinterp.cmi toplevel/toplevel.cmi -toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \ +toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmx \ kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \ lib/pp.cmx toplevel/protectedtoplevel.cmx lib/util.cmx \ toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi @@ -105,6 +105,9 @@ Tactiques - Unfold échoue si on lui donne en argument une définition non dépliable +- AutoRewrite ne s'occupe maintenant que du but principal et c'est les + Hint Rewrite qui gèrent les sous-buts générés + Outils - deux binaires maximum : coqtop.byte et coqtop.opt si plateforme native; @@ -118,7 +118,7 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo \ HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \ tactics/inv.cmo tactics/leminv.cmo tactics/eauto.cmo \ - tactics/refine.cmo + tactics/autorewrite.cmo tactics/refine.cmo SPECTAC=tactics/tauto.ml4 USERTAC = $(SPECTAC) @@ -229,7 +229,7 @@ theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) init: $(INITVO) TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo \ - tactics/EAuto.vo tactics/Refine.vo + tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo tactics/%.vo: tactics/%.v states/barestate.coq $(COQC) $(COQC) -$(BEST) -bindir bin -q -I tactics -is states/barestate.coq $< @@ -11,8 +11,6 @@ Environnement: Tactiques: -- Réécrire AutoRewrite avec le langage de tactiques - Noyau: - Gérer les alias avec un let in dans les cases @@ -30,6 +28,7 @@ Doc: - restriction de syntaxe pour Cbv Delta [- toto]. - documenter tactiques Induction, LetTac +- documenter AutoRewrite - Ajouter let dans les règles du CIC - changement syntaxe de AddPath - une passe sur le chapitre extensions de syntaxe @@ -38,4 +37,4 @@ Doc: - revoir le chapitre sur les tactiques utilisateur - clarifier la sémantique de Decompose (i.e. travaille pas sous les ->) - faut-il mieux spécifier la sémantique de Simpl (??) -- vérifier si Print Table id est à jour
\ No newline at end of file +- vérifier si Print Table id est à jour diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 028fe1530..dabe5cb00 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -398,7 +398,7 @@ let ast_of_cvt_arg = function (ast_of_cvt_bind (ast_of_constr false (Global.env ()))) bl) | Tacexp ast -> ope ("TACTIC",[ast]) - | Tac tac -> failwith "TODO: ast_of_cvt_arg: Tac" + | Tac (tac,ast) -> ast | Redexp red -> ope("REDEXP",[ast_of_cvt_redexp red]) | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); (num n); diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index ac1346409..e1cc05873 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -94,7 +94,7 @@ and tactic_arg = | Cbindings of constr substitution | Quoted_string of string | Tacexp of Coqast.t - | Tac of tactic + | Tac of tactic * Coqast.t | Redexp of Tacred.red_expr | Fixexp of identifier * int * Coqast.t | Cofixexp of identifier * Coqast.t diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index cc64be716..1c1b66077 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -97,7 +97,7 @@ and tactic_arg = | Cbindings of constr substitution | Quoted_string of string | Tacexp of Coqast.t - | Tac of tactic + | Tac of tactic * Coqast.t | Redexp of Tacred.red_expr | Fixexp of identifier * int * Coqast.t | Cofixexp of identifier * Coqast.t diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 53304fe37..840d24b41 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -361,9 +361,12 @@ let tclTHEN_i tac1 tac2 = tclTHENSi tac1 [] tac2;; let tclTHENS tac1 tac2l = tclTHENSi tac1 tac2l (fun _ -> tclFAIL_s "Wrong number of tactics.");; -(* Same as [tclTHENS] but completes with [Idtac] if the number resulting - subgoals is strictly less than [n] *) -let tclTHENSI tac1 tac2l = tclTHENSi tac1 tac2l (fun _ -> tclIDTAC);; +(* Same as [tclTHENS] but completes with [tac3] if the number resulting + subgoals is strictly less than [n] *) +let tclTHENST tac1 tac2l tac3 = tclTHENSi tac1 tac2l (fun _ -> tac3) + +(* Same as tclTHENST but completes with [Idtac] *) +let tclTHENSI tac1 tac2l = tclTHENST tac1 tac2l tclIDTAC (* [tclTHENL tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the last resulting subgoal *) @@ -477,6 +480,10 @@ let rec tclREPEAT t g = let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) +(* Repeat on the first subgoal *) +let rec tclREPEAT_MAIN t g = + (tclORELSE (tclTHEN_i t (fun i -> if i = 1 then (tclREPEAT_MAIN t) else + tclIDTAC)) tclIDTAC) g (*s Tactics handling a list of goals. *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 47d44a9f1..68767dc8c 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -59,8 +59,11 @@ val tclTHENL : tactic -> tactic -> tactic an error if the number of resulting subgoals is not [n] *) val tclTHENS : tactic -> tactic list -> tactic -(* Same as [tclTHENS] but completes with [Idtac] if the number resulting - subgoals is strictly less than [n] *) +(* Same as [tclTHENS] but completes with [tac3] if the number resulting + subgoals is strictly less than [n] *) +val tclTHENST : tactic -> tactic list -> tactic -> tactic + +(* Same as tclTHENST but completes with [Idtac] *) val tclTHENSI : tactic -> tactic list -> tactic (* A special exception for levels for the Fail tactic *) @@ -68,6 +71,7 @@ exception FailError of int val tclORELSE : tactic -> tactic -> tactic val tclREPEAT : tactic -> tactic +val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index e9eae9ac4..ec7082984 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -477,7 +477,7 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast = VArg (Clause (List.map (fun ast -> id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) ast))) cl)) | Node(_,"TACTIC",[ast]) -> - VArg (Tac (tac_interp lfun lmatch debug ast)) + VArg (Tac ((tac_interp lfun lmatch debug ast),ast)) (*Remains to treat*) | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) -> VArg ((Fixexp (id_of_string s,n,c))) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 481a3a616..4df69a0cd 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -206,8 +206,10 @@ let tclTHENLIST = tclTHENLIST let tclTHEN_i = tclTHEN_i let tclTHENL = tclTHENL let tclTHENS = tclTHENS +let tclTHENST = tclTHENST let tclTHENSI = tclTHENSI let tclREPEAT = tclREPEAT +let tclREPEAT_MAIN = tclREPEAT_MAIN let tclFIRST = tclFIRST let tclSOLVE = tclSOLVE let tclTRY = tclTRY diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 717c5212f..ee80beba8 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -126,8 +126,10 @@ val tclTHENLIST : tactic list -> tactic val tclTHEN_i : tactic -> (int -> tactic) -> tactic val tclTHENL : tactic -> tactic -> tactic val tclTHENS : tactic -> tactic list -> tactic +val tclTHENST : tactic -> tactic list -> tactic -> tactic val tclTHENSI : tactic -> tactic list -> tactic val tclREPEAT : tactic -> tactic +val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic diff --git a/states/MakeInitial.v b/states/MakeInitial.v index cfc3f5d2a..b8c75307a 100644 --- a/states/MakeInitial.v +++ b/states/MakeInitial.v @@ -5,5 +5,5 @@ Require Export Equality. Require Export Tauto. Require Export Inv. Require Export EAuto. +Require Export AutoRewrite. Require Export Refine. - diff --git a/tactics/AutoRewrite.v b/tactics/AutoRewrite.v new file mode 100644 index 000000000..531f4ee91 --- /dev/null +++ b/tactics/AutoRewrite.v @@ -0,0 +1,25 @@ +Declare ML Module "autorewrite". + +Grammar vernac orient : ast := +| lr ["->"] -> ["LR"] +| rl ["<-"] -> ["RL"] +| ng [] -> ["LR"] + +with vernac : ast := +| hint_rew_b [ "Hint" "Rewrite" orient($o) "[" ne_constrarg_list($l) "]" "in" + identarg($b) "."] -> [ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b) ] +| hint_rew_t [ "Hint" "Rewrite" orient($o) "[" ne_constrarg_list($l) "]" "in" + identarg($b) "using" tacarg($t) "." ] -> + [ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b (TACTIC $t)) ]. + +Grammar tactic simple_tactic : ast := +| auto_rew_b [ "AutoRewrite" "[" ne_identarg_list($l) "]" ] -> + [ (AutoRewrite ($LIST $l)) ] +| auto_rew_t [ "AutoRewrite" "[" ne_identarg_list($l) "]" "using" + tactic($t) ] -> [ (AutoRewrite (TACTIC $t) ($LIST $l)) ]. + +Syntax tactic level 0: +| auto_rew_b [<<(AutoRewrite $l)>>] -> + [ "AutoRewrite" [1 0] "[" [1 0] $l [1 0] "]" ] +| auto_rew_t [<<(AutoRewrite $t $l)>>] -> + [ "AutoRewrite" [1 0] "[" [1 0] $l [1 0] "]" [1 0] "using" [1 0] $t ]. diff --git a/tactics/Equality.v b/tactics/Equality.v index 971d1e72c..057e6f900 100644 --- a/tactics/Equality.v +++ b/tactics/Equality.v @@ -3,71 +3,6 @@ Declare ML Module "equality". -Grammar vernac orient_rule: ast := - lr ["LR"] -> [ "LR" ] - |rl ["RL"] -> [ "RL" ] -with rule_list: ast list := - single_rlt [ constrarg($com) orient_rule($ort) ] -> - [ (VERNACARGLIST $com $ort) ] - |recursive_rlt [ constrarg($com) orient_rule($ort) rule_list($tail)] -> - [ (VERNACARGLIST $com $ort) ($LIST $tail) ] -with base_list: ast list := - single_blt [identarg($rbase) "[" rule_list($rlt) "]"] -> - [ (VERNACARGLIST $rbase ($LIST $rlt)) ] - |recursive_blt [identarg($rbase) "[" rule_list($rlt) "]" - base_list($blt)] -> - [ (VERNACARGLIST $rbase ($LIST $rlt)) ($LIST $blt) ] -with vernac: ast := - addrule ["HintRewrite" base_list($blt) "."] -> - [ (HintRewrite ($LIST $blt)) ]. - -Grammar tactic list_tactics: ast list := - single_lt [tactic($tac)] -> [$tac] - |recursive_lt [tactic($tac) "|" list_tactics($tail)] -> - [ $tac ($LIST $tail) ] - -with step_largs: ast list := - nil_step [] -> [] - |solve_step ["with" "Solve"] -> [(REDEXP (SolveStep))] - |use_step ["with" "Use"] -> [(REDEXP (Use))] - |all_step ["with" "All"] -> [(REDEXP (All))] - -with rest_largs: ast list := - nil_rest [] -> [] - |solve_rest ["with" "Solve"] -> [(REDEXP (SolveRest))] - |cond_rest ["with" "Cond"] -> [(REDEXP (Cond))] - -with autorew_largs: ast list := - step_arg ["Step" "=" "[" list_tactics($ltac) "]" step_largs($slargs)] -> - [(REDEXP (Step ($LIST $ltac))) ($LIST $slargs)] - |rest_arg ["Rest" "=" "[" list_tactics($ltac) "]" rest_largs($llargs)] -> - [(REDEXP (Rest ($LIST $ltac))) ($LIST $llargs)] - |depth_arg ["Depth" "=" numarg($dth)] -> - [(REDEXP (Depth $dth))] - -with list_args_autorew: ast list := - nil_laa [] -> [] - |recursive_laa [autorew_largs($largs) list_args_autorew($laa)] -> - [($LIST $largs) ($LIST $laa)] - -with hintbase_list: ast list := - nil_hintbase [] -> [] -| base_by_name [identarg($id) hintbase_list($tail)] -> - [ (REDEXP (ByName $id)) ($LIST $tail)] -| explicit_base ["[" hintbase($b) "]" hintbase_list($tail)] -> - [(REDEXP (Explicit ($LIST $b))) ($LIST $tail) ] - -with hintbase: ast list := - onehint_lr [ constrarg($c) "LR" ] -> [(REDEXP (LR $c))] -| onehint_rl [ constrarg($c) "RL" ] -> [(REDEXP (RL $c))] -| conshint_lr [ constrarg($c) "LR" hintbase($tail)] -> [(REDEXP (LR $c)) ($LIST $tail)] -| conshint_rl [ constrarg($c) "RL" hintbase($tail)] -> [(REDEXP (RL $c)) ($LIST $tail)] - -with simple_tactic: ast := - AutoRewrite [ "AutoRewrite" "[" hintbase_list($lbase) "]" - list_args_autorew($laa)] -> - [(AutoRewrite (REDEXP (BaseList ($LIST $lbase))) ($LIST $laa))]. - Grammar tactic simple_tactic: ast := replace [ "Replace" constrarg($c1) "with" constrarg($c2) ] -> [(Replace $c1 $c2)] @@ -153,26 +88,4 @@ Syntax tactic level 0: | cutrewriteRL [<<(SubstConcl_RL $eqn)>>] -> ["CutRewrite <- " $eqn:E] | cutrewriteRLin [<<(SubstHyp_RL $eqn $id)>>] - -> ["CutRewrite <- " $eqn:E [1 1]"in " $id] -|nil_consbase [<<(CONSBASE)>>] -> [] -|single_consbase [<<(CONSBASE $tac)>>] -> [[1 0] $tac] -|nil_ortactic [<<(ORTACTIC)>>] -> [] -|single_ortactic [<<(ORTACTIC $tac)>>] -> ["|" $tac] -|AutoRewrite [<<(AutoRewrite $id)>>] -> ["AutoRewrite " $id] -|AutoRewriteBaseList [<<(REDEXP (BaseList $ft ($LIST $tl)))>>] -> - ["[" $ft (CONSBASE ($LIST $tl)) "]"] -|AutoRewriteStep [<<(REDEXP (Step $ft ($LIST $tl)))>>] -> - [[0 1] "Step=" "[" $ft (ORTACTIC ($LIST $tl)) "]"] -|AutoRewriteRest [<<(REDEXP (Rest $ft ($LIST $tl)))>>] -> - [[0 1] "Rest=" "[" $ft (ORTACTIC ($LIST $tl)) "]"] -|AutoRewriteSolveStep [<<(REDEXP (SolveStep))>>] -> ["with Solve"] -|AutoRewriteSolveRest [<<(REDEXP (SolveRest))>>] -> ["with Solve"] -|AutoRewriteUse [<<(REDEXP (Use))>>] -> ["with Use"] -|AutoRewriteAll [<<(REDEXP (All))>>] -> ["with All"] -|AutoRewriteCond [<<(REDEXP (Cond))>>] -> ["with Cond"] -|AutoRewriteDepth [<<(REDEXP (Depth $dth))>>] -> [[0 1] "Depth=" $dth] -|AutoRewriteByName [<<(REDEXP (ByName $id))>>] -> [ $id ] -|AutoRewriteExplicit [<<(REDEXP (Explicit $l))>>] -> ["[" $l "]"] -|AutoRewriteLR [<<(REDEXP (LR $c))>>] -> [ $c "LR" ] -|AutoRewriteRL [<<(REDEXP (RL $c))>>] -> [ $c "RL" ] -. + -> ["CutRewrite <- " $eqn:E [1 1]"in " $id]. diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml new file mode 100644 index 000000000..921280f3c --- /dev/null +++ b/tactics/autorewrite.ml @@ -0,0 +1,120 @@ +open Ast +open Coqast +open Equality +open Hipattern +open Names +open Pp +open Proof_type +open Tacmach +open Tacinterp +open Tactics +open Term +open Util +open Vernacinterp + +(* Summary and Object declaration *) +let rewtab = + ref ((Hashtbl.create 53):(string,constr * bool * tactic) Hashtbl.t) + +let lookup id = Hashtbl.find id !rewtab + +let _ = + let init () = rewtab := (Hashtbl.create 53) in + let freeze () = !rewtab in + let unfreeze fs = rewtab := fs in + Summary.declare_summary "autorewrite" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_section = false } + +(* Rewriting rules *) +type rew_rule = constr * bool * tactic + +(* Applies all the rules of one base *) +let one_base tac_main bas = + let lrul = Hashtbl.find_all !rewtab bas in + if lrul = [] then + errorlabstrm "AutoRewrite" + [<'sTR ("Rewriting base "^(bas)^" does not exist") >] + else + tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) -> + tclTHEN tac + (if dir then tclREPEAT_MAIN (tclTHENST (rewriteLR csr) [tac_main] tc) + else tclREPEAT_MAIN (tclTHENST (rewriteRL csr) [tac_main] tc))) + tclIDTAC lrul)) + +(* The AutoRewrite tactic *) +let autorewrite tac_main lbas = + tclREPEAT_MAIN (tclPROGRESS + (List.fold_left (fun tac bas -> + tclTHEN tac (one_base tac_main bas)) tclIDTAC lbas)) + +(* Functions necessary to the library object declaration *) +let load_hintrewrite _ = () +let cache_hintrewrite (_,(rbase,lrl)) = + List.iter (fun c -> Hashtbl.add !rewtab rbase c) lrl +let export_hintrewrite x = Some x + +(* Declaration of the Hint Rewrite library object *) +let (in_hintrewrite,out_hintrewrite)= + Libobject.declare_object + ("HINT_REWRITE", + { Libobject.load_function = load_hintrewrite; + Libobject.open_function = cache_hintrewrite; + Libobject.cache_function = cache_hintrewrite; + Libobject.export_function = export_hintrewrite }) + +(* To add rewriting rules to a base *) +let add_rew_rules base lrul = + Lib.add_anonymous_leaf (in_hintrewrite (base,lrul)) + +(* The vernac declaration of HintRewrite *) +let _ = vinterp_add "HintRewrite" + (function + | [VARG_STRING ort;VARG_CONSTRLIST lcom;VARG_IDENTIFIER id] + when ort = "LR" || ort = "RL" -> + (fun () -> + let (evc,env) = Command.get_current_context () in + let lcsr = + List.map (function + | Node(loc,"CONSTR",l) -> + constr_of_Constr (interp_tacarg + (evc,env,[],[],None,Tactic_debug.DebugOff) + (Node(loc,"COMMAND",l))) + | _ -> bad_vernac_args "HintRewrite") lcom in + add_rew_rules (string_of_id id) + (List.map (fun csr -> (csr,ort = "LR",tclIDTAC)) lcsr)) + | [VARG_STRING ort;VARG_CONSTRLIST lcom;VARG_IDENTIFIER id;VARG_TACTIC t] + when ort = "LR" || ort = "RL" -> + (fun () -> + let (evc,env) = Command.get_current_context () in + let lcsr = + List.map (function + | Node(loc,"CONSTR",l) -> + constr_of_Constr (interp_tacarg + (evc,env,[],[],None,Tactic_debug.DebugOff) + (Node(loc,"COMMAND",l))) + | _ -> bad_vernac_args "HintRewrite") lcom + and tac = Tacinterp.interp t in + add_rew_rules (string_of_id id) + (List.map (fun csr -> (csr,ort = "LR",tac)) lcsr)) + | _ -> bad_vernac_args "HintRewrite") + +(* To get back the tactic arguments and call AutoRewrite *) +let v_autorewrite = function + | (Tac (t,_))::l -> + let lbas = + List.map (function + | Identifier id -> string_of_id id + | _ -> Tacinterp.bad_tactic_args "AutoRewrite") l in + autorewrite t lbas + | l -> + let lbas = + List.map (function + | Identifier id -> string_of_id id + | _ -> Tacinterp.bad_tactic_args "AutoRewrite") l in + autorewrite tclIDTAC lbas + +(* Declaration of AutoRewrite *) +let _ = hide_tactic "AutoRewrite" v_autorewrite diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli new file mode 100644 index 000000000..bbbc2b047 --- /dev/null +++ b/tactics/autorewrite.mli @@ -0,0 +1,11 @@ +open Tacmach +open Term + +(* Rewriting rules *) +type rew_rule = constr * bool * tactic + +(* To add rewriting rules to a base *) +val add_rew_rules : string -> rew_rule list -> unit + +(* The AutoRewrite tactic *) +val autorewrite : tactic -> string list -> tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index 6ba9f0076..8a6291c2d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1572,12 +1572,12 @@ let freeze () = !rew_tab let unfreeze ft = rew_tab := ft (*Declaration of the summary*) -let _ = +(*let _ = Summary.declare_summary "autorewrite" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; - Summary.survive_section = false } + Summary.survive_section = false }*) (*Adds a list of rules to the rule table*) let add_list_rules rbase lrl = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9dd71b75d..0e26d170e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1698,8 +1698,8 @@ let tclABSTRACT name_op tac gls = let dyn_tclABSTRACT = hide_tactic "ABSTRACT" (function - | [Tac tac] -> + | [Tac (tac,_)] -> tclABSTRACT None tac - | [Identifier s; Tac tac] -> + | [Identifier s; Tac (tac,_)] -> tclABSTRACT (Some s) tac | _ -> invalid_arg "tclABSTRACT") |