diff options
Diffstat (limited to 'kernel')
34 files changed, 468 insertions, 355 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 15e5c512ed..84eacb196c 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -253,7 +253,7 @@ let mkFloat f = Float f least one argument and the function is not itself an applicative term *) -let kind c = c +let kind (c:t) = c let rec kind_nocast_gen kind c = match kind c with @@ -338,6 +338,19 @@ let isProj c = match kind c with Proj _ -> true | _ -> false let isFix c = match kind c with Fix _ -> true | _ -> false let isCoFix c = match kind c with CoFix _ -> true | _ -> false +let isRef c = match kind c with + | Const _ | Ind _ | Construct _ | Var _ -> true + | _ -> false + +let isRefX x c = + let open GlobRef in + match x, kind c with + | ConstRef c, Const (c', _) -> Constant.equal c c' + | IndRef i, Ind (i', _) -> eq_ind i i' + | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | VarRef id, Var id' -> Id.equal id id' + | _ -> false + (* Destructs a de Bruijn index *) let destRel c = match kind c with | Rel n -> n diff --git a/kernel/constr.mli b/kernel/constr.mli index d4af1149c2..159570b5ea 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -256,6 +256,8 @@ val isRel : constr -> bool val isRelN : int -> constr -> bool val isVar : constr -> bool val isVarId : Id.t -> constr -> bool +val isRef : constr -> bool +val isRefX : GlobRef.t -> constr -> bool val isInd : constr -> bool val isEvar : constr -> bool val isMeta : constr -> bool diff --git a/kernel/context.ml b/kernel/context.ml index 7e394da2ed..500ed20343 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -196,12 +196,10 @@ struct (** Return a new rel-context enriched by with a given inner-most declaration. *) let add d ctx = d :: ctx - (** Return the number of {e local declarations} in a given context. *) + (** Return the number of {e local declarations} in a given rel-context. *) let length = List.length - (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] - with n = |Δ| and with the local definitions of [Γ] skipped in - [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) + (** Return the number of {e local assumptions} in a given rel-context. *) let nhyps ctx = let open Declaration in let rec nhyps acc = function @@ -413,7 +411,7 @@ struct (** empty named-context *) let empty = [] - (** empty named-context *) + (** Return a new named-context enriched by with a given inner-most declaration. *) let add d ctx = d :: ctx (** Return the number of {e local declarations} in a given named-context. *) diff --git a/kernel/context.mli b/kernel/context.mli index 8f233613da..04aa039a01 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -129,7 +129,7 @@ sig (** Return a new rel-context enriched by with a given inner-most declaration. *) val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt - (** Return the number of {e local declarations} in a given context. *) + (** Return the number of {e local declarations} in a given rel-context. *) val length : ('c, 't) pt -> int (** Check whether given two rel-contexts are equal. *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 261a3510d6..31dd26d2ba 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,148 @@ 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 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 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 ~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 None + 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 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 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 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 ~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..ac130d018d 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 = @@ -88,10 +89,6 @@ type typing_flags = { indices_matter: bool; (** The universe of an inductive type must be above that of its indices. *) - check_template : bool; - (* If [false] then we don't check that the universes template-polymorphic - inductive parameterize on are necessarily local and unbounded from below. - This potentially introduces inconsistencies. *) } (* some contraints are in constant_constraints, some other may be in @@ -223,6 +220,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..a3adac7a11 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -26,7 +26,6 @@ let safe_flags oracle = { enable_VM = true; enable_native_compiler = true; indices_matter = true; - check_template = true; } (** {6 Arities } *) @@ -49,7 +48,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 +248,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/environ.ml b/kernel/environ.ml index f04863386f..501ac99ff3 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -275,7 +275,6 @@ let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded let indices_matter env = env.env_typing_flags.indices_matter -let check_template env = env.env_typing_flags.check_template let universes env = env.env_stratification.env_universes let universes_lbound env = env.env_stratification.env_universes_lbound @@ -399,9 +398,6 @@ let add_constraints c env = let check_constraints c env = UGraph.check_constraints c env.env_stratification.env_universes -let push_constraints_to_env (_,univs) env = - add_constraints univs env - let add_universes ~lbound ~strict ctx g = let g = Array.fold_left (fun g v -> UGraph.add_universe ~lbound ~strict v g) @@ -449,7 +445,6 @@ let same_flags { share_reduction; enable_VM; enable_native_compiler; - check_template; } alt = check_guarded == alt.check_guarded && check_positive == alt.check_positive && @@ -458,8 +453,7 @@ let same_flags { indices_matter == alt.indices_matter && share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && - enable_native_compiler == alt.enable_native_compiler && - check_template == alt.check_template + enable_native_compiler == alt.enable_native_compiler [@warning "+9"] let set_typing_flags c env = (* Unsafe *) @@ -591,9 +585,6 @@ let polymorphic_pind (ind,u) env = let type_in_type_ind (mind,_i) env = not (lookup_mind mind env).mind_typing_flags.check_universes -let template_checked_ind (mind,_i) env = - (lookup_mind mind env).mind_typing_flags.check_template - let template_polymorphic_ind (mind,i) env = match (lookup_mind mind env).mind_packets.(i).mind_arity with | TemplateArity _ -> true @@ -802,14 +793,6 @@ let get_template_polymorphic_variables env r = | IndRef ind -> template_polymorphic_variables ind env | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env -let is_template_checked env r = - let open Names.GlobRef in - match r with - | VarRef _id -> false - | ConstRef _c -> false - | IndRef ind -> template_checked_ind ind env - | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env - let is_type_in_type env r = let open Names.GlobRef in match r with diff --git a/kernel/environ.mli b/kernel/environ.mli index bd5a000c2b..a596584cbe 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -112,7 +112,6 @@ val is_impredicative_set : env -> bool val type_in_type : env -> bool val deactivated_guard : env -> bool val indices_matter : env -> bool -val check_template : env -> bool val is_impredicative_sort : env -> Sorts.t -> bool val is_impredicative_univ : env -> Univ.Universe.t -> bool @@ -274,7 +273,6 @@ val type_in_type_ind : inductive -> env -> bool val template_polymorphic_ind : inductive -> env -> bool val template_polymorphic_variables : inductive -> env -> Univ.Level.t list val template_polymorphic_pind : pinductive -> env -> bool -val template_checked_ind : inductive -> env -> bool (** {5 Modules } *) @@ -288,22 +286,21 @@ val lookup_modtype : ModPath.t -> env -> module_type_body (** {5 Universe constraints } *) -(** Add universe constraints to the environment. - @raise UniverseInconsistency . -*) val add_constraints : Univ.Constraint.t -> env -> env +(** Add universe constraints to the environment. + @raise UniverseInconsistency. *) -(** Check constraints are satifiable in the environment. *) val check_constraints : Univ.Constraint.t -> env -> bool +(** Check constraints are satifiable in the environment. *) + val push_context : ?strict:bool -> Univ.UContext.t -> env -> env -(* [push_context ?(strict=false) ctx env] pushes the universe context to the environment. - @raise UGraph.AlreadyDeclared if one of the universes is already declared. -*) -val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env -(* [push_context_set ?(strict=false) ctx env] pushes the universe context set - to the environment. It does not fail if one of the universes is already declared. *) +(** [push_context ?(strict=false) ctx env] pushes the universe context to the environment. + @raise UGraph.AlreadyDeclared if one of the universes is already declared. *) -val push_constraints_to_env : 'a Univ.constrained -> env -> env +val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env +(** [push_context_set ?(strict=false) ctx env] pushes the universe + context set to the environment. It does not fail even if one of the + universes is already declared. *) val push_subgraph : Univ.ContextSet.t -> env -> env (** [push_subgraph univs env] adds the universes and constraints in @@ -373,7 +370,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat val is_polymorphic : env -> Names.GlobRef.t -> bool val is_template_polymorphic : env -> GlobRef.t -> bool val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list -val is_template_checked : env -> GlobRef.t -> bool val is_type_in_type : env -> GlobRef.t -> bool (** Native compiler *) 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..cc15109f06 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) @@ -195,37 +197,33 @@ let unbounded_from_below u cstrs = (starting from the most recent and ignoring let-definitions) is not contributing to the inductive type's sort or is Some u_k if its level is u_k and is contributing. *) -let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl = +let template_polymorphic_univs ~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 - else univs (* Doesn't check the universes can be generalized *) + Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with | Sort (Type u) -> - if template_check then (match Univ.Universe.level u with | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None | None -> None) - else Univ.Universe.level u | _ -> None) :: acc | LocalDef _ -> acc in let params = List.fold_left fold [] paramsctxt in params, univs -let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets 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 @@ -265,20 +263,20 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp splayed_lc in let param_levels, concl_levels = - template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ + template_polymorphic_univs ~ctor_levels ctx params min_univ in - if template_check && List.for_all (fun x -> Option.is_empty x) param_levels + if List.for_all (fun x -> Option.is_empty x) param_levels && Univ.LSet.is_empty concl_levels then 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,14 +335,24 @@ 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 let params = Vars.subst_univs_level_context usubst params in - let template_check = Environ.check_template env in - let data = List.map (abstract_packets ~template_check univs usubst params) data in + let data = List.map (abstract_packets univs usubst params) data in let env_ar_par = let ctx = Environ.rel_context env_ar_par in diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 5c04e860a2..723ba5459e 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) * @@ -37,7 +40,6 @@ val typecheck_inductive : env -> mutual_inductive_entry -> (* Utility function to compute the actual universe parameters of a template polymorphic inductive *) val template_polymorphic_univs : - template_check:bool -> ctor_levels:Univ.LSet.t -> Univ.ContextSet.t -> Constr.rel_context -> diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 750ac86908..b6b8e5265c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -158,7 +158,7 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let auxntyp = 1 in let specif = (lookup_mind_specif env mi, u) in - let ty = type_of_inductive env specif in + let ty = type_of_inductive specif in let env' = let r = (snd (fst specif)).mind_relevance in let anon = Context.make_annot Anonymous r in @@ -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/inductive.ml b/kernel/inductive.ml index ca4fea45c5..c6035f78ff 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -143,9 +143,16 @@ let remember_subst u subst = Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst with Not_found -> subst +type param_univs = (unit -> Universe.t) list + +let make_param_univs env argtys = + Array.map_to_list (fun arg () -> + Sorts.univ_of_sort (snd (Reduction.dest_arity env arg))) + argtys + (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let make_subst env = +let make_subst = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) @@ -158,8 +165,8 @@ let make_subst env = (* arity is a global level which, at typing time, will be enforce *) (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) - let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in - make (cons_subst u s subst) (sign, exp, args) + let s = a () in + make (cons_subst u s subst) (sign, exp, args) | LocalAssum (_na,_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 *) @@ -178,9 +185,8 @@ let make_subst env = exception SingletonInductiveBecomesProp of Id.t -let instantiate_universes env ctx ar argsorts = - let args = Array.to_list argsorts in - let subst = make_subst env (ctx,ar.template_param_levels,args) in +let instantiate_universes ctx ar args = + let subst = make_subst (ctx,ar.template_param_levels,args) in let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) @@ -198,12 +204,19 @@ let relevance_of_inductive env ind = let _, mip = lookup_mind_specif env ind in mip.mind_relevance -let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps = +let check_instance mib u = + if not (match mib.mind_universes with + | Monomorphic _ -> Instance.is_empty u + | Polymorphic uctx -> Instance.length u = AUContext.size uctx) + then CErrors.anomaly Pp.(str "bad instance length on mutind.") + +let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps = + check_instance mib u; match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes env ctx ar paramtyps in + let ctx,s = instantiate_universes ctx ar paramtyps in (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. the situation where a non-Prop singleton inductive becomes Prop when applied to Prop params *) @@ -211,21 +224,21 @@ let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps = then raise (SingletonInductiveBecomesProp mip.mind_typename); Term.mkArity (List.rev ctx,s) -let type_of_inductive env pind = - type_of_inductive_gen env pind [||] +let type_of_inductive pind = + type_of_inductive_gen pind [] -let constrained_type_of_inductive env ((mib,_mip),u as pind) = - let ty = type_of_inductive env pind in +let constrained_type_of_inductive ((mib,_mip),u as pind) = + let ty = type_of_inductive pind in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let constrained_type_of_inductive_knowing_parameters env ((mib,_mip),u as pind) args = - let ty = type_of_inductive_gen env pind args in +let constrained_type_of_inductive_knowing_parameters ((mib,_mip),u as pind) args = + let ty = type_of_inductive_gen pind args in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = - type_of_inductive_gen ~polyprop env mip args +let type_of_inductive_knowing_parameters ?(polyprop=true) mip args = + type_of_inductive_gen ~polyprop mip args (* The max of an array of universes *) @@ -244,6 +257,7 @@ let max_inductive_sort = (* Type of a constructor *) let type_of_constructor (cstr, u) (mib,mip) = + check_instance mib u; let ind = inductive_of_constructor cstr in let specif = mip.mind_user_lc in let i = index_of_constructor cstr in @@ -581,7 +595,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let push_ind specif env = let r = specif.mind_relevance in let anon = Context.make_annot Anonymous r in - let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive ((mib,specif),u)) lpar) in push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 8c40c318c5..b690fe1157 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -41,16 +41,22 @@ val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_contex val instantiate_inductive_constraints : mutual_inductive_body -> Instance.t -> Constraint.t -val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained +type param_univs = (unit -> Universe.t) list + +val make_param_univs : Environ.env -> constr array -> param_univs +(** The constr array is the types of the arguments to a template + polymorphic inductive. *) + +val constrained_type_of_inductive : mind_specif puniverses -> types constrained val constrained_type_of_inductive_knowing_parameters : - env -> mind_specif puniverses -> types Lazy.t array -> types constrained + mind_specif puniverses -> param_univs -> types constrained val relevance_of_inductive : env -> inductive -> Sorts.relevance -val type_of_inductive : env -> mind_specif puniverses -> types +val type_of_inductive : mind_specif puniverses -> types val type_of_inductive_knowing_parameters : - env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types + ?polyprop:bool -> mind_specif puniverses -> param_univs -> types val elim_sort : mind_specif -> Sorts.family @@ -117,8 +123,8 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : env -> Constr.rel_context -> - template_arity -> constr Lazy.t array -> Constr.rel_context * Sorts.t +val instantiate_universes : Constr.rel_context -> + template_arity -> param_univs -> Constr.rel_context * Sorts.t (** {6 Debug} *) 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/subtyping.ml b/kernel/subtyping.ml index 0a654adf7f..11c455de73 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -150,8 +150,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* nparams done *) (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let ty1 = type_of_inductive env ((mib1, p1), inst) in - let ty2 = type_of_inductive env ((mib2, p2), inst) in + let ty1 = type_of_inductive ((mib1, p1), inst) in + let ty2 = type_of_inductive ((mib2, p2), inst) in let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in cst in diff --git a/kernel/term.ml b/kernel/term.ml index 87678b911e..a2586e74f7 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -363,24 +363,3 @@ let rec isArity c = | Cast (c,_,_) -> isArity c | Sort _ -> true | _ -> false - -(** Kind of type *) - -(* Experimental, used in Presburger contrib *) -type ('constr, 'types) kind_of_type = - | SortType of Sorts.t - | CastType of 'types * 'types - | ProdType of Name.t Context.binder_annot * 'types * 'types - | LetInType of Name.t Context.binder_annot * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array - -let kind_of_type t = match kind t with - | Sort s -> SortType s - | Cast (c,_,t) -> CastType (c, t) - | Prod (na,t,c) -> ProdType (na, t, c) - | LetIn (na,b,t,c) -> LetInType (na, b, t, c) - | App (c,l) -> AtomicType (c, l) - | (Rel _ | Meta _ | Var _ | Evar _ | Const _ - | Proj _ | Case _ | Fix _ | CoFix _ | Ind _) - -> AtomicType (t,[||]) - | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type" diff --git a/kernel/term.mli b/kernel/term.mli index d2de4177ce..1fef54257a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -181,17 +181,6 @@ val destArity : types -> arity (** Tell if a term has the form of an arity *) val isArity : types -> bool -(** {5 Kind of type} *) - -type ('constr, 'types) kind_of_type = - | SortType of Sorts.t - | CastType of 'types * 'types - | ProdType of Name.t Context.binder_annot * 'types * 'types - | LetInType of Name.t Context.binder_annot * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array - -val kind_of_type : types -> (constr, types) kind_of_type - (* Deprecated *) type sorts_family = Sorts.family = InSProp | InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index f221ac7a4f..6c06c1e0f1 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. *) @@ -47,7 +48,7 @@ type ('constr, 'types) ptype_error = | UnboundVar of variable | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment - | ReferenceVariables of Id.t * 'constr + | ReferenceVariables of Id.t * GlobRef.t | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment * (Sorts.family * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment @@ -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 @@ -181,7 +182,7 @@ let map_ptype_error f = function | UnboundVar id -> UnboundVar id | NotAType j -> NotAType (on_judgment f j) | BadAssumption j -> BadAssumption (on_judgment f j) -| ReferenceVariables (id, c) -> ReferenceVariables (id, f c) +| ReferenceVariables (id, c) -> ReferenceVariables (id, c) | ElimArity (pi, c, j, ar) -> ElimArity (pi, f c, on_judgment f j, ar) | CaseNotInductive j -> CaseNotInductive (on_judgment f j) | WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index ae6fd31762..d9842ecefa 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} %} *) @@ -48,7 +49,7 @@ type ('constr, 'types) ptype_error = | UnboundVar of variable | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment - | ReferenceVariables of Id.t * 'constr + | ReferenceVariables of Id.t * GlobRef.t | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment * (Sorts.family * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment @@ -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 @@ -100,7 +102,7 @@ val error_not_type : env -> unsafe_judgment -> 'a val error_assumption : env -> unsafe_judgment -> 'a -val error_reference_variables : env -> Id.t -> constr -> 'a +val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a val error_elim_arity : env -> pinductive -> constr -> unsafe_judgment -> @@ -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/typeops.ml b/kernel/typeops.ml index c74bfd0688..80accc1ced 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -116,7 +116,7 @@ let type_of_variable env id = (* Checks if a context of variables can be instantiated by the variables of the current env. Order does not have to be checked assuming that all names are distinct *) -let check_hyps_inclusion env ?evars f c sign = +let check_hyps_inclusion env ?evars c sign = let conv env a b = conv env ?evars a b in Context.Named.fold_outside (fun d1 () -> @@ -133,7 +133,7 @@ let check_hyps_inclusion env ?evars f c sign = | LocalDef _, LocalAssum _ -> raise NotConvertible | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); with Not_found | NotConvertible | Option.Heterogeneous -> - error_reference_variables env id (f c)) + error_reference_variables env id c) sign ~init:() @@ -146,14 +146,14 @@ let check_hyps_inclusion env ?evars f c sign = let type_of_constant env (kn,_u as cst) = let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in + let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in let ty, cu = constant_type env cst in let () = check_constraints cu env in ty let type_of_constant_in env (kn,_u as cst) = let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in + let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in constant_type_in env cst (* Type of a lambda-abstraction. *) @@ -368,19 +368,19 @@ let check_cast env c ct k expected_type = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let type_of_inductive_knowing_parameters env (ind,u as indu) args = +let type_of_inductive_knowing_parameters env (ind,u) args = let (mib,_mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; + check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters - env (spec,u) args + (spec,u) (Inductive.make_param_univs env args) in check_constraints cst env; t -let type_of_inductive env (ind,u as indu) = +let type_of_inductive env (ind,u) = let (mib,mip) = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; + let t,cst = Inductive.constrained_type_of_inductive ((mib,mip),u) in check_constraints cst env; t @@ -390,7 +390,7 @@ let type_of_constructor env (c,_u as cu) = let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in - check_hyps_inclusion env mkConstructU cu mib.mind_hyps + check_hyps_inclusion env (GlobRef.ConstructRef c) mib.mind_hyps in let specif = lookup_mind_specif env (inductive_of_constructor c) in let t,cst = constrained_type_of_constructor cu specif in @@ -461,8 +461,7 @@ let type_of_global_in_context env r = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in let inst = Univ.make_abstract_instance univs in - let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in - Inductive.type_of_inductive env (specif, inst), univs + Inductive.type_of_inductive (specif, inst), univs | ConstructRef cstr -> let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) @@ -515,8 +514,7 @@ let rec execute env cstr = let f', ft = match kind f with | Ind ind when Environ.template_polymorphic_pind ind env -> - let args = Array.map (fun t -> lazy t) argst in - f, type_of_inductive_knowing_parameters env ind args + f, type_of_inductive_knowing_parameters env ind argst | _ -> (* No template polymorphism *) execute env f diff --git a/kernel/typeops.mli b/kernel/typeops.mli index ae816fe26e..f88bc653de 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t (** Check that hyps are included in env and fails with error otherwise *) val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> - ('a -> constr) -> 'a -> Constr.named_context -> unit + GlobRef.t -> Constr.named_context -> unit val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit 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/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 |