Prise en compte noms longs dans SuperAuto

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

8 files changed, 60 insertions, 59 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f4b0e01e58..4595c81b8f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -14,6 +14,31 @@ open Util
 (* Auxiliary grammar rules *)
 
 GEXTEND Gram
+  GLOBAL: autoargs;
+
+  autoarg_depth:
+  [ [ n = pure_numarg -> <:ast< $n>>
+     | -> Coqast.Str(loc,"NoAutoArg") ] ]
+  ;
+  autoarg_adding:
+  [ [ IDENT "Adding" ; "["; l = ne_qualidarg_list; "]" -> l
+      | -> [] ] ]
+  ;
+  autoarg_destructing:
+  [ [ IDENT "Destructing" -> Coqast.Str(loc,"Destructing")
+      | -> Coqast.Str(loc,"NoAutoArg") ] ]
+  ;
+  autoarg_usingTDB:
+  [ [ "Using"; "TDB"  ->  Coqast.Str(loc,"UsingTDB")
+      | -> Coqast.Str(loc,"NoAutoArg")  ] ]
+  ;
+  autoargs:
+  [ [ a0 = autoarg_depth; l = autoarg_adding; 
+      a2 = autoarg_destructing; a3 = autoarg_usingTDB -> a0::a2::a3::l ] ]
+  ;
+  END
+
+GEXTEND Gram
 
   identarg:
     [ [ id = Constr.ident -> id ] ]
@@ -63,9 +88,6 @@ GEXTEND Gram
   ne_qualidconstarg_list:
     [ [ l = LIST1 qualidconstarg -> l ] ]
   ;
-  ne_num_list:
-    [ [ n = numarg; l = ne_num_list -> n :: l | n = numarg -> [n] ] ]
-  ;
   pattern_occ:
     [ [ nl = LIST1 pure_numarg; c = constrarg ->
          <:ast< (PATTERN $c ($LIST $nl)) >>
@@ -175,23 +197,6 @@ GEXTEND Gram
     [ [ "in"; idl = ne_identarg_list -> <:ast< (CLAUSE ($LIST idl)) >>
       | -> <:ast< (CLAUSE) >> ] ]
   ;
-  autoarg_depth:
-  [ [ n = pure_numarg -> <:ast< $n>>
-     | -> Coqast.Str(loc,"NoAutoArg") ] ]
-  ;
-  autoarg_adding:
-  [ [ IDENT "Adding" ; "["; l = ne_identarg_list; "]" -> 
-        <:ast< (CLAUSE ($LIST $l))>>
-      | -> <:ast< (CLAUSE) >> ] ]
-  ;
-  autoarg_destructing:
-  [ [ IDENT "Destructing" -> Coqast.Str(loc,"Destructing")
-      | -> Coqast.Str(loc,"NoAutoArg") ] ]
-  ;
-  autoarg_usingTDB:
-  [ [ "Using"; "TDB"  ->  Coqast.Str(loc,"UsingTDB")
-      | -> Coqast.Str(loc,"NoAutoArg")  ] ]
-  ;
   fixdecl:
     [ [ id = identarg; n = pure_numarg; ":"; c = constrarg; fd = fixdecl ->
           <:ast< (FIXEXP $id $n $c) >> :: fd
@@ -362,12 +367,8 @@ GEXTEND Gram
       | IDENT "DHyp";  id=identarg  -> <:ast< (DHyp  $id)>>
       | IDENT "CDHyp"; id=identarg -> <:ast<  (CDHyp $id)>>
       | IDENT "DConcl"  -> <:ast< (DConcl)>>
-      | IDENT "SuperAuto"; 
-                       a0 = autoarg_depth;
-                       a1 = autoarg_adding; 
-                       a2 = autoarg_destructing; 
-                       a3 = autoarg_usingTDB -> 
-                   <:ast< (SuperAuto $a0 $a1 $a2 $a3) >>
+      | IDENT "SuperAuto"; l = autoargs ->
+                   <:ast< (SuperAuto ($LIST $l)) >>
       | IDENT "Auto"; n = pure_numarg; IDENT "Decomp" -> <:ast< (DAuto $n) >>
       | IDENT "Auto"; IDENT "Decomp" -> <:ast< (DAuto) >>
       | IDENT "Auto"; n = pure_numarg; IDENT "Decomp"; p = pure_numarg ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 5776cb811a..2d451839fb 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -272,7 +272,8 @@ module Tactic =
     let gec_list s =
       let e = Gram.Entry.create ("Tactic." ^ s) in
       Hashtbl.add utactic s (ListAst e); e
-    
+
+    let autoargs = gec_list "autoargs"    
     let binding_list = gec "binding_list"
     let castedopenconstrarg = gec "castedopenconstrarg"
     let castedconstrarg = gec "castedconstrarg"
@@ -300,7 +301,6 @@ module Tactic =
     let ne_identarg_list = gec_list "ne_identarg_list"
     let ne_qualidarg_list = gec_list "ne_qualidarg_list"
     let ne_qualidconstarg_list = gec_list "ne_qualidconstarg_list"
-    let ne_num_list = gec_list "ne_num_list"
     let ne_pattern_list = gec_list "ne_pattern_list"
     let clause_pattern = gec "clause_pattern"
     let one_intropattern = gec "one_intropattern"
@@ -311,11 +311,6 @@ module Tactic =
     let rec_clause = gec "rec_clause"
     let red_tactic = gec "red_tactic"
     let red_flag = gec "red_flag"
-    let autoarg_depth = gec "autoarg_depth"
-    let autoarg_excluding = gec "autoarg_excluding"
-    let autoarg_adding = gec "autoarg_adding"
-    let autoarg_destructing = gec "autoarg_destructing"
-    let autoarg_usingTDB = gec "autoarg_usingTDB"
     let numarg = gec "numarg"
     let pattern_occ = gec "pattern_occ"
     let pattern_occ_hyp = gec "pattern_occ_hyp"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1999733f0e..79d33a98bc 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -96,11 +96,7 @@ module Constr :
 
 module Tactic :
   sig
-    val autoarg_adding : Coqast.t Gram.Entry.e
-    val autoarg_depth : Coqast.t Gram.Entry.e
-    val autoarg_destructing : Coqast.t Gram.Entry.e
-    val autoarg_excluding : Coqast.t Gram.Entry.e
-    val autoarg_usingTDB : Coqast.t Gram.Entry.e
+    val autoargs : Coqast.t list Gram.Entry.e
     val binding_list : Coqast.t Gram.Entry.e
     val castedopenconstrarg : Coqast.t Gram.Entry.e
     val castedconstrarg : Coqast.t Gram.Entry.e
@@ -131,7 +127,6 @@ module Tactic :
     val ne_qualidarg_list : Coqast.t list Gram.Entry.e
     val ne_qualidconstarg_list : Coqast.t list Gram.Entry.e
     val ne_intropattern : Coqast.t Gram.Entry.e
-    val ne_num_list : Coqast.t list Gram.Entry.e
     val ne_pattern_list : Coqast.t list Gram.Entry.e
     val clause_pattern : Coqast.t Gram.Entry.e
     val ne_unfold_occ_list : Coqast.t list Gram.Entry.e
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 46c4e907d9..8a655b3da2 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -389,6 +389,7 @@ let ast_of_cvt_redexp = function
 (* Gives the ast corresponding to a tactic argument *)
 let ast_of_cvt_arg = function
   | Identifier id   -> nvar (string_of_id id) 
+  | Qualid qid      -> nvar (string_of_qualid qid) 
   | Quoted_string s -> str s
   | Integer n       -> num n 
   | Command c       -> ope ("COMMAND",[c])
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index e1cc05873b..319b7ff4f9 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -88,6 +88,7 @@ and tactic_arg =
   | OpenConstr     of ((int * constr) list * constr) (* constr with holes *)
   | Constr_context of constr
   | Identifier     of identifier
+  | Qualid         of qualid
   | Integer        of int
   | Clause         of identifier list
   | Bindings       of Coqast.t substitution
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 7025f450a1..e49faeb58e 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -120,6 +120,7 @@ and tactic_arg =
   | OpenConstr     of ((int * constr) list * constr) (* constr with holes *)
   | Constr_context of constr
   | Identifier     of identifier
+  | Qualid         of qualid
   | Integer        of int
   | Clause         of identifier list
   | Bindings       of Coqast.t substitution
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e87a6b24c5..7a9ba72b90 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -926,41 +926,47 @@ let rec super_search n db_list local_db argl goal =
       (compileAutoArgList  
          (super_search (n-1) db_list local_db argl) argl))) goal
 
-let search_superauto n ids argl g = 
+let search_superauto n to_add argl g = 
   let sigma =
     List.fold_right
-      (fun id -> add_named_assum (id, pf_type_of g (pf_global g id)))
-      ids empty_named_context in
+      (fun (id,c) -> add_named_assum (id, pf_type_of g c))
+      to_add empty_named_context in
   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
   let db = Hint_db.add_list db0 (make_local_hint_db g) in
   super_search n [Stringmap.find "core" !searchtable] db argl g
 
-let superauto n ids_add argl  = 
-  tclTRY (tclCOMPLETE (search_superauto n ids_add argl))
+let superauto n to_add argl  = 
+  tclTRY (tclCOMPLETE (search_superauto n to_add argl))
 
 let default_superauto g = superauto !default_search_depth [] [] g
 
-let cvt_autoArgs = function
+let cvt_autoArg = function
   | "Destructing"  -> [Destructing]
   | "UsingTDB"     -> [UsingTDB]
   | "NoAutoArg"    -> []
-  | x -> errorlabstrm "cvt_autoArgs"
+  | x -> errorlabstrm "cvt_autoArg"
         [< 'sTR "Unexpected argument for Auto!"; 'sTR x >]
 
+let cvt_autoArgs =
+  list_join_map
+    (function 
+       | Quoted_string s -> (cvt_autoArg s)
+       | _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "String expected" >])
+
+let interp_to_add gl = function
+  | (Qualid qid) ->
+      let _,id = repr_qualid qid in
+      (next_ident_away (id_of_string id) (pf_ids_of_hyps gl), 
+       Declare.constr_of_reference Evd.empty (Global.env()) (global qid))
+  | _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "Qualid expected" >]
+
 let dyn_superauto l g = 
   match l with
-    | (Integer n)::(Clause ids_add)::l -> 
-        superauto n ids_add 
-          (list_join_map
-             (function 
-		| Quoted_string s -> (cvt_autoArgs s)
-                | _ -> assert false) l) g
-    | _::(Clause ids_add)::l  -> 
-        superauto !default_search_depth ids_add 
-          (list_join_map
-             (function 
-		| Quoted_string s -> (cvt_autoArgs s)
-                | _ -> assert false) l) g
+    | (Integer n)::a::b::c::to_add ->
+        superauto n (List.map (interp_to_add g) to_add) (cvt_autoArgs [a;b;c])g
+    | _::a::b::c::to_add  -> 
+        superauto !default_search_depth (List.map (interp_to_add g) to_add)
+	  (cvt_autoArgs [a;b;c]) g
     | l -> bad_tactic_args "SuperAuto" l g
 
 let h_superauto = hide_tactic "SuperAuto" dyn_superauto
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 6a7e9d3e96..437b961ee1 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -145,4 +145,5 @@ type autoArguments =
   | UsingTDB       
   | Destructing   
 
-val superauto : int -> identifier list -> autoArguments list -> tactic
+val superauto : int -> (identifier * constr) list -> autoArguments list
+      -> tactic