Ajouts pour les tactiques utilisateur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@783 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 52 insertions, 24 deletions

diff --git a/.depend b/.depend
index 87b042eb77..757dd9860e 100644
--- a/.depend
+++ b/.depend
@@ -124,12 +124,14 @@ proofs/proof_type.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
 proofs/refiner.cmi: lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
     kernel/sign.cmi kernel/term.cmi 
 proofs/stock.cmi: kernel/names.cmi 
-proofs/tacinterp.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
-    lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi kernel/term.cmi 
+proofs/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \
+    kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi \
+    kernel/term.cmi 
 proofs/tacmach.cmi: parsing/coqast.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi lib/pp.cmi \
     proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
     proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi 
+proofs/tactic_debug.cmi: parsing/coqast.cmi proofs/proof_type.cmi 
 tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi parsing/coqast.cmi \
     kernel/environ.cmi kernel/evd.cmi kernel/names.cmi parsing/pattern.cmi \
     proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
@@ -693,18 +695,20 @@ proofs/stock.cmo: lib/bij.cmi lib/gmap.cmi lib/gmapl.cmi library/library.cmi \
 proofs/stock.cmx: lib/bij.cmx lib/gmap.cmx lib/gmapl.cmx library/library.cmx \
     kernel/names.cmx lib/pp.cmx lib/util.cmx proofs/stock.cmi 
 proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \
-    parsing/coqast.cmi library/declare.cmi kernel/environ.cmi lib/gmap.cmi \
-    library/lib.cmi library/libobject.cmi proofs/macros.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi parsing/pattern.cmi lib/pp.cmi \
-    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
-    library/summary.cmi proofs/tacmach.cmi pretyping/tacred.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 \
+    proofs/macros.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    parsing/pattern.cmi lib/pp.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/tacinterp.cmi 
 proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \
-    parsing/coqast.cmx library/declare.cmx kernel/environ.cmx lib/gmap.cmx \
-    library/lib.cmx library/libobject.cmx proofs/macros.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx parsing/pattern.cmx lib/pp.cmx \
-    proofs/proof_type.cmx pretyping/rawterm.cmx kernel/sign.cmx \
-    library/summary.cmx proofs/tacmach.cmx pretyping/tacred.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 \
+    proofs/macros.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    parsing/pattern.cmx lib/pp.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 proofs/tacinterp.cmi 
 proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \
     kernel/environ.cmi proofs/evar_refiner.cmi kernel/evd.cmi \
@@ -720,6 +724,10 @@ proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \
     kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx \
     pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     proofs/tacmach.cmi 
+proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    proofs/tacmach.cmi proofs/tactic_debug.cmi 
+proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx proofs/proof_trees.cmx \
+    proofs/tacmach.cmx proofs/tactic_debug.cmi 
 scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo 
 scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx 
 tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \
diff --git a/Makefile b/Makefile
index b90c7b7ae5..1a0d3b749a 100644
--- a/Makefile
+++ b/Makefile
@@ -101,7 +101,7 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
 PROOFS=proofs/proof_type.cmo proofs/proof_trees.cmo proofs/logic.cmo \
        proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \
        proofs/macros.cmo proofs/clenv.cmo proofs/stock.cmo proofs/pfedit.cmo \
-       proofs/tacinterp.cmo
+       proofs/tactic_debug.cmo proofs/tacinterp.cmo
 
 TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
         tactics/nbtermdn.cmo tactics/hipattern.cmo tactics/wcclausenv.cmo \
@@ -116,8 +116,10 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo \
          toplevel/usage.cmo toplevel/coqinit.cmo toplevel/coqtop.cmo
 
 HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \
-            tactics/tauto.cmo tactics/inv.cmo tactics/leminv.cmo \
-            tactics/eauto.cmo tactics/refine.cmo
+            tactics/inv.cmo tactics/leminv.cmo tactics/eauto.cmo \
+            tactics/refine.cmo
+
+SPECTAC=tactics/tauto.ml4
 
 CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
         contrib/ring/quote.cmo contrib/ring/ring.cmo \
@@ -143,11 +145,11 @@ COQBINARIES= $(COQMKTOP) $(COQC) coqtop.byte $(BESTCOQTOP)
 
 world: $(COQBINARIES) states theories contrib tools
 
-coqtop.opt: $(COQMKTOP) $(CMX)
+coqtop.opt: $(COQMKTOP) $(CMX) user-tac-opt
 	$(COQMKTOP) -opt $(OPTFLAGS) -o coqtop.opt
 	$(STRIP) ./coqtop.opt
 
-coqtop.byte: $(COQMKTOP) $(CMO) Makefile
+coqtop.byte: $(COQMKTOP) $(CMO) user-tac-byte Makefile
 	$(COQMKTOP) -top $(BYTEFLAGS) -o coqtop.byte
 
 # coqmktop 
@@ -167,7 +169,7 @@ scripts/tolink.ml: Makefile
 	echo "let proofs = \""$(PROOFS)"\"" >> $@
 	echo "let tactics = \""$(TACTICS)"\"" >> $@
 	echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@
-	echo "let hightactics = \""$(HIGHTACTICS)"\"" >> $@
+	echo "let hightactics = \""$(HIGHTACTICS)" "$(USERTAC:.ml4=.cmo)"\"" >> $@
 	echo "let contrib = \""$(CONTRIB)"\"" >> $@
 
 beforedepend:: scripts/tolink.ml
@@ -339,6 +341,25 @@ archclean::
 	rm -f contrib/*/*.cmx contrib/*/*.[so]
 
 ###########################################################################
+# ML user tactics
+# (intended to be rather generic)
+###########################################################################
+
+USERTAC = $(SPECTAC)
+
+CAMLP4GRAMMAR = camlp4o -I parsing pa_extend.cmo grammar.cma
+OPTCAMLP4GRAMMAR = camlp4o -I parsing pa_extend.cmo grammar.cma \
+                   $(OSDEPP4OPTFLAGS)
+
+COQCMO = names.cmo ast.cmo g_tactic.cmo g_constr.cmo
+
+user-tac-byte: parsing/grammar.cma
+	for i in $(USERTAC); do $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4GRAMMAR) -I kernel $(COQCMO) -impl" -impl $$i; done
+
+user-tac-opt: parsing/grammar.cma
+	for i in $(USERTAC); do $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(OPTCAMLP4GRAMMAR) -I kernel $(COQCMO) -impl" -impl $$i; done
+
+###########################################################################
 # tools
 ###########################################################################
 
@@ -481,9 +502,6 @@ parsing/grammar.cma: $(GRAMMARCMO)
 clean::
 	rm -f parsing/grammar.cma
 
-CAMLP4GRAMMAR=camlp4o -I parsing pa_extend.cmo grammar.cma
-OPTCAMLP4GRAMMAR=camlp4o -I parsing pa_extend.cmo grammar.cma $(OSDEPP4OPTFLAGS)
-
 parsing/g_%.cmo: parsing/g_%.ml4 parsing/grammar.cma
 	$(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4GRAMMAR) -impl" -impl $<
 
diff --git a/TODO b/TODO
index 0db457ab1c..3e348a1a69 100644
--- a/TODO
+++ b/TODO
@@ -9,15 +9,16 @@ Distribution:
 Environnement:
 
 - Faire fonctionner Search
+- Porter SearchIsos
 - Faire fonctionner Abstract
 - Faire fonctionner Reset
 - Décider s'il faut garder Transparent/Opaque et si oui, l'implanter
 - Ajouter "parsing" aux chemins par défaut (pour g_{nat,z}syntax.cmo) FAIT
 
-Tactiques
+Tactiques:
 
-- Choisir la précédence de Try/Orelse
 - Éviter si possible les '(
+- Réécrire AutoRewrite avec le langage de tactiques
 
 Noyau:
 
@@ -36,5 +37,6 @@ Doc:
 - une passe sur le chapitre extensions de syntaxe
 - une passe sur le chapitre Cases
 - documenter le langage de tactique et Field
+- 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 (??)
\ No newline at end of file
+- faut-il mieux spécifier la sémantique de Simpl (??)