Restructuration interpréteur de tactique: plus d'évaluation partielle à la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif

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

10 files changed, 41 insertions, 55 deletions

diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 12be9a651e..49a187caa2 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -100,10 +100,10 @@ open Genarg
 let wit_minus_div_arg, rawwit_minus_div_arg = Genarg.create_arg "minus_div_arg"
 let minus_div_arg = create_generic_entry "minus_div_arg" rawwit_minus_div_arg
 let _ = Tacinterp.add_genarg_interp "minus_div_arg"
-  (fun ist x ->
+  (fun ist gl x ->
     (in_gen wit_minus_div_arg
       (out_gen (wit_pair (wit_opt wit_constr) (wit_opt wit_constr))
-	(Tacinterp.genarg_interp ist
+	(Tacinterp.genarg_interp ist gl
 	  (in_gen (wit_pair (wit_opt rawwit_constr) (wit_opt rawwit_constr))
 	    (out_gen rawwit_minus_div_arg x))))))
 
@@ -134,11 +134,8 @@ END
 (* Guesses the type and calls Field_Gen with the right theory *)
 let field g =
   Library.check_required_library ["Coq";"field";"Field"];
-  let evc = project g
-  and env = pf_env g in
-  let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
-              goalopt=Some g; debug=get_debug () } in
-  let typ = constr_of_VConstr (val_interp ist
+  let ist = { lfun=[]; lmatch=[]; debug=get_debug () } in
+  let typ = constr_of_VConstr (pf_env g) (val_interp ist g
     <:tactic<
       Match Context With
       | [|- (eq ?1 ? ?)] -> ?1
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
index 6988f789ee..bcfcbd2ff6 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/contrib/xml/xmlentries.ml4
@@ -35,10 +35,10 @@ open Pcoq;;
 let wit_filename, rawwit_filename = Genarg.create_arg "filename"
 let filename = Pcoq.create_generic_entry "filename" rawwit_filename
 let _ = Tacinterp.add_genarg_interp "filename"
-  (fun ist x ->
+  (fun ist gl x ->
     (in_gen wit_filename
       (out_gen (wit_opt wit_string)
-	(Tacinterp.genarg_interp ist
+	(Tacinterp.genarg_interp ist gl
 	  (in_gen (wit_opt rawwit_string)
 	    (out_gen rawwit_filename x))))))
 
@@ -59,10 +59,10 @@ let _ =
 let wit_diskname, rawwit_diskname = Genarg.create_arg "diskname"
 let diskname = create_generic_entry "diskname" rawwit_diskname
 let _ = Tacinterp.add_genarg_interp "diskname"
-  (fun ist x ->
+  (fun ist gl x ->
     (in_gen wit_diskname
       (out_gen (wit_opt wit_string)
-	(Tacinterp.genarg_interp ist
+	(Tacinterp.genarg_interp ist gl
 	  (in_gen (wit_opt rawwit_string)
 	    (out_gen rawwit_diskname x))))))
 
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 3207748369..576c57a534 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -94,10 +94,10 @@ let declare_tactic_argument loc s typ pr f rawtyppr cl =
       value ($lid:"wit_"^s$, $lid:"rawwit_"^s$) = Genarg.create_arg $se$;
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$;
       Tacinterp.add_genarg_interp $se$
-        (fun ist x ->
+        (fun ist gl x ->
           (in_gen $wit$
              (out_gen $make_wit loc typ$
-          	($interp$ ist
+          	($interp$ ist gl
          	  (in_gen $make_rawwit loc rawtyp$
 	             (out_gen $rawwit$ x))))));
       Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None 
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 21206e6db7..7d82fa715c 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -14,6 +14,7 @@ open Ast
 open Topconstr
 open Rawterm
 open Tacexpr
+open Vernacexpr
 open Ast
 
 ifdef Quotify then
@@ -139,12 +140,10 @@ GEXTEND Gram
     [ [ IDENT "Fun"; it = LIST1 input_fun ; "->"; body = tactic_expr ->
           TacFun (it,body)
       | IDENT "Rec"; rc = rec_clause ->
-	  TacFunRec rc
-      |	IDENT "Rec"; rc = rec_clause; IDENT "In"; body = tactic_expr ->
-          TacLetRecIn ([rc],body)
-      | IDENT "Rec"; rc = rec_clause; "And";
-          rcl = LIST1 rec_clause SEP "And"; IDENT "In";
-          body = tactic_expr -> TacLetRecIn (rc::rcl,body)
+	  warning "'Rec f ...' is obsolete; use 'Rec f ... In f' instead";
+	  TacLetRecIn ([rc],TacArg (Reference (Libnames.Ident (fst rc))))
+      | IDENT "Rec"; rcl = LIST1 rec_clause SEP "And"; IDENT "In";
+          body = tactic_expr -> TacLetRecIn (rcl,body)
       | IDENT "Let"; llc = LIST1 let_clause SEP "And"; IDENT "In";
           u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
 (* Let cas LetCut est subsumé par "Assert id := c" tandis que le cas
@@ -183,12 +182,12 @@ GEXTEND Gram
 (*End of To do*)
       | IDENT "First" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
 	  TacFirst l
-      |	IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+      | IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
 	  TacSolve l
-      |	IDENT "Idtac" -> TacId
-      |	IDENT "Fail" -> TacFail fail_default_value
-      |	IDENT "Fail"; n = natural -> TacFail n
-      |	st = simple_tactic -> TacAtom (loc,st)
+      | IDENT "Idtac" -> TacId
+      | IDENT "Fail" -> TacFail fail_default_value
+      | IDENT "Fail"; n = natural -> TacFail n
+      | st = simple_tactic -> TacAtom (loc,st)
       | "("; a = tactic_expr; ")" -> a
       | a = tactic_arg -> TacArg a
     ] ]
@@ -206,7 +205,7 @@ GEXTEND Gram
 	  ConstrMayEval (ConstrContext (id,c))
       | IDENT "Check"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
-      | qid = lqualid -> Reference qid
+      | r = reference -> Reference r
       | ta = tactic_arg0 -> ta ] ]
   ;
   tactic_arg1:
@@ -216,32 +215,29 @@ GEXTEND Gram
 	  ConstrMayEval (ConstrContext (id,c))
       | IDENT "Check"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
-      | qid = lqualid; la = LIST1 tactic_arg0 -> TacCall (loc,qid,la)
-      | qid = lqualid -> Reference qid
+      | r = reference; la = LIST1 tactic_arg0 -> TacCall (loc,r,la)
+      | r = reference -> Reference r
       | ta = tactic_arg0 -> ta ] ]
   ;
   tactic_arg0:
     [ [ "("; a = tactic_expr; ")" -> Tacexp a
       | "()" -> TacVoid
-      | qid = lqualid -> Reference qid
+      | r = reference -> Reference r
       | n = integer -> Integer n
       | id = METAIDENT -> MetaIdArg (loc,id)
       |	"?" -> ConstrMayEval (ConstrTerm (CHole loc))
       | "?"; n = natural -> MetaNumArg (loc,n)
       |	"'"; c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ]
   ;
-  lqualid:
-    [ [ ref = reference -> ref ] ]
-  ;
 
   (* Definitions for tactics *)
   deftok:
     [ [ IDENT "Meta"
       | IDENT "Tactic" ] ]
   ;
-  vrec_clause:
+  tacdef_body:
     [ [ name = identref; it=LIST1 input_fun; ":="; body = tactic_expr ->
-	  (name, TacFunRec (name, (it, body)))
+	  (name, TacFun (it, body))
       | name = identref; ":="; body = tactic_expr ->
 	  (name, body) ] ]
   ;
@@ -249,14 +245,10 @@ GEXTEND Gram
     [ [ tac = tactic_expr -> tac ] ]
   ;
   Vernac_.command: 
-    [ [ deftok; "Definition"; name = identref; ":="; body = tactic ->
-        Vernacexpr.VernacDeclareTacticDefinition (loc, [name, body])
-      | deftok; "Definition"; name = identref; largs=LIST1 input_fun;
-        ":="; body=tactic_expr ->
-        Vernacexpr.VernacDeclareTacticDefinition
-	  (loc, [name, TacFun (largs,body)])
-      | IDENT "Recursive"; deftok; "Definition";
-	vcl=LIST1 vrec_clause SEP "And" -> 
-	  Vernacexpr.VernacDeclareTacticDefinition (loc, vcl) ] ]
+    [ [ deftok; "Definition"; b = tacdef_body ->
+          VernacDeclareTacticDefinition (false, [b])
+      | IDENT "Recursive"; deftok; "Definition"; 
+        l = LIST1 tacdef_body SEP "And" ->
+          VernacDeclareTacticDefinition (true, l) ] ]
   ;
   END
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index c44881614e..2f18076b7e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -162,8 +162,8 @@ let pr_let_clause k pr = function
 let pr_let_clauses pr = function
   | hd::tl ->
       hv 0
-        (pr_let_clause "Let " pr hd ++ spc () ++
-         prlist_with_sep spc (pr_let_clause "And " pr) tl)
+        (pr_let_clause "Let " pr hd ++
+         prlist (fun t -> spc () ++ pr_let_clause "And " pr t) tl)
   | [] -> anomaly "LetIn must declare at least one binding"
 
 let pr_rec_clause pr ((_,id),(l,t)) =
@@ -557,8 +557,6 @@ and pr6 = function
   | TacFun (lvar,body) ->
       hov 0 (str "Fun" ++
         prlist pr_funvar lvar ++ spc () ++ str "->" ++ spc () ++ prtac body)
-  | TacFunRec t ->
-      hov 0 (str "Rec " ++ pr_rec_clause prtac t)
 
   | TacArg c -> pr_tacarg c
 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index dc163ea210..2761fbbdf8 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -193,7 +193,6 @@ and ('constr,'cst,'ind,'id) gen_tactic_expr =
   | TacMatch of constr_expr may_eval * (pattern_expr,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
   | TacMatchContext of direction_flag * (pattern_expr,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
   | TacFun of ('constr,'cst,'ind,'id) gen_tactic_fun_ast
-  | TacFunRec of (identifier located * ('constr,'cst,'ind,'id) gen_tactic_fun_ast)
   | TacArg of ('constr,'cst,'ind,'id) gen_tactic_arg
 
 and ('constr,'cst,'ind,'id) gen_tactic_fun_ast =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 5667796fee..bb965213b8 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -349,10 +349,10 @@ open Genarg
 let wit_hintbases, rawwit_hintbases = Genarg.create_arg "hintbases"
 let hintbases = create_generic_entry "hintbases" rawwit_hintbases
 let _ = Tacinterp.add_genarg_interp "hintbases"
-  (fun ist x ->
+  (fun ist gl x ->
     (in_gen wit_hintbases
       (out_gen (wit_opt (wit_list0 wit_string))
-	(Tacinterp.genarg_interp ist
+	(Tacinterp.genarg_interp ist gl
 	  (in_gen (wit_opt (wit_list0 rawwit_string))
 	    (out_gen rawwit_hintbases x))))))
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 5a4c2fd65e..d0893107a7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -41,13 +41,13 @@ let constr_to_ast a =
 let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr
 
 let globalize_ref vars ref =
-  match Constrintern.interp_reference vars ref with
+  match Constrintern.interp_reference (vars,[]) ref with
   | RRef (loc,a) -> Constrextern.extern_reference loc a
   | RVar (loc,x) -> Ident (loc,x)
   | _ -> anomaly "globalize_ref: not a reference"
 
 let globalize_ref_term vars ref =
-  match Constrintern.interp_reference vars ref with
+  match Constrintern.interp_reference (vars,[]) ref with
   | RRef (loc,a) -> CRef (Constrextern.extern_reference loc a)
   | RVar (loc,x) -> CRef (Ident (loc,x))
   | c -> Constrextern.extern_rawconstr c 
@@ -641,7 +641,7 @@ let add_notation_in_scope df c (assoc,n,etyps,onlyparse) sc toks =
     if onlyparse then None
     else 
       let r = 
-	interp_rawconstr_gen false Evd.empty (Global.env()) [] false vars c in
+	interp_rawconstr_gen false Evd.empty (Global.env()) [] false (vars,[]) c in
       Some (make_old_pp_rule n symbols typs r notation scope vars) in
   (* Declare the interpretation *)
   let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 62a08d0492..321ce980b1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -628,7 +628,7 @@ let vernac_back n = Lib.back n
 (************)
 (* Commands *)
 
-let vernac_declare_tactic_definition _ l = Tacinterp.add_tacdef l
+let vernac_declare_tactic_definition = Tacinterp.add_tacdef
 
 let vernac_hints = Auto.add_hints
 
@@ -968,7 +968,7 @@ let vernac_check_guard () =
   msgnl message
 
 let vernac_debug b =
-  set_debug (if b then Tactic_debug.DebugOn else Tactic_debug.DebugOff)
+  set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
 
 
 (**************************)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 8980a7eaa2..30628bfb2b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -223,7 +223,7 @@ type vernac_expr =
 
   (* Commands *)
   | VernacDeclareTacticDefinition of
-      loc * (identifier located * raw_tactic_expr) list
+      rec_flag * (identifier located * raw_tactic_expr) list
   | VernacHints of string list * hints
   | VernacHintDestruct of
       identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr