aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml255
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/declarations.ml6
-rw-r--r--kernel/declareops.ml4
-rw-r--r--kernel/float64.ml16
-rw-r--r--kernel/indTyping.ml43
-rw-r--r--kernel/indTyping.mli9
-rw-r--r--kernel/indtypes.ml66
-rw-r--r--kernel/indtypes.mli3
-rw-r--r--kernel/inferCumulativity.ml28
-rw-r--r--kernel/inferCumulativity.mli13
-rw-r--r--kernel/nativelib.ml31
-rw-r--r--kernel/safe_typing.ml30
-rw-r--r--kernel/safe_typing.mli6
-rw-r--r--kernel/section.ml10
-rw-r--r--kernel/section.mli8
-rw-r--r--kernel/type_errors.ml7
-rw-r--r--kernel/type_errors.mli12
-rw-r--r--kernel/uGraph.ml2
-rw-r--r--kernel/uint63_31.ml43
-rw-r--r--kernel/univ.ml42
-rw-r--r--kernel/univ.mli9
22 files changed, 403 insertions, 242 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 261a3510d6..f1eb000c88 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -144,11 +144,11 @@ let abstract_context hyps =
in
Context.Named.fold_outside fold hyps ~init:([], [])
-let abstract_constant_type t (hyps, subst) =
+let abstract_as_type t (hyps, subst) =
let t = Vars.subst_vars subst t in
List.fold_left (fun c d -> mkProd_wo_LetIn d c) t hyps
-let abstract_constant_body c (hyps, subst) =
+let abstract_as_body c (hyps, subst) =
let c = Vars.subst_vars subst c in
it_mkLambda_or_LetIn c hyps
@@ -192,8 +192,7 @@ let discharge_abstract_universe_context subst abs_ctx auctx =
let auctx = Univ.subst_univs_level_abstract_universe_context substf auctx in
subst, (AUContext.union abs_ctx auctx)
-let lift_univs cb subst auctx0 =
- match cb.const_universes with
+let lift_univs subst auctx0 = function
| Monomorphic ctx ->
assert (AUContext.is_empty auctx0);
subst, (Monomorphic ctx)
@@ -219,7 +218,7 @@ let cook_constr { Opaqueproof.modlist ; abstract } (c, priv) =
let expmod = expmod_constr_subst cache modlist usubst in
let hyps = Context.Named.map expmod abstract in
let hyps = abstract_context hyps in
- let c = abstract_constant_body (expmod c) hyps in
+ let c = abstract_as_body (expmod c) hyps in
(c, priv)
let cook_constr infos c =
@@ -230,11 +229,11 @@ let cook_constant { from = cb; info } =
let { Opaqueproof.modlist; abstract } = info in
let cache = RefTable.create 13 in
let abstract, usubst, abs_ctx = abstract in
- let usubst, univs = lift_univs cb usubst abs_ctx in
+ let usubst, univs = lift_univs usubst abs_ctx cb.const_universes in
let expmod = expmod_constr_subst cache modlist usubst in
let hyps0 = Context.Named.map expmod abstract in
let hyps = abstract_context hyps0 in
- let map c = abstract_constant_body (expmod c) hyps in
+ let map c = abstract_as_body (expmod c) hyps in
let body = match cb.const_body with
| Undef _ as x -> x
| Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
@@ -243,7 +242,7 @@ let cook_constant { from = cb; info } =
| Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
in
let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in
- let typ = abstract_constant_type (expmod cb.const_type) hyps in
+ let typ = abstract_as_type (expmod cb.const_type) hyps in
{
cook_body = body;
cook_type = typ;
@@ -259,104 +258,160 @@ let cook_constant { from = cb; info } =
(********************************)
(* Discharging mutual inductive *)
-(* Replace
-
- Var(y1)..Var(yq):C1..Cq |- Ij:Bj
- Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti
-
- by
-
- |- Ij: (y1..yq:C1..Cq)Bj
- I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
-*)
-
-let it_mkNamedProd_wo_LetIn b d =
- List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) b d
-
-let abstract_inductive decls nparamdecls inds =
- let open Entries in
- let ntyp = List.length inds in
- let ndecls = Context.Named.length decls in
- let args = Context.Named.to_instance mkVar (List.rev decls) in
- let args = Array.of_list args in
- let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in
- let inds' =
- List.map
- (function (tname,arity,template,cnames,lc) ->
- let lc' = List.map (Vars.substl subs) lc in
- let lc'' = List.map (fun b -> it_mkNamedProd_wo_LetIn b decls) lc' in
- let arity' = it_mkNamedProd_wo_LetIn arity decls in
- (tname,arity',template,cnames,lc''))
- inds in
- let nparamdecls' = nparamdecls + Array.length args in
-(* To be sure to be the same as before, should probably be moved to cook_inductive *)
- let params' = let (_,arity,_,_,_) = List.hd inds' in
- let (params,_) = decompose_prod_n_assum nparamdecls' arity in
- params
+let template_level_of_var ~template_check d =
+ (* When [template_check], a universe from a section variable may not
+ be in the universes from the inductive (it must be pre-declared)
+ so always [None]. *)
+ if template_check then None
+ else
+ let c = Term.strip_prod_assum (RelDecl.get_type d) in
+ match kind c with
+ | Sort (Type u) -> Univ.Universe.level u
+ | _ -> None
+
+let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
+
+let abstract_rel_ctx (section_decls,subst) ctx =
+ (* Dealing with substitutions between contexts is too annoying, so
+ we reify [ctx] into a big [forall] term and work on that. *)
+ let t = it_mkProd_or_LetIn mkProp ctx in
+ let t = Vars.subst_vars subst t in
+ let t = it_mkProd_wo_LetIn t section_decls in
+ let ctx, t = decompose_prod_assum t in
+ assert (Constr.equal t mkProp);
+ ctx
+
+let abstract_lc ~ntypes expmod (newparams,subst) c =
+ let args = Array.rev_of_list (CList.map_filter (fun d ->
+ if RelDecl.is_local_def d then None
+ else match RelDecl.get_name d with
+ | Anonymous -> assert false
+ | Name id -> Some (mkVar id))
+ newparams)
in
- let ind'' =
- List.map
- (fun (a,arity,template,c,lc) ->
- let _, short_arity = decompose_prod_n_assum nparamdecls' arity in
- let shortlc =
- List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in
- { mind_entry_typename = a;
- mind_entry_arity = short_arity;
- mind_entry_template = template;
- mind_entry_consnames = c;
- mind_entry_lc = shortlc })
- inds'
- in (params',ind'')
-
-let refresh_polymorphic_type_of_inductive (_,mip) =
- match mip.mind_arity with
- | RegularArity s -> s.mind_user_arity, false
- | TemplateArity ar ->
- let ctx = List.rev mip.mind_arity_ctxt in
- mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
+ let diff = List.length newparams in
+ let subs = List.init ntypes (fun k ->
+ lift diff (mkApp (mkRel (k+1), args)))
+ in
+ let c = Vars.substl subs c in
+ let c = Vars.subst_vars subst (expmod c) in
+ let c = it_mkProd_wo_LetIn c newparams in
+ c
+
+let abstract_projection ~params expmod hyps t =
+ let t = it_mkProd_or_LetIn t params in
+ let t = mkArrowR mkProp t in (* dummy type standing in for the inductive *)
+ let t = abstract_as_type (expmod t) hyps in
+ let _, t = decompose_prod_n_assum (List.length params + 1 + Context.Rel.nhyps (fst hyps)) t in
+ t
+
+let cook_one_ind ~template_check ~ntypes
+ (section_decls,_ as hyps) expmod mip =
+ let mind_arity = match mip.mind_arity with
+ | RegularArity {mind_user_arity=arity;mind_sort=sort} ->
+ let arity = abstract_as_type (expmod arity) hyps in
+ let sort = destSort (expmod (mkSort sort)) in
+ RegularArity {mind_user_arity=arity; mind_sort=sort}
+ | TemplateArity {template_param_levels=levels;template_level;template_context} ->
+ let sec_levels = CList.map_filter (fun d ->
+ if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d)
+ else None)
+ section_decls
+ in
+ let levels = List.rev_append sec_levels levels in
+ TemplateArity {template_param_levels=levels;template_level;template_context}
+ in
+ let mind_arity_ctxt =
+ let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in
+ abstract_rel_ctx hyps ctx
+ in
+ let mind_user_lc =
+ Array.map (abstract_lc ~ntypes expmod hyps)
+ mip.mind_user_lc
+ in
+ let mind_nf_lc = Array.map (fun (ctx,t) ->
+ let lc = it_mkProd_or_LetIn t ctx in
+ let lc = abstract_lc ~ntypes expmod hyps lc in
+ decompose_prod_assum lc)
+ mip.mind_nf_lc
+ in
+ { mind_typename = mip.mind_typename;
+ mind_arity_ctxt;
+ mind_arity;
+ mind_consnames = mip.mind_consnames;
+ mind_user_lc;
+ mind_nrealargs = mip.mind_nrealargs;
+ mind_nrealdecls = mip.mind_nrealdecls;
+ mind_kelim = mip.mind_kelim;
+ mind_nf_lc;
+ mind_consnrealargs = mip.mind_consnrealargs;
+ mind_consnrealdecls = mip.mind_consnrealdecls;
+ mind_recargs = mip.mind_recargs; (* TODO is this correct? checker should tell us. *)
+ mind_relevance = mip.mind_relevance;
+ mind_nb_constant = mip.mind_nb_constant;
+ mind_nb_args = mip.mind_nb_args;
+ mind_reloc_tbl = mip.mind_reloc_tbl;
+ }
let cook_inductive { Opaqueproof.modlist; abstract } mib =
- let open Entries in
let (section_decls, subst, abs_uctx) = abstract in
- let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
- let subst, ind_univs =
- match mib.mind_universes with
- | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx
- | Polymorphic auctx ->
- let subst, auctx = discharge_abstract_universe_context subst abs_uctx auctx in
- let subst = Univ.make_instance_subst subst in
- let nas = Univ.AUContext.names auctx in
- let auctx = Univ.AUContext.repr auctx in
- subst, Polymorphic_entry (nas, auctx)
- in
+ let subst, mind_universes = lift_univs subst abs_uctx mib.mind_universes in
let cache = RefTable.create 13 in
- let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in
- let inds =
- Array.map_to_list
- (fun mip ->
- let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
- let arity = discharge ty in
- let lc = Array.map discharge mip.mind_user_lc in
- (mip.mind_typename,
- arity, template,
- Array.to_list mip.mind_consnames,
- Array.to_list lc))
- mib.mind_packets in
- let section_decls' = Context.Named.map discharge section_decls in
- let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
- let record = match mib.mind_record with
- | PrimRecord info ->
- Some (Some (Array.map (fun (x,_,_,_) -> x) info))
- | FakeRecord -> Some None
- | NotRecord -> None
+ let expmod = expmod_constr_subst cache modlist subst in
+ let section_decls = Context.Named.map expmod section_decls in
+ let removed_vars = Context.Named.to_vars section_decls in
+ let section_decls, _ as hyps = abstract_context section_decls in
+ let nnewparams = Context.Rel.nhyps section_decls in
+ let template_check = mib.mind_typing_flags.check_template in
+ let mind_params_ctxt =
+ let ctx = Context.Rel.map expmod mib.mind_params_ctxt in
+ abstract_rel_ctx hyps ctx
+ in
+ let ntypes = mib.mind_ntypes in
+ let mind_packets =
+ Array.map (cook_one_ind ~template_check ~ntypes hyps expmod)
+ mib.mind_packets
in
- { mind_entry_record = record;
- mind_entry_finite = mib.mind_finite;
- mind_entry_params = params';
- mind_entry_inds = inds';
- mind_entry_private = mib.mind_private;
- mind_entry_cumulative = Option.has_some mib.mind_variance;
- mind_entry_universes = ind_univs
+ let mind_record = match mib.mind_record with
+ | NotRecord -> NotRecord
+ | FakeRecord -> FakeRecord
+ | PrimRecord data ->
+ let data = Array.map (fun (id,projs,relevances,tys) ->
+ let tys = Array.map (abstract_projection ~params:mib.mind_params_ctxt expmod hyps) tys in
+ (id,projs,relevances,tys))
+ data
+ in
+ PrimRecord data
+ in
+ let mind_hyps =
+ List.filter (fun d -> not (Id.Set.mem (NamedDecl.get_id d) removed_vars))
+ mib.mind_hyps
+ in
+ let mind_variance, mind_sec_variance =
+ match mib.mind_variance, mib.mind_sec_variance with
+ | None, None -> None, None
+ | None, Some _ | Some _, None -> assert false
+ | Some variance, Some sec_variance ->
+ let sec_variance, newvariance =
+ Array.chop (Array.length sec_variance - AUContext.size abs_uctx)
+ sec_variance
+ in
+ Some (Array.append newvariance variance), Some sec_variance
+ in
+ {
+ mind_packets;
+ mind_record;
+ mind_finite = mib.mind_finite;
+ mind_ntypes = mib.mind_ntypes;
+ mind_hyps;
+ mind_nparams = mib.mind_nparams + nnewparams;
+ mind_nparams_rec = mib.mind_nparams_rec + nnewparams;
+ mind_params_ctxt;
+ mind_universes;
+ mind_variance;
+ mind_sec_variance;
+ mind_private = mib.mind_private;
+ mind_typing_flags = mib.mind_typing_flags;
}
let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 83a8b9edfc..c2d47735ec 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -31,7 +31,7 @@ val cook_constr : Opaqueproof.cooking_info list ->
(constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes)
val cook_inductive :
- Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
+ Opaqueproof.cooking_info -> mutual_inductive_body -> mutual_inductive_body
(** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9fd10b32e6..c550b0d432 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -32,6 +32,7 @@ type engagement = set_predicativity
type template_arity = {
template_param_levels : Univ.Level.t option list;
template_level : Univ.Universe.t;
+ template_context : Univ.ContextSet.t;
}
type ('a, 'b) declaration_arity =
@@ -223,6 +224,11 @@ type mutual_inductive_body = {
mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *)
+ mind_sec_variance : Univ.Variance.t array option;
+ (** Variance info for section polymorphic universes. [None]
+ outside sections. The final variance once all sections are
+ discharged is [mind_sec_variance ++ mind_variance]. *)
+
mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 35185b6a5e..047027984d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -49,7 +49,8 @@ let map_decl_arity f g = function
let hcons_template_arity ar =
{ template_param_levels = ar.template_param_levels;
(* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
- template_level = Univ.hcons_univ ar.template_level }
+ template_level = Univ.hcons_univ ar.template_level;
+ template_context = Univ.hcons_universe_context_set ar.template_context }
let universes_context = function
| Monomorphic _ -> Univ.AUContext.empty
@@ -248,6 +249,7 @@ let subst_mind_body sub mib =
mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
mind_universes = mib.mind_universes;
mind_variance = mib.mind_variance;
+ mind_sec_variance = mib.mind_sec_variance;
mind_private = mib.mind_private;
mind_typing_flags = mib.mind_typing_flags;
}
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 3e36373b77..cc661aeba3 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -12,7 +12,10 @@
format *)
type t = float
-let is_nan f = f <> f
+(* The [f : float] type annotation enable the compiler to compile f <> f
+ as comparison on floats rather than the polymorphic OCaml comparison
+ which is much slower. *)
+let is_nan (f : float) = f <> f
let is_infinity f = f = infinity
let is_neg_infinity f = f = neg_infinity
@@ -42,19 +45,20 @@ let abs = abs_float
type float_comparison = FEq | FLt | FGt | FNotComparable
-let eq x y = x = y
+(* See above comment on [is_nan] for the [float] type annotations. *)
+let eq (x : float) (y : float) = x = y
[@@ocaml.inline always]
-let lt x y = x < y
+let lt (x : float) (y : float) = x < y
[@@ocaml.inline always]
-let le x y = x <= y
+let le (x : float) (y : float) = x <= y
[@@ocaml.inline always]
(* inspired by lib/util.ml; see also #10471 *)
-let pervasives_compare = compare
+let pervasives_compare (x : float) (y : float) = compare x y
-let compare x y =
+let compare (x : float) (y : float) =
if x < y then FLt
else
(
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index d9ccf81619..113ee787f2 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -66,7 +66,9 @@ let mind_check_names mie =
type univ_info = { ind_squashed : bool; ind_has_relevant_arg : bool;
ind_min_univ : Universe.t option; (* Some for template *)
- ind_univ : Universe.t }
+ ind_univ : Universe.t;
+ missing : Universe.Set.t; (* missing u <= ind_univ constraints *)
+ }
let check_univ_leq ?(is_real_arg=false) env u info =
let ind_univ = info.ind_univ in
@@ -78,9 +80,8 @@ let check_univ_leq ?(is_real_arg=false) env u info =
if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
else if is_impredicative_univ env ind_univ
- then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
- else raise (InductiveError BadUnivs)
- else raise (InductiveError BadUnivs)
+ && Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
+ else {info with missing = Universe.Set.add u info.missing}
let check_context_univs ~ctor env info ctx =
let check_one d (info,env) =
@@ -109,6 +110,7 @@ let check_arity env_params env_ar ind =
ind_has_relevant_arg=false;
ind_min_univ;
ind_univ=Sorts.univ_of_sort ind_sort;
+ missing=Universe.Set.empty;
}
in
let univ_info = check_indices_matter env_params univ_info indices in
@@ -174,7 +176,7 @@ let check_record data =
(* - all_sorts in case of small, unitary Prop (not smashed) *)
(* - logical_sorts in case of large, unitary Prop (smashed) *)
-let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} =
+let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_;missing=_} =
if not ind_squashed then InType
else Sorts.family (Sorts.sort_of_univ ind_univ)
@@ -197,16 +199,14 @@ let unbounded_from_below u cstrs =
is u_k and is contributing. *)
let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl =
let check_level l =
- if Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
- unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
- not (Univ.LSet.mem l ctor_levels) then
- Some l
- else None
+ Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+ unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
+ not (Univ.LSet.mem l ctor_levels)
in
let univs = Univ.Universe.levels concl in
let univs =
if template_check then
- Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs
+ Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
else univs (* Doesn't check the universes can be generalized *)
in
let fold acc = function
@@ -226,6 +226,8 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc
params, univs
let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+ if not (Universe.Set.is_empty univ_info.missing)
+ then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ)));
let arity = Vars.subst_univs_level_constr usubst arity in
let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
let indices = Vars.subst_univs_level_context usubst indices in
@@ -272,13 +274,13 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
CErrors.user_err
Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
else
- TemplateArity {template_param_levels = param_levels; template_level = min_univ}
+ TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx }
in
let kelim = allowed_sorts univ_info in
(arity,lc), (indices,splayed_lc), kelim
-let typecheck_inductive env (mie:mutual_inductive_entry) =
+let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
let () = match mie.mind_entry_inds with
| [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.")
| _ -> ()
@@ -337,8 +339,19 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
data, Some None
in
- (* TODO pass only the needed bits *)
- let variance = InferCumulativity.infer_inductive env mie in
+ let variance = if not mie.mind_entry_cumulative then None
+ else match mie.mind_entry_universes with
+ | Monomorphic_entry _ ->
+ CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.")
+ | Polymorphic_entry (_,uctx) ->
+ let univs = Instance.to_array @@ UContext.instance uctx in
+ let univs = match sec_univs with
+ | None -> univs
+ | Some sec_univs -> Array.append sec_univs univs
+ in
+ let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in
+ Some variances
+ in
(* Abstract universes *)
let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 5c04e860a2..8dea8f046d 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -17,6 +17,7 @@ open Declarations
- environment with inductives + parameters in rel context
- abstracted universes
- checked variance info
+ (variance for section universes is at the beginning of the array)
- record entry (checked to be OK)
- parameters
- for each inductive,
@@ -24,9 +25,11 @@ open Declarations
* (indices * splayed constructor types) (both without params)
* top allowed elimination
*)
-val typecheck_inductive : env -> mutual_inductive_entry ->
- env
- * universes * Univ.Variance.t array option
+val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
+ -> mutual_inductive_entry
+ -> env
+ * universes
+ * Univ.Variance.t array option
* Names.Id.t array option option
* Constr.rel_context
* ((inductive_arity * Constr.types array) *
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 750ac86908..3771454db5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -379,17 +379,25 @@ let check_positivity ~chkpos kn names env_ar_par paramsctxt finite inds =
(************************************************************************)
(* Build the inductive packet *)
-let repair_arity indices = function
- | RegularArity ar -> ar.mind_user_arity
- | TemplateArity ar -> mkArity (indices,Sorts.sort_of_univ ar.template_level)
+let fold_arity f acc params arity indices = match arity with
+ | RegularArity ar -> f acc ar.mind_user_arity
+ | TemplateArity _ ->
+ let fold_ctx acc ctx =
+ List.fold_left (fun acc d ->
+ Context.Rel.Declaration.fold_constr (fun c acc -> f acc c) d acc)
+ acc
+ ctx
+ in
+ fold_ctx (fold_ctx acc params) indices
-let fold_inductive_blocks f =
+let fold_inductive_blocks f acc params inds =
Array.fold_left (fun acc ((arity,lc),(indices,_),_) ->
- f (Array.fold_left f acc lc) (repair_arity indices arity))
+ fold_arity f (Array.fold_left f acc lc) params arity indices)
+ acc inds
-let used_section_variables env inds =
+let used_section_variables env params inds =
let fold l c = Id.Set.union (Environ.global_vars_set env c) l in
- let ids = fold_inductive_blocks fold Id.Set.empty inds in
+ let ids = fold_inductive_blocks fold Id.Set.empty params inds in
keep_hyps env ids
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
@@ -458,10 +466,11 @@ let compute_projections (kn, i as ind) mib =
Array.of_list (List.rev rs),
Array.of_list (List.rev pbs)
-let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs =
+let build_inductive env ~sec_univs names prv univs variance
+ paramsctxt kn isrecord isfinite inds nmr recargs =
let ntypes = Array.length inds in
(* Compute the set of used section variables *)
- let hyps = used_section_variables env inds in
+ let hyps = used_section_variables env paramsctxt inds in
let nparamargs = Context.Rel.nhyps paramsctxt in
(* Check one inductive *)
let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg =
@@ -479,18 +488,17 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
in
(* Assigning VM tags to constructors *)
let nconst, nblock = ref 0, ref 0 in
- let transf num =
- let arity = List.length (dest_subterms recarg).(num) in
- if Int.equal arity 0 then
- let p = (!nconst, 0) in
- incr nconst; p
- else
- let p = (!nblock + 1, arity) in
- incr nblock; p
- (* les tag des constructeur constant commence a 0,
- les tag des constructeur non constant a 1 (0 => accumulator) *)
+ let transf arity =
+ if Int.equal arity 0 then
+ let p = (!nconst, 0) in
+ incr nconst; p
+ else
+ let p = (!nblock + 1, arity) in
+ incr nblock; p
+ (* les tag des constructeur constant commence a 0,
+ les tag des constructeur non constant a 1 (0 => accumulator) *)
in
- let rtbl = Array.init (List.length cnames) transf in
+ let rtbl = Array.map transf consnrealargs in
(* Build the inductive packet *)
{ mind_typename = id;
mind_arity = arity;
@@ -510,6 +518,15 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
mind_reloc_tbl = rtbl;
} in
let packets = Array.map3 build_one_packet names inds recargs in
+ let variance, sec_variance = match variance with
+ | None -> None, None
+ | Some variance -> match sec_univs with
+ | None -> Some variance, None
+ | Some sec_univs ->
+ let nsec = Array.length sec_univs in
+ Some (Array.sub variance nsec (Array.length variance - nsec)),
+ Some (Array.sub variance 0 nsec)
+ in
let mib =
(* Build the mutual inductive *)
{ mind_record = NotRecord;
@@ -522,6 +539,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
mind_packets = packets;
mind_universes = univs;
mind_variance = variance;
+ mind_sec_variance = sec_variance;
mind_private = prv;
mind_typing_flags = Environ.typing_flags env;
}
@@ -542,9 +560,11 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
(************************************************************************)
(************************************************************************)
-let check_inductive env kn mie =
+let check_inductive env ~sec_univs kn mie =
(* First type-check the inductive definition *)
- let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
+ let (env_ar_par, univs, variance, record, paramsctxt, inds) =
+ IndTyping.typecheck_inductive env ~sec_univs mie
+ in
(* Then check positivity conditions *)
let chkpos = (Environ.typing_flags env).check_positive in
let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
@@ -555,6 +575,6 @@ let check_inductive env kn mie =
(Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
in
(* Build the inductive packets *)
- build_inductive env names mie.mind_entry_private univs variance
+ build_inductive env ~sec_univs names mie.mind_entry_private univs variance
paramsctxt kn record mie.mind_entry_finite
inds nmr recargs
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 240ba4e2bb..9b54e8b878 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -14,4 +14,5 @@ open Environ
open Entries
(** Check an inductive. *)
-val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
+val check_inductive : env -> sec_univs:Univ.Level.t array option
+ -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 77abe6b410..211c909241 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -188,15 +188,12 @@ let infer_arity_constructor is_arity env variances arcn =
open Entries
-let infer_inductive_core env params entries uctx =
- let uarray = Instance.to_array @@ UContext.instance uctx in
- if Array.is_empty uarray then raise TrivialVariance;
- let env = Environ.push_context uctx env in
+let infer_inductive_core env univs entries =
+ if Array.is_empty univs then raise TrivialVariance;
let variances =
Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
- LMap.empty uarray
+ LMap.empty univs
in
- let env, _ = Typeops.check_context env params in
let variances = List.fold_left (fun variances entry ->
let variances = infer_arity_constructor true
env variances entry.mind_entry_arity
@@ -210,17 +207,8 @@ let infer_inductive_core env params entries uctx =
| exception Not_found -> Invariant
| IrrelevantI -> Irrelevant
| CovariantI -> Covariant)
- uarray
-
-let infer_inductive env mie =
- let open Entries in
- let params = mie.mind_entry_params in
- let entries = mie.mind_entry_inds in
- if not mie.mind_entry_cumulative then None
- else
- let uctx = match mie.mind_entry_universes with
- | Monomorphic_entry _ -> assert false
- | Polymorphic_entry (_,uctx) -> uctx
- in
- try Some (infer_inductive_core env params entries uctx)
- with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
+ univs
+
+let infer_inductive ~env_params univs entries =
+ try infer_inductive_core env_params univs entries
+ with TrivialVariance -> Array.make (Array.length univs) Invariant
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index 2bddfe21e2..a8f593c7f9 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -8,5 +8,14 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
- Univ.Variance.t array option
+val infer_inductive
+ : env_params:Environ.env
+ (** Environment containing the polymorphic universes and the
+ parameters. *)
+ -> Univ.Level.t array
+ (** Universes whose cumulativity we want to infer. *)
+ -> Entries.one_inductive_entry list
+ (** The inductive block data we want to infer cumulativity for.
+ NB: we ignore the template bool and the names, only the terms
+ are used. *)
+ -> Univ.Variance.t array
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 1cef729916..a62b51e8aa 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -27,15 +27,35 @@ let open_header = List.map mk_open open_header
(* Directory where compiled files are stored *)
let output_dir = ".coq-native"
-(* Extension of genereted ml files, stored for debugging purposes *)
+(* Extension of generated ml files, stored for debugging purposes *)
let source_ext = ".native"
let ( / ) = Filename.concat
-(* We have to delay evaluation of include_dirs because coqlib cannot be guessed
-until flags have been properly initialized *)
+(* Directory for temporary files for the conversion and normalisation
+ (as opposed to compiling the library itself, which uses [output_dir]). *)
+let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "")
+
+let () = at_exit (fun () ->
+ if Lazy.is_val my_temp_dir then
+ try
+ let d = Lazy.force my_temp_dir in
+ Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d);
+ Unix.rmdir d
+ with e ->
+ Feedback.msg_warning
+ Pp.(str "Native compile: failed to cleanup: " ++
+ str(Printexc.to_string e) ++ fnl()))
+
+(* We have to delay evaluation of include_dirs because coqlib cannot
+ be guessed until flags have been properly initialized. It also lets
+ us avoid forcing [my_temp_dir] if we don't need it (eg stdlib file
+ without native compute or native conv uses). *)
let include_dirs () =
- [Filename.get_temp_dir_name (); Envars.coqlib () / "kernel"; Envars.coqlib () / "library"]
+ let base = [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] in
+ if Lazy.is_val my_temp_dir
+ then (Lazy.force my_temp_dir) :: base
+ else base
(* Pointer to the function linking an ML object into coq's toplevel *)
let load_obj = ref (fun _x -> () : string -> unit)
@@ -44,7 +64,8 @@ let rt1 = ref (dummy_value ())
let rt2 = ref (dummy_value ())
let get_ml_filename () =
- let filename = Filename.temp_file "Coq_native" source_ext in
+ let temp_dir = Lazy.force my_temp_dir in
+ let filename = Filename.temp_file ~temp_dir "Coq_native" source_ext in
let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in
filename, prefix
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ee101400d6..8db8a044a8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -321,6 +321,8 @@ let universes_of_private eff =
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
+let structure_body_of_safe_env env = env.revstruct
+
let sections_of_safe_env senv = senv.sections
let get_section = function
@@ -757,7 +759,7 @@ let translate_direct_opaque env kn ce =
let () = assert (is_empty_private u) in
{ cb with const_body = OpaqueDef c }
-let export_side_effects mb env (b_ctx, eff) =
+let export_side_effects mb env eff =
let not_exists e = not (Environ.mem_constant e.seff_constant env) in
let aux (acc,sl) e =
if not (not_exists e) then acc, sl
@@ -774,7 +776,7 @@ let export_side_effects mb env (b_ctx, eff) =
in
let rec translate_seff sl seff acc env =
match seff with
- | [] -> List.rev acc, b_ctx
+ | [] -> List.rev acc
| eff :: rest ->
if Int.equal sl 0 then
let env, cb =
@@ -803,8 +805,8 @@ let push_opaque_proof pf senv =
let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
senv, o
-let export_private_constants ce senv =
- let exported, ce = export_side_effects senv.revstruct senv.env ce in
+let export_private_constants eff senv =
+ let exported = export_side_effects senv.revstruct senv.env eff in
let map senv (kn, c) = match c.const_body with
| OpaqueDef p ->
let local = empty_private c.const_universes in
@@ -817,7 +819,7 @@ let export_private_constants ce senv =
let exported = List.map (fun (kn, _) -> kn) exported in
(* No delayed constants to declare *)
let senv = List.fold_left add_constant_aux senv bodies in
- (ce, exported), senv
+ exported, senv
let add_constant l decl senv =
let kn = Constant.make2 senv.modpath l in
@@ -908,14 +910,19 @@ let check_mind mie lab =
(* The label and the first inductive type name should match *)
assert (Id.equal (Label.to_id lab) oie.mind_entry_typename)
+let add_checked_mind kn mib senv =
+ let mib =
+ match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
+ in
+ add_field (MutInd.label kn,SFBmind mib) (I kn) senv
+
let add_mind l mie senv =
let () = check_mind mie l in
let kn = MutInd.make2 senv.modpath l in
- let mib = Indtypes.check_inductive senv.env kn mie in
- let mib =
- match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
+ let sec_univs = Option.map Section.all_poly_univs senv.sections
in
- kn, add_field (l,SFBmind mib) (I kn) senv
+ let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in
+ kn, add_checked_mind kn mib senv
(** Insertion of module types *)
@@ -1014,9 +1021,8 @@ let close_section senv =
add_constant_aux senv (kn, cb)
| `Inductive (ind, mib) ->
let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
- let mie = Cooking.cook_inductive info mib in
- let _, senv = add_mind (MutInd.label ind) mie senv in
- senv
+ let mib = Cooking.cook_inductive info mib in
+ add_checked_mind ind mib senv
in
List.fold_left fold senv redo
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 92bbd264fa..e472dfd5e5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -37,6 +37,8 @@ val env_of_safe_env : safe_environment -> Environ.env
val sections_of_safe_env : safe_environment -> section_data Section.t option
+val structure_body_of_safe_env : safe_environment -> Declarations.structure_body
+
(** The safe_environment state monad *)
type safe_transformer0 = safe_environment -> safe_environment
@@ -84,8 +86,8 @@ type side_effect_declaration =
type exported_private_constant = Constant.t
val export_private_constants :
- private_constants Entries.proof_output ->
- (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
+ private_constants ->
+ exported_private_constant list safe_transformer
(** returns the main constant *)
val add_constant :
diff --git a/kernel/section.ml b/kernel/section.ml
index 603ef5d006..6fa0543b23 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -28,6 +28,8 @@ type 'a t = {
sec_mono_universes : ContextSet.t;
sec_poly_universes : Name.t array * UContext.t;
(** Universes local to the section *)
+ all_poly_univs : Univ.Level.t array;
+ (** All polymorphic universes, including from previous sections. *)
has_poly_univs : bool;
(** Are there polymorphic universes or constraints, including in previous sections. *)
sec_entries : section_entry list;
@@ -41,6 +43,8 @@ let rec depth sec = 1 + match sec.sec_prev with None -> 0 | Some prev -> depth p
let has_poly_univs sec = sec.has_poly_univs
+let all_poly_univs sec = sec.all_poly_univs
+
let find_emap e (cmap, imap) = match e with
| SecDefinition con -> Cmap.find con cmap
| SecInductive ind -> Mindmap.find ind imap
@@ -57,7 +61,10 @@ let push_context (nas, ctx) sec =
else
let (snas, sctx) = sec.sec_poly_universes in
let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in
- { sec with sec_poly_universes; has_poly_univs = true }
+ let all_poly_univs =
+ Array.append sec.all_poly_univs (Instance.to_array @@ UContext.instance ctx)
+ in
+ { sec with sec_poly_universes; all_poly_univs; has_poly_univs = true }
let rec is_polymorphic_univ u sec =
let (_, uctx) = sec.sec_poly_universes in
@@ -81,6 +88,7 @@ let open_section ~custom sec_prev =
sec_context = 0;
sec_mono_universes = ContextSet.empty;
sec_poly_universes = ([||], UContext.empty);
+ all_poly_univs = Option.cata (fun sec -> sec.all_poly_univs) [| |] sec_prev;
has_poly_univs = Option.cata has_poly_univs false sec_prev;
sec_entries = [];
sec_data = (Cmap.empty, Mindmap.empty);
diff --git a/kernel/section.mli b/kernel/section.mli
index fbd3d8254e..37d0dab317 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -57,6 +57,14 @@ val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t
(** {6 Retrieving section data} *)
+val all_poly_univs : 'a t -> Univ.Level.t array
+(** Returns all polymorphic universes, including those from previous
+ sections. Earlier sections are earlier in the array.
+
+ NB: even if the array is empty there may be polymorphic
+ constraints about monomorphic universes, which prevent declaring
+ monomorphic globals. *)
+
type abstr_info = private {
abstr_ctx : Constr.named_context;
(** Section variables of this prefix *)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f221ac7a4f..c2cdf98ee8 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -12,6 +12,7 @@ open Names
open Constr
open Environ
open Reduction
+open Univ
(* Type errors. *)
@@ -63,8 +64,8 @@ type ('constr, 'types) ptype_error =
| IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
- | UnsatisfiedConstraints of Univ.Constraint.t
- | UndeclaredUniverse of Univ.Level.t
+ | UnsatisfiedConstraints of Constraint.t
+ | UndeclaredUniverse of Level.t
| DisallowedSProp
| BadRelevance
@@ -83,7 +84,7 @@ type inductive_error =
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
- | BadUnivs
+ | MissingConstraints of (Universe.Set.t * Universe.t)
exception InductiveError of inductive_error
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index ae6fd31762..0f29717f12 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -11,6 +11,7 @@
open Names
open Constr
open Environ
+open Univ
(** Type errors. {% \label{typeerrors} %} *)
@@ -64,8 +65,8 @@ type ('constr, 'types) ptype_error =
| IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
- | UnsatisfiedConstraints of Univ.Constraint.t
- | UndeclaredUniverse of Univ.Level.t
+ | UnsatisfiedConstraints of Constraint.t
+ | UndeclaredUniverse of Level.t
| DisallowedSProp
| BadRelevance
@@ -86,7 +87,8 @@ type inductive_error =
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
- | BadUnivs
+ | MissingConstraints of (Universe.Set.t * Universe.t)
+ (* each universe in the set should have been <= the other one *)
exception InductiveError of inductive_error
@@ -133,9 +135,9 @@ val error_ill_typed_rec_body :
val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
-val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
+val error_unsatisfied_constraints : env -> Constraint.t -> 'a
-val error_undeclared_universe : env -> Univ.Level.t -> 'a
+val error_undeclared_universe : env -> Level.t -> 'a
val error_disallowed_sprop : env -> 'a
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 33336079bb..4d15ce741c 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -128,7 +128,7 @@ let enforce_leq_alg u v g =
| exception (UniverseInconsistency _ as e) -> Inr e)
in
(* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *)
- let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in
+ let c = List.map (fun u -> List.map (fun v -> (u,v)) (Universe.repr v)) (Universe.repr u) in
let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in
(* We pick a best constraint: smallest number of constraints, not an error if possible. *)
let order x y = match x, y with
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index e38389ca13..445166f6af 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -15,8 +15,8 @@ let _ = assert (Sys.word_size = 32)
let uint_size = 63
-let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF"
-let maxuint31 = Int64.of_string "0x7FFFFFFF"
+let maxuint63 = 0x7FFF_FFFF_FFFF_FFFFL
+let maxuint31 = 0x7FFF_FFFFL
let zero = Int64.zero
let one = Int64.one
@@ -118,27 +118,30 @@ let div21 xh xl y =
let div21 xh xl y =
if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y
- (* exact multiplication *)
+(* exact multiplication *)
let mulc x y =
- let lx = ref (Int64.logand x maxuint31) in
- let ly = ref (Int64.logand y maxuint31) in
+ let lx = Int64.logand x maxuint31 in
+ let ly = Int64.logand y maxuint31 in
let hx = Int64.shift_right x 31 in
let hy = Int64.shift_right y 31 in
- let hr = ref (Int64.mul hx hy) in
- let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in
- hr := (Int64.shift_right_logical !hr 1);
- lx := Int64.mul !lx hy;
- ly := Int64.mul hx !ly;
- hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32));
- lr := Int64.add !lr (Int64.shift_left !lx 31);
- hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
- lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr);
- hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
- if Int64.logand !lr Int64.min_int <> 0L
- then Int64.(sub !hr one, mask63 !lr)
- else (!hr, !lr)
-
-let equal x y = mask63 x = mask63 y
+ (* compute the median products *)
+ let s = Int64.add (Int64.mul lx hy) (Int64.mul hx ly) in
+ (* s fits on 64 bits, split it into a 33-bit high part and a 31-bit low part *)
+ let lr = Int64.shift_left (Int64.logand s maxuint31) 31 in
+ let hr = Int64.shift_right_logical s 31 in
+ (* add the outer products *)
+ let lr = Int64.add (Int64.mul lx ly) lr in
+ let hr = Int64.add (Int64.mul hx hy) hr in
+ (* hr fits on 64 bits, since the final result fits on 126 bits *)
+ (* now x * y = hr * 2^62 + lr and lr < 2^63 *)
+ let lr = Int64.add lr (Int64.shift_left (Int64.logand hr 1L) 62) in
+ let hr = Int64.shift_right_logical hr 1 in
+ (* now x * y = hr * 2^63 + lr, but lr might be too large *)
+ if Int64.logand lr Int64.min_int <> 0L
+ then Int64.add hr 1L, mask63 lr
+ else hr, lr
+
+let equal (x : t) y = x = y
let compare x y = Int64.compare x y
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0029ff96d5..94f7076c02 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -42,6 +42,8 @@ struct
let make dp i = (DirPath.hcons dp,i)
+ let repr x : t = x
+
let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d)
@@ -320,8 +322,9 @@ struct
if u == v then 0
else
let (x, n) = u and (x', n') = v in
- if Int.equal n n' then Level.compare x x'
- else n - n'
+ let c = Int.compare n n' in
+ if Int.equal 0 c then Level.compare x x'
+ else c
let sprop = hcons (Level.sprop, 0)
let prop = hcons (Level.prop, 0)
@@ -345,8 +348,8 @@ struct
(Level.is_prop u && not (Level.is_sprop v))
else false
- let successor (u,n) =
- if Level.is_small u then type1
+ let successor (u,n as e) =
+ if is_small e then type1
else (u, n + 1)
let addn k (u,n as x) =
@@ -427,6 +430,10 @@ struct
let hcons = Hashcons.recursive_hcons Huniv.generate Huniv.hcons Expr.hcons
+ module Self = struct type nonrec t = t let compare = compare end
+ module Map = CMap.Make(Self)
+ module Set = CSet.Make(Self)
+
let make l = tip (Expr.make l)
let tip x = tip x
@@ -524,15 +531,10 @@ struct
Used to type the products. *)
let sup x y = merge_univs x y
- let empty = []
-
let exists = List.exists
let for_all = List.for_all
-
- let smart_map = List.Smart.map
-
- let map = List.map
+ let repr x : t = x
end
type universe = Universe.t
@@ -550,8 +552,6 @@ let pr_uni = Universe.pr
let sup = Universe.sup
let super = Universe.super
-open Universe
-
let universe_level = Universe.level
@@ -576,7 +576,7 @@ type univ_inconsistency = constraint_type * universe * universe * explanation La
exception UniverseInconsistency of univ_inconsistency
let error_inconsistency o u v p =
- raise (UniverseInconsistency (o,make u,make v,p))
+ raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
(* Constraints and sets of constraints. *)
@@ -677,7 +677,7 @@ let enforce_eq u v c =
let constraint_add_leq v u c =
(* We just discard trivial constraints like u<=u *)
- if Expr.equal v u then c
+ if Universe.Expr.equal v u then c
else
match v, u with
| (x,n), (y,m) ->
@@ -695,13 +695,13 @@ let constraint_add_leq v u c =
else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *)
-let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
+let check_univ_leq_one u v = Universe.exists (Universe.Expr.leq u) v
let check_univ_leq u v =
Universe.for_all (fun u -> check_univ_leq_one u v) u
let enforce_leq u v c =
- match is_sprop u, is_sprop v with
+ match Universe.is_sprop u, Universe.is_sprop v with
| true, true -> c
| true, false | false, true ->
raise (UniverseInconsistency (Le, u, v, None))
@@ -755,6 +755,10 @@ struct
| Invariant, _ | _, Invariant -> Invariant
| Covariant, Covariant -> Covariant
+ let equal a b = match a,b with
+ | Irrelevant, Irrelevant | Covariant, Covariant | Invariant, Invariant -> true
+ | (Irrelevant | Covariant | Invariant), _ -> false
+
let check_subtype x y = match x, y with
| (Irrelevant | Covariant | Invariant), Irrelevant -> true
| Irrelevant, Covariant -> false
@@ -921,7 +925,7 @@ let subst_instance_instance s i =
let subst_instance_universe s u =
let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
- let u' = Universe.smart_map f u in
+ let u' = List.Smart.map f u in
if u == u' then u
else Universe.sort u'
@@ -1104,7 +1108,7 @@ let subst_univs_level_level subst l =
let subst_univs_level_universe subst u =
let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in
- let u' = Universe.smart_map f u in
+ let u' = List.Smart.map f u in
if u == u' then u
else Universe.sort u'
@@ -1146,7 +1150,7 @@ let subst_univs_universe fn ul =
if CList.is_empty subst then ul
else
let substs =
- List.fold_left Universe.merge_univs Universe.empty subst
+ List.fold_left Universe.merge_univs [] subst
in
List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
substs nosubst
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ccb5c80cbf..94e57b9efc 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -16,6 +16,7 @@ sig
type t
val make : Names.DirPath.t -> int -> t
+ val repr : t -> Names.DirPath.t * int
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
@@ -138,8 +139,10 @@ sig
val exists : (Level.t * int -> bool) -> t -> bool
val for_all : (Level.t * int -> bool) -> t -> bool
+ val repr : t -> (Level.t * int) list
- val map : (Level.t * int -> 'a) -> t -> 'a list
+ module Set : CSet.S with type elt = t
+ module Map : CMap.ExtS with type key = t and module Set := Set
end
@@ -263,6 +266,8 @@ sig
val pr : t -> Pp.t
+ val equal : t -> t -> bool
+
end
(** {6 Universe instances} *)
@@ -320,7 +325,7 @@ val in_punivs : 'a -> 'a puniverses
val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
(** A vector of universe levels with universe Constraint.t,
- representiong local universe variables and associated Constraint.t *)
+ representing local universe variables and associated Constraint.t *)
module UContext :
sig
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 01:44:00 +0000