aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--clib/cMap.ml10
-rw-r--r--clib/hMap.ml5
-rw-r--r--clib/int.ml7
-rw-r--r--kernel/environ.ml16
-rw-r--r--kernel/environ.mli10
-rw-r--r--kernel/names.ml3
-rw-r--r--kernel/names.mli15
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--pretyping/indrec.ml28
-rw-r--r--pretyping/tacred.ml6
-rw-r--r--vernac/assumptions.ml13
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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 10:55:35 +0000