diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 16 | ||||
| -rw-r--r-- | kernel/environ.mli | 10 | ||||
| -rw-r--r-- | kernel/names.ml | 3 | ||||
| -rw-r--r-- | kernel/names.mli | 15 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 12 |
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 |