diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 22 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
2 files changed, 16 insertions, 10 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index b8fe1571c8..0e5af77372 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -89,9 +89,6 @@ type module_info = variant : modvariant; resolver : delta_resolver; resolver_of_param : delta_resolver;} - -let check_label l labset = - if Labset.mem l labset then error_existing_label l let set_engagement_opt oeng env = match oeng with @@ -112,6 +109,11 @@ type safe_environment = loads : (module_path * module_body) list; local_retroknowledge : Retroknowledge.action list} +let exists_label l senv = Labset.mem l senv.labset + +let check_label l senv = + if exists_label l senv then error_existing_label l + (* a small hack to avoid variants and an unused case in all functions *) let rec empty_environment = { old = empty_environment; @@ -276,7 +278,7 @@ let hcons_constant_body cb = const_type = hcons_const_type cb.const_type } let add_constant dir l decl senv = - check_label l senv.labset; + check_label l senv; let kn = make_con senv.modinfo.modpath dir l in let cb = match decl with @@ -303,7 +305,7 @@ let add_mind dir l mie senv = if l <> label_of_id id then anomaly ("the label of inductive packet and its first inductive"^ " type do not match"); - check_label l senv.labset; + check_label l senv; (* TODO: when we will allow reorderings we will have to verify all labels *) let kn = make_mind senv.modinfo.modpath dir l in @@ -314,7 +316,7 @@ let add_mind dir l mie senv = (* Insertion of module types *) let add_modtype l mte inl senv = - check_label l senv.labset; + check_label l senv; let mp = MPdot(senv.modinfo.modpath, l) in let mtb = translate_module_type senv.env mp inl mte in let senv' = add_field (l,SFBmodtype mtb) (MT mp) senv in @@ -328,7 +330,7 @@ let full_add_module mb senv = (* Insertion of modules *) let add_module l me inl senv = - check_label l senv.labset; + check_label l senv; let mp = MPdot(senv.modinfo.modpath, l) in let mb = translate_module senv.env mp inl me in let senv' = add_field (l,SFBmodule mb) M senv in @@ -341,7 +343,7 @@ let add_module l me inl senv = (* Interactive modules *) let start_module l senv = - check_label l senv.labset; + check_label l senv; let mp = MPdot(senv.modinfo.modpath, l) in let modinfo = { modpath = mp; label = l; @@ -491,7 +493,7 @@ let end_module l restype senv = let senv = update_resolver (add_delta_resolver resolver) senv in let add senv ((l,elem) as field) = - check_label l senv.labset; + check_label l senv; let new_name = match elem with | SFBconst _ -> let kn = make_kn mp_sup empty_dirpath l in @@ -552,7 +554,7 @@ let add_module_parameter mbid mte inl senv = (* Interactive module types *) let start_modtype l senv = - check_label l senv.labset; + check_label l senv; let mp = MPdot(senv.modinfo.modpath, l) in let modinfo = { modpath = mp; label = l; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 3a79548741..6f46a45be9 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -136,6 +136,10 @@ val safe_infer : safe_environment -> constr -> judgment * Univ.constraints val typing : safe_environment -> constr -> judgment +(** {7 Query } *) + +val exists_label : label -> safe_environment -> bool + (*spiwack: safe retroknowledge functionalities *) open Retroknowledge |