aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend70
-rw-r--r--CHANGES3
-rw-r--r--Makefile4
-rw-r--r--TODO5
-rw-r--r--proofs/proof_trees.ml2
-rw-r--r--proofs/proof_type.ml2
-rw-r--r--proofs/proof_type.mli2
-rw-r--r--proofs/refiner.ml13
-rw-r--r--proofs/refiner.mli8
-rw-r--r--proofs/tacinterp.ml2
-rw-r--r--proofs/tacmach.ml2
-rw-r--r--proofs/tacmach.mli2
-rw-r--r--states/MakeInitial.v2
-rw-r--r--tactics/AutoRewrite.v25
-rw-r--r--tactics/Equality.v89
-rw-r--r--tactics/autorewrite.ml120
-rw-r--r--tactics/autorewrite.mli11
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/tactics.ml4
19 files changed, 246 insertions, 124 deletions
diff --git a/.depend b/.depend
index 36d802bf9..358126b6b 100644
--- a/.depend
+++ b/.depend
@@ -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
diff --git a/CHANGES b/CHANGES
index 08f607557..145493bce 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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;
diff --git a/Makefile b/Makefile
index ac5621dbd..22d13c3f1 100644
--- a/Makefile
+++ b/Makefile
@@ -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 $<
diff --git a/TODO b/TODO
index 3a29f4108..43ff76050 100644
--- a/TODO
+++ b/TODO
@@ -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")
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 08:47:33 +0000