Small cleaning of printing coercion failures in Ltac interpretation.

Now we at least print the type of the offending object.

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

4 files changed, 64 insertions, 57 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e3efd196c..89e2d7ddd 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -348,29 +348,6 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 let pploc x = let (l,r) = Loc.unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
 
-(* extendable tactic arguments *)
-let rec pr_argument_type = function
-  (* Basic types *)
-  | IntOrVarArgType -> str"int-or-var"
-  | IdentArgType true -> str"ident"
-  | IdentArgType false -> str"pattern_ident"
-  | VarArgType -> str"var"
-  | RefArgType -> str"ref"
-  (* Specific types *)
-  | GenArgType -> str"genarg"
-  | ConstrArgType -> str"constr"
-  | ConstrMayEvalArgType -> str"constr-may-eval"
-  | QuantHypArgType -> str"qhyp"
-  | OpenConstrArgType _ -> str"open-constr"
-  | ConstrWithBindingsArgType -> str"constr-with-bindings"
-  | BindingsArgType -> str"bindings"
-  | RedExprArgType -> str"redexp"
-  | ListArgType t -> pr_argument_type t ++ str" list"
-  | OptArgType t -> pr_argument_type t ++ str" opt"
-  | PairArgType (t1,t2) ->
-      str"("++ pr_argument_type t1 ++ str"*" ++ pr_argument_type t2 ++str")"
-  | ExtraArgType s -> str"\"" ++ str s ++ str "\""
-
 let pp_argument_type t = pp (pr_argument_type t)
 
 let pp_generic_argument arg =
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 8e18be3d0..98287d184 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -49,6 +49,27 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2
 | _ -> false
 
+let rec pr_argument_type = function
+| IntOrVarArgType -> str "int_or_var"
+| IdentArgType true -> str "ident"
+| IdentArgType false -> str "pattern_ident"
+| VarArgType -> str "var"
+| RefArgType -> str "ref"
+| GenArgType -> str "genarg"
+| ConstrArgType -> str "constr"
+| ConstrMayEvalArgType -> str "constr_may_eval"
+| QuantHypArgType -> str "qhyp"
+| OpenConstrArgType _ -> str "open_constr"
+| ConstrWithBindingsArgType -> str "constr_with_bindings"
+| BindingsArgType -> str "bindings"
+| RedExprArgType -> str "redexp"
+| ListArgType t -> pr_argument_type t ++ spc () ++ str "list"
+| OptArgType t -> pr_argument_type t ++ spc () ++ str "opt"
+| PairArgType (t1, t2) ->
+    str "("++ pr_argument_type t1 ++ spc () ++
+    str "*" ++ spc () ++ pr_argument_type t2 ++ str ")"
+| ExtraArgType s -> str s
+
 type ('raw, 'glob, 'top) genarg_type = argument_type
 
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
diff --git a/lib/genarg.mli b/lib/genarg.mli
index b8dd08f96..e2654fcf5 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -210,6 +210,9 @@ type argument_type =
 
 val argument_type_eq : argument_type -> argument_type -> bool
 
+val pr_argument_type : argument_type -> Pp.std_ppcmds
+(** Print a human-readable representation for a given type. *)
+
 val genarg_tag : 'a generic_argument -> argument_type
 
 val unquote : ('a, 'co) abstract_argument_type -> argument_type
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 30813d530..1918ddc0c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -112,24 +112,55 @@ let check_is_value v =
     | _ -> ()
   else ()
 
-(* Displays a value *)
-let rec pr_value env v = str "a tactic"
+(** TODO: unify printing of generic Ltac values in case of coercion failure. *)
 
+(* Displays a value *)
 let pr_value env v =
   let v = Value.normalize v in
-  if has_type v (topwit wit_tacvalue) then
-    pr_value env (to_tacvalue v)
+  if has_type v (topwit wit_tacvalue) then str "a tactic"
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
-    match env with Some env -> pr_lconstr_env env c | _ -> str "a term"
+    match env with
+    | Some env -> pr_lconstr_env env c
+    | _ -> str "a term"
   else if has_type v (topwit wit_constr) then
     let c = out_gen (topwit wit_constr) v in
-    match env with Some env -> pr_lconstr_env env c | _ -> str "a term"
+    match env with
+    | Some env -> pr_lconstr_env env c
+    | _ -> str "a term"
   else if has_type v (topwit wit_constr_under_binders) then
     let c = out_gen (topwit wit_constr_under_binders) v in
-    match env with Some env -> pr_lconstr_under_binders_env  env c | _ -> str "a term"
+    match env with
+    | Some env -> pr_lconstr_under_binders_env  env c
+    | _ -> str "a term"
   else
-    str "an unknown type" (** TODO *)
+    str "a value of type" ++ spc () ++ pr_argument_type (genarg_tag v)
+
+let pr_inspect env expr result =
+  let pp_expr = Pptactic.pr_glob_tactic env expr in
+  let pp_result =
+    if has_type result (topwit wit_tacvalue) then
+    match to_tacvalue result with
+    | VRTactic _ -> str "a VRTactic"
+    | VFun (_, il, ul, b) ->
+      let pp_body = Pptactic.pr_glob_tactic env b in
+      let pr_sep () = str ", " in
+      let pr_iarg (id, _) = pr_id id in
+      let pr_uarg = function
+      | None -> str "_"
+      | Some id -> pr_id id
+      in
+      let pp_iargs = prlist_with_sep pr_sep pr_iarg (Id.Map.bindings il) in
+      let pp_uargs = prlist_with_sep pr_sep pr_uarg ul in
+      str "a VFun with body " ++ fnl() ++ pp_body ++ fnl() ++
+        str "instantiated arguments " ++ fnl() ++ pp_iargs ++ fnl () ++
+        str "uninstantiated arguments " ++ fnl() ++ pp_uargs
+    | VRec _ -> str "a VRec"
+    else
+      let pp_type = pr_argument_type (genarg_tag result) in
+      str "an object of type" ++ spc () ++ pp_type
+  in
+  pp_expr ++ fnl() ++ str "this is " ++ pp_result
 
 (* Transforms an id into a constr if possible, or fails with Not_found *)
 let constr_of_id env id =
@@ -1542,32 +1573,7 @@ and interp_ltac_constr ist gl e =
   with CannotCoerceTo _ ->
     errorlabstrm ""
       (str "Must evaluate to a closed term" ++ fnl() ++
-	  str "offending expression: " ++ fnl() ++
-          Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ str "this is a " ++
-          (if has_type result (topwit wit_tacvalue) then match to_tacvalue result with
-            | VRTactic _ -> str "VRTactic"
-            | VFun (_,il,ul,b) ->
-                (str "VFun with body " ++ fnl() ++
-                    Pptactic.pr_glob_tactic (pf_env gl) b ++ fnl() ++
-		    str "instantiated arguments " ++ fnl() ++
-                    Id.Map.fold
-                    (fun i v s -> str (Id.to_string i) ++ str ", " ++ s)
-                    il (str "") ++
-                    str "uninstantiated arguments " ++ fnl() ++
-                    List.fold_right
-                    (fun opt_id s ->
-                      (match opt_id with
-                          Some id -> str (Id.to_string id)
-                        | None -> str "_") ++ str ", " ++ s)
-                    ul (mt()))
-(*             | VVoid -> str "VVoid" *)
-(*             | VInteger _ -> str "VInteger" *)
-(*             | VConstr _ -> str "VConstr" *)
-(*             | VIntroPattern _ -> str "VIntroPattern" *)
-(*             | VConstr_context _ -> str "VConstrr_context" *)
-            | VRec _ -> str "VRec"
-(*            | VList _ -> str "VList"*)
-          else str "unknown object") ++ str".")
+      str "offending expression: " ++ fnl() ++ pr_inspect (pf_env gl) e result)
 
 (* Interprets tactic expressions : returns a "tactic" *)
 and interp_tactic ist tac gl =