aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.mli4
-rw-r--r--kernel/environ.ml42
-rw-r--r--kernel/environ.mli4
-rw-r--r--kernel/indtypes.ml5
-rw-r--r--kernel/inductive.ml5
-rw-r--r--kernel/mod_typing.ml97
-rw-r--r--kernel/mod_typing.mli2
-rw-r--r--kernel/modops.ml6
-rw-r--r--kernel/safe_typing.ml97
-rw-r--r--kernel/safe_typing.mli12
-rw-r--r--kernel/subtyping.ml13
-rw-r--r--kernel/term_typing.ml46
-rw-r--r--kernel/univ.ml127
-rw-r--r--kernel/univ.mli17
14 files changed, 283 insertions, 194 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 561c66b422..7def963e73 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -246,8 +246,8 @@ and module_body =
mod_type : module_signature; (** expanded type *)
(** algebraic type, kept if it's relevant for extraction *)
mod_type_alg : module_expression option;
- (** set of all constraints in the module *)
- mod_constraints : Univ.constraints;
+ (** set of all universes constraints in the module *)
+ mod_constraints : Univ.ContextSet.t;
(** quotiented set of equivalent constants and inductive names *)
mod_delta : Mod_subst.delta_resolver;
mod_retroknowledge : Retroknowledge.action list }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index bf12d6c6dc..1cc07c0ab8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -181,26 +181,44 @@ let fold_named_context_reverse f ~init env =
(* Universe constraints *)
-let add_constraints c env =
- if Univ.Constraint.is_empty c then
- env
- else
- let s = env.env_stratification in
+let map_universes f env =
+ let s = env.env_stratification in
{ env with env_stratification =
- { s with env_universes = Univ.merge_constraints c s.env_universes } }
+ { s with env_universes = f s.env_universes } }
+
+let add_constraints c env =
+ if Univ.Constraint.is_empty c then env
+ else map_universes (Univ.merge_constraints c) env
let check_constraints c env =
Univ.check_constraints c env.env_stratification.env_universes
-let set_engagement c env = (* Unsafe *)
- { env with env_stratification =
- { env.env_stratification with env_engagement = c } }
-
let push_constraints_to_env (_,univs) env =
add_constraints univs env
-let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env
-let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env
+let add_universes strict ctx g =
+ let g = Array.fold_left
+ (* Be lenient, module typing reintroduces universes and constraints due to includes *)
+ (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+ g (Univ.Instance.to_array (Univ.UContext.instance ctx))
+ in
+ Univ.merge_constraints (Univ.UContext.constraints ctx) g
+
+let push_context ?(strict=false) ctx env =
+ map_universes (add_universes strict ctx) env
+
+let add_universes_set strict ctx g =
+ let g = Univ.LSet.fold
+ (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+ (Univ.ContextSet.levels ctx) g
+ in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g
+
+let push_context_set ?(strict=false) ctx env =
+ map_universes (add_universes_set strict ctx) env
+
+let set_engagement c env = (* Unsafe *)
+ { env with env_stratification =
+ { env.env_stratification with env_engagement = c } }
(* Global constants *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4ad0327fc7..9f6ea522a7 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -208,8 +208,8 @@ val add_constraints : Univ.constraints -> env -> env
(** Check constraints are satifiable in the environment. *)
val check_constraints : Univ.constraints -> env -> bool
-val push_context : Univ.universe_context -> env -> env
-val push_context_set : Univ.universe_context_set -> env -> env
+val push_context : ?strict:bool -> Univ.universe_context -> env -> env
+val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
val push_constraints_to_env : 'a Univ.constrained -> env -> env
val set_engagement : engagement -> env -> env
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e3457006d0..5a234d09b9 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -291,7 +291,10 @@ let typecheck_inductive env mie =
let defu = Term.univ_of_sort def_level in
let is_natural =
type_in_type env || (check_leq (universes env') infu defu &&
- not (is_type0m_univ defu && not is_unit))
+ not (is_type0m_univ defu && not is_unit)
+ (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *)
+
+ )
in
let _ =
(** Impredicative sort, always allow *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 87c139f48d..a02d5e2055 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -165,7 +165,10 @@ let rec make_subst env =
(* to be greater than the level of the argument; this is probably *)
(* a useless extra constraint *)
let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
- make (cons_subst u s subst) (sign, exp, args)
+ if Univ.Universe.is_levels s then
+ make (cons_subst u s subst) (sign, exp, args)
+ else (* Cannot handle substitution by i+n universes. *)
+ make subst (sign, exp, args)
| (na,None,t)::sign, Some u::exp, [] ->
(* No more argument here: we add the remaining universes to the *)
(* substitution (when [u] is distinct from all other universes in the *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 4f20e5f62a..922652287b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -21,7 +21,7 @@ open Modops
open Mod_subst
type 'alg translation =
- module_signature * 'alg option * delta_resolver * Univ.constraints
+ module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
let rec mp_from_mexpr = function
| MEident mp -> mp
@@ -52,7 +52,7 @@ let rec rebuild_mp mp l =
| []-> mp
| i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r
-let (+++) = Univ.Constraint.union
+let (+++) = Univ.ContextSet.union
let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let lab,idl = match idl with
@@ -72,33 +72,65 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
(* In the spirit of subtyping.check_constant, we accept
any implementations of parameters and opaques terms,
as long as they have the right type *)
- let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
- let env' = Environ.add_constraints ccst env' in
- let newus, cst = Univ.UContext.dest ctx in
- let env' = Environ.add_constraints cst env' in
- let c',cst = match cb.const_body with
- | Undef _ | OpaqueDef _ ->
- let j = Typeops.infer env' c in
- let typ = Typeops.type_of_constant_type env' cb.const_type in
- let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
- j.uj_type typ in
- j.uj_val,cst' +++ cst
- | Def cs ->
- let cst' = Reduction.infer_conv env' (Environ.universes env') c
- (Mod_subst.force_constr cs) in
- let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
- if cb.const_polymorphic then cst' +++ cst
- else cst' +++ cst
+ let uctx = Declareops.universes_of_constant (opaque_tables env) cb in
+ let uctx = (* Context of the spec *)
+ if cb.const_polymorphic then
+ Univ.instantiate_univ_context uctx
+ else uctx
+ in
+ let c', univs, ctx' =
+ if not cb.const_polymorphic then
+ let env' = Environ.push_context ~strict:true uctx env' in
+ let env' = Environ.push_context ~strict:true ctx env' in
+ let c',cst = match cb.const_body with
+ | Undef _ | OpaqueDef _ ->
+ let j = Typeops.infer env' c in
+ let typ = Typeops.type_of_constant_type env' cb.const_type in
+ let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+ j.uj_type typ in
+ j.uj_val, cst'
+ | Def cs ->
+ let c' = Mod_subst.force_constr cs in
+ c, Reduction.infer_conv env' (Environ.universes env') c c'
+ in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+ else
+ let cus, ccst = Univ.UContext.dest uctx in
+ let newus, cst = Univ.UContext.dest ctx in
+ let () =
+ if not (Univ.Instance.length cus == Univ.Instance.length newus) then
+ error_incorrect_with_constraint lab
+ in
+ let inst = Univ.Instance.append cus newus in
+ let csti = Univ.enforce_eq_instances cus newus cst in
+ let csta = Univ.Constraint.union csti ccst in
+ let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in
+ let () = if not (Univ.check_constraints cst (Environ.universes env')) then
+ error_incorrect_with_constraint lab
+ in
+ let cst = match cb.const_body with
+ | Undef _ | OpaqueDef _ ->
+ let j = Typeops.infer env' c in
+ let typ = Typeops.type_of_constant_type env' cb.const_type in
+ let typ = Vars.subst_instance_constr cus typ in
+ let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+ j.uj_type typ in
+ cst'
+ | Def cs ->
+ let c' = Vars.subst_instance_constr cus (Mod_subst.force_constr cs) in
+ let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
+ cst'
in
- c, cst
+ if not (Univ.Constraint.is_empty cst) then
+ error_incorrect_with_constraint lab;
+ let subst, ctx = Univ.abstract_universes true ctx in
+ Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty
in
let def = Def (Mod_subst.from_val c') in
- let ctx' = Univ.UContext.make (newus, cst) in
let cb' =
{ cb with
const_body = def;
- const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def);
- const_universes = ctx' }
+ const_universes = univs;
+ const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def) }
in
before@(lab,SFBconst(cb'))::after, c', ctx'
else
@@ -145,8 +177,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
begin
try
let mtb_old = module_type_of_module old in
- Subtyping.check_subtypes env' mtb_mp1 mtb_old
- +++ old.mod_constraints
+ Univ.ContextSet.add_constraints (Subtyping.check_subtypes env' mtb_mp1 mtb_old) old.mod_constraints
with Failure _ -> error_incorrect_with_constraint lab
end
| Algebraic (NoFunctor (MEident(mp'))) ->
@@ -194,7 +225,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
| Algebraic (NoFunctor (MEident mp0)) ->
let mpnew = rebuild_mp mp0 idl in
check_modpath_equiv env' mpnew mp;
- before@(lab,spec)::after, equiv, Univ.Constraint.empty
+ before@(lab,spec)::after, equiv, Univ.ContextSet.empty
| _ -> error_generative_module_expected lab
end
with
@@ -207,8 +238,8 @@ let check_with env mp (sign,alg,reso,cst) = function
|WithDef(idl,c) ->
let struc = destr_nofunctor sign in
let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
- let alg' = mk_alg_with alg (WithDef (idl,(c',cst'))) in
- (NoFunctor struc'),alg',reso, cst+++(Univ.UContext.constraints cst')
+ let alg' = mk_alg_with alg (WithDef (idl,(c',Univ.ContextSet.to_context cst'))) in
+ (NoFunctor struc'),alg',reso, cst+++cst'
|WithMod(idl,mp1) as wd ->
let struc = destr_nofunctor sign in
let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
@@ -238,7 +269,7 @@ let rec translate_mse env mpo inl = function
let mtb = lookup_modtype mp1 env in
mtb.mod_type, mtb.mod_delta
in
- sign,Some (MEident mp1),reso,Univ.Constraint.empty
+ sign,Some (MEident mp1),reso,Univ.ContextSet.empty
|MEapply (fe,mp1) ->
translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
|MEwith(me, with_decl) ->
@@ -256,7 +287,7 @@ and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
let body = subst_signature subst fbody_b in
let alg' = mkalg alg mp1 in
let reso' = subst_codom_delta_resolver subst reso in
- body,alg',reso', cst1 +++ cst2
+ body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
| Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
@@ -301,7 +332,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
mk_mod mp impl sign None cst reso
|Some (params_mte,inl) ->
let res_mtb = translate_modtype env mp inl params_mte in
- let auto_mtb = mk_modtype mp sign Univ.Constraint.empty reso in
+ let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
{ res_mtb with
@@ -309,7 +340,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
mod_expr = impl;
(** cst from module body typing, cst' from subtyping,
and constraints from module type. *)
- mod_constraints = cst +++ cst' +++ res_mtb.mod_constraints }
+ mod_constraints = Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
let translate_module env mp inl = function
|MType (params,ty) ->
@@ -324,7 +355,7 @@ let rec translate_mse_incl env mp inl = function
|MEident mp1 ->
let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
let sign = clean_bounded_mod_expr mb.mod_type in
- sign,None,mb.mod_delta,Univ.Constraint.empty
+ sign,None,mb.mod_delta,Univ.ContextSet.empty
|MEapply (fe,arg) ->
let ftrans = translate_mse_incl env mp inl fe in
translate_apply env inl ftrans arg (fun _ _ -> None)
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index b39e821254..80db12b0d3 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -30,7 +30,7 @@ val translate_modtype :
*)
type 'alg translation =
- module_signature * 'alg option * delta_resolver * Univ.constraints
+ module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
val translate_mse :
env -> module_path option -> inline -> module_struct_entry ->
diff --git a/kernel/modops.ml b/kernel/modops.ml
index d52fe611c0..8733ca8c2f 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -331,8 +331,10 @@ let strengthen_const mp_from l cb resolver =
let kn = KerName.make2 mp_from l in
let con = constant_of_delta_kn resolver kn in
let u =
- if cb.const_polymorphic then
- Univ.UContext.instance cb.const_universes
+ if cb.const_polymorphic then
+ let u = Univ.UContext.instance cb.const_universes in
+ let s = Univ.make_instance_subst u in
+ Univ.subst_univs_level_instance s u
else Univ.Instance.empty
in
{ cb with
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 55e767321b..9329b16861 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -118,8 +118,8 @@ type safe_environment =
revstruct : structure_body;
modlabels : Label.Set.t;
objlabels : Label.Set.t;
- univ : Univ.constraints;
- future_cst : Univ.constraints Future.computation list;
+ univ : Univ.ContextSet.t;
+ future_cst : Univ.ContextSet.t Future.computation list;
engagement : engagement option;
required : vodigest DPMap.t;
loads : (module_path * module_body) list;
@@ -148,7 +148,7 @@ let empty_environment =
modlabels = Label.Set.empty;
objlabels = Label.Set.empty;
future_cst = [];
- univ = Univ.Constraint.empty;
+ univ = Univ.ContextSet.empty;
engagement = None;
required = DPMap.empty;
loads = [];
@@ -221,22 +221,23 @@ let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
type constraints_addition =
- Now of Univ.constraints | Later of Univ.constraints Future.computation
+ | Now of bool * Univ.ContextSet.t
+ | Later of Univ.ContextSet.t Future.computation
let add_constraints cst senv =
match cst with
| Later fc ->
{senv with future_cst = fc :: senv.future_cst}
- | Now cst ->
+ | Now (poly,cst) ->
{ senv with
- env = Environ.add_constraints cst senv.env;
- univ = Univ.Constraint.union cst senv.univ }
+ env = Environ.push_context_set ~strict:(not poly) cst senv.env;
+ univ = Univ.ContextSet.union cst senv.univ }
let add_constraints_list cst senv =
- List.fold_right add_constraints cst senv
+ List.fold_left (fun acc c -> add_constraints c acc) senv cst
-let push_context_set ctx = add_constraints (Now (Univ.ContextSet.constraints ctx))
-let push_context ctx = add_constraints (Now (Univ.UContext.constraints ctx))
+let push_context_set poly ctx = add_constraints (Now (poly,ctx))
+let push_context poly ctx = add_constraints (Now (poly,Univ.ContextSet.of_context ctx))
let is_curmod_library senv =
match senv.modvariant with LIBRARY -> true | _ -> false
@@ -246,7 +247,7 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e =
List.fold_left
(fun e fc ->
if Future.UUIDSet.mem (Future.uuid fc) except then e
- else add_constraints (Now (Future.join fc)) e)
+ else add_constraints (Now (false, Future.join fc)) e)
{e with future_cst = []} e.future_cst
let is_joined_environment e = List.is_empty e.future_cst
@@ -337,20 +338,21 @@ let safe_push_named (id,_,_ as d) env =
let push_named_def (id,de) senv =
let c,typ,univs = Term_typing.translate_local_def senv.env id de in
- let senv' = push_context univs senv in
- let c, senv' = match c with
- | Def c -> Mod_subst.force_constr c, senv'
+ let poly = de.Entries.const_entry_polymorphic in
+ let univs = Univ.ContextSet.of_context univs in
+ let c, univs = match c with
+ | Def c -> Mod_subst.force_constr c, univs
| OpaqueDef o ->
- Opaqueproof.force_proof (Environ.opaque_tables senv'.env) o,
- push_context_set
- (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o)
- senv'
+ Opaqueproof.force_proof (Environ.opaque_tables senv.env) o,
+ Univ.ContextSet.union univs
+ (Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
| _ -> assert false in
+ let senv' = push_context_set poly univs senv in
let env'' = safe_push_named (id,Some c,typ) senv'.env in
- {senv' with env=env''}
+ univs, {senv' with env=env''}
-let push_named_assum ((id,t),ctx) senv =
- let senv' = push_context_set ctx senv in
+let push_named_assum ((id,t,poly),ctx) senv =
+ let senv' = push_context_set poly ctx senv in
let t = Term_typing.translate_local_assum senv'.env t in
let env'' = safe_push_named (id,None,t) senv'.env in
{senv' with env=env''}
@@ -373,10 +375,10 @@ let labels_of_mib mib =
let globalize_constant_universes env cb =
if cb.const_polymorphic then
- [Now Univ.Constraint.empty]
+ [Now (true, Univ.ContextSet.empty)]
else
- let cstrs = Univ.UContext.constraints cb.const_universes in
- Now cstrs ::
+ let cstrs = Univ.ContextSet.of_context cb.const_universes in
+ Now (false, cstrs) ::
(match cb.const_body with
| (Undef _ | Def _) -> []
| OpaqueDef lc ->
@@ -384,23 +386,21 @@ let globalize_constant_universes env cb =
| None -> []
| Some fc ->
match Future.peek_val fc with
- | None -> [Later (Future.chain
- ~greedy:(not (Future.is_exn fc))
- ~pure:true fc Univ.ContextSet.constraints)]
- | Some c -> [Now (Univ.ContextSet.constraints c)])
+ | None -> [Later fc]
+ | Some c -> [Now (false, c)])
let globalize_mind_universes mb =
if mb.mind_polymorphic then
- [Now Univ.Constraint.empty]
+ [Now (true, Univ.ContextSet.empty)]
else
- [Now (Univ.UContext.constraints mb.mind_universes)]
+ [Now (false, Univ.ContextSet.of_context mb.mind_universes)]
let constraints_of_sfb env sfb =
match sfb with
| SFBconst cb -> globalize_constant_universes env cb
| SFBmind mib -> globalize_mind_universes mib
- | SFBmodtype mtb -> [Now mtb.mod_constraints]
- | SFBmodule mb -> [Now mb.mod_constraints]
+ | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)]
+ | SFBmodule mb -> [Now (false, mb.mod_constraints)]
(** A generic function for adding a new field in a same environment.
It also performs the corresponding [add_constraints]. *)
@@ -503,13 +503,13 @@ let add_modtype l params_mte inl senv =
(** full_add_module adds module with universes and constraints *)
let full_add_module mb senv =
- let senv = add_constraints (Now mb.mod_constraints) senv in
+ let senv = add_constraints (Now (false, mb.mod_constraints)) senv in
let dp = ModPath.dp mb.mod_mp in
let linkinfo = Nativecode.link_info_of_dirpath dp in
{ senv with env = Modops.add_linked_module mb linkinfo senv.env }
let full_add_module_type mp mt senv =
- let senv = add_constraints (Now mt.mod_constraints) senv in
+ let senv = add_constraints (Now (false, mt.mod_constraints)) senv in
{ senv with env = Modops.add_module_type mp mt senv.env }
(** Insertion of modules *)
@@ -617,8 +617,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv =
modlabels = Label.Set.add (fst newdef) oldsenv.modlabels;
univ =
List.fold_left (fun acc cst ->
- Univ.Constraint.union acc (Future.force cst))
- (Univ.Constraint.union senv.univ oldsenv.univ)
+ Univ.ContextSet.union acc (Future.force cst))
+ (Univ.ContextSet.union senv.univ oldsenv.univ)
now_cst;
future_cst = later_cst @ oldsenv.future_cst;
(* engagement is propagated to the upper level *)
@@ -641,8 +641,8 @@ let end_module l restype senv =
let senv'=
propagate_loads { senv with
env = newenv;
- univ = Univ.Constraint.union senv.univ mb.mod_constraints} in
- let newenv = Environ.add_constraints mb.mod_constraints senv'.env in
+ univ = Univ.ContextSet.union senv.univ mb.mod_constraints} in
+ let newenv = Environ.push_context_set ~strict:true mb.mod_constraints senv'.env in
let newenv = Modops.add_module mb newenv in
let newresolver =
if Modops.is_functor mb.mod_type then oldsenv.modresolver
@@ -667,7 +667,7 @@ let end_modtype l senv =
let () = check_empty_context senv in
let mbids = List.rev_map fst params in
let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
- let newenv = Environ.add_constraints senv.univ newenv in
+ let newenv = Environ.push_context_set ~strict:true senv.univ newenv in
let newenv = set_engagement_opt newenv senv.engagement in
let senv' = propagate_loads {senv with env=newenv} in
let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in
@@ -690,13 +690,16 @@ let add_include me is_module inl senv =
let mtb = translate_modtype senv.env mp_sup inl ([],me) in
mtb.mod_type,mtb.mod_constraints,mtb.mod_delta
in
- let senv = add_constraints (Now cst) senv in
+ let senv = add_constraints (Now (false, cst)) senv in
(* Include Self support *)
let rec compute_sign sign mb resolver senv =
match sign with
| MoreFunctor(mbid,mtb,str) ->
let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
- let senv = add_constraints (Now cst_sub) senv in
+ let senv =
+ add_constraints
+ (Now (false, Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty))
+ senv in
let mpsup_delta =
Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta
in
@@ -707,7 +710,7 @@ let add_include me is_module inl senv =
in
let resolver,sign,senv =
let struc = NoFunctor (List.rev senv.revstruct) in
- let mtb = build_mtb mp_sup struc Univ.Constraint.empty senv.modresolver in
+ let mtb = build_mtb mp_sup struc Univ.ContextSet.empty senv.modresolver in
compute_sign sign mtb resolver senv
in
let str = match sign with
@@ -801,8 +804,10 @@ let import lib cst vodigest senv =
check_engagement senv.env lib.comp_enga;
let mp = MPfile lib.comp_name in
let mb = lib.comp_mod in
- let env = Environ.add_constraints mb.mod_constraints senv.env in
- let env = Environ.push_context_set cst env in
+ let env = Environ.push_context_set ~strict:true
+ (Univ.ContextSet.union mb.mod_constraints cst)
+ senv.env
+ in
mp,
{ senv with
env =
@@ -855,7 +860,9 @@ let register_inline kn senv =
let env = { env with env_globals = new_globals } in
{ senv with env = env_of_pre_env env }
-let add_constraints c = add_constraints (Now c)
+let add_constraints c =
+ add_constraints
+ (Now (false, Univ.ContextSet.add_constraints c Univ.ContextSet.empty))
(* NB: The next old comment probably refers to [propagate_loads] above.
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2b4324b96f..eac08eb834 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -57,9 +57,13 @@ val is_joined_environment : safe_environment -> bool
(** Insertion of local declarations (Local or Variables) *)
val push_named_assum :
- (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0
+ (Id.t * Term.types * bool (* polymorphic *))
+ Univ.in_universe_context_set -> safe_transformer0
+
+(** Returns the full universe context necessary to typecheck the definition
+ (futures are forced) *)
val push_named_def :
- Id.t * Entries.definition_entry -> safe_transformer0
+ Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer
(** Insertion of global axioms or definitions *)
@@ -88,10 +92,10 @@ val add_modtype :
(** Adding universe constraints *)
val push_context_set :
- Univ.universe_context_set -> safe_transformer0
+ bool -> Univ.universe_context_set -> safe_transformer0
val push_context :
- Univ.universe_context -> safe_transformer0
+ bool -> Univ.universe_context -> safe_transformer0
val add_constraints :
Univ.constraints -> safe_transformer0
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index db155e6c86..58f3bcdf00 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -311,15 +311,19 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
try
(* The environment with the expected universes plus equality
of the body instances with the expected instance *)
- let env = Environ.add_constraints cstrs env in
- (* Check that the given definition does not add any constraint over
- the expected ones, so that it can be used in place of the original. *)
+ let ctxi = Univ.Instance.append inst1 inst2 in
+ let ctx = Univ.UContext.make (ctxi, cstrs) in
+ let env = Environ.push_context ctx env in
+ (* Check that the given definition does not add any constraint over
+ the expected ones, so that it can be used in place of
+ the original. *)
if Univ.check_constraints ctx1 (Environ.universes env) then
cstrs, env, inst2
else error (IncompatibleConstraints ctx1)
with Univ.UniverseInconsistency incon ->
error (IncompatibleUniverses incon)
- else cst, env, Univ.Instance.empty
+ else
+ cst, env, Univ.Instance.empty
in
(* Now check types *)
let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
@@ -456,6 +460,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
let check_subtypes env sup super =
let env = add_module_type sup.mod_mp sup env in
+ let env = Environ.push_context_set ~strict:true super.mod_constraints env in
check_modtypes Univ.Constraint.empty env
(strengthen sup sup.mod_mp) super empty_subst
(map_mp super.mod_mp sup.mod_mp sup.mod_delta) false
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 83e566041f..926b387942 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -45,8 +45,8 @@ let map_option_typ = function None -> `None | Some x -> `Some x
let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff
-let handle_side_effects env body side_eff =
- let handle_sideff t se =
+let handle_side_effects env body ctx side_eff =
+ let handle_sideff (t,ctx) se =
let cbl = match se with
| SEsubproof (c,cb,b) -> [c,cb,b]
| SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in
@@ -66,7 +66,7 @@ let handle_side_effects env body side_eff =
| Const (c',u') when eq_constant c c' ->
Vars.subst_instance_constr u' b
| _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
- let fix_body (c,cb,b) t =
+ let fix_body (c,cb,b) (t,ctx) =
match cb.const_body, b with
| Def b, _ ->
let b = Mod_subst.force_constr b in
@@ -74,25 +74,29 @@ let handle_side_effects env body side_eff =
if not poly then
let b_ty = Typeops.type_of_constant_type env cb.const_type in
let t = sub c 1 (Vars.lift 1 t) in
- mkLetIn (cname c, b, b_ty, t)
+ mkLetIn (cname c, b, b_ty, t),
+ Univ.ContextSet.union ctx
+ (Univ.ContextSet.of_context cb.const_universes)
else
let univs = cb.const_universes in
- sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+ sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
| OpaqueDef _, `Opaque (b,_) ->
let poly = cb.const_polymorphic in
if not poly then
let b_ty = Typeops.type_of_constant_type env cb.const_type in
let t = sub c 1 (Vars.lift 1 t) in
- mkApp (mkLambda (cname c, b_ty, t), [|b|])
+ mkApp (mkLambda (cname c, b_ty, t), [|b|]),
+ Univ.ContextSet.union ctx
+ (Univ.ContextSet.of_context cb.const_universes)
else
let univs = cb.const_universes in
- sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+ sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
| _ -> assert false
in
- List.fold_right fix_body cbl t
+ List.fold_right fix_body cbl (t,ctx)
in
(* CAVEAT: we assure a proper order *)
- Declareops.fold_side_effects handle_sideff body
+ Declareops.fold_side_effects handle_sideff (body,ctx)
(Declareops.uniquize_side_effects side_eff)
let hcons_j j =
@@ -100,11 +104,11 @@ let hcons_j j =
let feedback_completion_typecheck =
Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-
+
let infer_declaration env kn dcl =
match dcl with
| ParameterEntry (ctx,poly,(t,uctx),nl) ->
- let env = push_context uctx env in
+ let env = push_context ~strict:(not poly) uctx env in
let j = infer env t in
let abstract = poly && not (Option.is_empty kn) in
let usubst, univs = Univ.abstract_universes abstract uctx in
@@ -115,12 +119,12 @@ let infer_declaration env kn dcl =
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true;
const_entry_polymorphic = false} as c) ->
- let env = push_context c.const_entry_universes env in
+ let env = push_context ~strict:true c.const_entry_universes env in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let tyj = infer_type env typ in
let proofterm =
Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
- let body = handle_side_effects env body side_eff in
+ let body,ctx = handle_side_effects env body ctx side_eff in
let env' = push_context_set ctx env in
let j = infer env' body in
let j = hcons_j j in
@@ -135,14 +139,16 @@ let infer_declaration env kn dcl =
c.const_entry_inline_code, c.const_entry_secctx
| DefinitionEntry c ->
- let env = push_context c.const_entry_universes env in
let { const_entry_type = typ; const_entry_opaque = opaque } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let (body, ctx), side_eff = Future.join body in
- assert(Univ.ContextSet.is_empty ctx);
- let body = handle_side_effects env body side_eff in
+ let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
+ let body, ctx = handle_side_effects env body
+ (Univ.ContextSet.union univsctx ctx) side_eff in
+ let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
- let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
+ let usubst, univs =
+ Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in
let j = infer env body in
let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
@@ -306,5 +312,9 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie
let handle_entry_side_effects env ce = { ce with
const_entry_body = Future.chain ~greedy:true ~pure:true
ce.const_entry_body (fun ((body, ctx), side_eff) ->
- (handle_side_effects env body side_eff, ctx), Declareops.no_seff);
+ let body, ctx' = handle_side_effects env body ctx side_eff in
+ (body, ctx'), Declareops.no_seff);
}
+
+let handle_side_effects env body side_eff =
+ fst (handle_side_effects env body Univ.ContextSet.empty side_eff)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 336cdb653e..73d323426b 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -270,8 +270,10 @@ module Level = struct
let is_small x =
match data x with
| Level _ -> false
- | _ -> true
-
+ | Var _ -> false
+ | Prop -> true
+ | Set -> true
+
let is_prop x =
match data x with
| Prop -> true
@@ -551,6 +553,10 @@ struct
| Cons (l, _, Nil) -> Expr.is_level l
| _ -> false
+ let rec is_levels l = match l with
+ | Cons (l, _, r) -> Expr.is_level l && is_levels r
+ | Nil -> true
+
let level l = match l with
| Cons (l, _, Nil) -> Expr.level l
| _ -> None
@@ -655,7 +661,6 @@ type canonical_arc =
lt: Level.t list;
le: Level.t list;
rank : int;
- predicative : bool;
mutable status : status;
(** Guaranteed to be unset out of the [compare_neq] functions. It is used
to do an imperative traversal of the graph, ensuring a O(1) check that
@@ -670,7 +675,7 @@ let arc_is_lt arc = match arc.status with
| Unset | SetLe -> false
| SetLt -> true
-let terminal u = {univ=u; lt=[]; le=[]; rank=0; predicative=false; status = Unset}
+let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset}
module UMap :
sig
@@ -720,6 +725,16 @@ let enter_arc ca g =
(* Every Level.t has a unique canonical arc representative *)
+(** The graph always contains nodes for Prop and Set. *)
+
+let terminal_lt u v =
+ {(terminal u) with lt=[v]}
+
+let empty_universes =
+ let g = enter_arc (terminal Level.set) UMap.empty in
+ let g = enter_arc (terminal_lt Level.prop Level.set) g in
+ g
+
(* repr : universes -> Level.t -> canonical_arc *)
(* canonical representative : we follow the Equiv links *)
@@ -733,19 +748,28 @@ let rec repr g u =
| Equiv v -> repr g v
| Canonical arc -> arc
-(* [safe_repr] also search for the canonical representative, but
- if the graph doesn't contain the searched universe, we add it. *)
+let get_prop_arc g = repr g Level.prop
+let get_set_arc g = repr g Level.set
+let is_set_arc u = Level.is_set u.univ
+let is_prop_arc u = Level.is_prop u.univ
-let safe_repr g u =
- let rec safe_repr_rec g u =
- match UMap.find u g with
- | Equiv v -> safe_repr_rec g v
- | Canonical arc -> arc
- in
- try g, safe_repr_rec g u
- with Not_found ->
- let can = terminal u in
- enter_arc can g, can
+exception AlreadyDeclared
+
+let add_universe vlev strict g =
+ try
+ let _arcv = UMap.find vlev g in
+ raise AlreadyDeclared
+ with Not_found ->
+ let v = terminal vlev in
+ let arc =
+ let arc = get_set_arc g in
+ if strict then
+ { arc with lt=vlev::arc.lt}
+ else
+ { arc with le=vlev::arc.le}
+ in
+ let g = enter_arc arc g in
+ enter_arc v g
(* reprleq : canonical_arc -> canonical_arc list *)
(* All canonical arcv such that arcu<=arcv with arcv#arcu *)
@@ -789,7 +813,6 @@ let between g arcu arcv =
in
let good,_,_ = explore ([arcv],[],false) arcu in
good
-
(* We assume compare(u,v) = LE with v canonical (see compare below).
In this case List.hd(between g u v) = repr u
Otherwise, between g u v = []
@@ -900,8 +923,9 @@ let get_explanation strict g arcu arcv =
in
find [] arc.lt
in
+ let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in
try
- let (to_revert, c) = cmp [] [] [] [(arcu, [])] in
+ let (to_revert, c) = cmp start [] [] [(arcu, [])] in
(** Reset all the touched arcs. *)
let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
List.rev c
@@ -972,7 +996,6 @@ let fast_compare_neq strict g arcu arcv =
else process_le c to_revert (arc :: lt_todo) le_todo lt le
in
-
try
let (to_revert, c) = cmp FastNLE [] [] [arcu] in
(** Reset all the touched arcs. *)
@@ -1015,24 +1038,18 @@ let is_lt g arcu arcv =
(** First, checks on universe levels *)
let check_equal g u v =
- let g, arcu = safe_repr g u in
- let _, arcv = safe_repr g v in
- arcu == arcv
+ let arcu = repr g u and arcv = repr g v in
+ arcu == arcv
let check_eq_level g u v = u == v || check_equal g u v
-let is_set_arc u = Level.is_set u.univ
-let is_prop_arc u = Level.is_prop u.univ
-let get_prop_arc g = snd (safe_repr g Level.prop)
-
let check_smaller g strict u v =
- let g, arcu = safe_repr g u in
- let g, arcv = safe_repr g v in
+ let arcu = repr g u and arcv = repr g v in
if strict then
is_lt g arcu arcv
else
is_prop_arc arcu
- || (is_set_arc arcu && arcv.predicative)
+ || (is_set_arc arcu && not (is_prop_arc arcv))
|| is_leq g arcu arcv
(** Then, checks on universes *)
@@ -1074,19 +1091,11 @@ let check_leq g u v =
(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
-(** To speed up tests of Set </<= i *)
-let set_predicative g arcv =
- enter_arc {arcv with predicative = true} g
-
(* setlt : Level.t -> Level.t -> reason -> unit *)
(* forces u > v *)
(* this is normally an update of u in g rather than a creation. *)
let setlt g arcu arcv =
let arcu' = {arcu with lt=arcv.univ::arcu.lt} in
- let g =
- if is_set_arc arcu then set_predicative g arcv
- else g
- in
enter_arc arcu' g, arcu'
(* checks that non-redundant *)
@@ -1100,11 +1109,6 @@ let setlt_if (g,arcu) v =
(* this is normally an update of u in g rather than a creation. *)
let setleq g arcu arcv =
let arcu' = {arcu with le=arcv.univ::arcu.le} in
- let g =
- if is_set_arc arcu' then
- set_predicative g arcv
- else g
- in
enter_arc arcu' g, arcu'
(* checks that non-redundant *)
@@ -1120,7 +1124,8 @@ let merge g arcu arcv =
(* we find the arc with the biggest rank, and we redirect all others to it *)
let arcu, g, v =
let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
- if Level.is_small arc.univ || arc.rank >= max_rank
+ if Level.is_small arc.univ ||
+ (arc.rank >= max_rank && not (Level.is_small best_arc.univ))
then (arc.rank, max_rank, arc, best_arc::rest)
else (max_rank, old_max_rank, best_arc, arc::rest)
in
@@ -1150,7 +1155,7 @@ let merge g arcu arcv =
(* we assume compare(u,v) = compare(v,u) = NLE *)
(* merge_disc u v forces u ~ v with repr u as canonical repr *)
let merge_disc g arc1 arc2 =
- let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
+ let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
let arcu, g =
if not (Int.equal arc1.rank arc2.rank) then arcu, g
else
@@ -1173,12 +1178,11 @@ exception UniverseInconsistency of univ_inconsistency
let error_inconsistency o u v (p:explanation option) =
raise (UniverseInconsistency (o,make u,make v,p))
-(* enforc_univ_eq : Level.t -> Level.t -> unit *)
-(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
+(* enforce_univ_eq : Level.t -> Level.t -> unit *)
+(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *)
let enforce_univ_eq u v g =
- let g,arcu = safe_repr g u in
- let g,arcv = safe_repr g v in
+ let arcu = repr g u and arcv = repr g v in
match fast_compare g arcu arcv with
| FastEQ -> g
| FastLT ->
@@ -1197,8 +1201,7 @@ let enforce_univ_eq u v g =
(* enforce_univ_leq : Level.t -> Level.t -> unit *)
(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
let enforce_univ_leq u v g =
- let g,arcu = safe_repr g u in
- let g,arcv = safe_repr g v in
+ let arcu = repr g u and arcv = repr g v in
if is_leq g arcu arcv then g
else
match fast_compare g arcv arcu with
@@ -1211,8 +1214,7 @@ let enforce_univ_leq u v g =
(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
let enforce_univ_lt u v g =
- let g,arcu = safe_repr g u in
- let g,arcv = safe_repr g v in
+ let arcu = repr g u and arcv = repr g v in
match fast_compare g arcu arcv with
| FastLT -> g
| FastLE -> fst (setlt g arcu arcv)
@@ -1225,18 +1227,10 @@ let enforce_univ_lt u v g =
let p = get_explanation false g arcv arcu in
error_inconsistency Lt u v p
-let empty_universes = UMap.empty
-
(* Prop = Set is forbidden here. *)
-let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+let initial_universes = empty_universes
let is_initial_universes g = UMap.equal (==) g initial_universes
-
-let add_universe vlev g =
- let v = terminal vlev in
- let proparc = get_prop_arc g in
- enter_arc {proparc with le=vlev::proparc.le}
- (enter_arc v g)
(* Constraints and sets of constraints. *)
@@ -1370,10 +1364,12 @@ let check_univ_leq u v =
let enforce_leq u v c =
let open Universe.Huniv in
+ let rec aux acc v =
match v with
- | Cons (v, _, Nil) ->
- fold (fun u -> constraint_add_leq u v) u c
- | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+ | Cons (v, _, l) ->
+ aux (fold (fun u -> constraint_add_leq u v) u c) l
+ | Nil -> acc
+ in aux c v
let enforce_leq u v c =
if check_univ_leq u v then c
@@ -1444,7 +1440,6 @@ let normalize_universes g =
lt = LSet.elements lt;
le = LSet.elements le;
rank = rank;
- predicative = false;
status = Unset;
}
in
@@ -1589,7 +1584,7 @@ let sort_universes orig =
let fold i accu u =
if 0 < i then
let pred = types.(i - 1) in
- let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false; status = Unset; } in
+ let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in
UMap.add u (Canonical arc) accu
else accu
in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7aaf2ffe61..4cc8a2528f 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -20,7 +20,11 @@ sig
val is_small : t -> bool
(** Is the universe set or prop? *)
-
+
+ val is_prop : t -> bool
+ val is_set : t -> bool
+ (** Is it specifically Prop or Set *)
+
val compare : t -> t -> int
(** Comparison function *)
@@ -87,6 +91,9 @@ sig
val is_level : t -> bool
(** Test if the universe is a level or an algebraic universe. *)
+ val is_levels : t -> bool
+ (** Test if the universe is a lub of levels or contains +n's. *)
+
val level : t -> Level.t option
(** Try to get a level out of a universe, returns [None] if it
is an algebraic universe. *)
@@ -159,8 +166,12 @@ val is_initial_universes : universes -> bool
val sort_universes : universes -> universes
-(** Adds a universe to the graph, ensuring it is >= Prop. *)
-val add_universe : universe_level -> universes -> universes
+(** Adds a universe to the graph, ensuring it is >= or > Set.
+ @raises AlreadyDeclared if the level is already declared in the graph. *)
+
+exception AlreadyDeclared
+
+val add_universe : universe_level -> bool -> universes -> universes
(** {6 Constraints. } *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:05:04 +0000