diff options
Diffstat (limited to 'toplevel/ind_tables.ml')
| -rw-r--r-- | toplevel/ind_tables.ml | 119 |
1 files changed, 69 insertions, 50 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 932bdfe7..138e5189 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,6 +18,7 @@ open Libobject open Nameops open Declarations open Term +open Errors open Util open Declare open Entries @@ -26,23 +27,28 @@ open Decl_kinds (**********************************************************************) (* Registering schemes in the environment *) -type mutual_scheme_object_function = mutual_inductive -> constr array -type individual_scheme_object_function = inductive -> constr + +type mutual_scheme_object_function = + 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 type 'a scheme_kind = string -let scheme_map = ref Indmap.empty +let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" + +let pr_scheme_kind = Pp.str let cache_one_scheme kind (ind,const) = - let map = try Indmap.find ind !scheme_map with Not_found -> Stringmap.empty in - scheme_map := Indmap.add ind (Stringmap.add kind const map) !scheme_map + let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in + scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map let cache_scheme (_,(kind,l)) = Array.iter (cache_one_scheme kind) l -let subst_one_scheme subst ((mind,i),const) = +let subst_one_scheme subst (ind,const) = (* Remark: const is a def: the result of substitution is a constant *) - ((subst_ind subst mind,i),fst (subst_con subst const)) + (subst_ind subst ind,subst_constant subst const) let subst_scheme (subst,(kind,l)) = (kind,Array.map (subst_one_scheme subst) l) @@ -60,36 +66,24 @@ let inScheme : string * (inductive * constant) array -> obj = discharge_function = discharge_scheme} (**********************************************************************) -(* Saving/restoring the table of scheme *) - -let freeze_schemes () = !scheme_map -let unfreeze_schemes sch = scheme_map := sch -let init_schemes () = scheme_map := Indmap.empty - -let _ = - Summary.declare_summary "Schemes" - { Summary.freeze_function = freeze_schemes; - Summary.unfreeze_function = unfreeze_schemes; - Summary.init_function = init_schemes } - -(**********************************************************************) (* The table of scheme building functions *) type individual type mutual type scheme_object_function = - | MutualSchemeFunction of (mutual_inductive -> constr array) - | IndividualSchemeFunction of (inductive -> constr) + | MutualSchemeFunction of mutual_scheme_object_function + | IndividualSchemeFunction of individual_scheme_object_function let scheme_object_table = (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t) let declare_scheme_object s aux f = - (try check_ident ("ind"^s) - with e when Errors.noncritical e -> - error ("Illegal induction scheme suffix: "^s)); - let key = if aux = "" then s else aux in + let () = + if not (Id.is_valid ("ind" ^ s)) then + error ("Illegal induction scheme suffix: " ^ s) + in + let key = if String.is_empty aux then s else aux in try let _ = Hashtbl.find scheme_object_table key in (* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*) @@ -110,6 +104,8 @@ let declare_individual_scheme_object s ?(aux="") f = let declare_scheme kind indcl = Lib.add_anonymous_leaf (inScheme (kind,indcl)) +let () = Declare.set_declare_scheme declare_scheme + let is_visible_name id = try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true with Not_found -> false @@ -120,30 +116,39 @@ let compute_name internal id = | KernelSilent -> Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name -let define internal id c = +let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in - let kn = fd id - (DefinitionEntry - { const_entry_body = c; - const_entry_secctx = None; - const_entry_type = None; - const_entry_opaque = false }, - Decl_kinds.IsDefinition Scheme) in - (match internal with - | KernelSilent -> () - | _-> definition_message id); + let ctx = Evd.normalize_evar_universe_context univs in + let c = Vars.subst_univs_fn_constr + (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in + let entry = { + const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff); + const_entry_secctx = None; + const_entry_type = None; + const_entry_polymorphic = p; + const_entry_universes = Evd.evar_context_universe_context ctx; + const_entry_opaque = false; + const_entry_inline_code = false; + const_entry_feedback = None; + } in + let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let () = match internal with + | KernelSilent -> () + | _-> definition_message id + in kn let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) = - let c = f ind in + let (c, ctx), eff = f 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 in + let const = define internal id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; - 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) = match Hashtbl.find scheme_object_table kind with @@ -152,14 +157,21 @@ let define_individual_scheme kind internal names (mind,i as ind) = define_individual_scheme_base kind s f internal names ind let define_mutual_scheme_base kind suff f internal names mind = - let cl = f mind in + let (cl, ctx), eff = f mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> - try List.assoc i names + try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in - let consts = array_map2 (define internal) ids cl in - declare_scheme kind (Array.mapi (fun i cst -> ((mind,i),cst)) consts); - consts + + let consts = Array.map2 (fun id cl -> + define internal 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, + Declareops.cons_side_effects + (Safe_typing.sideff_of_scheme + kind (Global.safe_env()) (Array.to_list schemes)) + eff let define_mutual_scheme kind internal names mind = match Hashtbl.find scheme_object_table kind with @@ -167,16 +179,23 @@ let define_mutual_scheme kind internal names mind = | s,MutualSchemeFunction f -> define_mutual_scheme_base kind s f internal names mind +let find_scheme_on_env_too kind ind = + let s = String.Map.find kind (Indmap.find ind !scheme_map) in + s, Declareops.cons_side_effects + (Safe_typing.sideff_of_scheme + kind (Global.safe_env()) [ind, s]) + Declareops.no_seff + let find_scheme kind (mind,i as ind) = - try Stringmap.find kind (Indmap.find ind !scheme_map) + 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 | s,MutualSchemeFunction f -> - (define_mutual_scheme_base kind s f KernelSilent [] mind).(i) + let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in + ca.(i), eff let check_scheme kind ind = - try let _ = Stringmap.find kind (Indmap.find ind !scheme_map) in true + try let _ = find_scheme_on_env_too kind ind in true with Not_found -> false - |