summaryrefslogtreecommitdiff
path: root/toplevel/ind_tables.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/ind_tables.ml')
-rw-r--r--toplevel/ind_tables.ml119
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
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 20:58:43 +0000