From 13716dc6561a3379ba130f07ce7ecd1df379475c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jul 2015 18:45:41 +0200 Subject: Give a way to control if the decidable-equality schemes are built like in 8.4 with the schemes of the subcomponent of an inductive added to the environment or discharged as let-ins over the main scheme. As of today, decidable-equality schemes are built when calling vernacular command (Inductive with option Set Dedicable Equality Schemes, or Scheme Equality), so there is no need to discharge the sub-schemes as let-ins. But if ever the schemes are built from within an opaque proof and one would not like the schemes and a fortiori the subschemes to appear in the env, the new addition of a parameter internal_flag to "find_scheme" allows this possibility (then to be set to KernelSilent). --- toplevel/ind_tables.ml | 32 +++++++++++++++----------------- 1 file changed, 15 insertions(+), 17 deletions(-) (limited to 'toplevel/ind_tables.ml') diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 0d39466ed..b59d6fc8a 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -28,11 +28,10 @@ open Pp (**********************************************************************) (* Registering schemes in the environment *) - type mutual_scheme_object_function = - mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects type 'a scheme_kind = string @@ -141,32 +140,31 @@ let define internal id c p univs = in kn -let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) = - let (c, ctx), eff = f ind in +let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = + let (c, ctx), eff = f mode ind in let mib = Global.lookup_mind mind in let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define internal id c mib.mind_polymorphic ctx in + let const = define mode id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; const, Declareops.cons_side_effects (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff -let define_individual_scheme kind internal names (mind,i as ind) = +let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with | _,MutualSchemeFunction f -> assert false | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f internal names ind + define_individual_scheme_base kind s f mode names ind -let define_mutual_scheme_base kind suff f internal names mind = - let (cl, ctx), eff = f mind in +let define_mutual_scheme_base kind suff f mode names mind = + let (cl, ctx), eff = f mode mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in - let consts = Array.map2 (fun id cl -> - define internal id cl mib.mind_polymorphic ctx) ids cl in + define mode id cl mib.mind_polymorphic ctx) ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, @@ -175,11 +173,11 @@ let define_mutual_scheme_base kind suff f internal names mind = kind (Global.safe_env()) (Array.to_list schemes)) eff -let define_mutual_scheme kind internal names mind = +let define_mutual_scheme kind mode names mind = match Hashtbl.find scheme_object_table kind with | _,IndividualSchemeFunction _ -> assert false | s,MutualSchemeFunction f -> - define_mutual_scheme_base kind s f internal names mind + define_mutual_scheme_base kind s f mode names mind let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in @@ -188,14 +186,14 @@ let find_scheme_on_env_too kind ind = kind (Global.safe_env()) [ind, s]) Declareops.no_seff -let find_scheme kind (mind,i as ind) = +let find_scheme ?(mode=KernelSilent) kind (mind,i as ind) = try find_scheme_on_env_too kind ind with Not_found -> match Hashtbl.find scheme_object_table kind with | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f KernelSilent None ind + define_individual_scheme_base kind s f mode None ind | s,MutualSchemeFunction f -> - let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in + let ca, eff = define_mutual_scheme_base kind s f mode [] mind in ca.(i), eff let check_scheme kind ind = -- cgit v1.2.3