aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include4
-rw-r--r--dev/top_printers.ml6
-rw-r--r--interp/constrextern.ml23
-rw-r--r--interp/constrextern.mli9
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/modops.mli2
-rw-r--r--kernel/subtyping.ml6
-rw-r--r--printing/printer.ml59
-rw-r--r--printing/printer.mli11
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2995.v9
-rw-r--r--test-suite/bugs/closed/shouldsucceed/3008.v29
-rw-r--r--toplevel/himsg.ml11
12 files changed, 143 insertions, 28 deletions
diff --git a/dev/base_include b/dev/base_include
index c75413a38..ca40f5f7a 100644
--- a/dev/base_include
+++ b/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
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index db895fc0f..ec9c0a95e 100644
--- a/dev/top_printers.ml
+++ b/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)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 47753c158..84baefe61 100644
--- a/interp/constrextern.ml
+++ b/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 *)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 0e40e83e6..0a4192c3e 100644
--- a/interp/constrextern.mli
+++ b/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
diff --git a/kernel/modops.ml b/kernel/modops.ml
index c1b5d788d..6c46ad510 100644
--- a/kernel/modops.ml
+++ b/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
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 600e631a7..66aadd124 100644
--- a/kernel/modops.mli
+++ b/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
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index e5b81c72f..99c1b8483 100644
--- a/kernel/subtyping.ml
+++ b/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 =
diff --git a/printing/printer.ml b/printing/printer.ml
index ea6e79876..8fc38bc6c 100644
--- a/printing/printer.ml
+++ b/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
diff --git a/printing/printer.mli b/printing/printer.mli
index 2c6800a11..2bc589b63 100644
--- a/printing/printer.mli
+++ b/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
diff --git a/test-suite/bugs/closed/shouldsucceed/2995.v b/test-suite/bugs/closed/shouldsucceed/2995.v
new file mode 100644
index 000000000..ba3acd088
--- /dev/null
+++ b/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 *) \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/shouldsucceed/3008.v
new file mode 100644
index 000000000..3f3a979a3
--- /dev/null
+++ b/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. *) \ No newline at end of file
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 58bfe0832..a050e45c3 100644
--- a/toplevel/himsg.ml
+++ b/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 ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 12:02:13 +0000