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.

3 files changed, 20 insertions, 2 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) ->