Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et fail peuvent maintenant être des listes de string, int et variables ltac

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

7 files changed, 82 insertions, 35 deletions

diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index dbb85895a1..56abfb82b5 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -276,7 +276,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
 	  Report_node(true, n, l) -> tac
       	| Report_node(false, n, rl) ->
 	    TacThens (a,List.map2 reconstruct_success_tac l rl)
-      	| Failed n -> TacId ""
+      	| Failed n -> TacId []
       	| Tree_fail r -> reconstruct_success_tac a r
       	| Mismatch (n,p) -> a)
   | TacThen (a,b) ->
@@ -288,13 +288,13 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
 	      [in_gen globwit_main_tactic a;
 	       in_gen globwit_main_tactic b;
 	       in_gen (wit_list0 globwit_int) selected_indices]))
-	| Failed n -> TacId ""
+	| Failed n -> TacId []
 	| Tree_fail r -> reconstruct_success_tac a r
 	| _ -> error "this error case should not happen in a THEN tactic")
   | _ -> 
       (function
 	  Report_node(true, n, l) -> tac
-	| Failed n -> TacId ""
+	| Failed n -> TacId []
 	| _ ->
 	    errorlabstrm
 	      "this error case should not happen on an unknown tactic"
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index bc789fd0dc..19b06a30d3 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -154,7 +154,7 @@ let make_pbp_pattern x =
      [make_var (id_of_string ("Value_for_" ^ (string_of_id x)))]
 
 let rec make_then = function
-  | [] -> TacId ""
+  | [] -> TacId []
   | [t] -> t
   | t1::t2::l -> make_then (TacThen (t1,t2)::l)
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 8150d34e42..a42af9abf1 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -776,6 +776,7 @@ and xlate_tactic =
    | TacFirst(t1::l)-> CT_first(xlate_tactic t1, List.map xlate_tactic l)
    | TacSolve([]) -> assert false
    | TacSolve(t1::l)-> CT_tacsolve(xlate_tactic t1, List.map xlate_tactic l)
+   | TacComplete _ -> xlate_error "TODO: tactical complete"
    | TacDo(count, t) -> CT_do(xlate_id_or_int count, xlate_tactic t)
    | TacTry t -> CT_try (xlate_tactic t)
    | TacRepeat t -> CT_repeat(xlate_tactic t)
@@ -844,11 +845,13 @@ and xlate_tactic =
 		   (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
        CT_rec_tactic_in(tl, xlate_tactic t)
    | TacAtom (_, t) -> xlate_tac t 
-   | TacFail (count, "") -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
-   | TacFail (count, s) -> CT_fail(xlate_id_or_int count,
+   | TacFail (count, []) -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
+   | TacFail (count, [MsgString s]) -> CT_fail(xlate_id_or_int count,
 				   ctf_STRING_OPT_SOME (CT_string s))
-   | TacId "" -> CT_idtac ctf_STRING_OPT_NONE
-   | TacId s -> CT_idtac(ctf_STRING_OPT_SOME (CT_string s))
+   | TacFail (count, _) -> xlate_error "TODO: generic fail message"
+   | TacId [] -> CT_idtac ctf_STRING_OPT_NONE
+   | TacId [MsgString s] -> CT_idtac(ctf_STRING_OPT_SOME (CT_string s))
+   | TacId _ -> xlate_error "TODO: generic idtac message"
    | TacInfo t -> CT_info(xlate_tactic t)
    | TacArg a -> xlate_call_or_tacarg a
 
@@ -1167,9 +1170,9 @@ and xlate_tac =
         CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
     | TacAssert (None, IntroAnonymous, c) -> 
         CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
-    | TacAssert (Some (TacId ""), IntroIdentifier id, c) -> 
+    | TacAssert (Some (TacId []), IntroIdentifier id, c) -> 
         CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (Some (TacId ""), IntroAnonymous, c) -> 
+    | TacAssert (Some (TacId []), IntroAnonymous, c) -> 
         CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
     | TacAssert _ ->
 	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
@@ -1653,7 +1656,7 @@ let rec xlate_vernac =
       let formula_list = out_gen (wit_list1 rawwit_constr) f in
       let base = out_gen rawwit_pre_ident b in
       let t = 
-	match args with [t;_] -> out_gen rawwit_main_tactic t | _ -> TacId ""
+	match args with [t;_] -> out_gen rawwit_main_tactic t | _ -> TacId []
       in
       let ct_orient = match orient with
 	| true  -> CT_lr
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 313886e9ae..1deffe6d35 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -45,7 +45,7 @@ GEXTEND Gram
       [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
       | ta = tactic_expr; ";"; 
 	"["; lta = LIST0 OPT tactic_expr SEP "|"; "]" ->
-	  let lta = List.map (function None -> TacId "" | Some t -> t) lta in 
+	  let lta = List.map (function None -> TacId [] | Some t -> t) lta in 
 	  TacThens (ta, lta) ]
     | "4"
       [ ]
@@ -80,9 +80,10 @@ GEXTEND Gram
 	  TacFirst l
       | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
 	  TacSolve l
-      | IDENT "idtac"; s = [ s = STRING -> s | -> ""] -> TacId s		
+      | IDENT "complete" ; ta = tactic_expr -> TacComplete ta
+      | IDENT "idtac"; l = LIST0 message_token -> TacId l
       | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ];
-	  s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
+	  l = LIST0 message_token -> TacFail (n,l)
       | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg ->
 	  TacArg (TacExternal (loc,com,req,la))
       | st = simple_tactic -> TacAtom (loc,st)
@@ -172,14 +173,13 @@ GEXTEND Gram
     [ [ mrl = LIST1 match_rule SEP "|" -> mrl
       | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ]
   ;
+  message_token:
+    [ [ id = identref -> MsgIdent (AI id)
+      | s = STRING -> MsgString s
+      | n = integer -> MsgInt n ] ]
+  ;
 
   (* Definitions for tactics *)
-(*
-  deftok:
-    [ [ IDENT "Meta"
-      | IDENT "Tactic" ] ]
-  ;
-*)
   tacdef_body:
     [ [ name = identref; it=LIST1 input_fun; ":="; body = tactic_expr ->
 	  (name, TacFun (it, body))
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index ea693afa43..d9ef227f69 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -122,6 +122,11 @@ let pr_with_names = function
   | None -> mt ()
   | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
 
+let rec pr_message_token prid = function
+  | MsgString s -> qs s
+  | MsgInt n -> int n
+  | MsgIdent id -> prid id
+
 let rec pr_raw_generic prc prlc prtac prref x =
   match Genarg.genarg_tag x with
   | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
@@ -373,7 +378,7 @@ let pr_assumption prlc prc ipat c = match ipat with
       spc() ++ prc c ++ pr_with_names ipat
 
 let pr_by_tactic prt = function
-  | TacId "" -> mt ()
+  | TacId [] -> mt ()
   | tac -> spc() ++ str "by " ++ prt tac
 
 let pr_occs pp = function
@@ -510,6 +515,7 @@ let ltactical = 3
 let lorelse = 2
 let llet = 1
 let lfun = 1
+let lcomplete = 1
 let labstract = 3
 let lmatch = 1
 let latom = 0
@@ -845,16 +851,17 @@ let rec pr_tac env inherited tac =
       hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
              pr_tac env (lorelse,E) t2),
       lorelse
-  | TacFail (ArgArg 0,"") -> str "fail", latom
-  | TacFail (n,s) -> 
+  | TacFail (n,l) -> 
       str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
-      (if s="" then mt() else (spc() ++ qs s)), latom
+      prlist (pr_arg (pr_message_token pr_ident)) l, latom
   | TacFirst tl ->
       str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
   | TacSolve tl ->
       str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
-  | TacId "" -> str "idtac", latom
-  | TacId s -> str "idtac" ++ (qs s), latom
+  | TacComplete t ->
+      str "complete" ++ spc () ++ pr_tac env (lcomplete,E) t, lcomplete
+  | TacId l ->
+      str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
   | TacAtom (loc,TacAlias (_,s,l,_)) ->
       pr_with_comments loc
         (pr_extend env (level_of inherited) s (List.map snd l)),
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 8f27088f0d..5da2f2a30f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -75,6 +75,11 @@ type ('c,'id) inversion_strength =
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
 
+type 'id message_token =
+  | MsgString of string
+  | MsgInt of int
+  | MsgIdent of 'id
+
 type 'id gsimple_clause = ('id raw_hyp_location) option
 (* onhyps:
      [None] means *on every hypothesis*
@@ -194,6 +199,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
   | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+  | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
   | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
@@ -201,8 +207,8 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * identifier option
-  | TacId of string
-  | TacFail of int or_var * string
+  | TacId of 'id message_token list
+  | TacFail of int or_var * 'id message_token list
   | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacLetIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d1bf4389d9..476332bdaa 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -245,8 +245,8 @@ let _ =
       ];
   List.iter
       (fun (s,t) -> add_primitive_tactic s t)
-      [ "idtac",TacId "";
-        "fail", TacFail(ArgArg 0,"");
+      [ "idtac",TacId [];
+        "fail", TacFail(ArgArg 0,[]);
         "fresh", TacArg(TacFreshId None)
       ]
  
@@ -414,6 +414,12 @@ let intern_reference strict ist r =
               let (loc,qid) = qualid_of_reference r in
               error_global_not_found_loc loc qid)))
 
+let intern_message_token ist = function
+  | (MsgString _ | MsgInt _ as x) -> x
+  | MsgIdent id -> MsgIdent (intern_hyp_or_metaid ist id)
+
+let intern_message ist = List.map (intern_message_token ist)
+
 let rec intern_intro_pattern lf ist = function
   | IntroOrAndPattern l ->
       IntroOrAndPattern (intern_case_intro_pattern lf ist l)
@@ -747,8 +753,9 @@ and intern_tactic_seq ist = function
       ist.ltacvars, TacMatchContext(lz,lr, intern_match_rule ist lmr)
   | TacMatch (lz,c,lmr) ->
       ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr)
-  | TacId _ as x -> ist.ltacvars, x
-  | TacFail (n,x) -> ist.ltacvars, TacFail (intern_int_or_var ist n,x)
+  | TacId l -> ist.ltacvars, TacId (intern_message ist l)
+  | TacFail (n,l) -> 
+      ist.ltacvars, TacFail (intern_int_or_var ist n,intern_message ist l)
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
   | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
   | TacThen (t1,t2) ->
@@ -769,6 +776,7 @@ and intern_tactic_seq ist = function
       ist.ltacvars, TacOrelse (intern_tactic ist tac1,intern_tactic ist tac2)
   | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_tactic ist) l)
   | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_tactic ist) l)
+  | TacComplete tac -> ist.ltacvars, TacComplete (intern_tactic ist tac)
   | TacArg a -> ist.ltacvars, TacArg (intern_tacarg true ist a)
 
 and intern_tactic_fun ist (var,body) = 
@@ -928,7 +936,7 @@ let rec read_match_rule evc env lfun = function
 
 (* For Match Context and Match *)
 exception Not_coherent_metas
-exception Eval_fail of string
+exception Eval_fail of std_ppcmds
 
 let is_match_catchable = function
   | PatternMatchingFailure | Eval_fail _ -> true
@@ -1287,6 +1295,27 @@ let interp_constr_may_eval ist gl c =
     csr
   end
 
+let message_of_value = function
+  | VVoid -> str "()"
+  | VInteger n -> int n
+  | VIntroPattern ipat -> pr_intro_pattern ipat
+  | VConstr_context c | VConstr c -> pr_constr c
+  | VRec _ | VTactic _ | VRTactic _ | VFun _ -> str "<tactic>"
+
+let rec interp_message ist = function
+  | [] -> mt()
+  | MsgString s :: l -> pr_arg str s ++ interp_message ist l
+  | MsgInt n :: l -> pr_arg int n ++ interp_message ist l
+  | MsgIdent (_,id) :: l ->
+      let v =
+	try List.assoc id ist.lfun
+	with Not_found -> user_err_loc (loc,"",pr_id id ++ str " not found") in
+      pr_arg message_of_value v ++ interp_message ist l
+
+let rec interp_message_nl ist = function
+  | [] -> mt()
+  | l -> interp_message ist l ++ fnl()
+
 let rec interp_intro_pattern ist = function
   | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist l)
   | IntroIdentifier id -> interp_intro_pattern_var ist id
@@ -1361,8 +1390,8 @@ and eval_tactic ist = function
   | TacAtom (loc,t) -> fun gl -> catch_error loc (interp_atomic ist gl t) gl
   | TacFun _ | TacLetRecIn _ | TacLetIn _ -> assert false
   | TacMatchContext _ | TacMatch _ -> assert false
-  | TacId s -> tclIDTAC_MESSAGE s
-  | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) s
+  | TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s)
+  | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s)
   | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
   | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac)
   | TacThen (t1,t2) -> tclTHEN (interp_tactic ist t1) (interp_tactic ist t2)
@@ -1376,6 +1405,7 @@ and eval_tactic ist = function
         tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2)
   | TacFirst l -> tclFIRST (List.map (interp_tactic ist) l)
   | TacSolve l -> tclSOLVE (List.map (interp_tactic ist) l)
+  | TacComplete tac -> tclCOMPLETE (interp_tactic ist tac)
   | TacArg a -> assert false
 
 and interp_ltac_reference isapplied ist gl = function
@@ -2073,6 +2103,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2)
   | TacFirst l -> TacFirst (List.map (subst_tactic subst) l)
   | TacSolve l -> TacSolve (List.map (subst_tactic subst) l)
+  | TacComplete tac -> TacComplete (subst_tactic subst tac)
   | TacArg a -> TacArg (subst_tacarg subst a)
 
 and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)