aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml27
-rw-r--r--library/declaremods.ml7
-rw-r--r--library/global.ml38
-rw-r--r--library/lib.ml19
-rw-r--r--library/lib.mli7
-rw-r--r--library/library.ml2
-rw-r--r--library/library.mllib1
-rw-r--r--library/univops.ml79
-rw-r--r--library/univops.mli17
9 files changed, 142 insertions, 55 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 7d0edbc8b3..db3dbcbd92 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -158,7 +158,7 @@ let cache_constant ((sp,kn), obj) =
assert (eq_constant kn' (constant_of_kn kn));
Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
let cst = Global.lookup_constant kn' in
- add_section_constant cst.const_polymorphic kn' cst.const_hyps;
+ add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
add_constant_kind (constant_of_kn kn) obj.cst_kind
@@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
let kn' = Global.add_mind dir id mie in
assert (eq_mind kn' (mind_of_kn kn));
let mind = Global.lookup_mind kn' in
- add_section_kn mind.mind_polymorphic kn' mind.mind_hyps;
+ add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
Dischargedhypsmap.set_discharged_hyps sp dhyps;
List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
@@ -351,11 +351,27 @@ let dummy_inductive_entry (_,m) = ([],{
mind_entry_record = None;
mind_entry_finite = Decl_kinds.BiFinite;
mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
- mind_entry_polymorphic = false;
- mind_entry_universes = Univ.UContext.empty;
+ mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty;
mind_entry_private = None;
})
+(* reinfer subtyping constraints for inductive after section is dischared. *)
+let infer_inductive_subtyping (pth, mind_ent) =
+ match mind_ent.mind_entry_universes with
+ | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
+ (pth, mind_ent)
+ | Cumulative_ind_entry cumi ->
+ begin
+ let env = Global.env () in
+ let env' =
+ Environ.push_context
+ (Univ.CumulativityInfo.univ_context cumi) env
+ in
+ (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
+ let evd = Evd.from_env env' in
+ (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent)
+ end
+
type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
let inInductive : inductive_obj -> obj =
@@ -365,7 +381,8 @@ let inInductive : inductive_obj -> obj =
open_function = open_inductive;
classify_function = (fun a -> Substitute (dummy_inductive_entry a));
subst_function = ident_subst_function;
- discharge_function = discharge_inductive }
+ discharge_function = discharge_inductive;
+ rebuild_function = infer_inductive_subtyping }
let declare_projections mind =
let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
diff --git a/library/declaremods.ml b/library/declaremods.ml
index c98d4a7f31..187b749b87 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -589,7 +589,6 @@ let start_module interp_modast export id args res fs =
openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
let prefix = Lib.start_module export id mp fs in
Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
- Lib.add_frozen_state ();
if_xml (Hook.get f_xml_start_module) mp;
mp
@@ -629,7 +628,6 @@ let end_module () =
assert (eq_full_path (fst newoname) (fst oldoname));
assert (ModPath.equal (mp_of_kn (snd newoname)) mp);
- Lib.add_frozen_state () (* to prevent recaching *);
if_xml (Hook.get f_xml_end_module) mp;
mp
@@ -701,7 +699,6 @@ let start_modtype interp_modast id args mtys fs =
openmodtype_info := sub_mty_l;
let prefix = Lib.start_modtype id mp fs in
Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
- Lib.add_frozen_state ();
if_xml (Hook.get f_xml_start_module_type) mp;
mp
@@ -719,7 +716,6 @@ let end_modtype () =
assert (eq_full_path (fst oname) (fst oldoname));
assert (ModPath.equal (mp_of_kn (snd oname)) mp);
- Lib.add_frozen_state ()(* to prevent recaching *);
if_xml (Hook.get f_xml_end_module_type) mp;
mp
@@ -894,8 +890,7 @@ let get_library_native_symbols dir =
let start_library dir =
let mp = Global.start_library dir in
openmod_info := default_module_info;
- Lib.start_compilation dir mp;
- Lib.add_frozen_state ()
+ Lib.start_compilation dir mp
let end_library_hook = ref ignore
let append_end_library_hook f =
diff --git a/library/global.ml b/library/global.ml
index 1ba86699d3..6d80012f47 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -176,19 +176,14 @@ let type_of_global_unsafe r =
Vars.subst_instance_constr (Univ.UContext.instance univs) ty
| IndRef ind ->
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- let inst =
- if mib.Declarations.mind_polymorphic then
- Univ.UContext.instance mib.Declarations.mind_universes
- else Univ.Instance.empty
- in
+ let inst = Declareops.inductive_polymorphic_instance mib in
Inductive.type_of_inductive env (specif, inst)
| ConstructRef cstr ->
let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- let inst = Univ.UContext.instance mib.Declarations.mind_universes in
- Inductive.type_of_constructor (cstr,inst) specif
+ let inst = Declareops.inductive_polymorphic_instance mib in
+ Inductive.type_of_constructor (cstr,inst) specif
let type_of_global_in_context env r =
- let open Declarations in
match r with
| VarRef id -> Environ.named_type id env, Univ.UContext.empty
| ConstRef c ->
@@ -199,21 +194,17 @@ let type_of_global_in_context env r =
Typeops.type_of_constant_type env cb.Declarations.const_type, univs
| IndRef ind ->
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- let univs =
- if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes
- else Univ.UContext.empty
- in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
+ let univs = Declareops.inductive_polymorphic_context mib in
+ Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
| ConstructRef cstr ->
- let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- let univs =
- if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes
- else Univ.UContext.empty
- in
- let inst = Univ.UContext.instance univs in
- Inductive.type_of_constructor (cstr,inst) specif, univs
+ let (mib,oib as specif) =
+ Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+ in
+ let univs = Declareops.inductive_polymorphic_context mib in
+ let inst = Univ.UContext.instance univs in
+ Inductive.type_of_constructor (cstr,inst) specif, univs
let universes_of_global env r =
- let open Declarations in
match r with
| VarRef id -> Univ.UContext.empty
| ConstRef c ->
@@ -222,10 +213,11 @@ let universes_of_global env r =
(Environ.opaque_tables env) cb
| IndRef ind ->
let (mib, oib) = Inductive.lookup_mind_specif env ind in
- Univ.instantiate_univ_context mib.mind_universes
+ Declareops.inductive_polymorphic_context mib
| ConstructRef cstr ->
- let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Univ.instantiate_univ_context mib.mind_universes
+ let (mib,oib) =
+ Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+ Declareops.inductive_polymorphic_context mib
let universes_of_global gr =
universes_of_global (env ()) gr
diff --git a/library/lib.ml b/library/lib.ml
index 9d71a854f0..8127316d73 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -27,7 +27,6 @@ type node =
| ClosedModule of library_segment
| OpenedSection of object_prefix * Summary.frozen
| ClosedSection of library_segment
- | FrozenState of Summary.frozen
and library_entry = object_name * node
@@ -80,7 +79,6 @@ let classify_segment seg =
| (_,OpenedModule (ty,_,_,_)) :: _ ->
user_err ~hdr:"Lib.classify_segment"
(str "there are still opened " ++ str (module_kind ty) ++ str "s")
- | (_,FrozenState _) :: stk -> clean acc stk
in
clean ([],[],[]) (List.rev seg)
@@ -254,10 +252,6 @@ let add_anonymous_leaf ?(cache_first = true) obj =
cache_object (oname,obj)
end
-let add_frozen_state () =
- add_anonymous_entry
- (FrozenState (Summary.freeze_summaries ~marshallable:`No))
-
(* Modules. *)
let is_opening_node = function
@@ -408,7 +402,7 @@ let find_opening_node id =
type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
type variable_context = variable_info list
-type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
+type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t
type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
@@ -471,9 +465,9 @@ let add_section_replacement f g poly hyps =
let () = check_same_poly poly vars in
let sechyps,ctx = extract_hyps (vars,hyps) in
let ctx = Univ.ContextSet.to_context ctx in
- let subst, ctx = Univ.abstract_universes true ctx in
+ let subst, ctx = Univ.abstract_universes ctx in
let args = instance_from_variable_context (List.rev sechyps) in
- sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
+ sectab := (vars,f (Univ.AUContext.instance ctx,args) exps,
g (sechyps,subst,ctx) abs)::sl
let add_section_kn poly kn =
@@ -544,7 +538,6 @@ let discharge_item ((sp,_ as oname),e) =
match e with
| Leaf lobj ->
Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
- | FrozenState _ -> None
| ClosedSection _ | ClosedModule _ -> None
| OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
anomaly (Pp.str "discharge_item.")
@@ -585,8 +578,7 @@ let freeze ~marshallable =
| n, ClosedModule _ -> Some (n,ClosedModule [])
| n, OpenedSection (op, _) ->
Some(n,OpenedSection(op,Summary.empty_frozen))
- | n, ClosedSection _ -> Some (n,ClosedSection [])
- | _, FrozenState _ -> None)
+ | n, ClosedSection _ -> Some (n,ClosedSection []))
!lib_state.lib_stk in
{ !lib_state with lib_stk }
| _ ->
@@ -596,8 +588,7 @@ let unfreeze st = lib_state := st
let init () =
unfreeze initial_lib_state;
- Summary.init_summaries ();
- add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *)
+ Summary.init_summaries ()
(* Misc *)
diff --git a/library/lib.mli b/library/lib.mli
index 9f9d8c7e5f..284d339801 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -23,7 +23,6 @@ type node =
| ClosedModule of library_segment
| OpenedSection of Libnames.object_prefix * Summary.frozen
| ClosedSection of library_segment
- | FrozenState of Summary.frozen
and library_segment = (Libnames.object_name * node) list
@@ -61,8 +60,6 @@ val pull_to_head : Libnames.object_name -> unit
for each of them *)
val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name
-val add_frozen_state : unit -> unit
-
(** {6 ... } *)
(** The function [contents] gives access to the current entire segment *)
@@ -123,8 +120,6 @@ val end_modtype :
Libnames.object_name * Libnames.object_prefix *
Summary.frozen * library_segment
-(** [Lib.add_frozen_state] must be called after each of the above functions *)
-
(** {6 Compilation units } *)
val start_compilation : Names.DirPath.t -> Names.module_path -> unit
@@ -162,7 +157,7 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t
(** {6 Section management for discharge } *)
type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
type variable_context = variable_info list
-type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
+type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t
val instance_from_variable_context : variable_context -> Names.Id.t array
val named_of_variable_context : variable_context -> Context.Named.t
diff --git a/library/library.ml b/library/library.ml
index 5a5f99cc51..db05ad2b7b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -575,7 +575,7 @@ let require_library_from_dirpath modrefl export =
else
add_anonymous_leaf (in_require (needed,modrefl,export));
if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
- add_frozen_state ()
+ ()
(* the function called by Vernacentries.vernac_import *)
diff --git a/library/library.mllib b/library/library.mllib
index 6f433b77d1..d94fc22919 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,3 +1,4 @@
+Univops
Nameops
Libnames
Globnames
diff --git a/library/univops.ml b/library/univops.ml
new file mode 100644
index 0000000000..60c12f0d81
--- /dev/null
+++ b/library/univops.ml
@@ -0,0 +1,79 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Term
+open Univ
+open Declarations
+
+let universes_of_constr c =
+ let rec aux s c =
+ match kind_of_term c with
+ | Const (_, u) | Ind (_, u) | Construct (_, u) ->
+ LSet.fold LSet.add (Instance.levels u) s
+ | Sort u when not (Sorts.is_small u) ->
+ let u = univ_of_sort u in
+ LSet.fold LSet.add (Universe.levels u) s
+ | _ -> fold_constr aux s c
+ in aux LSet.empty c
+
+let universes_of_inductive mind =
+ let process auctx =
+ let u = Univ.AUContext.instance auctx in
+ let univ_of_one_ind oind =
+ let arity_univs =
+ Context.Rel.fold_outside
+ (fun decl unvs ->
+ Univ.LSet.union
+ (Context.Rel.Declaration.fold_constr
+ (fun cnstr unvs ->
+ let cnstr = Vars.subst_instance_constr u cnstr in
+ Univ.LSet.union
+ (universes_of_constr cnstr) unvs)
+ decl Univ.LSet.empty) unvs)
+ oind.mind_arity_ctxt ~init:Univ.LSet.empty
+ in
+ Array.fold_left (fun unvs cns ->
+ let cns = Vars.subst_instance_constr u cns in
+ Univ.LSet.union (universes_of_constr cns) unvs) arity_univs
+ oind.mind_nf_lc
+ in
+ let univs =
+ Array.fold_left
+ (fun unvs pk ->
+ Univ.LSet.union
+ (univ_of_one_ind pk) unvs
+ )
+ Univ.LSet.empty mind.mind_packets
+ in
+ let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context auctx) in
+ let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in
+ univs
+ in
+ match mind.mind_universes with
+ | Monomorphic_ind _ -> LSet.empty
+ | Polymorphic_ind auctx -> process auctx
+ | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi)
+
+let restrict_universe_context (univs,csts) s =
+ (* Universes that are not necessary to typecheck the term.
+ E.g. univs introduced by tactics and not used in the proof term. *)
+ let diff = LSet.diff univs s in
+ let rec aux diff candid univs ness =
+ let (diff', candid', univs', ness') =
+ Constraint.fold
+ (fun (l, d, r as c) (diff, candid, univs, csts) ->
+ if not (LSet.mem l diff) then
+ (LSet.remove r diff, candid, univs, Constraint.add c csts)
+ else if not (LSet.mem r diff) then
+ (LSet.remove l diff, candid, univs, Constraint.add c csts)
+ else (diff, Constraint.add c candid, univs, csts))
+ candid (diff, Constraint.empty, univs, ness)
+ in
+ if ness' == ness then (LSet.diff univs diff', ness)
+ else aux diff' candid' univs' ness'
+ in aux diff csts univs Constraint.empty
diff --git a/library/univops.mli b/library/univops.mli
new file mode 100644
index 0000000000..5b499c75bc
--- /dev/null
+++ b/library/univops.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Term
+open Univ
+open Declarations
+
+(** Shrink a universe context to a restricted set of variables *)
+
+val universes_of_constr : constr -> universe_set
+val universes_of_inductive : mutual_inductive_body -> universe_set
+val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 11:10:21 +0000