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.

5 files changed, 34 insertions, 22 deletions

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