Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Robust display of NotConvertibleTypeField errors (fix #3008, #2995)

 Since the nametab isn't aware of everything needed to print mismatched
 types (cf the bug test-cases), we create a robust term printer that
 known how to print a fully-qualified name when [shortest_qualid_of_global]
 has failed. These Printer.safe_pr_constr and alii are meant to never fail
 (at worse they display "??", for instance when the env isn't rich enough).

 Moreover, the environnement may have changed between the raise
 of NotConvertibleTypeField and its display, so we store the original
 env in the exception.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16342 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit 5cff8a26e6444a4523eb8f471a1203a33c611b5b 1 parent 4da7ddb
letouzey authored
View
4 dev/base_include
@@ -210,8 +210,8 @@ let pf_e gl s =
(* Set usual printing since the global env is available from the tracer *)
let _ = Constrextern.in_debugger := false
-let _ = Constrextern.set_debug_global_reference_printer
- (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+let _ = Constrextern.set_extern_reference
+ (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
open Toplevel
let go = loop
View
6 dev/top_printers.ml
@@ -454,7 +454,7 @@ let encode_path loc prefix mpdir suffix id =
Qualid (loc, make_qualid
(DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
-let raw_string_of_ref loc = function
+let raw_string_of_ref loc _ = function
| ConstRef cst ->
let (mp,dir,id) = repr_con cst in
encode_path loc "CST" (Some (mp,dir)) [] (Label.to_id id)
@@ -470,7 +470,7 @@ let raw_string_of_ref loc = function
| VarRef id ->
encode_path loc "SECVAR" None [] id
-let short_string_of_ref loc = function
+let short_string_of_ref loc _ = function
| VarRef id -> Ident (loc,id)
| ConstRef cst -> Ident (loc,Label.to_id (pi3 (repr_con cst)))
| IndRef (kn,0) -> Ident (loc,Label.to_id (pi3 (repr_mind kn)))
@@ -486,5 +486,5 @@ let short_string_of_ref loc = function
pretty-printer should not make calls to the global env since ocamldebug
runs in a different process and does not have the proper env at hand *)
let _ = Constrextern.in_debugger := true
-let _ = Constrextern.set_debug_global_reference_printer
+let _ = Constrextern.set_extern_reference
(if !rawdebug then raw_string_of_ref else short_string_of_ref)
View
23 interp/constrextern.ml
@@ -140,20 +140,21 @@ let insert_pat_alias loc p = function
let extern_evar loc n l =
if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
-let debug_global_reference_printer =
- ref (fun _ -> failwith "Cannot print a global reference")
+(** We allow customization of the global_reference printer.
+ For instance, in the debugger the tables of global references
+ may be inaccurate *)
-let in_debugger = ref false
+let default_extern_reference loc vars r =
+ Qualid (loc,shortest_qualid_of_global vars r)
-let set_debug_global_reference_printer f =
- debug_global_reference_printer := f
+let my_extern_reference = ref default_extern_reference
-let extern_reference loc vars r =
- if !in_debugger then
- (* Debugger does not have the tables of global reference at hand *)
- !debug_global_reference_printer loc r
- else
- Qualid (loc,shortest_qualid_of_global vars r)
+let set_extern_reference f = my_extern_reference := f
+let get_extern_reference () = !my_extern_reference
+
+let extern_reference loc vars l = !my_extern_reference loc vars l
+
+let in_debugger = ref false
(**********************************************************************)
(* mapping patterns to cases_pattern_expr *)
View
9 interp/constrextern.mli
@@ -51,9 +51,12 @@ val print_universes : bool ref
val print_no_symbol : bool ref
val print_projections : bool ref
-(** Debug printing options *)
-val set_debug_global_reference_printer :
- (Loc.t -> global_reference -> reference) -> unit
+(** Customization of the global_reference printer *)
+val set_extern_reference :
+ (Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+val get_extern_reference :
+ unit -> (Loc.t -> Id.Set.t -> global_reference -> reference)
+
val in_debugger : bool ref
(** This governs printing of implicit arguments. If [with_implicits] is
View
2  kernel/modops.ml
@@ -33,7 +33,7 @@ type signature_mismatch_error =
| NotConvertibleInductiveField of Id.t
| NotConvertibleConstructorField of Id.t
| NotConvertibleBodyField
- | NotConvertibleTypeField of types * types
+ | NotConvertibleTypeField of env * types * types
| NotSameConstructorNamesField
| NotSameInductiveNameInBlockField
| FiniteInductiveFieldExpected of bool
View
2  kernel/modops.mli
@@ -60,7 +60,7 @@ type signature_mismatch_error =
| NotConvertibleInductiveField of Id.t
| NotConvertibleConstructorField of Id.t
| NotConvertibleBodyField
- | NotConvertibleTypeField of types * types
+ | NotConvertibleTypeField of env * types * types
| NotSameConstructorNamesField
| NotSameInductiveNameInBlockField
| FiniteInductiveFieldExpected of bool
View
6 kernel/subtyping.ml
@@ -219,7 +219,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
let check_conv cst f = check_conv_error error cst f in
let check_type cst env t1 t2 =
- let err = NotConvertibleTypeField (t1, t2) in
+ let err = NotConvertibleTypeField (env, t1, t2) in
(* If the type of a constant is generated, it may mention
non-variable algebraic universes that the general conversion
@@ -303,7 +303,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
- let error = NotConvertibleTypeField (arity1, typ2) in
+ let error = NotConvertibleTypeField (env, arity1, typ2) in
check_conv error cst conv_leq env arity1 typ2
| IndConstr (((kn,i),j) as cstr,mind1) ->
ignore (Errors.error (
@@ -315,7 +315,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
- let error = NotConvertibleTypeField (ty1, ty2) in
+ let error = NotConvertibleTypeField (env, ty1, ty2) in
check_conv error cst conv env ty1 ty2
let rec check_modules cst env msb1 msb2 subst1 subst2 =
View
59 printing/printer.ml
@@ -21,6 +21,7 @@ open Refiner
open Pfedit
open Constrextern
open Ppconstr
+open Declarations
let emacs_str s =
if !Flags.print_emacs then s else ""
@@ -120,6 +121,63 @@ let pr_univ_cstr (c:Univ.constraints) =
else
mt()
+
+(** Term printers resilient to [Nametab] errors *)
+
+(** When the nametab isn't up-to-date, the term printers above
+ could raise [Not_found] during [Nametab.shortest_qualid_of_global].
+ In this case, we build here a fully-qualified name based upon
+ the kernel modpath and label of constants, and the idents in
+ the [mutual_inductive_body] for the inductives and constructors
+ (needs an environment for this). *)
+
+let id_of_global env = function
+ | ConstRef kn -> Label.to_id (Constant.label kn)
+ | IndRef (kn,0) -> Label.to_id (MutInd.label kn)
+ | IndRef (kn,i) ->
+ (Environ.lookup_mind kn env).mind_packets.(i).mind_typename
+ | ConstructRef ((kn,i),j) ->
+ (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1)
+ | VarRef v -> v
+
+let cons_dirpath id dp = DirPath.make (id :: DirPath.repr dp)
+
+let rec dirpath_of_mp = function
+ | MPfile sl -> sl
+ | MPbound uid -> DirPath.make [MBId.to_id uid]
+ | MPdot (mp,l) -> cons_dirpath (Label.to_id l) (dirpath_of_mp mp)
+
+let dirpath_of_global = function
+ | ConstRef kn -> dirpath_of_mp (Constant.modpath kn)
+ | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+ dirpath_of_mp (MutInd.modpath kn)
+ | VarRef _ -> DirPath.empty
+
+let qualid_of_global env r =
+ Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+
+let safe_gen f env c =
+ let orig_extern_ref = Constrextern.get_extern_reference () in
+ let extern_ref loc vars r =
+ try orig_extern_ref loc vars r
+ with e when Errors.noncritical e ->
+ Libnames.Qualid (loc, qualid_of_global env r)
+ in
+ Constrextern.set_extern_reference extern_ref;
+ try
+ let p = f env c in
+ Constrextern.set_extern_reference orig_extern_ref;
+ p
+ with e when Errors.noncritical e ->
+ Constrextern.set_extern_reference orig_extern_ref;
+ str "??"
+
+let safe_pr_lconstr_env = safe_gen pr_lconstr_env
+let safe_pr_constr_env = safe_gen pr_constr_env
+let safe_pr_lconstr t = safe_pr_lconstr_env (Global.env()) t
+let safe_pr_constr t = safe_pr_constr_env (Global.env()) t
+
+
(**********************************************************************)
(* Global references *)
@@ -643,7 +701,6 @@ let pr_instance_gmap insts =
(** Inductive declarations *)
-open Declarations
open Termops
open Reduction
View
11 printing/printer.mli
@@ -32,6 +32,17 @@ val pr_lconstr : constr -> std_ppcmds
val pr_constr_env : env -> constr -> std_ppcmds
val pr_constr : constr -> std_ppcmds
+(** Same, but resilient to [Nametab] errors. Prints fully-qualified
+ names when [shortest_qualid_of_global] has failed. Prints "??"
+ in case of remaining issues (such as reference not in env). *)
+
+val safe_pr_lconstr_env : env -> constr -> std_ppcmds
+val safe_pr_lconstr : constr -> std_ppcmds
+
+val safe_pr_constr_env : env -> constr -> std_ppcmds
+val safe_pr_constr : constr -> std_ppcmds
+
+
val pr_open_constr_env : env -> open_constr -> std_ppcmds
val pr_open_constr : open_constr -> std_ppcmds
View
9 test-suite/bugs/closed/shouldsucceed/2995.v
@@ -0,0 +1,9 @@
+Module Type Interface.
+ Parameter error: nat.
+End Interface.
+
+Module Implementation <: Interface.
+ Definition t := bool.
+ Definition error: t := false.
+Fail End Implementation.
+(* A UserError here is expected, not an uncaught Not_found *)
View
29 test-suite/bugs/closed/shouldsucceed/3008.v
@@ -0,0 +1,29 @@
+Module Type Intf1.
+Parameter T : Type.
+Inductive a := A.
+End Intf1.
+
+Module Impl1 <: Intf1.
+Definition T := unit.
+Inductive a := A.
+End Impl1.
+
+Module Type Intf2
+ (Impl1 : Intf1).
+Parameter x : Impl1.A=Impl1.A -> Impl1.T.
+End Intf2.
+
+Module Type Intf3
+ (Impl1 : Intf1)
+ (Impl2 : Intf2(Impl1)).
+End Intf3.
+
+Fail Module Toto
+ (Impl1' : Intf1)
+ (Impl2 : Intf2(Impl1'))
+ (Impl3 : Intf3(Impl1)(Impl2)).
+(* A UserError is expected here, not an uncaught Not_found *)
+
+(* NB : the Inductive above and the A=A weren't in the initial test,
+ they are here only to force an access to the environment
+ (cf [Printer.qualid_of_global]) and check that this env is ok. *)
View
11 toplevel/himsg.ml
@@ -24,6 +24,9 @@ open Cases
open Logic
open Printer
open Evd
+open Libnames
+open Globnames
+open Declarations
let pr_lconstr c = quote (pr_lconstr c)
let pr_lconstr_env e c = quote (pr_lconstr_env e c)
@@ -598,9 +601,11 @@ let explain_not_match_error = function
str "types given to " ++ str (Id.to_string id) ++ str " differ"
| NotConvertibleBodyField ->
str "the body of definitions differs"
- | NotConvertibleTypeField (typ1, typ2) ->
- str "expected type" ++ spc () ++ pr_lconstr typ2 ++ spc () ++
- str "but found type" ++ spc () ++ pr_lconstr typ1
+ | NotConvertibleTypeField (env, typ1, typ2) ->
+ str "expected type" ++ spc () ++
+ quote (Printer.safe_pr_lconstr_env env typ2) ++ spc () ++
+ str "but found type" ++ spc () ++
+ quote (Printer.safe_pr_lconstr_env env typ1)
| NotSameConstructorNamesField ->
str "constructor names differ"
| NotSameInductiveNameInBlockField ->
Please sign in to comment.
Something went wrong with that request. Please try again.