Raise an anomaly when looking up unknown constant/inductive

If you have access to a kernel name you also should have the
environment in which it is defined, barring hacks. In order to
disfavor hacks we make the standard lookups raise anomalies so that
people are forced to admit they rely on the internals of the
environment.

We find that hackers operated on the code for side effects, for
finding inductive schemes, for simpl and for Print Assumptions. They
attempted to operate on funind but the error handling code they wrote
would have raised another Not_found instead of being useful.

All these uses are indeed hacky so I am satisfied that we are not
forcing new hacks on callers.

11 files changed, 79 insertions, 46 deletions

diff --git a/clib/cMap.ml b/clib/cMap.ml
index baac892b9e..8d822667c3 100644
--- a/clib/cMap.ml
+++ b/clib/cMap.ml
@@ -58,6 +58,7 @@ module MapExt (M : Map.OrderedType) :
 sig
   type 'a map = 'a Map.Make(M).t
   val set : M.t -> 'a -> 'a map -> 'a map
+  val get : M.t -> 'a map -> 'a
   val modify : M.t -> (M.t -> 'a -> 'a) -> 'a map -> 'a map
   val domain : 'a map -> Set.Make(M).t
   val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map
@@ -124,6 +125,14 @@ struct
       if r == r' then s
       else map_inj (MNode {l; v=k'; d=v'; r=r'; h})
 
+  let rec get k (s:'a map) : 'a = match map_prj s with
+    | MEmpty -> assert false
+    | MNode {l; v=k'; d=v; r; h} ->
+      let c = M.compare k k' in
+      if c < 0 then get k l
+      else if c = 0 then v
+      else get k r
+
   let rec modify k f (s : 'a map) : 'a map = match map_prj s with
   | MEmpty -> raise Not_found
   | MNode {l; v; d; r; h} ->
@@ -324,5 +333,4 @@ module Make(M : Map.OrderedType) =
 struct
   include Map.Make(M)
   include MapExt(M)
-  let get k m = try find k m with Not_found -> assert false
 end
diff --git a/clib/hMap.ml b/clib/hMap.ml
index f77068b477..9858477489 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -367,7 +367,10 @@ struct
     | None -> None
     | Some m -> Map.find_opt k m
 
-  let get k s = try find k s with Not_found -> assert false
+  let get k s =
+    let h = M.hash k in
+    let m = Int.Map.get h s in
+    Map.get k m
 
   let split k s = assert false (** Cannot be implemented efficiently *)
 
diff --git a/clib/int.ml b/clib/int.ml
index ee4b3128d5..e0dbfb5274 100644
--- a/clib/int.ml
+++ b/clib/int.ml
@@ -42,6 +42,13 @@ struct
     else if i = k then v
     else find i r
 
+  let rec get i s = match map_prj s with
+  | MEmpty -> assert false
+  | MNode (l, k, v, r, h) ->
+    if i < k then get i l
+    else if i = k then v
+    else get i r
+
   let rec find_opt i s = match map_prj s with
   | MEmpty -> None
   | MNode (l, k, v, r, h) ->
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 98d66cafa1..2bee2f7a8e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -231,22 +231,26 @@ let fold_inductives f env acc =
 (* Global constants *)
 
 let lookup_constant_key kn env =
-  Cmap_env.find kn env.env_globals.Globals.constants
+  Cmap_env.get kn env.env_globals.Globals.constants
 
 let lookup_constant kn env =
-  fst (Cmap_env.find kn env.env_globals.Globals.constants)
+  fst (lookup_constant_key kn env)
+
+let mem_constant kn env = Cmap_env.mem kn env.env_globals.Globals.constants
 
 (* Mutual Inductives *)
+let lookup_mind_key kn env =
+  Mindmap_env.get kn env.env_globals.Globals.inductives
+
 let lookup_mind kn env =
-  fst (Mindmap_env.find kn env.env_globals.Globals.inductives)
+  fst (lookup_mind_key kn env)
+
+let mem_mind kn env = Mindmap_env.mem kn env.env_globals.Globals.inductives
 
 let mind_context env mind =
   let mib = lookup_mind mind env in
   Declareops.inductive_polymorphic_context mib
 
-let lookup_mind_key kn env =
-  Mindmap_env.find kn env.env_globals.Globals.inductives
-
 let oracle env = env.env_typing_flags.conv_oracle
 let set_oracle env o =
   let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 5af2a7288b..782ea1c666 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -201,10 +201,12 @@ val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_in
 val lookup_constant_key :  Constant.t -> env -> constant_key
 
 (** Looks up in the context of global constant names 
-   raises [Not_found] if the required path is not found *)
+   raises an anomaly if the required path is not found *)
 val lookup_constant    : Constant.t -> env -> Opaqueproof.opaque constant_body
 val evaluable_constant : Constant.t -> env -> bool
 
+val mem_constant : Constant.t -> env -> bool
+
 (** New-style polymorphism *)
 val polymorphic_constant  : Constant.t -> env -> bool
 val polymorphic_pconstant : pconstant -> env -> bool
@@ -215,7 +217,7 @@ val type_in_type_constant : Constant.t -> env -> bool
    [c] is opaque, [NotEvaluableConst NoBody] if it has no
    body, [NotEvaluableConst IsProj] if [c] is a projection,
    [NotEvaluableConst (IsPrimitive p)] if [c] is primitive [p]
-   and [Not_found] if it does not exist in [env] *)
+   and an anomaly if it does not exist in [env] *)
 
 type const_evaluation_result =
   | NoBody
@@ -254,9 +256,11 @@ val add_mind_key : MutInd.t -> mind_key -> env -> env
 val add_mind : MutInd.t -> mutual_inductive_body -> env -> env
 
 (** Looks up in the context of global inductive names 
-   raises [Not_found] if the required path is not found *)
+   raises an anomaly if the required path is not found *)
 val lookup_mind : MutInd.t -> env -> mutual_inductive_body
 
+val mem_mind : MutInd.t -> env -> bool
+
 (** The universe context associated to the inductive, empty if not
     polymorphic *)
 val mind_context : env -> MutInd.t -> Univ.AUContext.t
diff --git a/kernel/names.ml b/kernel/names.ml
index 9802d4f531..b755ff0e08 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -675,6 +675,7 @@ module InductiveOrdered_env = struct
 end
 
 module Indset = Set.Make(InductiveOrdered)
+module Indset_env = Set.Make(InductiveOrdered_env)
 module Indmap = Map.Make(InductiveOrdered)
 module Indmap_env = Map.Make(InductiveOrdered_env)
 
@@ -688,6 +689,8 @@ module ConstructorOrdered_env = struct
   let compare = constructor_user_ord
 end
 
+module Constrset = Set.Make(ConstructorOrdered)
+module Constrset_env = Set.Make(ConstructorOrdered_env)
 module Constrmap = Map.Make(ConstructorOrdered)
 module Constrmap_env = Map.Make(ConstructorOrdered_env)
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 78eb9295d4..0c92a2f2bc 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -471,7 +471,7 @@ end
 
 module Mindset : CSig.SetS with type elt = MutInd.t
 module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset
-module Mindmap_env : CSig.MapS with type key = MutInd.t
+module Mindmap_env : CMap.ExtS with type key = MutInd.t
 
 (** Designation of a (particular) inductive type. *)
 type inductive = MutInd.t      (* the name of the inductive type *)
@@ -484,11 +484,14 @@ type constructor = inductive   (* designates the inductive type *)
                  * int         (* the index of the constructor
                                   BEWARE: indexing starts from 1. *)
 
-module Indset : CSig.SetS with type elt = inductive
-module Indmap : CSig.MapS with type key = inductive
-module Constrmap : CSig.MapS with type key = constructor
-module Indmap_env : CSig.MapS with type key = inductive
-module Constrmap_env : CSig.MapS with type key = constructor
+module Indset : CSet.S with type elt = inductive
+module Constrset : CSet.S with type elt = constructor
+module Indset_env : CSet.S with type elt = inductive
+module Constrset_env : CSet.S with type elt = constructor
+module Indmap : CMap.ExtS with type key = inductive and module Set := Indset
+module Constrmap : CMap.ExtS with type key = constructor and module Set := Constrset
+module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset_env
+module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env
 
 val ind_modpath : inductive -> ModPath.t
 val constr_modpath : constructor -> ModPath.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 00559206ee..e846b17aa0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -302,8 +302,8 @@ let lift_constant c =
 let push_private_constants env eff =
   let eff = side_effects_of_private_constants eff in
   let add_if_undefined env eff =
-    try ignore(Environ.lookup_constant eff.seff_constant env); env
-    with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env
+    if Environ.mem_constant eff.seff_constant env then env
+    else Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env
   in
   List.fold_left add_if_undefined env eff
 
@@ -598,8 +598,8 @@ let inline_side_effects env body side_eff =
   (** First step: remove the constants that are still in the environment *)
   let filter e =
     let cb = (e.seff_constant, e.seff_body) in
-    try ignore (Environ.lookup_constant e.seff_constant env); None
-    with Not_found -> Some (cb, e.from_env)
+    if Environ.mem_constant e.seff_constant env then None
+    else Some (cb, e.from_env)
   in
   (* CAVEAT: we assure that most recent effects come first *)
   let side_eff = List.map_filter filter (SideEffects.repr side_eff) in
@@ -750,9 +750,7 @@ let translate_direct_opaque env kn ce =
   { cb with const_body = OpaqueDef c }
 
 let export_side_effects mb env (b_ctx, eff) =
-      let not_exists e =
-        try ignore(Environ.lookup_constant e.seff_constant env); false
-        with Not_found -> true in
+      let not_exists e = not (Environ.mem_constant e.seff_constant env) in
       let aux (acc,sl) e =
         if not (not_exists e) then acc, sl
         else e :: acc, e.from_env :: sl in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index a43549f6c3..0a6c3afd0d 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -620,18 +620,16 @@ let lookup_eliminator env ind_sp s =
   let knc = KerName.make mpc l in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
-  try
-    let cst = Constant.make knu knc in
-    let _ = lookup_constant cst env in
-      GlobRef.ConstRef cst
-  with Not_found ->
-  (* Then try to get a user-defined eliminator in some other places *)
-  (* using short name (e.g. for "eq_rec") *)
-  try Nametab.locate (qualid_of_ident id)
-  with Not_found ->
-    user_err ~hdr:"default_elim"
-      (strbrk "Cannot find the elimination combinator " ++
-       Id.print id ++ strbrk ", the elimination of the inductive definition " ++
-       Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind_sp) ++
-       strbrk " on sort " ++ Sorts.pr_sort_family s ++
-       strbrk " is probably not allowed.")
+  let cst = Constant.make knu knc in
+  if mem_constant cst env then GlobRef.ConstRef cst
+  else
+    (* Then try to get a user-defined eliminator in some other places *)
+    (* using short name (e.g. for "eq_rec") *)
+    try Nametab.locate (qualid_of_ident id)
+    with Not_found ->
+      user_err ~hdr:"default_elim"
+        (strbrk "Cannot find the elimination combinator " ++
+         Id.print id ++ strbrk ", the elimination of the inductive definition " ++
+         Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind_sp) ++
+         strbrk " on sort " ++ Sorts.pr_sort_family s ++
+         strbrk " is probably not allowed.")
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 866c0da555..e8a2189611 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -241,8 +241,10 @@ let invert_name labs l {binder_name=na0} env sigma ref na =
 	let refi = match ref with
 	  | EvalRel _ | EvalEvar _ -> None
 	  | EvalVar id' -> Some (EvalVar id)
-	  | EvalConst kn ->
-	      Some (EvalConst (Constant.change_label kn (Label.of_id id))) in
+          | EvalConst kn ->
+            let kn = Constant.change_label kn (Label.of_id id) in
+            if Environ.mem_constant kn env then Some (EvalConst kn) else None
+        in
 	match refi with
 	  | None -> None
 	  | Some ref ->
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index cb034bdff6..dacef1cb18 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -135,11 +135,13 @@ let lookup_constant_in_impl cst fallback =
       | None -> anomaly (str "Print Assumption: unknown constant " ++ Constant.print cst ++ str ".")
 
 let lookup_constant cst =
-  try
-    let cb = Global.lookup_constant cst in
+  let env = Global.env() in
+  if not (Environ.mem_constant cst env)
+  then lookup_constant_in_impl cst None
+  else
+    let cb = Environ.lookup_constant cst env in
     if Declareops.constant_has_body cb then cb
     else lookup_constant_in_impl cst (Some cb)
-  with Not_found -> lookup_constant_in_impl cst None
 
 let lookup_mind_in_impl mind =
   try
@@ -150,8 +152,9 @@ let lookup_mind_in_impl mind =
     anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind ++ str ".")
 
 let lookup_mind mind =
-  try Global.lookup_mind mind
-  with Not_found -> lookup_mind_in_impl mind
+  let env = Global.env() in
+  if Environ.mem_mind mind env then Environ.lookup_mind mind env
+  else lookup_mind_in_impl mind
 
 (** Graph traversal of an object, collecting on the way the dependencies of
     traversed objects *)