Ajout du langage de tactiques

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

19 files changed, 45 insertions, 228 deletions

diff --git a/tactics/Equality.v b/tactics/Equality.v
index 66f5252a99..1cbf506270 100644
--- a/tactics/Equality.v
+++ b/tactics/Equality.v
@@ -84,9 +84,9 @@ Grammar tactic simple_tactic :=
 | rewriteRL [ "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(RewriteRL ($LIST $cl))]
 | rewrite [ "Rewrite" constrarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))]
 
-| condrewriteLR [ "Conditional" tactic_com($tac) "Rewrite" "->" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
-| condrewriteRL [ "Conditional" tactic_com($tac) "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(CondRewriteRL (TACTIC $tac) ($LIST $cl))]
-| condrewrite [ "Conditional" tactic_com($tac) "Rewrite" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
+| condrewriteLR [ "Conditional" tactic_expr($tac) "Rewrite" "->" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
+| condrewriteRL [ "Conditional" tactic_expr($tac) "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(CondRewriteRL (TACTIC $tac) ($LIST $cl))]
+| condrewrite [ "Conditional" tactic_expr($tac) "Rewrite" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
 
 | rewrite_in [ "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ]
        -> [(RewriteLRin $h ($LIST $cl))]
@@ -96,15 +96,15 @@ Grammar tactic simple_tactic :=
        -> [(RewriteRLin $h ($LIST $cl))]
 
 | condrewriteLRin 
-  [ "Conditional" tactic_com($tac) "Rewrite" "->" constrarg_binding_list($cl) 
+  [ "Conditional" tactic_expr($tac) "Rewrite" "->" constrarg_binding_list($cl) 
 	"in" identarg($h) ] ->
 	   [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))]
 | condrewriteRLin 
-  [ "Conditional" tactic_com($tac) "Rewrite" "<-" constrarg_binding_list($cl) 
+  [ "Conditional" tactic_expr($tac) "Rewrite" "<-" constrarg_binding_list($cl) 
 	"in" identarg($h)] ->
   	   [(CondRewriteRLin (TACTIC $tac) $h ($LIST $cl))]
 | condrewritein 
-  [ "Conditional" tactic_com($tac) "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ] 
+  [ "Conditional" tactic_expr($tac) "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ] 
         -> [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))]
 
 | DRewriteLR [ "Dependent" "Rewrite" "->" identarg($id) ]
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f0b4e81add..2a98b8e2fb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -13,7 +13,7 @@ open Reduction
 open Typing
 open Pattern
 open Tacmach
-open Proof_trees
+open Proof_type
 open Pfedit
 open Rawterm
 open Tacred
diff --git a/tactics/auto.mli b/tactics/auto.mli
index d97e82df63..50460de17a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,7 +6,7 @@ open Util
 open Names
 open Term
 open Sign
-open Proof_trees
+open Proof_type
 open Tacmach
 open Clenv
 open Pattern
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index a21b3e6d7c..237af5c060 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -111,8 +111,8 @@ open Generic
 open Term
 open Environ
 open Reduction
+open Proof_type
 open Rawterm
-open Proof_trees
 open Tacmach
 open Tactics
 open Clenv
@@ -279,17 +279,17 @@ let dHyp id gls = destructHyp false id gls
 
 open Tacinterp
 
-let _ = 
-  tacinterp_add
-    ("DHyp",(function
-	       | [Identifier id] -> dHyp id
-	       | _ -> bad_tactic_args "DHyp"))
+let _=
+  add_tactic "DHyp"
+    (function
+       | [Identifier id] -> dHyp id
+       | _ -> bad_tactic_args "DHyp")
 
-let _ = 
-  tacinterp_add
-    ("CDHyp",(function
-		| [Identifier id] -> cDHyp id
-		| _ -> bad_tactic_args "CDHyp"))
+let _=
+  add_tactic "CDHyp"
+    (function
+       | [Identifier id] -> cDHyp id
+       | _ -> bad_tactic_args "CDHyp")
 
 (* [DConcl gls]
 
@@ -302,11 +302,11 @@ let dConcl gls =
   let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
   tclFIRST (List.map (applyDestructor None false) sorted_ddl) gls
 
-let _ = 
-  tacinterp_add
-    ("DConcl",(function
-		 | [] -> dConcl
-		 | _ -> bad_tactic_args "DConcl"))
+let _=
+  add_tactic "DConcl"
+    (function
+       | [] -> dConcl
+       | _ -> bad_tactic_args "DConcl")
 
 let to2Lists (table : t) = Nbtermdn.to2lists table
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 4abff0e4d2..ff07f6c09a 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -7,7 +7,7 @@ open Names
 open Generic
 open Term
 open Reduction
-open Proof_trees
+open Proof_type
 open Clenv
 open Hipattern
 open Tacmach
diff --git a/tactics/elim.mli b/tactics/elim.mli
index ee1b10a377..594dc62eaf 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Names
 open Term
-open Proof_trees
+open Proof_type
 open Tacmach
 open Tacticals
 (*i*)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b282309927..72f02e7205 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -14,7 +14,7 @@ open Instantiate
 open Typeops
 open Typing
 open Tacmach
-open Proof_trees
+open Proof_type
 open Logic
 open Wcclausenv
 open Pattern
@@ -1936,7 +1936,7 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
     (repackage sigr gl,validation_fun)
 
 (*Collects the arguments of AutoRewrite ast node*)
-let dyn_autorewrite largs=
+(*let dyn_autorewrite largs=
   let rec explicit_base largs =
     let tacargs = List.map cvt_arg largs in 
     List.map 
@@ -2016,8 +2016,7 @@ let dyn_autorewrite largs=
 	anomalylabstrm "dyn_autorewrite" 
 	  [<'sTR "Bad call of list_args (not a REDEXP)">]
   in
-  list_args largs
+  list_args largs*)
 
 (*Adds and hides the AutoRewrite tactic*)
-let h_autorewrite = hide_tactic "AutoRewrite" dyn_autorewrite
-
+(*let h_autorewrite = hide_tactic "AutoRewrite" dyn_autorewrite*)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 789328f51b..3341167d86 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -7,7 +7,7 @@ open Term
 open Sign
 open Evd
 open Environ
-open Proof_trees
+open Proof_type
 open Tacmach
 open Hipattern
 open Pattern
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 049fb1e14b..48b29ea5ed 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 open Term
-open Proof_trees
+open Proof_type
 open Tacmach
 open Tacentries
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 3929903644..183558f601 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Names
 open Term
-open Proof_trees
+open Proof_type
 open Tacmach
 open Tacentries
 (*i*)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 53eaa4ad15..8f19a69248 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -13,7 +13,7 @@ open Printer
 open Reduction
 open Retyping
 open Tacmach
-open Proof_trees
+open Proof_type
 open Clenv
 open Tactics
 open Wcclausenv
diff --git a/tactics/stock.ml b/tactics/stock.ml
deleted file mode 100644
index ef0feec952..0000000000
--- a/tactics/stock.ml
+++ /dev/null
@@ -1,147 +0,0 @@
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Library
-
-(* The pattern table for tactics. *)
-
-(* The idea is that we want to write tactic files which are only
-   "activated" when certain modules are loaded and imported.  Already,
-   the question of how to store the tactics is hard, and we will not
-   address that here.  However, the question arises of how to store
-   the patterns that we will want to use for term-destructuring, and
-   the solution proposed is that we will store patterns with a
-   "module-marker", telling us which modules have to be open in order
-   to use the pattern.  So we will write:
-
-   let mark = make_module_marker ["<module-name>";<module-name>;...]
-
-   let p1 = put_pat mark "<parseable pattern goes here>"
-
-   And now, we can use:
-
-             (get p1)
-
-   to get the term which corresponds to this pattern, already parsed
-   and with the global names adjusted.
-
-   In other words, we will have the term which we would have had if we
-   had done an:
-
-        constr_of_com mt_ctxt (initial_sign()) "<text here>"
-
-   except that it will be computed at module-opening time, rather than
-   at tactic-application time.  The ONLY difference will be that
-   no implicit syntax resolution will happen.
-
-   So the entries we provide are:
-
-   type module_mark
-
-   value make_module_marker : string list -> module_mark
-
-   type marked_term
-
-   value put_pat : module_mark -> string -> marked_term
-
-   value get_pat : marked_term -> constr
-
- *)
-
-type module_mark = Mmk of int
-
-let path_mark_bij = ref (Bij.empty : (string list,module_mark) Bij.t)
-
-let mmk_ctr = ref 0
-
-let new_mmk () = (incr mmk_ctr; !mmk_ctr)
-
-let make_module_marker sl =
-  let sorted_sl = Sort.list (<) sl in 
-  try 
-    Bij.map !path_mark_bij sorted_sl
-  with Not_found -> begin
-    let mmk = Mmk(new_mmk()) in 
-    path_mark_bij := Bij.add !path_mark_bij (sorted_sl,mmk);
-    mmk
-  end
-      
-let mark_satisfied mmk =
-  let spl = Bij.pam !path_mark_bij mmk in 
-  list_subset spl (loaded_modules())
-
-(* src_tab: for each module_mark, stores the tickets of objects which
-   need to be compiled when that mark becomes active.
-
-   obj_tab: for each ticket, stores the (possibly nonexistent)
-   compiled object
-
-   ticket_tab: for each ticket, stores its module_mark and the string
-   (source)
-
-   string_tab: for each string * module_mark, stores the ticket. *)
-
-type 'a stock_args = {
-  name : string;
-  proc : string -> 'a }
-
-type 'a stock = {
-  mutable src_tab : (module_mark,int) Gmapl.t;
-  mutable obj_tab : (int,'a) Gmap.t;
-  mutable ticket_string_bij : (int,string * module_mark) Bij.t;
-  args : 'a stock_args }
-
-type 'a stocked = int
-
-let stock_ctr = ref 0
-
-let new_stock () = (incr stock_ctr; !stock_ctr)
-
-let make_stock args =
-  { src_tab = Gmapl.empty;
-    obj_tab = Gmap.empty;
-    ticket_string_bij = Bij.empty;
-    args = args }
-  
-let stock stock mmk s =
-  try 
-    Bij.pam stock.ticket_string_bij (s,mmk)
-  with Not_found -> begin
-    let idx = new_stock() in 
-    stock.src_tab <- Gmapl.add mmk idx stock.src_tab;
-    stock.ticket_string_bij <- Bij.add stock.ticket_string_bij (idx,(s,mmk));
-    idx
-  end
-
-let pr_mm mm =
-  let sl = Bij.pam !path_mark_bij mm in
-  prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) sl
-
-(* TODO: traiter a part les erreurs provenant de stock.args.proc
-   ( = parsing quand [so]pattern appelle retrieve)
-    -> eviter d'avoir l'erreur stocked datum *)
-
-let retrieve stock idx =
-  try 
-    Gmap.find idx stock.obj_tab
-  with Not_found ->
-    let (s,mmk) = Bij.map stock.ticket_string_bij idx in 
-    if mark_satisfied mmk then
-      try
-        let c = stock.args.proc s in 
-	stock.obj_tab <- Gmap.add idx c stock.obj_tab;
-        c
-      with e -> begin
-        mSGNL [< 'sTR"Processing of the stocked datum " ; 'sTR s ;
-                 'sTR" failed." ; 'fNL;
-                 Library.fmt_modules_state() >];
-	raise e
-      end
-    else
-      errorlabstrm "Stock.retrieve"
-        [< 'sTR"The stocked object "; 'sTR s; 'sTR" was not compilable"; 
-	   'fNL; 'sTR"Its module mark was: "; pr_mm mmk ; 'fNL ;
-           Library.fmt_modules_state() >]
diff --git a/tactics/stock.mli b/tactics/stock.mli
deleted file mode 100644
index c0cd43c7d5..0000000000
--- a/tactics/stock.mli
+++ /dev/null
@@ -1,24 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Names
-(*i*)
-
-(* Module markers. *)
-
-type 'a stock
-
-type module_mark
-
-type 'a stocked
-
-type 'a stock_args = {
-  name : string;
-  proc : string -> 'a }
-
-val make_stock : 'a stock_args -> 'a stock
-val make_module_marker : string list -> module_mark
-val stock : 'a stock -> module_mark -> string -> 'a stocked
-val retrieve : 'a stock -> 'a stocked -> 'a
-
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index 687de4d7d1..bc9e836ab6 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 (*i*)
-open Proof_trees
+open Proof_type
 open Tacmach
 (*i*)
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6e7831b1cb..888785ae92 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -12,7 +12,6 @@ open Reduction
 open Environ
 open Declare
 open Tacmach
-open Proof_trees
 open Clenv
 open Pattern
 open Wcclausenv
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 24b705ac72..ae38c210e4 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,7 +6,7 @@ open Names
 open Term
 open Sign
 open Tacmach
-open Proof_trees
+open Proof_type
 open Clenv
 open Reduction
 open Pattern
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 66dd8b1ad6..b21ac1825b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -16,6 +16,7 @@ open Pfedit
 open Tacred
 open Tacmach
 open Proof_trees
+open Proof_type
 open Logic
 open Clenv
 open Tacticals
@@ -37,13 +38,6 @@ let get_pairs_from_bindings =
     | _                  -> error "not a binding list!"
   in 
   List.map pair_from_binding
-
-let get_commands = 
-  let command_from_tacarg = function 
-    | (Command x) -> x
-    | _           -> error "get_commands: not a command!"
-  in 
-  List.map command_from_tacarg
     
 let rec string_head_bound = function 
   | DOPN(Const _,_) as x -> 
@@ -211,9 +205,9 @@ let unfold_option   loccname   = reduct_option   (unfoldn loccname)
 let pattern_option l = reduct_option (pattern_occs l)
 
 let dyn_change = function
-  | [Command (com); Clause cl] ->
+  | [Constr c; Clause cl] ->
       (fun goal -> 
-         let c = Astterm.interp_type (project goal) (pf_env goal) com in
+(*         let c = Astterm.interp_type (project goal) (pf_env goal) com in*)
          in_combinator (change_in_concl c) (change_in_hyp c) cl goal)
   | l -> bad_tactic_args "change" l
 
@@ -224,11 +218,7 @@ let reduce redexp cl goal =
   redin_combinator (reduction_of_redexp redexp) cl goal
 
 let dyn_reduce = function
-  | [Redexp (redn,args); Clause cl] ->
-      (fun goal -> 
-         let redexp =
-	   Astterm.redexp_of_ast (project goal) (pf_env goal) (redn,args) in  
-	 reduce redexp cl goal)
+  | [Redexp redexp; Clause cl] -> (fun goal -> reduce redexp cl goal)
   | l -> bad_tactic_args "reduce" l
 
 (* Unfolding occurrences of a constant *)
@@ -242,7 +232,7 @@ let unfold_constr c =
 	  [< 'sTR "Cannot unfold a non-constant." >]
 
 (*******************************************)
-(*         Introduction tactics        *)
+(*         Introduction tactics            *)
 (*******************************************)
 
 let next_global_ident_from id avoid = 
@@ -603,10 +593,10 @@ let generalize lconstr gl =
   apply_type newcl lconstr gl
 
 let dyn_generalize =
-  fun argsl -> tactic_com_list generalize (get_commands argsl)
+  fun argsl -> generalize (List.map Tacinterp.constr_of_Constr argsl)
       
 let dyn_generalize_dep = function
-  | [Command com] -> tactic_com generalize_dep com
+  | [Constr csr] -> generalize_dep csr
   | l -> bad_tactic_args "dyn_generalize_dep" l
 
 (* Faudra-t-il une version avec plusieurs args de generalize_dep ?
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d36b162adf..6ee8b95481 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -6,7 +6,7 @@ open Names
 open Term
 open Environ
 open Tacmach
-open Proof_trees
+open Proof_type
 open Reduction
 open Evd
 open Clenv
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index deae4091ff..01d05a690d 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -7,7 +7,7 @@ open Term
 open Sign
 open Environ
 open Evd
-open Proof_trees
+open Proof_type
 open Tacmach
 open Clenv
 (*i*)