From 256ca51bafc7200c8c006981cad60e57014e0dbc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 26 Feb 2017 21:14:52 +0100 Subject: Do not recompute twice the whnf of terms in conversion. This performance bug was introduced 9 years ago in a8b0345, where the responsibility of normalizing the term went from ccnv to eqappr in Reduction. As a result, all recursive calls to eqappr that were preemptively reducing the term ended up calling whd_stack twice, once by themselves, and once in the subsequent call to eqappr. This caused an important slowdown for conversion-intensive proofs, as the whd_stack calls CClosure.zip to perfom in-place term sharing, leading to useless huge re-allocations and repetitive write barriers. Now that eqappr always head-normalizes the term beforehand, we simply don't call whd_stack anymore when jumping to eqappr. --- kernel/reduction.ml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1ae89347ad..fc379fb7d8 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -322,17 +322,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let (app1,app2) = if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd def1 v1), appr2) + | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> (match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd def2 v2)) + | Some def2 -> (appr1, (lft2, (def2, v2))) | None -> raise NotConvertible) else match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd def2 v2)) + | Some def2 -> (appr1, (lft2, (def2, v2))) | None -> (match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd def1 v1), appr2) + | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> raise NotConvertible) in eqappr cv_pb l2r infos app1 app2 cuniv) @@ -343,11 +343,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = form *) (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv | None -> match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then @@ -359,26 +359,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FProj (p1,c1), t2) -> (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv | None -> (match t2 with | FFlex fl2 -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) | (t1, FProj (p2,c2)) -> (match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv | None -> (match t1 with | FFlex fl1 -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) @@ -424,7 +424,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FFlex fl1, c2) -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> match c2 with | FConstruct ((ind2,j2),u2) -> @@ -438,7 +438,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (c1, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> match c1 with | FConstruct ((ind1,j1),u1) -> -- cgit v1.2.3 From 9ea1cae62c5335eb7f1dcc14df1dc0b97dfb48e7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Jun 2017 15:17:30 +0200 Subject: [kernel] Improve proof using message, fixes bugzilla #3613 --- kernel/term_typing.ml | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'kernel') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index eeb9c421a1..bdfd00a8d3 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -344,11 +344,18 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Idset.diff inferred_set declared_set) in let n = List.length l in - user_err (Pp.(str "The following section " ++ - str (String.plural n "variable") ++ - str " " ++ str (String.conjugate_verb_to_be n) ++ - str " used but not declared:" ++ - fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in + let declared_vars = Pp.pr_sequence Id.print (Idset.elements declared_set) in + let inferred_vars = Pp.pr_sequence Id.print (Idset.elements inferred_set) in + let missing_vars = Pp.pr_sequence Id.print (List.rev l) in + user_err Pp.(prlist str + ["The following section "; (String.plural n "variable"); " "; + (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++ + missing_vars ++ str "." ++ fnl () ++ fnl () ++ + str "You can either update your proof to not depend on " ++ missing_vars ++ + str ", or you can update your Proof line from" ++ fnl () ++ + str "Proof using " ++ declared_vars ++ fnl () ++ + str "to" ++ fnl () ++ + str "Proof using " ++ inferred_vars) in let sort evn l = List.filter (fun decl -> let id = NamedDecl.get_id decl in -- cgit v1.2.3 From 44f462aa380de847452c0809d15c86649d5d6a7a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 28 Mar 2017 19:24:02 +0200 Subject: Extend definition of inductives to include subtyping info --- kernel/declarations.ml | 2 ++ kernel/declareops.ml | 1 + kernel/entries.mli | 4 +++- kernel/indtypes.ml | 29 +++++++++++++++++------------ 4 files changed, 23 insertions(+), 13 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 71e228b19c..9536407d38 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -190,6 +190,8 @@ type mutual_inductive_body = { mind_universes : Univ.universe_context; (** Local universe variables and constraints *) + mind_subtyping : Univ.universe_context; (** Constraints for subtyping *) + 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 0a822d6fad..47a23c8555 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -261,6 +261,7 @@ let subst_mind_body sub mib = mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; + mind_subtyping = mib.mind_subtyping; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } diff --git a/kernel/entries.mli b/kernel/entries.mli index 1e07c96909..88584e3b3d 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -50,7 +50,9 @@ type mutual_inductive_entry = { mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_polymorphic : bool; - mind_entry_universes : Univ.universe_context; + mind_entry_universes : Univ.universe_context * Univ.universe_context; + (* universe constraints and the constraints for subtyping of + inductive types in the block. *) mind_entry_private : bool option; } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1e13239bfc..5d928facc7 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -220,7 +220,7 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let env' = push_context mie.mind_entry_universes env in + let env' = push_context (fst mie.mind_entry_universes) env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -822,17 +822,18 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let hyps = used_section_variables env inds in let nparamargs = Context.Rel.nhyps paramsctxt in let nparamsctxt = Context.Rel.length paramsctxt in - let subst, ctx = Univ.abstract_universes p ctx in - let paramsctxt = Vars.subst_univs_level_context subst paramsctxt in + let substunivs, ctxunivs = Univ.abstract_universes p (fst ctx) in + let substsbt, ctxsbt = Univ.abstract_universes p (snd ctx) in + let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in let env_ar = - let ctx = Environ.rel_context env_ar in - let ctx' = Vars.subst_univs_level_context subst ctx in - Environ.push_rel_context ctx' env + let ctxunivs = Environ.rel_context env_ar in + let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in + Environ.push_rel_context ctxunivs' env in (* Check one inductive *) let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg = (* Type of constructors in normal form *) - let lc = Array.map (Vars.subst_univs_level_constr subst) lc in + let lc = Array.map (Vars.subst_univs_level_constr substunivs) lc in let splayed_lc = Array.map (dest_prod_assum env_ar) lc in let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in let consnrealdecls = @@ -841,6 +842,9 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let consnrealargs = Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs) splayed_lc in + (* Check that the subtyping constraints (inferred outside kernel) + are valid. If so return (), otherwise raise an anomaly! *) + let () = () in (* Elimination sorts *) let arkind,kelim = match ar_kind with @@ -851,8 +855,8 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let s = sort_of_univ defs in let kelim = allowed_sorts info s in let ar = RegularArity - { mind_user_arity = Vars.subst_univs_level_constr subst ar; - mind_sort = sort_of_univ (Univ.subst_univs_level_universe subst defs); } in + { mind_user_arity = Vars.subst_univs_level_constr substunivs ar; + mind_sort = sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in ar, kelim in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in @@ -871,7 +875,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm (* Build the inductive packet *) { mind_typename = id; mind_arity = arkind; - mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign; + mind_arity_ctxt = Vars.subst_univs_level_context substunivs ar_sign; mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs; mind_nrealdecls = Context.Rel.length ar_sign - nparamsctxt; mind_kelim = kelim; @@ -895,7 +899,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm (** The elimination criterion ensures that all projections can be defined. *) let u = if p then - subst_univs_level_instance subst (Univ.UContext.instance ctx) + subst_univs_level_instance substunivs (Univ.UContext.instance ctxunivs) else Univ.Instance.empty in let indsp = ((kn, 0), u) in @@ -920,7 +924,8 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_params_ctxt = paramsctxt; mind_packets = packets; mind_polymorphic = p; - mind_universes = ctx; + mind_universes = ctxunivs; + mind_subtyping = ctxsbt; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } -- cgit v1.2.3 From 4dd4f186895d16510f217778bb83933be8956082 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 30 Mar 2017 18:12:43 +0200 Subject: New datastructure for universes of inductive types --- kernel/univ.ml | 83 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ kernel/univ.mli | 48 +++++++++++++++++++++++++++++++++ 2 files changed, 131 insertions(+) (limited to 'kernel') diff --git a/kernel/univ.ml b/kernel/univ.ml index d53dd8e733..e8b9ae33a0 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1028,6 +1028,83 @@ end type universe_context = UContext.t let hcons_universe_context = UContext.hcons +(** Universe info for inductive types: A context of universe levels + with universe constraints, representing local universe variables + and constraints, together with a context of universe levels with + universe constraints, representing conditions for subtyping used + for inductive types. + + This data structure maintains the invariant that the context for + subtyping constraints is exactly twice as big as the context for + universe constraints. *) +module UInfoInd = +struct + type t = universe_context * universe_context + + let make x = + if (Instance.length (UContext.instance (snd x))) = + (Instance.length (UContext.instance (fst x))) * 2 then x + else anomaly (Pp.str "Invalid subtyping information encountered!") + + let empty = (UContext.empty, UContext.empty) + let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst + + let halve_context (ctx : Instance.t) : Instance.t * Instance.t = + let len = Array.length (Instance.to_array ctx) in + let halflen = len / 2 in + (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen), + Instance.of_array (Array.sub (Instance.to_array ctx) halflen len)) + + let pr prl (univcst, subtypcst) = + if UContext.is_empty univcst then mt() else + let (ctx, ctx') = halve_context (UContext.instance subtypcst) in + (UContext.pr prl univcst) ++ + h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "}") + ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst))) + + let hcons (univcst, subtypcst) = + (UContext.hcons univcst, UContext.hcons subtypcst) + + let univ_context (univcst, subtypcst) = univcst + let subtyp_context (univcst, subtypcst) = subtypcst + + let create_trivial_subtyping ctx ctx' = + CArray.fold_left_i + (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst) + Constraint.empty (Instance.to_array ctx) + + (** This function takes a universe context representing constraints + of an inductive and a Instance.t of fresh universe names for the + subtyping (with the same length as the context in the given + universe context) and produces a UInfoInd.t that with the + trivial subtyping relation. *) + let from_universe_context univcst freshunivs = + let inst = (UContext.instance univcst) in + assert (Instance.length freshunivs = Instance.length inst); + (univcst, UContext.make (Instance.append inst freshunivs, + create_trivial_subtyping inst freshunivs)) + + (** This function adds universe constraints to the universe + constraints of the given universe_info_ind. However one must be + CAUTIOUS as it resets the subtyping constraints to equality. It + also requires fresh universes for the newly introduced + universes *) + let union (univcst, _) univcst' freshunivs = + assert (Instance.length freshunivs = Instance.length (UContext.instance univcst')); + let (ctx, ctx') = halve_context (UContext.instance univcst) in + let newctx' = Instance.append ctx' freshunivs in + let univcstunion = UContext.union univcst univcst' in + (univcstunion, subtyp_context (from_universe_context univcstunion newctx')) + + let dest x = x + + let size ((x,_), _) = Instance.length x + +end + +type universe_info_ind = UInfoInd.t +let hcons_universe_info_ind = UInfoInd.hcons + (** A set of universes with universe constraints. We linearize the set to a list after typechecking. Beware, representation could change. @@ -1203,6 +1280,10 @@ let subst_instance_constraints s csts = let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) +(** Substitute instance inst for ctx in universe constraints and subtyping constraints *) +let instantiate_univ_info_ind (univcst, subtpcst) = + (instantiate_univ_context univcst, instantiate_univ_context subtpcst) + let instantiate_univ_constraints u (_, csts) = subst_instance_constraints u csts @@ -1235,6 +1316,8 @@ let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr +let pr_universe_info_ind = UInfoInd.pr + let pr_universe_context_set = ContextSet.pr let pr_universe_subst = diff --git a/kernel/univ.mli b/kernel/univ.mli index 1ccdebd501..630d0d9498 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -315,6 +315,49 @@ end type universe_context = UContext.t +(** Universe info for inductive types: A context of universe levels + with universe constraints, representing local universe variables + and constraints, together with a context of universe levels with + universe constraints, representing conditions for subtyping used + for inductive types. + + This data structure maintains the invariant that the context for + subtyping constraints is exactly twice as big as the context for + universe constraints. *) +module UInfoInd : +sig + type t + + val make : universe_context * universe_context -> t + + val empty : t + val is_empty : t -> bool + + val univ_context : t -> universe_context + val subtyp_context : t -> universe_context + + val dest : t -> universe_context * universe_context + + (** This function takes a universe context representing constraints + of an inductive and a Instance.t of fresh universe names for the + subtyping (with the same length as the context in the given + universe context) and produces a UInfoInd.t that with the + trivial subtyping relation. *) + val from_universe_context : universe_context -> universe_instance -> t + + (** This function adds universe constraints to the universe + constraints of the given universe_info_ind. However one must be + CAUTIOUS as it resets the subtyping constraints to equality. It + also requires fresh universes for the newly introduced + universes *) + val union : t -> universe_context -> universe_instance -> t + + val size : t -> int + +end + +type universe_info_ind = UInfoInd.t + (** Universe contexts (as sets) *) module ContextSet : @@ -389,6 +432,9 @@ val abstract_universes : bool -> universe_context -> universe_level_subst * univ (** Get the instantiated graph. *) val instantiate_univ_context : universe_context -> universe_context +(** Get the instantiated graphs for both universe constraints and subtyping constraints. *) +val instantiate_univ_info_ind : universe_info_ind -> universe_info_ind + val instantiate_univ_constraints : universe_instance -> universe_context -> constraints (** {6 Pretty-printing of universes. } *) @@ -396,6 +442,7 @@ val instantiate_univ_constraints : universe_instance -> universe_context -> cons val pr_constraint_type : constraint_type -> Pp.std_ppcmds val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds +val pr_universe_info_ind : (Level.t -> Pp.std_ppcmds) -> universe_info_ind -> Pp.std_ppcmds val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> univ_inconsistency -> Pp.std_ppcmds @@ -410,6 +457,7 @@ val hcons_constraints : constraints -> constraints val hcons_universe_set : universe_set -> universe_set val hcons_universe_context : universe_context -> universe_context val hcons_universe_context_set : universe_context_set -> universe_context_set +val hcons_universe_info_ind : universe_info_ind -> universe_info_ind (******) -- cgit v1.2.3 From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: Using UInfoInd for universes in inductive types It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. --- kernel/declarations.ml | 4 +--- kernel/declareops.ml | 7 +++---- kernel/entries.mli | 2 +- kernel/indtypes.ml | 14 +++++--------- kernel/inductive.ml | 2 +- kernel/safe_typing.ml | 2 +- kernel/term_typing.ml | 2 +- kernel/univ.ml | 8 ++++---- kernel/vconv.ml | 2 +- 9 files changed, 18 insertions(+), 25 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 9536407d38..1bb1e885f2 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -188,9 +188,7 @@ type mutual_inductive_body = { mind_polymorphic : bool; (** Is it polymorphic or not *) - mind_universes : Univ.universe_context; (** Local universe variables and constraints *) - - mind_subtyping : Univ.universe_context; (** Constraints for subtyping *) + mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 47a23c8555..cdea468adf 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -261,19 +261,18 @@ let subst_mind_body sub mib = mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; - mind_subtyping = mib.mind_subtyping; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } let inductive_instance mib = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty let inductive_context mib = if mib.mind_polymorphic then - Univ.instantiate_univ_context mib.mind_universes + Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.UContext.empty (** {6 Hash-consing of inductive declarations } *) @@ -306,7 +305,7 @@ let hcons_mind mib = { mib with mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; - mind_universes = Univ.hcons_universe_context mib.mind_universes } + mind_universes = Univ.hcons_universe_info_ind mib.mind_universes } (** {6 Stm machinery } *) diff --git a/kernel/entries.mli b/kernel/entries.mli index 88584e3b3d..97c28025a4 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -50,7 +50,7 @@ type mutual_inductive_entry = { mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_polymorphic : bool; - mind_entry_universes : Univ.universe_context * Univ.universe_context; + mind_entry_universes : Univ.universe_info_ind; (* universe constraints and the constraints for subtyping of inductive types in the block. *) mind_entry_private : bool option; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5d928facc7..94bf1a7704 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -220,7 +220,7 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let env' = push_context (fst mie.mind_entry_universes) env in + let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -822,10 +822,10 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let hyps = used_section_variables env inds in let nparamargs = Context.Rel.nhyps paramsctxt in let nparamsctxt = Context.Rel.length paramsctxt in - let substunivs, ctxunivs = Univ.abstract_universes p (fst ctx) in - let substsbt, ctxsbt = Univ.abstract_universes p (snd ctx) in + let substunivs, ctxunivs = Univ.abstract_universes p (Univ.UInfoInd.univ_context ctx) in + let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) in let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in - let env_ar = + let env_ar = let ctxunivs = Environ.rel_context env_ar in let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in Environ.push_rel_context ctxunivs' env @@ -842,9 +842,6 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let consnrealargs = Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs) splayed_lc in - (* Check that the subtyping constraints (inferred outside kernel) - are valid. If so return (), otherwise raise an anomaly! *) - let () = () in (* Elimination sorts *) let arkind,kelim = match ar_kind with @@ -924,8 +921,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_params_ctxt = paramsctxt; mind_packets = packets; mind_polymorphic = p; - mind_universes = ctxunivs; - mind_subtyping = ctxsbt; + mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp); mind_private = prv; mind_typing_flags = Environ.typing_flags env; } diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f3b03252db..0f0dc0d607 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -55,7 +55,7 @@ let inductive_paramdecls (mib,u) = let instantiate_inductive_constraints mib u = if mib.mind_polymorphic then - Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes) + Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes)) else Univ.Constraint.empty diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f5e8e86530..1568fe0bf2 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -429,7 +429,7 @@ let globalize_mind_universes mb = if mb.mind_polymorphic then [Now (true, Univ.ContextSet.empty)] else - [Now (false, Univ.ContextSet.of_context mb.mind_universes)] + [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))] let constraints_of_sfb env sfb = match sfb with diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index bdfd00a8d3..3cf2299d83 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -313,7 +313,7 @@ let infer_declaration ~trust env kn dcl = in let term, typ = pb.proj_eta in Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, - mib.mind_polymorphic, mib.mind_universes, false, None + mib.mind_polymorphic, Univ.UInfoInd.univ_context mib.mind_universes, false, None let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t diff --git a/kernel/univ.ml b/kernel/univ.ml index e8b9ae33a0..f124bb39eb 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1053,14 +1053,14 @@ struct let len = Array.length (Instance.to_array ctx) in let halflen = len / 2 in (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen), - Instance.of_array (Array.sub (Instance.to_array ctx) halflen len)) + Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen)) let pr prl (univcst, subtypcst) = if UContext.is_empty univcst then mt() else let (ctx, ctx') = halve_context (UContext.instance subtypcst) in - (UContext.pr prl univcst) ++ - h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "}") - ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst))) + (UContext.pr prl univcst) ++ fnl () ++ fnl () ++ + h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ") + ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst))) let hcons (univcst, subtypcst) = (UContext.hcons univcst, UContext.hcons subtypcst) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 74d956bef0..fa16622702 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = if Environ.polymorphic_ind ind1 env then let mib = Environ.lookup_mind mi env in - let ulen = Univ.UContext.size mib.Declarations.mind_universes in + let ulen = Univ.UContext.size (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in match stk1 , stk2 with | [], [] -> assert (Int.equal ulen 0); cu | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> -- cgit v1.2.3 From f27f3ca3a39f5320a60c82c601525e7f0fe666cb Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Mon, 3 Apr 2017 16:06:07 +0200 Subject: Check subtyping of inductive types in Kernel --- kernel/indtypes.ml | 34 ++++++++++++++++++++++++++++++++++ kernel/univ.ml | 16 ++++------------ kernel/univ.mli | 7 +------ 3 files changed, 39 insertions(+), 18 deletions(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 94bf1a7704..068332406e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -207,6 +207,24 @@ let param_ccls paramsctxt = in List.fold_left fold [] paramsctxt +(* Check arities and constructors *) +let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) is_arity = + let basic_check ev tp = conv_leq ev tp (subst tp) in + let check_typ typ typ_env = + match typ with + | LocalAssum (_, typ') -> + begin + try + basic_check env typ'; Environ.push_rel typ typ_env + with NotConvertible -> + anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation!") + end + | _ -> anomaly (Pp.str "") + in + let typs, codom = dest_prod env arcn in + let last_env = Context.Rel.fold_outside check_typ typs ~init:env in + if not is_arity then basic_check last_env codom else () + (* Type-check an inductive definition. Does not check positivity conditions. *) (* TODO check that we don't overgeneralize construcors/inductive arities with @@ -345,6 +363,22 @@ let typecheck_inductive env mie = in (id,cn,lc,(sign,arity))) inds + in + (* Check that the subtyping information inferred for inductive types in the block is correct. *) + (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) + let () = + let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in + let dosubst = subst_univs_level_constr sbsubst in + let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env_ar_par in + (* process individual inductive types: *) + Array.iter (fun (id,cn,lc,(sign,arity)) -> + match arity with + | RegularArity (_, full_arity, _) -> + check_subtyping_arity_constructor envsb dosubst full_arity true; + Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt true) lc + | TemplateArity _ -> () + (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *) + ) inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) diff --git a/kernel/univ.ml b/kernel/univ.ml index f124bb39eb..4a4cf1baa7 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1049,7 +1049,7 @@ struct let empty = (UContext.empty, UContext.empty) let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst - let halve_context (ctx : Instance.t) : Instance.t * Instance.t = + let halve_context ctx = let len = Array.length (Instance.to_array ctx) in let halflen = len / 2 in (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen), @@ -1084,17 +1084,9 @@ struct (univcst, UContext.make (Instance.append inst freshunivs, create_trivial_subtyping inst freshunivs)) - (** This function adds universe constraints to the universe - constraints of the given universe_info_ind. However one must be - CAUTIOUS as it resets the subtyping constraints to equality. It - also requires fresh universes for the newly introduced - universes *) - let union (univcst, _) univcst' freshunivs = - assert (Instance.length freshunivs = Instance.length (UContext.instance univcst')); - let (ctx, ctx') = halve_context (UContext.instance univcst) in - let newctx' = Instance.append ctx' freshunivs in - let univcstunion = UContext.union univcst univcst' in - (univcstunion, subtyp_context (from_universe_context univcstunion newctx')) + let subtyping_susbst (univcst, subtypcst) = + let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in + Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx' let dest x = x diff --git a/kernel/univ.mli b/kernel/univ.mli index 630d0d9498..f139a8b334 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -345,12 +345,7 @@ sig trivial subtyping relation. *) val from_universe_context : universe_context -> universe_instance -> t - (** This function adds universe constraints to the universe - constraints of the given universe_info_ind. However one must be - CAUTIOUS as it resets the subtyping constraints to equality. It - also requires fresh universes for the newly introduced - universes *) - val union : t -> universe_context -> universe_instance -> t + val subtyping_susbst : t -> universe_level_subst val size : t -> int -- cgit v1.2.3 From 47e010c2dd0ab6370704d8ab24552753e4e1b1dc Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Mon, 3 Apr 2017 16:28:20 +0200 Subject: Fix typo in error message --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 068332406e..91e6ec2855 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -217,7 +217,7 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter try basic_check env typ'; Environ.push_rel typ typ_env with NotConvertible -> - anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation!") + anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") end | _ -> anomaly (Pp.str "") in -- cgit v1.2.3 From 34c1fee1c980b433b069a59f408792142ba00f6e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 4 Apr 2017 11:54:37 +0200 Subject: Correct subtyping check for constructors --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 91e6ec2855..17ce5483c7 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -375,7 +375,7 @@ let typecheck_inductive env mie = match arity with | RegularArity (_, full_arity, _) -> check_subtyping_arity_constructor envsb dosubst full_arity true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt true) lc + Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt false) lc | TemplateArity _ -> () (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *) ) inds -- cgit v1.2.3 From d83a4a93202c91095c5528fe4b54c83737e5a151 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 4 Apr 2017 19:44:31 +0200 Subject: Add subtyping inference for inductive types --- kernel/indtypes.ml | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 17ce5483c7..15fe908359 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -208,8 +208,12 @@ let param_ccls paramsctxt = List.fold_left fold [] paramsctxt (* Check arities and constructors *) -let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) is_arity = - let basic_check ev tp = conv_leq ev tp (subst tp) in +let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) numparams is_arity = + let numchecked = ref 0 in + let basic_check ev tp = + if !numchecked < numparams then () else conv_leq ev tp (subst tp); + numchecked := !numchecked + 1 + in let check_typ typ typ_env = match typ with | LocalAssum (_, typ') -> @@ -367,15 +371,22 @@ let typecheck_inductive env mie = (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) let () = + let numparams = List.length paramsctxt in let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in let dosubst = subst_univs_level_constr sbsubst in - let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env_ar_par in + let uctx = UInfoInd.univ_context mie.mind_entry_universes in + let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in + let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in + let uctx_other = Univ.UContext.make (instance_other, constraints_other) in + let env' = Environ.push_context uctx env_ar_par in + let env'' = Environ.push_context uctx_other env' in + let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in (* process individual inductive types: *) Array.iter (fun (id,cn,lc,(sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> - check_subtyping_arity_constructor envsb dosubst full_arity true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt false) lc + check_subtyping_arity_constructor envsb dosubst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc | TemplateArity _ -> () (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *) ) inds -- cgit v1.2.3 From ab86b9b3999f3860bdb69824f585b9cf461ff295 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Fri, 7 Apr 2017 12:44:12 +0200 Subject: Use inductive subtyping for conv/cumul --- kernel/reduction.ml | 139 ++++++++++++++++++++++++++++++++++----------------- kernel/reduction.mli | 2 + 2 files changed, 96 insertions(+), 45 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b6786c045c..0d2399e025 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -191,6 +191,7 @@ type 'a universe_compare = { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + leq_inductives : flex:bool -> Univ.UInfoInd.t -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } type 'a universe_state = 'a * 'a universe_compare @@ -207,6 +208,9 @@ let sort_cmp_universes env pb s0 s1 (u, check) = let convert_instances ~flex u u' (s, check) = (check.compare_instances ~flex u u' s, check) +let compare_leq_inductives ~flex uinfind u u' (s, check) = + (check.leq_inductives ~flex uinfind u u' s, check) + let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else match k1, k2 with @@ -299,11 +303,11 @@ let unfold_projection infos p c = else None (* Conversion between [lft1]term1 and [lft2]term2 *) -let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = - eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv +let rec ccnv env cv_pb l2r infos lft1 lft2 term1 term2 cuniv = + eqappr env cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *) -and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = +and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Control.check_for_interrupt (); (* First head reduce both terms *) let whd = whd_stack (infos_with_reds infos betaiotazeta) in @@ -328,13 +332,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m - then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | _ -> raise NotConvertible) | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> if Evar.equal ev1 ev2 then - let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in - convert_vect l2r infos el1 el2 + let cuniv = convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv in + convert_vect env l2r infos el1 el2 (Array.map (mk_clos env1) args1) (Array.map (mk_clos env2) args2) cuniv else raise NotConvertible @@ -342,14 +346,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 2 index known to be bound to no constant *) | (FRel n, FRel m) -> if Int.equal (reloc_rel n el1) (reloc_rel m el2) - then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try let cuniv = conv_table_key infos fl1 fl2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos in @@ -369,7 +373,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> raise NotConvertible) in - eqappr cv_pb l2r infos app1 app2 cuniv) + eqappr env cv_pb l2r infos app1 app2 cuniv) | (FProj (p1,c1), FProj (p2, c2)) -> (* Projections: prefer unfolding to first-order unification, @@ -377,42 +381,42 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = form *) (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv + eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv | None -> match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv + eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then - let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 u1 + let u1 = ccnv env CONV l2r infos el1 el2 c1 c2 cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 u1 else (* Two projections in WHNF: unfold *) raise NotConvertible) | (FProj (p1,c1), t2) -> (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv + eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv | None -> (match t2 with | FFlex fl2 -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv + eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) | (t1, FProj (p2,c2)) -> (match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv + eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv | None -> (match t1 with | FFlex fl1 -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv + eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) @@ -424,15 +428,15 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given ill-typed terms (FLambda)."); let (_,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in - let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in - ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv + let cuniv = ccnv env CONV l2r infos el1 el2 ty1 ty2 cuniv in + ccnv env CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv | (FProd (_,c1,c2), FProd (_,c'1,c'2)) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (FProd)."); (* Luo's system *) - let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in - ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv + let cuniv = ccnv env CONV l2r infos el1 el2 c1 c'1 cuniv in + ccnv env cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv (* Eta-expansion on the fly *) | (FLambda _, _) -> @@ -442,7 +446,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty1,bd1) = destFLambda mk_clos hd1 in - eqappr CONV l2r infos + eqappr env CONV l2r infos (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv | (_, FLambda _) -> let () = match v2 with @@ -451,34 +455,34 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty2,bd2) = destFLambda mk_clos hd2 in - eqappr CONV l2r infos + eqappr env CONV l2r infos (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv (* only one constant, defined var or defined rel *) | (FFlex fl1, c2) -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv + eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> match c2 with | FConstruct ((ind2,j2),u2) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) | (c1, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv + eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> match c1 with | FConstruct ((ind1,j1),u1) -> (try let v1, v2 = eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) @@ -487,15 +491,33 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FInd (ind1,u1), FInd (ind2,u2)) -> if eq_ind ind1 ind2 then - (let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) + begin + let mind = Environ.lookup_mind (fst ind1) env in + if mind.Declarations.mind_polymorphic then + begin + let num_param_arity = + Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt) + in + (if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then + raise NotConvertible else ()); + let uinfind = mind.Declarations.mind_universes in + let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in + let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + end + else + begin + let cuniv = convert_instances ~flex:false u1 u2 cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + end + end else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> if Int.equal j1 j2 && eq_ind ind1 ind2 then (let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible (* Eta expansion of records *) @@ -503,14 +525,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (try let v1, v2 = eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | (_, FConstruct ((ind2,j2),u2)) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) -> @@ -521,11 +543,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let fty2 = Array.map (mk_clos e2) tys2 in let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in - let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in + let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = - convert_vect l2r infos + convert_vect env l2r infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) -> @@ -536,11 +558,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let fty2 = Array.map (mk_clos e2) tys2 in let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in - let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in + let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = - convert_vect l2r infos + convert_vect env l2r infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) @@ -551,13 +573,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* In all other cases, terms are not convertible *) | _ -> raise NotConvertible -and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = +and convert_stacks env l2r infos lft1 lft2 stk1 stk2 cuniv = compare_stacks - (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) + (fun (l1,t1) (l2,t2) cuniv -> ccnv env CONV l2r infos l1 l2 t1 t2 cuniv) (eq_ind) lft1 stk1 lft2 stk2 cuniv -and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = +and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv = let lv1 = Array.length v1 in let lv2 = Array.length v2 in if Int.equal lv1 lv2 @@ -565,7 +587,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = let rec fold n cuniv = if n >= lv1 then cuniv else - let cuniv = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in + let cuniv = ccnv env CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in fold (n+1) cuniv in fold 0 cuniv else raise NotConvertible @@ -573,7 +595,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in - ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs + ccnv env cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs let check_eq univs u u' = @@ -610,9 +632,24 @@ let check_convert_instances ~flex u u' univs = if UGraph.check_eq_instances univs u u' then univs else raise NotConvertible +let check_leq_inductives ~flex uinfind u u' univs = + let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in + let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && + (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + begin + let comp_subst = (Univ.Instance.append u u') in + let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in + if UGraph.check_constraints comp_cst univs then univs + else raise NotConvertible + end + let checked_universes = { compare = checked_sort_cmp_universes; - compare_instances = check_convert_instances } + compare_instances = check_convert_instances; + leq_inductives = check_leq_inductives } let infer_eq (univs, cstrs as cuniv) u u' = if UGraph.check_eq univs u u' then cuniv @@ -649,9 +686,21 @@ let infer_cmp_universes env pb s0 s1 univs = let infer_convert_instances ~flex u u' (univs,cstrs) = (univs, Univ.enforce_eq_instances u u' cstrs) +let infer_leq_inductives ~flex uinfind u u' (univs, cstrs) = + let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in + let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && + (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + let comp_subst = (Univ.Instance.append u u') in + let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in + (univs, Univ.Constraint.union cstrs comp_cst) + let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; - compare_instances = infer_convert_instances } + compare_instances = infer_convert_instances; + leq_inductives = infer_leq_inductives } let gen_conv cv_pb l2r reds env evars univs t1 t2 = let b = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 8a2b2469d6..72f0ecffd0 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -40,6 +40,8 @@ type 'a universe_compare = compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + leq_inductives : flex:bool -> Univ.UInfoInd.t -> + Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } type 'a universe_state = 'a * 'a universe_compare -- cgit v1.2.3 From 0d884e0852ae388becc5b74c6a8cb30088f7b79b Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 8 Apr 2017 16:10:19 +0200 Subject: Fix cum/conv for inductive types Fall back to the equating levels in case inductive is not fully applied instead of failing. --- kernel/reduction.ml | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 0d2399e025..c8fad60ebe 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -492,24 +492,28 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if eq_ind ind1 ind2 then begin + let fall_back () = + let cuniv = convert_instances ~flex:false u1 u2 cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in let mind = Environ.lookup_mind (fst ind1) env in if mind.Declarations.mind_polymorphic then begin let num_param_arity = Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt) in - (if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then - raise NotConvertible else ()); - let uinfind = mind.Declarations.mind_universes in - let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in - let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then + fall_back () + else + begin + let uinfind = mind.Declarations.mind_universes in + let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in + let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + end end else - begin - let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv - end + fall_back () end else raise NotConvertible -- cgit v1.2.3 From 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sun, 21 May 2017 14:46:30 +0200 Subject: Squashed commit of the following: Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints. --- kernel/declareops.ml | 21 ++++++++++------ kernel/kernel.mllib | 1 + kernel/reduction.ml | 70 ++++++++++++++++++++++++++++++++++++---------------- kernel/subtyping.ml | 5 ++++ kernel/univ.ml | 3 +++ kernel/univ.mli | 3 +++ kernel/univops.ml | 70 ++++++++++++++++++++++++++++++++++++++++++++++++++++ kernel/univops.mli | 17 +++++++++++++ 8 files changed, 162 insertions(+), 28 deletions(-) create mode 100644 kernel/univops.ml create mode 100644 kernel/univops.mli (limited to 'kernel') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index cdea468adf..8838966520 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -49,6 +49,11 @@ let instantiate cb c = Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c else c +let instantiate_constraints cb cst = + if cb.const_polymorphic then + Univ.subst_instance_constraints (Univ.UContext.instance cb.const_universes) cst + else cst + let body_of_constant otab cb = match cb.const_body with | Undef _ -> None | Def c -> Some (instantiate cb (force_constr c)) @@ -61,13 +66,15 @@ let type_of_constant cb = if t' == t then x else RegularArity t' | TemplateArity _ as x -> x -let constraints_of_constant otab cb = Univ.Constraint.union - (Univ.UContext.constraints cb.const_universes) - (match cb.const_body with - | Undef _ -> Univ.empty_constraint - | Def c -> Univ.empty_constraint - | OpaqueDef o -> - Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) +let constraints_of_constant otab cb = + let cst = Univ.Constraint.union + (Univ.UContext.constraints cb.const_universes) + (match cb.const_body with + | Undef _ -> Univ.empty_constraint + | Def c -> Univ.empty_constraint + | OpaqueDef o -> + Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) + in instantiate_constraints cb cst let universes_of_constant otab cb = match cb.const_body with diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 2f49982ce2..8132d66850 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -43,3 +43,4 @@ Vm Csymtable Vconv Declarations +Univops diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c8fad60ebe..a872a103a5 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -489,8 +489,8 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd (ind1,u1), FInd (ind2,u2)) -> - if eq_ind ind1 ind2 - then + if eq_ind ind1 ind2 + then begin let fall_back () = let cuniv = convert_instances ~flex:false u1 u2 cuniv in @@ -498,31 +498,54 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = in let mind = Environ.lookup_mind (fst ind1) env in if mind.Declarations.mind_polymorphic then - begin - let num_param_arity = - Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt) - in - if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then - fall_back () - else begin - let uinfind = mind.Declarations.mind_universes in - let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in - let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + let num_param_arity = + Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt) + in + if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then + fall_back () + else + begin + let uinfind = mind.Declarations.mind_universes in + let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in + let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + end end - end else fall_back () end - else raise NotConvertible + else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> - if Int.equal j1 j2 && eq_ind ind1 ind2 - then - (let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv) - else raise NotConvertible + if Int.equal j1 j2 && eq_ind ind1 ind2 + then + begin + let fall_back () = + let cuniv = convert_instances ~flex:false u1 u2 cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in + let mind = Environ.lookup_mind (fst ind1) env in + if mind.Declarations.mind_polymorphic then + begin + let num_cnstr_args = + let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in + nparamsctxt + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_consnrealargs.(j1 - 1) + in + if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then + fall_back () + else + begin (* we don't consider subtyping for constructors. *) + let uinfind = mind.Declarations.mind_universes in + let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in + let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + end + end + else + fall_back () + end + else raise NotConvertible (* Eta expansion of records *) | (FConstruct ((ind1,j1),u1), _) -> @@ -688,7 +711,12 @@ let infer_cmp_universes env pb s0 s1 univs = else univs let infer_convert_instances ~flex u u' (univs,cstrs) = - (univs, Univ.enforce_eq_instances u u' cstrs) + let cstrs' = + if flex then + if UGraph.check_eq_instances univs u u' then cstrs + else raise NotConvertible + else Univ.enforce_eq_instances u u' cstrs + in (univs, cstrs') let infer_leq_inductives ~flex uinfind u u' (univs, cstrs) = let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index f779f68be4..60cd77f402 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -90,6 +90,7 @@ let check_conv_error error why cst poly u f env a1 a2 = else error (IncompatiblePolymorphism (env, a1, a2)) else Constraint.union cst cst' with NotConvertible -> error why + | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e) (* for now we do not allow reorderings *) @@ -302,6 +303,10 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let ctx2 = Univ.instantiate_univ_context cb2.const_universes in let inst1, ctx1 = Univ.UContext.dest ctx1 in let inst2, ctx2 = Univ.UContext.dest ctx2 in + output_string stderr "\ninst1:\n"; + output_string stderr (Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr inst1)); + output_string stderr "\ninst2:\n"; + output_string stderr (Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr inst2)); flush stderr; if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then error IncompatibleInstances else diff --git a/kernel/univ.ml b/kernel/univ.ml index 4a4cf1baa7..5de45cf2b9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -725,8 +725,11 @@ struct pp_std ++ prl u1 ++ pr_constraint_type op ++ prl u2 ++ fnl () ) c (str "") + let universes_of c = + fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty end +let universes_of_constraints = Constraint.universes_of let empty_constraint = Constraint.empty let union_constraint = Constraint.union let eq_constraint = Constraint.equal diff --git a/kernel/univ.mli b/kernel/univ.mli index f139a8b334..1141933293 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -462,3 +462,6 @@ val eq_levels : universe_level -> universe_level -> bool (** deprecated: Equality of formal universe expressions. *) val equal_universes : universe -> universe -> bool + +(** Universes of constraints *) +val universes_of_constraints : constraints -> universe_set diff --git a/kernel/univops.ml b/kernel/univops.ml new file mode 100644 index 0000000000..e9383c6d9f --- /dev/null +++ b/kernel/univops.ml @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> fold_constr aux s c + in aux LSet.empty c + +let universes_of_inductive mind = + if mind.mind_polymorphic then + begin + let u = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in + let univ_of_one_ind oind = + let arity_univs = + Context.Rel.fold_outside + (fun decl unvs -> + Univ.LSet.union + (Context.Rel.Declaration.fold_constr + (fun cnstr unvs -> + let cnstr = Vars.subst_instance_constr u cnstr in + Univ.LSet.union + (universes_of_constr cnstr) unvs) + decl Univ.LSet.empty) unvs) + oind.mind_arity_ctxt ~init:Univ.LSet.empty + in + Array.fold_left (fun unvs cns -> + let cns = Vars.subst_instance_constr u cns in + Univ.LSet.union (universes_of_constr cns) unvs) arity_univs + oind.mind_nf_lc + in + let univs = Array.fold_left (fun unvs pk -> Univ.LSet.union (univ_of_one_ind pk) unvs) Univ.LSet.empty mind.mind_packets in + let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mind.mind_universes)) in + let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in + univs + end + else LSet.empty + +let restrict_universe_context (univs,csts) s = + (* Universes that are not necessary to typecheck the term. + E.g. univs introduced by tactics and not used in the proof term. *) + let diff = LSet.diff univs s in + let rec aux diff candid univs ness = + let (diff', candid', univs', ness') = + Constraint.fold + (fun (l, d, r as c) (diff, candid, univs, csts) -> + if not (LSet.mem l diff) then + (LSet.remove r diff, candid, univs, Constraint.add c csts) + else if not (LSet.mem r diff) then + (LSet.remove l diff, candid, univs, Constraint.add c csts) + else (diff, Constraint.add c candid, univs, csts)) + candid (diff, Constraint.empty, univs, ness) + in + if ness' == ness then (LSet.diff univs diff', ness) + else aux diff' candid' univs' ness' + in aux diff csts univs Constraint.empty diff --git a/kernel/univops.mli b/kernel/univops.mli new file mode 100644 index 0000000000..5b499c75bc --- /dev/null +++ b/kernel/univops.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* universe_set +val universes_of_inductive : mutual_inductive_body -> universe_set +val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set -- cgit v1.2.3 From 7b5fcef8a0fb3b97a3980f10596137234061990f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 26 Apr 2017 15:24:35 +0200 Subject: Fix bugs --- kernel/indtypes.ml | 61 ++++++++++++++++++++++++++++------------------------- kernel/indtypes.mli | 11 ++++++++++ kernel/reduction.ml | 4 ++-- 3 files changed, 45 insertions(+), 31 deletions(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 15fe908359..a4c7a0573c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -215,20 +215,42 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter numchecked := !numchecked + 1 in let check_typ typ typ_env = - match typ with - | LocalAssum (_, typ') -> - begin - try - basic_check env typ'; Environ.push_rel typ typ_env - with NotConvertible -> - anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") - end - | _ -> anomaly (Pp.str "") + match typ with + | LocalAssum (_, typ') -> + begin + try + basic_check typ_env typ'; Environ.push_rel typ typ_env + with NotConvertible -> + anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") + end + | _ -> anomaly (Pp.str "") in let typs, codom = dest_prod env arcn in let last_env = Context.Rel.fold_outside check_typ typs ~init:env in if not is_arity then basic_check last_env codom else () +(* Check that the subtyping information inferred for inductive types in the block is correct. *) +(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) +let check_subtyping mie paramsctxt env_ar inds = + let numparams = Context.Rel.nhyps paramsctxt in + let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in + let dosubst = subst_univs_level_constr sbsubst in + let uctx = UInfoInd.univ_context mie.mind_entry_universes in + let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in + let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in + let uctx_other = Univ.UContext.make (instance_other, constraints_other) in + let env' = Environ.push_context uctx env_ar in + let env'' = Environ.push_context uctx_other env' in + let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in + (* process individual inductive types: *) + Array.iter (fun (id,cn,lc,(sign,arity)) -> + match arity with + | RegularArity (_, full_arity, _) -> + check_subtyping_arity_constructor envsb dosubst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc + | TemplateArity _ -> () + ) inds + (* Type-check an inductive definition. Does not check positivity conditions. *) (* TODO check that we don't overgeneralize construcors/inductive arities with @@ -370,26 +392,7 @@ let typecheck_inductive env mie = in (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) - let () = - let numparams = List.length paramsctxt in - let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in - let dosubst = subst_univs_level_constr sbsubst in - let uctx = UInfoInd.univ_context mie.mind_entry_universes in - let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in - let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env' = Environ.push_context uctx env_ar_par in - let env'' = Environ.push_context uctx_other env' in - let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in - (* process individual inductive types: *) - Array.iter (fun (id,cn,lc,(sign,arity)) -> - match arity with - | RegularArity (_, full_arity, _) -> - check_subtyping_arity_constructor envsb dosubst full_arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc - | TemplateArity _ -> () - (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *) - ) inds + let () = check_subtyping mie paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 5b4615399d..7b0f017941 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -32,6 +32,17 @@ type inductive_error = exception InductiveError of inductive_error +val check_subtyping_arity_constructor : Environ.env -> +(Term.constr -> Term.constr) -> Term.types -> int -> bool -> unit + +(* This needs not be exposed. Exposing for debugging purposes! *) +val check_subtyping : Entries.mutual_inductive_entry -> +Context.Rel.t -> +Environ.env -> +('b * 'c * Term.types array * + ('d * ('e * Term.types * 'f, 'g) Declarations.declaration_arity)) +array -> unit + (** The following function does checks on inductive declarations. *) val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a872a103a5..33dd53a5b1 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -500,7 +500,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if mind.Declarations.mind_polymorphic then begin let num_param_arity = - Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt) + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_nrealargs in if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then fall_back () @@ -535,7 +535,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then fall_back () else - begin (* we don't consider subtyping for constructors. *) + begin (* we consider subtyping for constructors. *) let uinfind = mind.Declarations.mind_universes in let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in -- cgit v1.2.3 From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- kernel/declarations.ml | 2 + kernel/declareops.ml | 1 + kernel/entries.mli | 3 +- kernel/indtypes.ml | 7 +- kernel/reduction.ml | 190 +++++++++++++++++++++++++++++++------------------ kernel/reduction.mli | 11 +-- 6 files changed, 136 insertions(+), 78 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 1bb1e885f2..ae47324560 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -188,6 +188,8 @@ type mutual_inductive_body = { mind_polymorphic : bool; (** Is it polymorphic or not *) + mind_cumulative : bool; (** Is it cumulative or not *) + mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 8838966520..1d91b2d414 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -267,6 +267,7 @@ let subst_mind_body sub mib = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; + mind_cumulative = mib.mind_cumulative; mind_universes = mib.mind_universes; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; diff --git a/kernel/entries.mli b/kernel/entries.mli index 97c28025a4..9c17346f22 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -49,7 +49,8 @@ type mutual_inductive_entry = { mind_entry_finite : Decl_kinds.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; - mind_entry_polymorphic : bool; + mind_entry_polymorphic : bool; + mind_entry_cumulative : bool; mind_entry_universes : Univ.universe_info_ind; (* universe constraints and the constraints for subtyping of inductive types in the block. *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a4c7a0573c..5cfcbba606 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -392,7 +392,7 @@ let typecheck_inductive env mie = in (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) - let () = check_subtyping mie paramsctxt env_arities inds + let () = if mie.mind_entry_cumulative then check_subtyping mie paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) @@ -864,7 +864,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = +let build_inductive env cum p prv ctx env_ar 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 @@ -969,6 +969,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_params_ctxt = paramsctxt; mind_packets = packets; mind_polymorphic = p; + mind_cumulative = cum; mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp); mind_private = prv; mind_typing_flags = Environ.typing_flags env; @@ -984,7 +985,7 @@ let check_inductive env kn mie = let chkpos = (Environ.typing_flags env).check_guarded in let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in (* Build the inductive packets *) - build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private + build_inductive env mie.mind_entry_cumulative mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 33dd53a5b1..ea583fdac8 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -191,7 +191,10 @@ type 'a universe_compare = { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - leq_inductives : flex:bool -> Univ.UInfoInd.t -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> + Univ.Instance.t -> int -> 'a -> 'a; + conv_constructors : (Declarations.mutual_inductive_body * int * int) -> + Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a; } type 'a universe_state = 'a * 'a universe_compare @@ -207,9 +210,12 @@ let sort_cmp_universes env pb s0 s1 (u, check) = constructors. *) let convert_instances ~flex u u' (s, check) = (check.compare_instances ~flex u u' s, check) + +let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) = + (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check) -let compare_leq_inductives ~flex uinfind u u' (s, check) = - (check.leq_inductives ~flex uinfind u u' s, check) +let convert_constructors cons u1 sv1 u2 sv2 (s, check) = + (check.conv_constructors cons u1 sv1 u2 sv2 s, check) let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else @@ -487,64 +493,31 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | _ -> raise NotConvertible) (* Inductive types: MutInd MutConstruct Fix Cofix *) - | (FInd (ind1,u1), FInd (ind2,u2)) -> - if eq_ind ind1 ind2 - then - begin - let fall_back () = - let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv - in - let mind = Environ.lookup_mind (fst ind1) env in - if mind.Declarations.mind_polymorphic then - begin - let num_param_arity = - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_nrealargs - in - if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then - fall_back () - else - begin - let uinfind = mind.Declarations.mind_universes in - let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in - let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv - end - end + if eq_ind ind1 ind2 then + let mind = Environ.lookup_mind (fst ind1) env in + let cuniv = + if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then + convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1) + u2 (CClosure.stack_args_size v2) cuniv else - fall_back () - end + convert_instances ~flex:false u1 u2 cuniv + in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> - if Int.equal j1 j2 && eq_ind ind1 ind2 - then - begin - let fall_back () = - let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv - in - let mind = Environ.lookup_mind (fst ind1) env in - if mind.Declarations.mind_polymorphic then - begin - let num_cnstr_args = - let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in - nparamsctxt + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_consnrealargs.(j1 - 1) - in - if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then - fall_back () - else - begin (* we consider subtyping for constructors. *) - let uinfind = mind.Declarations.mind_universes in - let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in - let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv - end - end + if Int.equal j1 j2 && eq_ind ind1 ind2 then + let mind = Environ.lookup_mind (fst ind1) env in + let cuniv = + if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then + convert_constructors + (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1) + u2 (CClosure.stack_args_size v2) cuniv else - fall_back () - end + convert_instances ~flex:false u1 u2 cuniv + in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Eta expansion of records *) @@ -659,24 +632,79 @@ let check_convert_instances ~flex u u' univs = if UGraph.check_eq_instances univs u u' then univs else raise NotConvertible -let check_leq_inductives ~flex uinfind u u' univs = +(* general conversion and inference functions *) +let infer_check_conv_inductives + infer_check_convert_instances + infer_check_inductive_instances + cv_pb (mind, ind) u1 sv1 u2 sv2 univs = + if mind.Declarations.mind_polymorphic then + let num_param_arity = + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + if not (num_param_arity = sv1 && num_param_arity = sv2) then + infer_check_convert_instances ~flex:false u1 u2 univs + else + let uinfind = mind.Declarations.mind_universes in + infer_check_inductive_instances cv_pb uinfind u1 u2 univs + else infer_check_convert_instances ~flex:false u1 u2 univs + +let infer_check_conv_constructors + infer_check_convert_instances + infer_check_inductive_instances + (mind, ind, cns) u1 sv1 u2 sv2 univs = + if mind.Declarations.mind_polymorphic then + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in + nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) + in + if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then + infer_check_convert_instances ~flex:false u1 u2 univs + else + let uinfind = mind.Declarations.mind_universes in + infer_check_inductive_instances CONV uinfind u1 u2 univs + else infer_check_convert_instances ~flex:false u1 u2 univs + +let check_inductive_instances cv_pb uinfind u u' univs = let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else - begin - let comp_subst = (Univ.Instance.append u u') in - let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in - if UGraph.check_constraints comp_cst univs then univs - else raise NotConvertible - end + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.subst_instance_constraints comp_subst ind_sbcst + in + let comp_cst = + match cv_pb with + CONV -> + let comp_subst = (Univ.Instance.append u' u) in + let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + Univ.Constraint.union comp_cst comp_cst' + | CUMUL -> comp_cst + in + if (UGraph.check_constraints comp_cst univs) then univs + else raise NotConvertible + +let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs = + infer_check_conv_inductives + check_convert_instances + check_inductive_instances + cv_pb ind u1 sv1 u2 sv2 univs + +let check_conv_constructors cns u1 sv1 u2 sv2 univs = + infer_check_conv_constructors + check_convert_instances + check_inductive_instances + cns u1 sv1 u2 sv2 univs let checked_universes = { compare = checked_sort_cmp_universes; compare_instances = check_convert_instances; - leq_inductives = check_leq_inductives } + conv_inductives = check_conv_inductives; + conv_constructors = check_conv_constructors} let infer_eq (univs, cstrs as cuniv) u u' = if UGraph.check_eq univs u u' then cuniv @@ -718,21 +746,45 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = else Univ.enforce_eq_instances u u' cstrs in (univs, cstrs') -let infer_leq_inductives ~flex uinfind u u' (univs, cstrs) = +let infer_inductive_instances cv_pb uinfind u u' (univs, cstrs) = let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else - let comp_subst = (Univ.Instance.append u u') in - let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in - (univs, Univ.Constraint.union cstrs comp_cst) - + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.subst_instance_constraints comp_subst ind_sbcst + in + let comp_cst = + match cv_pb with + CONV -> + let comp_subst = (Univ.Instance.append u' u) in + let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + Univ.Constraint.union comp_cst comp_cst' + | CUMUL -> comp_cst + in + (univs, Univ.Constraint.union cstrs comp_cst) + + +let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs = + infer_check_conv_inductives + infer_convert_instances + infer_inductive_instances + cv_pb ind u1 sv1 u2 sv2 univs + +let infer_conv_constructors cns u1 sv1 u2 sv2 univs = + infer_check_conv_constructors + infer_convert_instances + infer_inductive_instances + cns u1 sv1 u2 sv2 univs + let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; compare_instances = infer_convert_instances; - leq_inductives = infer_leq_inductives } + conv_inductives = infer_conv_inductives; + conv_constructors = infer_conv_constructors} let gen_conv cv_pb l2r reds env evars univs t1 t2 = let b = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 72f0ecffd0..b6d88c2b9b 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,12 +36,13 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL type 'a universe_compare = - { (* Might raise NotConvertible or UnivInconsistency *) + { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; - compare_instances: flex:bool -> - Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - leq_inductives : flex:bool -> Univ.UInfoInd.t -> - Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> + Univ.Instance.t -> int -> 'a -> 'a; + conv_constructors : (Declarations.mutual_inductive_body * int * int) -> + Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a; } type 'a universe_state = 'a * 'a universe_compare -- cgit v1.2.3 From 9903b47cdccc2fe98a905ab085cb24ca36de1aed Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Fri, 28 Apr 2017 11:12:26 +0200 Subject: Disable debug printing Fix a mistake in record declaration --- kernel/subtyping.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'kernel') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 60cd77f402..60e630a6db 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -303,10 +303,6 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let ctx2 = Univ.instantiate_univ_context cb2.const_universes in let inst1, ctx1 = Univ.UContext.dest ctx1 in let inst2, ctx2 = Univ.UContext.dest ctx2 in - output_string stderr "\ninst1:\n"; - output_string stderr (Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr inst1)); - output_string stderr "\ninst2:\n"; - output_string stderr (Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr inst2)); flush stderr; if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then error IncompatibleInstances else -- cgit v1.2.3 From 4bf85270a36a0a3f9517d8bce92d843f882af00a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 2 May 2017 12:56:14 +0200 Subject: Simplify Univ.ml --- kernel/univ.ml | 4 ---- kernel/univ.mli | 4 ---- 2 files changed, 8 deletions(-) (limited to 'kernel') diff --git a/kernel/univ.ml b/kernel/univ.ml index 5de45cf2b9..eb45f022e9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1091,10 +1091,6 @@ struct let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx' - let dest x = x - - let size ((x,_), _) = Instance.length x - end type universe_info_ind = UInfoInd.t diff --git a/kernel/univ.mli b/kernel/univ.mli index 1141933293..53af804488 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -336,8 +336,6 @@ sig val univ_context : t -> universe_context val subtyp_context : t -> universe_context - val dest : t -> universe_context * universe_context - (** This function takes a universe context representing constraints of an inductive and a Instance.t of fresh universe names for the subtyping (with the same length as the context in the given @@ -347,8 +345,6 @@ sig val subtyping_susbst : t -> universe_level_subst - val size : t -> int - end type universe_info_ind = UInfoInd.t -- cgit v1.2.3 From 47ce63d23b8efe35babe0f4429c550400afd6b4f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 4 May 2017 17:53:12 +0200 Subject: Move univops from kernel to library --- kernel/kernel.mllib | 3 +-- kernel/univops.ml | 70 ----------------------------------------------------- kernel/univops.mli | 17 ------------- 3 files changed, 1 insertion(+), 89 deletions(-) delete mode 100644 kernel/univops.ml delete mode 100644 kernel/univops.mli (limited to 'kernel') diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 8132d66850..0813315b5b 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -41,6 +41,5 @@ Nativelibrary Safe_typing Vm Csymtable -Vconv Declarations -Univops +Vconv diff --git a/kernel/univops.ml b/kernel/univops.ml deleted file mode 100644 index e9383c6d9f..0000000000 --- a/kernel/univops.ml +++ /dev/null @@ -1,70 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> - let u = univ_of_sort u in - LSet.fold LSet.add (Universe.levels u) s - | _ -> fold_constr aux s c - in aux LSet.empty c - -let universes_of_inductive mind = - if mind.mind_polymorphic then - begin - let u = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in - let univ_of_one_ind oind = - let arity_univs = - Context.Rel.fold_outside - (fun decl unvs -> - Univ.LSet.union - (Context.Rel.Declaration.fold_constr - (fun cnstr unvs -> - let cnstr = Vars.subst_instance_constr u cnstr in - Univ.LSet.union - (universes_of_constr cnstr) unvs) - decl Univ.LSet.empty) unvs) - oind.mind_arity_ctxt ~init:Univ.LSet.empty - in - Array.fold_left (fun unvs cns -> - let cns = Vars.subst_instance_constr u cns in - Univ.LSet.union (universes_of_constr cns) unvs) arity_univs - oind.mind_nf_lc - in - let univs = Array.fold_left (fun unvs pk -> Univ.LSet.union (univ_of_one_ind pk) unvs) Univ.LSet.empty mind.mind_packets in - let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mind.mind_universes)) in - let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in - univs - end - else LSet.empty - -let restrict_universe_context (univs,csts) s = - (* Universes that are not necessary to typecheck the term. - E.g. univs introduced by tactics and not used in the proof term. *) - let diff = LSet.diff univs s in - let rec aux diff candid univs ness = - let (diff', candid', univs', ness') = - Constraint.fold - (fun (l, d, r as c) (diff, candid, univs, csts) -> - if not (LSet.mem l diff) then - (LSet.remove r diff, candid, univs, Constraint.add c csts) - else if not (LSet.mem r diff) then - (LSet.remove l diff, candid, univs, Constraint.add c csts) - else (diff, Constraint.add c candid, univs, csts)) - candid (diff, Constraint.empty, univs, ness) - in - if ness' == ness then (LSet.diff univs diff', ness) - else aux diff' candid' univs' ness' - in aux diff csts univs Constraint.empty diff --git a/kernel/univops.mli b/kernel/univops.mli deleted file mode 100644 index 5b499c75bc..0000000000 --- a/kernel/univops.mli +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* universe_set -val universes_of_inductive : mutual_inductive_body -> universe_set -val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set -- cgit v1.2.3 From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- kernel/cbytegen.ml | 4 +- kernel/cbytegen.mli | 2 +- kernel/cooking.ml | 43 +++++++++-------- kernel/cooking.mli | 3 +- kernel/declarations.ml | 16 ++++--- kernel/declareops.ml | 124 ++++++++++++++++++++++++++++++++++--------------- kernel/declareops.mli | 15 +++++- kernel/entries.mli | 9 ++-- kernel/environ.ml | 46 +++++++++++------- kernel/environ.mli | 5 +- kernel/indtypes.ml | 69 +++++++++++++++++---------- kernel/indtypes.mli | 11 ----- kernel/inductive.ml | 10 ++-- kernel/mod_typing.ml | 23 ++++----- kernel/modops.ml | 11 ++--- kernel/modops.mli | 1 + kernel/nativecode.ml | 7 +-- kernel/opaqueproof.ml | 2 +- kernel/opaqueproof.mli | 2 +- kernel/reduction.ml | 67 +++++++++++++++----------- kernel/safe_typing.ml | 79 ++++++++++++++++++------------- kernel/subtyping.ml | 87 +++++++++++++++++++--------------- kernel/term_typing.ml | 97 ++++++++++++++++++++++++-------------- kernel/typeops.ml | 2 +- kernel/univ.ml | 66 +++++++++++++++++++------- kernel/univ.mli | 55 ++++++++++++++++++---- kernel/vconv.ml | 50 +++++++++++--------- 27 files changed, 568 insertions(+), 338 deletions(-) (limited to 'kernel') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 57b397e6f8..02c6a2c715 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -992,8 +992,8 @@ let compile_constant_body fail_on_error env univs = function let body = Mod_subst.force_constr sb in let instance_size = match univs with - | None -> 0 - | Some univ -> Univ.UContext.size univ + | Monomorphic_const _ -> 0 + | Polymorphic_const univ -> Univ.AUContext.size univ in match kind_of_term body with | Const (kn',u) when is_univ_copy instance_size u -> diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index c0f48641ce..48c2e45332 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -10,7 +10,7 @@ val compile : bool -> (* Fail on error with a nice user message, otherwise simpl (** init, fun, fv *) val compile_constant_body : bool -> - env -> constant_universes option -> constant_def -> body_code option + env -> constant_universes -> constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4deadff0a7..0008653644 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -153,8 +153,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * - bool * constant_universes * inline - * Context.Named.t option + constant_universes * inline * Context.Named.t option let on_body ml hy f = function | Undef _ as x -> x @@ -179,17 +178,21 @@ let cook_constr { Opaqueproof.modlist ; abstract } c = abstract_constant_body (expmod c) hyps let lift_univs cb subst = - if cb.const_polymorphic && not (Univ.LMap.is_empty subst) then - let inst = Univ.UContext.instance cb.const_universes in - let cstrs = Univ.UContext.constraints cb.const_universes in - let len = Univ.LMap.cardinal subst in - let subst = - Array.fold_left_i (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc) - subst (Univ.Instance.to_array inst) - in - let cstrs' = Univ.subst_univs_level_constraints subst cstrs in - subst, Univ.UContext.make (inst,cstrs') - else subst, cb.const_universes + match cb.const_universes with + | Monomorphic_const ctx -> subst, (Monomorphic_const ctx) + | Polymorphic_const auctx -> + if (Univ.LMap.is_empty subst) then + subst, (Polymorphic_const auctx) + else + let inst = Univ.AUContext.instance auctx in + let len = Univ.LMap.cardinal subst in + let subst = + Array.fold_left_i + (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc) + subst (Univ.Instance.to_array inst) + in + let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in + subst, (Polymorphic_const auctx') let cook_constant ~hcons env { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in @@ -243,15 +246,15 @@ let cook_constant ~hcons env { from = cb; info } = proj_eta = etab, etat; proj_type = ty'; proj_body = c' } in - let univs = - let abs' = - if cb.const_polymorphic then abs_ctx - else instantiate_univ_context abs_ctx - in - UContext.union abs' univs + let univs = + match univs with + | Monomorphic_const ctx -> + Monomorphic_const (UContext.union (instantiate_univ_context abs_ctx) ctx) + | Polymorphic_const auctx -> + Polymorphic_const (AUContext.union abs_ctx auctx) in (body, typ, Option.map projection cb.const_proj, - cb.const_polymorphic, univs, cb.const_inline_code, + univs, cb.const_inline_code, Some const_hyps) (* let cook_constant_key = Profile.declare_profile "cook_constant" *) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7d47eba23e..9db85a4a11 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -18,8 +18,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * - bool * constant_universes * inline - * Context.Named.t option + constant_universes * inline * Context.Named.t option val cook_constant : hcons:bool -> env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr diff --git a/kernel/declarations.ml b/kernel/declarations.ml index ae47324560..f3b7ae2b24 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -64,7 +64,9 @@ type constant_def = | Def of constr Mod_subst.substituted (** or a transparent global definition *) | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) -type constant_universes = Univ.universe_context +type constant_universes = + | Monomorphic_const of Univ.universe_context + | Polymorphic_const of Univ.abstract_universe_context (** The [typing_flags] are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking @@ -83,7 +85,6 @@ type constant_body = { const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; - const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; @@ -168,6 +169,11 @@ type one_inductive_body = { mind_reloc_tbl : Cbytecodes.reloc_table; } +type abstrac_inductive_universes = + | Monomorphic_ind of Univ.universe_context + | Polymorphic_ind of Univ.abstract_universe_context + | Cumulative_ind of Univ.abstract_cumulativity_info + type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) @@ -186,11 +192,7 @@ type mutual_inductive_body = { mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) - mind_polymorphic : bool; (** Is it polymorphic or not *) - - mind_cumulative : bool; (** Is it cumulative or not *) - - mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *) + mind_universes : abstrac_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 1d91b2d414..72b4907680 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -45,14 +45,15 @@ let hcons_template_arity ar = (** {6 Constants } *) let instantiate cb c = - if cb.const_polymorphic then - Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c - else c + match cb.const_universes with + | Monomorphic_const _ -> c + | Polymorphic_const ctx -> + Vars.subst_instance_constr (Univ.AUContext.instance ctx) c -let instantiate_constraints cb cst = - if cb.const_polymorphic then - Univ.subst_instance_constraints (Univ.UContext.instance cb.const_universes) cst - else cst +let constant_is_polymorphic cb = + match cb.const_universes with + | Monomorphic_const _ -> false + | Polymorphic_const _ -> true let body_of_constant otab cb = match cb.const_body with | Undef _ -> None @@ -67,34 +68,55 @@ let type_of_constant cb = | TemplateArity _ as x -> x let constraints_of_constant otab cb = - let cst = Univ.Constraint.union - (Univ.UContext.constraints cb.const_universes) - (match cb.const_body with - | Undef _ -> Univ.empty_constraint - | Def c -> Univ.empty_constraint - | OpaqueDef o -> - Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) - in instantiate_constraints cb cst + match cb.const_universes with + | Polymorphic_const ctx -> + Univ.UContext.constraints (Univ.instantiate_univ_context ctx) + | Monomorphic_const ctx -> + Univ.Constraint.union + (Univ.UContext.constraints ctx) + (match cb.const_body with + | Undef _ -> Univ.empty_constraint + | Def c -> Univ.empty_constraint + | OpaqueDef o -> + Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) let universes_of_constant otab cb = match cb.const_body with - | Undef _ | Def _ -> cb.const_universes + | Undef _ | Def _ -> + begin + match cb.const_universes with + | Monomorphic_const ctx -> ctx + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + end | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints otab o in - assert(not cb.const_polymorphic || Univ.ContextSet.is_empty body_uctxs); - let uctxs = Univ.ContextSet.of_context cb.const_universes in - Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) + let body_uctxs = Opaqueproof.force_constraints otab o in + match cb.const_universes with + | Monomorphic_const ctx -> + let uctxs = Univ.ContextSet.of_context ctx in + Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) + | Polymorphic_const ctx -> + assert(Univ.ContextSet.is_empty body_uctxs); + Univ.instantiate_univ_context ctx let universes_of_polymorphic_constant otab cb = - if cb.const_polymorphic then - let univs = universes_of_constant otab cb in - Univ.instantiate_univ_context univs - else Univ.UContext.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.UContext.empty + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx let constant_has_body cb = match cb.const_body with | Undef _ -> false | Def _ | OpaqueDef _ -> true +let constant_polymorphic_instance cb = + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.AUContext.instance ctx + +let constant_polymorphic_context cb = + match cb.const_universes with + | Monomorphic_const _ -> Univ.UContext.empty + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Undef _ | Def _ -> false @@ -142,7 +164,6 @@ let subst_const_body sub cb = const_proj = proj'; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; - const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -173,11 +194,18 @@ let hcons_const_def = function Def (from_val (Term.hcons_constr constr)) | OpaqueDef _ as x -> x (* hashconsed when turned indirect *) +let hcons_const_universes cbu = + match cbu with + | Monomorphic_const ctx -> + Monomorphic_const (Univ.hcons_universe_context ctx) + | Polymorphic_const ctx -> + Polymorphic_const (Univ.hcons_abstract_universe_context ctx) + let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = hcons_const_type cb.const_type; - const_universes = Univ.hcons_universe_context cb.const_universes } + const_universes = hcons_const_universes cb.const_universes } (** {6 Inductive types } *) @@ -266,22 +294,36 @@ let subst_mind_body sub mib = mind_params_ctxt = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_polymorphic = mib.mind_polymorphic; - mind_cumulative = mib.mind_cumulative; mind_universes = mib.mind_universes; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } -let inductive_instance mib = - if mib.mind_polymorphic then - Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) - else Univ.Instance.empty - -let inductive_context mib = - if mib.mind_polymorphic then - Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) - else Univ.UContext.empty +let inductive_polymorphic_instance mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind ctx -> Univ.AUContext.instance ctx + | Cumulative_ind cumi -> + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + +let inductive_polymorphic_context mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.UContext.empty + | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx + | Cumulative_ind cumi -> + Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) + +let inductive_is_polymorphic mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> true + | Cumulative_ind cumi -> true + +let inductive_is_cumulative mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> false + | Cumulative_ind cumi -> true (** {6 Hash-consing of inductive declarations } *) @@ -309,11 +351,17 @@ let hcons_mind_packet oib = mind_user_lc = user; mind_nf_lc = nf } +let hcons_mind_universes miu = + match miu with + | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx) + | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx) + | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui) + let hcons_mind mib = { mib with mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; - mind_universes = Univ.hcons_universe_info_ind mib.mind_universes } + mind_universes = hcons_mind_universes mib.mind_universes } (** {6 Stm machinery } *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 6650b6b7b0..811a28aa65 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -27,6 +27,12 @@ val subst_const_body : substitution -> constant_body -> constant_body val constant_has_body : constant_body -> bool +val constant_polymorphic_instance : constant_body -> universe_instance +val constant_polymorphic_context : constant_body -> universe_context + +(** Is the constant polymorphic? *) +val constant_is_polymorphic : constant_body -> bool + (** Accessing const_body, forcing access to opaque proof term if needed. Only use this function if you know what you're doing. *) @@ -66,8 +72,13 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body -val inductive_instance : mutual_inductive_body -> universe_instance -val inductive_context : mutual_inductive_body -> universe_context +val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance +val inductive_polymorphic_context : mutual_inductive_body -> universe_context + +(** Is the inductive polymorphic? *) +val inductive_is_polymorphic : mutual_inductive_body -> bool +(** Is the inductive cumulative? *) +val inductive_is_cumulative : mutual_inductive_body -> bool (** {6 Kernel flags} *) diff --git a/kernel/entries.mli b/kernel/entries.mli index 9c17346f22..f133587c16 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -34,6 +34,11 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; [mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]]. *) +type inductive_universes = + | Monomorphic_ind_entry of Univ.universe_context + | Polymorphic_ind_entry of Univ.universe_context + | Cumulative_ind_entry of Univ.cumulativity_info + type one_inductive_entry = { mind_entry_typename : Id.t; mind_entry_arity : constr; @@ -49,9 +54,7 @@ type mutual_inductive_entry = { mind_entry_finite : Decl_kinds.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; - mind_entry_polymorphic : bool; - mind_entry_cumulative : bool; - mind_entry_universes : Univ.universe_info_ind; + mind_entry_universes : inductive_universes; (* universe constraints and the constraints for subtyping of inductive types in the block. *) mind_entry_private : bool option; diff --git a/kernel/environ.ml b/kernel/environ.ml index 5727bf2ea1..1ab5b7a8d1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -228,8 +228,10 @@ let add_constant kn cb env = add_constant_key kn cb no_link_info env let constraints_of cb u = - let univs = cb.const_universes in - Univ.subst_instance_constraints u (Univ.UContext.constraints univs) + match cb.const_universes with + | Monomorphic_const _ -> Univ.Constraint.empty + | Polymorphic_const ctx -> + Univ.UContext.constraints (Univ.subst_instance_context u ctx) let map_regular_arity f = function | RegularArity a as ar -> @@ -240,15 +242,23 @@ let map_regular_arity f = function (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then - let csts = constraints_of cb u in - (map_regular_arity (subst_instance_constr u) cb.const_type, csts) - else cb.const_type, Univ.Constraint.empty + match cb.const_universes with + | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty + | Polymorphic_const ctx -> + let csts = constraints_of cb u in + (map_regular_arity (subst_instance_constr u) cb.const_type, csts) + +let constant_instance env kn = + let cb = lookup_constant kn env in + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.AUContext.instance ctx let constant_context env kn = let cb = lookup_constant kn env in - if cb.const_polymorphic then cb.const_universes - else Univ.UContext.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.UContext.empty + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx type const_evaluation_result = NoBody | Opaque | IsProj @@ -259,10 +269,14 @@ let constant_value env (kn,u) = if cb.const_proj = None then match cb.const_body with | Def l_body -> - if cb.const_polymorphic then - let csts = constraints_of cb u in - (subst_instance_constr u (Mod_subst.force_constr l_body), csts) - else Mod_subst.force_constr l_body, Univ.Constraint.empty + begin + match cb.const_universes with + | Monomorphic_const _ -> + (Mod_subst.force_constr l_body, Univ.Constraint.empty) + | Polymorphic_const _ -> + let csts = constraints_of cb u in + (subst_instance_constr u (Mod_subst.force_constr l_body), csts) + end | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) else raise (NotEvaluableConst IsProj) @@ -273,7 +287,7 @@ let constant_opt_value env cst = let constant_value_and_type env (kn, u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then + if Declareops.constant_is_polymorphic cb then let cst = constraints_of cb u in let b' = match cb.const_body with | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body)) @@ -295,7 +309,7 @@ let constant_value_and_type env (kn, u) = (* constant_type gives the type of a constant *) let constant_type_in env (kn,u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then + if Declareops.constant_is_polymorphic cb then map_regular_arity (subst_instance_constr u) cb.const_type else cb.const_type @@ -321,7 +335,7 @@ let evaluable_constant kn env = | Undef _ -> false let polymorphic_constant cst env = - (lookup_constant cst env).const_polymorphic + Declareops.constant_is_polymorphic (lookup_constant cst env) let polymorphic_pconstant (cst,u) env = if Univ.Instance.is_empty u then false @@ -353,7 +367,7 @@ let is_projection cst env = let lookup_mind = lookup_mind let polymorphic_ind (mind,i) env = - (lookup_mind mind env).mind_polymorphic + Declareops.inductive_is_polymorphic (lookup_mind mind env) let polymorphic_pind (ind,u) env = if Univ.Instance.is_empty u then false diff --git a/kernel/environ.mli b/kernel/environ.mli index b7431dbe5f..ae3afcb355 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -161,6 +161,9 @@ val constant_value_and_type : env -> constant puniverses -> (** The universe context associated to the constant, empty if not polymorphic *) val constant_context : env -> constant -> Univ.universe_context +(** The universe isntance associated to the constant, empty if not + polymorphic *) +val constant_instance : env -> constant -> Univ.universe_instance (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant @@ -256,7 +259,7 @@ type unsafe_type_judgment = types punsafe_type_judgment (** {6 Compilation of global declaration } *) -val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option +val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option exception Hyp_not_found diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5cfcbba606..00fbe27a70 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -231,23 +231,23 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) -let check_subtyping mie paramsctxt env_ar inds = +let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in - let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in + let sbsubst = CumulativityInfo.subtyping_susbst cumi in let dosubst = subst_univs_level_constr sbsubst in - let uctx = UInfoInd.univ_context mie.mind_entry_universes in + let uctx = CumulativityInfo.univ_context cumi in let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env' = Environ.push_context uctx env_ar in - let env'' = Environ.push_context uctx_other env' in - let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in + let env = Environ.push_context uctx env_ar in + let env = Environ.push_context uctx_other env in + let env = push_context (CumulativityInfo.subtyp_context cumi) env in (* process individual inductive types: *) Array.iter (fun (id,cn,lc,(sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> - check_subtyping_arity_constructor envsb dosubst full_arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc + check_subtyping_arity_constructor env dosubst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc | TemplateArity _ -> () ) inds @@ -264,7 +264,13 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in + let univctx = + match mie.mind_entry_universes with + | Monomorphic_ind_entry ctx -> ctx + | Polymorphic_ind_entry ctx -> ctx + | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi + in + let env' = push_context univctx env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -383,16 +389,21 @@ let typecheck_inductive env mie = | _ (* Not an explicit occurrence of Type *) -> full_polymorphic () in - let arity = - if mie.mind_entry_polymorphic then full_polymorphic () - else template_polymorphic () + let arity = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ -> template_polymorphic () + | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> full_polymorphic () in (id,cn,lc,(sign,arity))) inds in (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) - let () = if mie.mind_entry_cumulative then check_subtyping mie paramsctxt env_arities inds + let () = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ -> () + | Polymorphic_ind_entry _ -> () + | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) @@ -864,14 +875,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = +let abstract_inductive_universes iu = + match iu with + | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) + | Polymorphic_ind_entry ctx -> + let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx) + | Cumulative_ind_entry cumi -> + let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi) + +let build_inductive env prv iu env_ar 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 nparamargs = Context.Rel.nhyps paramsctxt in let nparamsctxt = Context.Rel.length paramsctxt in - let substunivs, ctxunivs = Univ.abstract_universes p (Univ.UInfoInd.univ_context ctx) in - let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) in + let substunivs, aiu = abstract_inductive_universes iu in let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in let env_ar = let ctxunivs = Environ.rel_context env_ar in @@ -942,10 +960,14 @@ let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite ind && Array.length pkt.mind_consnames == 1 && pkt.mind_consnrealargs.(0) > 0 -> (** The elimination criterion ensures that all projections can be defined. *) - let u = - if p then - subst_univs_level_instance substunivs (Univ.UContext.instance ctxunivs) - else Univ.Instance.empty + let u = + let process auctx = + subst_univs_level_instance substunivs (Univ.AUContext.instance auctx) + in + match aiu with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind acumi -> process (Univ.ACumulativityInfo.univ_context acumi) in let indsp = ((kn, 0), u) in let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in @@ -968,9 +990,7 @@ let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite ind mind_nparams_rec = nmr; mind_params_ctxt = paramsctxt; mind_packets = packets; - mind_polymorphic = p; - mind_cumulative = cum; - mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp); + mind_universes = aiu; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -985,7 +1005,6 @@ let check_inductive env kn mie = let chkpos = (Environ.typing_flags env).check_guarded in let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in (* Build the inductive packets *) - build_inductive env mie.mind_entry_cumulative mie.mind_entry_polymorphic mie.mind_entry_private - mie.mind_entry_universes + build_inductive env mie.mind_entry_private mie.mind_entry_universes env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 7b0f017941..5b4615399d 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -32,17 +32,6 @@ type inductive_error = exception InductiveError of inductive_error -val check_subtyping_arity_constructor : Environ.env -> -(Term.constr -> Term.constr) -> Term.types -> int -> bool -> unit - -(* This needs not be exposed. Exposing for debugging purposes! *) -val check_subtyping : Entries.mutual_inductive_entry -> -Context.Rel.t -> -Environ.env -> -('b * 'c * Term.types array * - ('d * ('e * Term.types * 'f, 'g) Declarations.declaration_arity)) -array -> unit - (** The following function does checks on inductive declarations. *) val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 0f0dc0d607..e81a1cb587 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -54,9 +54,13 @@ let inductive_paramdecls (mib,u) = Vars.subst_instance_context u mib.mind_params_ctxt let instantiate_inductive_constraints mib u = - if mib.mind_polymorphic then - Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes)) - else Univ.Constraint.empty + let process auctx = + Univ.UContext.constraints (Univ.subst_instance_context u auctx) + in + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Constraint.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) (************************************************************************) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index ff44f0f540..79016735bc 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -74,12 +74,13 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = as long as they have the right type *) let uctx = Declareops.universes_of_constant (opaque_tables env) cb in let uctx = (* Context of the spec *) - if cb.const_polymorphic then - Univ.instantiate_univ_context uctx - else uctx + match cb.const_universes with + | Monomorphic_const _ -> uctx + | Polymorphic_const auctx -> + Univ.instantiate_univ_context auctx in let c', univs, ctx' = - if not cb.const_polymorphic then + if not (Declareops.constant_is_polymorphic cb) then let env' = Environ.push_context ~strict:true uctx env' in let env' = Environ.push_context ~strict:true ctx env' in let c',cst = match cb.const_body with @@ -92,7 +93,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = | Def cs -> let c' = Mod_subst.force_constr cs in c, Reduction.infer_conv env' (Environ.universes env') c c' - in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) + in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) else let cus, ccst = Univ.UContext.dest uctx in let newus, cst = Univ.UContext.dest ctx in @@ -122,21 +123,17 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = in if not (Univ.Constraint.is_empty cst) then error_incorrect_with_constraint lab; - let subst, ctx = Univ.abstract_universes true ctx in - Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty + let subst, ctx = Univ.abstract_universes ctx in + Vars.subst_univs_level_constr subst c, Polymorphic_const ctx, Univ.ContextSet.empty in let def = Def (Mod_subst.from_val c') in (* let ctx' = Univ.UContext.make (newus, cst) in *) - let univs = - if cb.const_polymorphic then Some cb.const_universes - else None - in let cb' = { cb with const_body = def; - const_universes = ctx ; + const_universes = univs ; const_body_code = Option.map Cemitcodes.from_val - (compile_constant_body env' univs def) } + (compile_constant_body env' cb.const_universes def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else diff --git a/kernel/modops.ml b/kernel/modops.ml index 1f8b97ae6a..33d13f1ba0 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -35,6 +35,7 @@ type signature_mismatch_error = | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField | NotConvertibleTypeField of env * types * types + | CumulativeStatusExpected of bool | PolymorphicStatusExpected of bool | NotSameConstructorNamesField | NotSameInductiveNameInBlockField @@ -327,12 +328,10 @@ let strengthen_const mp_from l cb resolver = |_ -> let kn = KerName.make2 mp_from l in let con = constant_of_delta_kn resolver kn in - let u = - if cb.const_polymorphic then - let u = Univ.UContext.instance cb.const_universes in - let s = Univ.make_instance_subst u in - Univ.subst_univs_level_instance s u - else Univ.Instance.empty + let u = + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.make_abstract_instance ctx in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); diff --git a/kernel/modops.mli b/kernel/modops.mli index e9f3db6e91..4b533c7efd 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -94,6 +94,7 @@ type signature_mismatch_error = | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField | NotConvertibleTypeField of env * types * types + | CumulativeStatusExpected of bool | PolymorphicStatusExpected of bool | NotSameConstructorNamesField | NotSameInductiveNameInBlockField diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d3cd6b62a5..4941d64d82 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1863,8 +1863,9 @@ let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with | None -> let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes - else Univ.Instance.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.AUContext.instance ctx in begin match cb.const_body with | Def t -> @@ -1960,7 +1961,7 @@ let param_name = Name (id_of_string "params") let arg_name = Name (id_of_string "arg") let compile_mind prefix ~interactive mb mind stack = - let u = Declareops.inductive_instance mb in + let u = Declareops.inductive_polymorphic_instance mb in let f i stack ob = let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in let j = push_symbol (SymbInd (mind,i)) in diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 59e90ca2e9..3e15ff7401 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } + abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } type proofterm = (constr * Univ.universe_context_set) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 3897d5e51e..be1f4b13f0 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } + abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } (* The type has two caveats: 1) cook_constr is defined after diff --git a/kernel/reduction.ml b/kernel/reduction.ml index ea583fdac8..8bf95e5de9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -497,11 +497,12 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if eq_ind ind1 ind2 then let mind = Environ.lookup_mind (fst ind1) env in let cuniv = - if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + convert_instances ~flex:false u1 u2 cuniv + | Declarations.Cumulative_ind cumi -> convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1) u2 (CClosure.stack_args_size v2) cuniv - else - convert_instances ~flex:false u1 u2 cuniv in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible @@ -510,12 +511,13 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if Int.equal j1 j2 && eq_ind ind1 ind2 then let mind = Environ.lookup_mind (fst ind1) env in let cuniv = - if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + convert_instances ~flex:false u1 u2 cuniv + | Declarations.Cumulative_ind _ -> convert_constructors (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1) u2 (CClosure.stack_args_size v2) cuniv - else - convert_instances ~flex:false u1 u2 cuniv in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible @@ -637,22 +639,26 @@ let infer_check_conv_inductives infer_check_convert_instances infer_check_inductive_instances cv_pb (mind, ind) u1 sv1 u2 sv2 univs = - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + infer_check_convert_instances ~flex:false u1 u2 univs + | Declarations.Cumulative_ind cumi -> let num_param_arity = mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs in if not (num_param_arity = sv1 && num_param_arity = sv2) then infer_check_convert_instances ~flex:false u1 u2 univs else - let uinfind = mind.Declarations.mind_universes in - infer_check_inductive_instances cv_pb uinfind u1 u2 univs - else infer_check_convert_instances ~flex:false u1 u2 univs + infer_check_inductive_instances cv_pb cumi u1 u2 univs let infer_check_conv_constructors infer_check_convert_instances infer_check_inductive_instances (mind, ind, cns) u1 sv1 u2 sv2 univs = - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + infer_check_convert_instances ~flex:false u1 u2 univs + | Declarations.Cumulative_ind cumi -> let num_cnstr_args = let nparamsctxt = mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs @@ -662,26 +668,30 @@ let infer_check_conv_constructors if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then infer_check_convert_instances ~flex:false u1 u2 univs else - let uinfind = mind.Declarations.mind_universes in - infer_check_inductive_instances CONV uinfind u1 u2 univs - else infer_check_convert_instances ~flex:false u1 u2 univs + infer_check_inductive_instances CONV cumi u1 u2 univs -let check_inductive_instances cv_pb uinfind u u' univs = - let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in - let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in +let check_inductive_instances cv_pb cumi u u' univs = + let ind_instance = + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + in + let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.subst_instance_constraints comp_subst ind_sbcst + Univ.UContext.constraints + (Univ.subst_instance_context comp_subst ind_subtypctx) in let comp_cst = match cv_pb with CONV -> - let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + let comp_cst' = + let comp_subst = (Univ.Instance.append u' u) in + Univ.UContext.constraints + (Univ.subst_instance_context comp_subst ind_subtypctx) + in Univ.Constraint.union comp_cst comp_cst' | CUMUL -> comp_cst in @@ -746,22 +756,27 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = else Univ.enforce_eq_instances u u' cstrs in (univs, cstrs') -let infer_inductive_instances cv_pb uinfind u u' (univs, cstrs) = - let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in - let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in +let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = + let ind_instance = + Univ.AUContext.instance (Univ.ACumulativityInfo.subtyp_context cumi) + in + let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.subst_instance_constraints comp_subst ind_sbcst + Univ.UContext.constraints + (Univ.subst_instance_context comp_subst ind_subtypctx) in let comp_cst = match cv_pb with CONV -> - let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + let comp_cst' = + let comp_subst = (Univ.Instance.append u' u) in + Univ.UContext.constraints + (Univ.subst_instance_context comp_subst ind_subtypctx) in Univ.Constraint.union comp_cst comp_cst' | CUMUL -> comp_cst in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 1568fe0bf2..946222ef2f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -237,20 +237,29 @@ let private_con_of_scheme ~kind env cl = let universes_of_private eff = let open Declarations in - List.fold_left (fun acc { Entries.eff } -> - match eff with - | Entries.SEscheme (l,s) -> - List.fold_left (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (_, ctx) -> ctx :: acc in - if cb.const_polymorphic then acc - else (Univ.ContextSet.of_context cb.const_universes) :: acc) - acc l - | Entries.SEsubproof (c, cb, e) -> - if cb.const_polymorphic then acc - else Univ.ContextSet.of_context cb.const_universes :: acc) - [] (Term_typing.uniq_seff eff) + List.fold_left + (fun acc { Entries.eff } -> + match eff with + | Entries.SEscheme (l,s) -> + List.fold_left + (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc + in + match cb.const_universes with + | Monomorphic_const ctx -> + (Univ.ContextSet.of_context ctx) :: acc + | Polymorphic_const _ -> acc + ) + acc l + | Entries.SEsubproof (c, cb, e) -> + match cb.const_universes with + | Monomorphic_const ctx -> + (Univ.ContextSet.of_context ctx) :: acc + | Polymorphic_const _ -> acc + ) + [] (Term_typing.uniq_seff eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -373,7 +382,11 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in + let c,typ,univs = + match Term_typing.translate_local_def senv.revstruct senv.env id de with + | c, typ, Monomorphic_const ctx -> c, typ, ctx + | _, _, Polymorphic_const _ -> assert false + in let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with @@ -410,26 +423,28 @@ let labels_of_mib mib = get () let globalize_constant_universes env cb = - if cb.const_polymorphic then - [Now (true, Univ.ContextSet.empty)] - else - let cstrs = Univ.ContextSet.of_context cb.const_universes in - Now (false, cstrs) :: - (match cb.const_body with - | (Undef _ | Def _) -> [] - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with - | None -> [] - | Some fc -> + match cb.const_universes with + | Monomorphic_const ctx -> + let cstrs = Univ.ContextSet.of_context ctx in + Now (false, cstrs) :: + (match cb.const_body with + | (Undef _ | Def _) -> [] + | OpaqueDef lc -> + match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with + | None -> [] + | Some fc -> match Future.peek_val fc with - | None -> [Later fc] - | Some c -> [Now (false, c)]) + | None -> [Later fc] + | Some c -> [Now (false, c)]) + | Polymorphic_const _ -> + [Now (true, Univ.ContextSet.empty)] let globalize_mind_universes mb = - if mb.mind_polymorphic then - [Now (true, Univ.ContextSet.empty)] - else - [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))] + match mb.mind_universes with + | Monomorphic_ind ctx -> + [Now (false, Univ.ContextSet.of_context ctx)] + | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)] + | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)] let constraints_of_sfb env sfb = match sfb with diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 60e630a6db..1bd9d6e495 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -104,15 +104,21 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib | _ -> error (InductiveFieldExpected mib2) in - let poly = - if not (mib1.mind_polymorphic == mib2.mind_polymorphic) then - error (PolymorphicStatusExpected mib2.mind_polymorphic) - else mib2.mind_polymorphic - in - let u = - if poly then - CErrors.user_err Pp.(str "Checking of subtyping of polymorphic inductive types not implemented") - else Instance.empty + let u = + let process inst inst' = + if Univ.Instance.equal inst inst' then inst else error IncompatibleInstances + in + match mib1.mind_universes, mib2.mind_universes with + | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx, Polymorphic_ind auctx' -> + process + (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx') + | Cumulative_ind cumi, Cumulative_ind cumi' -> + process + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi')) + | _ -> error + (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2)) in let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name env t1 t2 = @@ -148,7 +154,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 error (NotConvertibleInductiveField name) | _ -> (s1, s2) in check_conv (NotConvertibleInductiveField name) - cst poly u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) + cst (inductive_is_polymorphic mib1) u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) in let check_packet cst p1 p2 = @@ -176,7 +182,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let check_cons_types i cst p1 p2 = Array.fold_left3 (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst - poly u infer_conv env t1 t2) + (inductive_is_polymorphic mib1) u infer_conv env t1 t2) cst p2.mind_consnames (arities_of_specif (mind,u) (mib1,p1)) @@ -293,37 +299,42 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let cb2 = Declareops.subst_const_body subst2 cb2 in (* Start by checking universes *) let poly = - if not (cb1.const_polymorphic == cb2.const_polymorphic) then - error (PolymorphicStatusExpected cb2.const_polymorphic) - else cb2.const_polymorphic + if not (Declareops.constant_is_polymorphic cb1 + == Declareops.constant_is_polymorphic cb2) then + error (PolymorphicStatusExpected (Declareops.constant_is_polymorphic cb2)) + else Declareops.constant_is_polymorphic cb2 in - let cst', env', u = - if poly then - let ctx1 = Univ.instantiate_univ_context cb1.const_universes in - let ctx2 = Univ.instantiate_univ_context cb2.const_universes in - let inst1, ctx1 = Univ.UContext.dest ctx1 in - let inst2, ctx2 = Univ.UContext.dest ctx2 in + let cst', env', u = + match cb1.const_universes, cb2.const_universes with + | Monomorphic_const _, Monomorphic_const _ -> + cst, env, Univ.Instance.empty + | Polymorphic_const auctx1, Polymorphic_const auctx2 -> + begin + let ctx1 = Univ.instantiate_univ_context auctx1 in + let ctx2 = Univ.instantiate_univ_context auctx2 in + let inst1, ctx1 = Univ.UContext.dest ctx1 in + let inst2, ctx2 = Univ.UContext.dest ctx2 in if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then error IncompatibleInstances else let cstrs = Univ.enforce_eq_instances inst1 inst2 cst in let cstrs = Univ.Constraint.union cstrs ctx2 in - try - (* The environment with the expected universes plus equality - of the body instances with the expected instance *) - let ctxi = Univ.Instance.append inst1 inst2 in - let ctx = Univ.UContext.make (ctxi, cstrs) in - let env = Environ.push_context ctx env in - (* Check that the given definition does not add any constraint over - the expected ones, so that it can be used in place of - the original. *) - if UGraph.check_constraints ctx1 (Environ.universes env) then - cstrs, env, inst2 - else error (IncompatibleConstraints ctx1) - with Univ.UniverseInconsistency incon -> - error (IncompatibleUniverses incon) - else - cst, env, Univ.Instance.empty + try + (* The environment with the expected universes plus equality + of the body instances with the expected instance *) + let ctxi = Univ.Instance.append inst1 inst2 in + let ctx = Univ.UContext.make (ctxi, cstrs) in + let env = Environ.push_context ctx env in + (* Check that the given definition does not add any constraint over + the expected ones, so that it can be used in place of + the original. *) + if UGraph.check_constraints ctx1 (Environ.universes env) then + cstrs, env, inst2 + else error (IncompatibleConstraints ctx1) + with Univ.UniverseInconsistency incon -> + error (IncompatibleUniverses incon) + end + | _ -> assert false in (* Now check types *) let typ1 = Typeops.type_of_constant_type env' cb1.const_type in @@ -354,7 +365,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "name.")); let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; - let u1 = inductive_instance mind1 in + let u1 = inductive_polymorphic_instance mind1 in let arity1,cst1 = constrained_type_of_inductive env ((mind1,mind1.mind_packets.(i)),u1) in let cst2 = @@ -371,7 +382,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "name.")); let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; - let u1 = inductive_instance mind1 in + let u1 = inductive_polymorphic_instance mind1 in let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in let cst2 = Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3cf2299d83..5370bcea43 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -121,18 +121,19 @@ let inline_side_effects env body ctx side_eff = | OpaqueDef _, `Opaque (b,_) -> (b, true) | _ -> assert false in - if cb.const_polymorphic then - (** Inline the term to emulate universe polymorphism *) - let data = (Univ.UContext.instance cb.const_universes, b) in - let subst = Cmap_env.add c (Inl data) subst in - (subst, var, ctx, args) - else + match cb.const_universes with + | Monomorphic_const cnstctx -> (** Abstract over the term at the top of the proof *) let ty = Typeops.type_of_constant_type env cb.const_type in let subst = Cmap_env.add c (Inr var) subst in - let univs = Univ.ContextSet.of_context cb.const_universes in + let univs = Univ.ContextSet.of_context cnstctx in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) + | Polymorphic_const auctx -> + (** Inline the term to emulate universe polymorphism *) + let data = (Univ.AUContext.instance auctx, b) in + let subst = Cmap_env.add c (Inl data) subst in + (subst, var, ctx, args) in let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in (** Third step: inline the definitions *) @@ -225,16 +226,25 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:state_id Feedback.Complete) +let abstract_constant_universes abstract uctx = + if not abstract then + Univ.empty_level_subst, Monomorphic_const uctx + else + let sbst, auctx = Univ.abstract_universes uctx in + sbst, Polymorphic_const auctx + let infer_declaration ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in let j = infer env t in let abstract = poly && not (Option.is_empty kn) in - let usubst, univs = Univ.abstract_universes abstract uctx in + let usubst, univs = + abstract_constant_universes abstract uctx + in let c = Typeops.assumption_of_judgment env j in let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in - Undef nl, RegularArity t, None, poly, univs, false, ctx + Undef nl, RegularArity t, None, univs, false, ctx (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. @@ -264,9 +274,9 @@ let infer_declaration ~trust env kn dcl = feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in - def, RegularArity typ, None, c.const_entry_polymorphic, - c.const_entry_universes, - c.const_entry_inline_code, c.const_entry_secctx + def, RegularArity typ, None, + (Monomorphic_const c.const_entry_universes), + c.const_entry_inline_code, c.const_entry_secctx (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> @@ -279,7 +289,8 @@ let infer_declaration ~trust env kn dcl = let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = - Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in + abstract_constant_universes abstract (Univ.ContextSet.to_context ctx) + in let j = infer env body in let typ = match typ with | None -> @@ -298,8 +309,7 @@ let infer_declaration ~trust env kn dcl = else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; - def, typ, None, c.const_entry_polymorphic, - univs, c.const_entry_inline_code, c.const_entry_secctx + def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> let mib, _ = Inductive.lookup_mind_specif env (ind,0) in @@ -311,9 +321,16 @@ let infer_declaration ~trust env kn dcl = else assert false | _ -> assert false in + let univs = + match mib.mind_universes with + | Monomorphic_ind ctx -> Monomorphic_const ctx + | Polymorphic_ind auctx -> Polymorphic_const auctx + | Cumulative_ind acumi -> + Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) + in let term, typ = pb.proj_eta in Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, - mib.mind_polymorphic, Univ.UInfoInd.univ_context mib.mind_universes, false, None + univs, false, None let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t @@ -337,7 +354,7 @@ let record_aux env s_ty s_bo suggested_expr = let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = +let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -409,9 +426,8 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) check declared inferred) lc) in let tps = let res = - let comp_univs = if poly then Some univs else None in match proj with - | None -> compile_constant_body env comp_univs def + | None -> compile_constant_body env univs def | Some pb -> (* The compilation of primitive projections is a bit tricky, because they refer to themselves (the body of p looks like fun c => @@ -425,14 +441,13 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_type = typ; const_proj = proj; const_body_code = None; - const_polymorphic = poly; const_universes = univs; const_inline_code = inline_code; const_typing_flags = Environ.typing_flags env; } in let env = add_constant kn cb env in - compile_constant_body env comp_univs def + compile_constant_body env univs def in Option.map Cemitcodes.from_val res in { const_hyps = hyps; @@ -440,7 +455,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_type = typ; const_proj = proj; const_body_code = tps; - const_polymorphic = poly; const_universes = univs; const_inline_code = inline_code; const_typing_flags = Environ.typing_flags env } @@ -452,6 +466,12 @@ let translate_constant mb env kn ce = (infer_declaration ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = + let poly, univs = + match cb.const_universes with + | Monomorphic_const ctx -> false, ctx + | Polymorphic_const auctx -> + true, Univ.instantiate_univ_context auctx + in let pt = match cb.const_body, u with | OpaqueDef _, `Opaque (b, c) -> b, c @@ -463,8 +483,8 @@ let constant_entry_of_side_effect cb u = const_entry_feedback = None; const_entry_type = (match cb.const_type with RegularArity t -> Some t | _ -> None); - const_entry_polymorphic = cb.const_polymorphic; - const_entry_universes = cb.const_universes; + const_entry_polymorphic = poly; + const_entry_universes = univs; const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } ;; @@ -508,16 +528,23 @@ let export_side_effects mb env ce = let trusted = check_signatures mb signatures in let push_seff env = function | kn, cb, `Nothing, _ -> - let env = Environ.add_constant kn cb env in - if not cb.const_polymorphic then - Environ.push_context ~strict:true cb.const_universes env - else env - | kn, cb, `Opaque(_, ctx), _ -> - let env = Environ.add_constant kn cb env in - if not cb.const_polymorphic then - let env = Environ.push_context ~strict:true cb.const_universes env in - Environ.push_context_set ~strict:true ctx env - else env in + begin + let env = Environ.add_constant kn cb env in + match cb.const_universes with + | Monomorphic_const ctx -> + Environ.push_context ~strict:true ctx env + | Polymorphic_const _ -> env + end + | kn, cb, `Opaque(_, ctx), _ -> + begin + let env = Environ.add_constant kn cb env in + match cb.const_universes with + | Monomorphic_const cstctx -> + let env = Environ.push_context ~strict:true cstctx env in + Environ.push_context_set ~strict:true ctx env + | Polymorphic_const _ -> env + end + in let rec translate_seff sl seff acc env = match sl, seff with | _, [] -> List.rev acc, ce @@ -553,7 +580,7 @@ let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) let translate_local_def mb env id centry = - let def,typ,proj,poly,univs,inline_code,ctx = + let def,typ,proj,univs,inline_code,ctx = infer_declaration ~trust:mb env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1a07bb2fc6..e08f3362db 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -555,7 +555,7 @@ let type_of_projection_constant env (p,u) = let cb = lookup_constant cst env in match cb.const_proj with | Some pb -> - if cb.const_polymorphic then + if Declareops.constant_is_polymorphic cb then Vars.subst_instance_constr u pb.proj_type else pb.proj_type | None -> raise (Invalid_argument "type_of_projection: not a projection") diff --git a/kernel/univ.ml b/kernel/univ.ml index eb45f022e9..8cbb20a051 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1031,7 +1031,13 @@ end type universe_context = UContext.t let hcons_universe_context = UContext.hcons -(** Universe info for inductive types: A context of universe levels +module AUContext = UContext + +type abstract_universe_context = AUContext.t +let hcons_abstract_universe_context = AUContext.hcons + +(** Universe info for cumulative inductive types: + A context of universe levels with universe constraints, representing local universe variables and constraints, together with a context of universe levels with universe constraints, representing conditions for subtyping used @@ -1040,7 +1046,7 @@ let hcons_universe_context = UContext.hcons This data structure maintains the invariant that the context for subtyping constraints is exactly twice as big as the context for universe constraints. *) -module UInfoInd = +module CumulativityInfo = struct type t = universe_context * universe_context @@ -1093,8 +1099,13 @@ struct end -type universe_info_ind = UInfoInd.t -let hcons_universe_info_ind = UInfoInd.hcons +type cumulativity_info = CumulativityInfo.t +let hcons_cumulativity_info = CumulativityInfo.hcons + +module ACumulativityInfo = CumulativityInfo + +type abstract_cumulativity_info = ACumulativityInfo.t +let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons (** A set of universes with universe constraints. We linearize the set to a list after typechecking. @@ -1200,6 +1211,9 @@ let subst_univs_level_constraints subst csts = (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c)) csts Constraint.empty +let subst_univs_level_abstract_universe_context subst (inst, csts) = + inst, subst_univs_level_constraints subst csts + (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe @@ -1272,12 +1286,9 @@ let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) (** Substitute instance inst for ctx in universe constraints and subtyping constraints *) -let instantiate_univ_info_ind (univcst, subtpcst) = +let instantiate_cumulativity_info (univcst, subtpcst) = (instantiate_univ_context univcst, instantiate_univ_context subtpcst) -let instantiate_univ_constraints u (_, csts) = - subst_instance_constraints u csts - let make_instance_subst i = let arr = Instance.to_array i in Array.fold_left_i (fun i acc l -> @@ -1290,16 +1301,22 @@ let make_inverse_instance_subst i = LMap.add (Level.var i) l acc) LMap.empty arr -let abstract_universes poly ctx = +let make_abstract_instance (ctx, _) = + Array.mapi (fun i l -> Level.var i) ctx + +let abstract_universes ctx = let instance = UContext.instance ctx in - if poly then - let subst = make_instance_subst instance in - let cstrs = subst_univs_level_constraints subst - (UContext.constraints ctx) - in - let ctx = UContext.make (instance, cstrs) in - subst, ctx - else empty_level_subst, ctx + let subst = make_instance_subst instance in + let cstrs = subst_univs_level_constraints subst + (UContext.constraints ctx) + in + let ctx = UContext.make (instance, cstrs) in + subst, ctx + +let abstract_cumulativity_info (univcst, substcst) = + let instance, univcst = abstract_universes univcst in + let _, substcst = abstract_universes substcst in + (instance, (univcst, substcst)) (** Pretty-printing *) @@ -1307,7 +1324,11 @@ let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr -let pr_universe_info_ind = UInfoInd.pr +let pr_cumulativity_info = CumulativityInfo.pr + +let pr_abstract_universe_context = AUContext.pr + +let pr_abstract_cumulativity_info = ACumulativityInfo.pr let pr_universe_context_set = ContextSet.pr @@ -1364,3 +1385,12 @@ let subst_instance_constraints = let key = Profile.declare_profile "subst_instance_constraints" in Profile.profile2 key subst_instance_constraints else subst_instance_constraints + +let subst_instance_context = + let subst_instance_context_body inst (inner_inst, inner_constr) = + (inner_inst, subst_instance_constraints inst inner_constr) + in + if Flags.profile then + let key = Profile.declare_profile "subst_instance_constraints" in + Profile.profile2 key subst_instance_context_body + else subst_instance_context_body diff --git a/kernel/univ.mli b/kernel/univ.mli index 53af804488..ecc72701d4 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -315,6 +315,23 @@ end type universe_context = UContext.t +module AUContext : +sig + type t + + val empty : t + + val instance : t -> Instance.t + + val size : t -> int + + (** Keeps the order of the instances *) + val union : t -> t -> t + +end + +type abstract_universe_context = AUContext.t + (** Universe info for inductive types: A context of universe levels with universe constraints, representing local universe variables and constraints, together with a context of universe levels with @@ -324,7 +341,7 @@ type universe_context = UContext.t This data structure maintains the invariant that the context for subtyping constraints is exactly twice as big as the context for universe constraints. *) -module UInfoInd : +module CumulativityInfo : sig type t @@ -347,7 +364,17 @@ sig end -type universe_info_ind = UInfoInd.t +type cumulativity_info = CumulativityInfo.t + +module ACumulativityInfo : +sig + type t + + val univ_context : t -> abstract_universe_context + val subtyp_context : t -> abstract_universe_context +end + +type abstract_cumulativity_info = ACumulativityInfo.t (** Universe contexts (as sets) *) @@ -399,6 +426,8 @@ val is_empty_level_subst : universe_level_subst -> bool val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level val subst_univs_level_universe : universe_level_subst -> universe -> universe val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints +val subst_univs_level_abstract_universe_context : + universe_level_subst -> abstract_universe_context -> abstract_universe_context val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance (** Level to universe substitutions. *) @@ -413,27 +442,31 @@ val subst_univs_constraints : universe_subst_fn -> constraints -> constraints (** Substitution of instances *) val subst_instance_instance : universe_instance -> universe_instance -> universe_instance val subst_instance_universe : universe_instance -> universe -> universe -val subst_instance_constraints : universe_instance -> constraints -> constraints +val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context val make_instance_subst : universe_instance -> universe_level_subst val make_inverse_instance_subst : universe_instance -> universe_level_subst -val abstract_universes : bool -> universe_context -> universe_level_subst * universe_context +val abstract_universes : universe_context -> universe_level_subst * abstract_universe_context + +val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abstract_cumulativity_info + +val make_abstract_instance : abstract_universe_context -> universe_instance (** Get the instantiated graph. *) -val instantiate_univ_context : universe_context -> universe_context +val instantiate_univ_context : abstract_universe_context -> universe_context (** Get the instantiated graphs for both universe constraints and subtyping constraints. *) -val instantiate_univ_info_ind : universe_info_ind -> universe_info_ind - -val instantiate_univ_constraints : universe_instance -> universe_context -> constraints +val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info (** {6 Pretty-printing of universes. } *) val pr_constraint_type : constraint_type -> Pp.std_ppcmds val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds -val pr_universe_info_ind : (Level.t -> Pp.std_ppcmds) -> universe_info_ind -> Pp.std_ppcmds +val pr_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> cumulativity_info -> Pp.std_ppcmds +val pr_abstract_universe_context : (Level.t -> Pp.std_ppcmds) -> abstract_universe_context -> Pp.std_ppcmds +val pr_abstract_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> abstract_cumulativity_info -> Pp.std_ppcmds val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> univ_inconsistency -> Pp.std_ppcmds @@ -447,8 +480,10 @@ val hcons_univ : universe -> universe val hcons_constraints : constraints -> constraints val hcons_universe_set : universe_set -> universe_set val hcons_universe_context : universe_context -> universe_context +val hcons_abstract_universe_context : abstract_universe_context -> abstract_universe_context val hcons_universe_context_set : universe_context_set -> universe_context_set -val hcons_universe_info_ind : universe_info_ind -> universe_info_ind +val hcons_cumulativity_info : cumulativity_info -> cumulativity_info +val hcons_abstract_cumulativity_info : abstract_cumulativity_info -> abstract_cumulativity_info (******) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index fa16622702..0e452621c8 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -88,30 +88,34 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = (* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with | Aind ((mi,i) as ind1) , Aind ind2 -> - if eq_ind ind1 ind2 && compare_stack stk1 stk2 - then - if Environ.polymorphic_ind ind1 env - then - let mib = Environ.lookup_mind mi env in - let ulen = Univ.UContext.size (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in - match stk1 , stk2 with - | [], [] -> assert (Int.equal ulen 0); cu - | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> - assert (ulen <= nargs args1); - assert (ulen <= nargs args2); - let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in - let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in - let u1 = Univ.Instance.of_array u1 in - let u2 = Univ.Instance.of_array u2 in - let cu = convert_instances ~flex:false u1 u2 cu in - conv_arguments env ~from:ulen k args1 args2 - (conv_stack env k stk1' stk2' cu) - | _, _ -> assert false (* Should not happen if problem is well typed *) - else - conv_stack env k stk1 stk2 cu - else raise NotConvertible + if eq_ind ind1 ind2 && compare_stack stk1 stk2 then + if Environ.polymorphic_ind ind1 env then + let mib = Environ.lookup_mind mi env in + let ulen = + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx + | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx + | Declarations.Cumulative_ind cumi -> + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) + in + match stk1 , stk2 with + | [], [] -> assert (Int.equal ulen 0); cu + | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> + assert (ulen <= nargs args1); + assert (ulen <= nargs args2); + let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in + let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in + let u1 = Univ.Instance.of_array u1 in + let u2 = Univ.Instance.of_array u2 in + let cu = convert_instances ~flex:false u1 u2 cu in + conv_arguments env ~from:ulen k args1 args2 + (conv_stack env k stk1' stk2' cu) + | _, _ -> assert false (* Should not happen if problem is well typed *) + else + conv_stack env k stk1 stk2 cu + else raise NotConvertible | Aid ik1, Aid ik2 -> - if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then + if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible | Atype _ , _ | _, Atype _ -> assert false -- cgit v1.2.3 From 49e4acab949da9861adcd37b8511a89c221ae129 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 17:05:52 +0200 Subject: Use a smart map_constr --- kernel/vars.ml | 44 ++++++++++++-------------------------------- 1 file changed, 12 insertions(+), 32 deletions(-) (limited to 'kernel') diff --git a/kernel/vars.ml b/kernel/vars.ml index 629de80f7c..89c17b850e 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -316,38 +316,18 @@ let subst_univs_level_context s = Context.Rel.map (subst_univs_level_constr s) let subst_instance_constr subst c = - if Univ.Instance.is_empty subst then c - else - let f u = Univ.subst_instance_instance subst u in - let changed = ref false in - let rec aux t = - match kind t with - | Const (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; mkConstU (c, u')) - | Ind (i, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; mkIndU (i, u')) - | Construct (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; mkConstructU (c, u')) - | Sort (Sorts.Type u) -> - let u' = Univ.subst_instance_universe subst u in - if u' == u then t else - (changed := true; mkSort (Sorts.sort_of_univ u')) - | _ -> Constr.map aux t - in - let c' = aux c in - if !changed then c' else c + let f u = Univ.subst_instance_instance subst u in + let rec aux t = + match kind t with + | Const (c, u) -> mkConstU (c, f u) + | Ind (i, u) -> mkIndU (i, f u) + | Construct (c, u) -> mkConstructU (c, f u) + | Sort (Sorts.Type u) -> + let u' = Univ.subst_instance_universe subst u in + mkSort (Sorts.sort_of_univ u') + | _ -> Constr.map aux t + in + aux c (* let substkey = Profile.declare_profile "subst_instance_constr";; *) (* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) -- cgit v1.2.3 From ab0c49baa8d57ed92a79e7d0b0737267042210f8 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 17:46:16 +0200 Subject: Optimization Only try using cumulativity in conversion/subtyping if the universe instances are non-empty --- kernel/reduction.ml | 50 +++++++++++++++++++++++++++++--------------------- 1 file changed, 29 insertions(+), 21 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 8bf95e5de9..a9e2ce78c7 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -495,31 +495,39 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd (ind1,u1), FInd (ind2,u2)) -> if eq_ind ind1 ind2 then - let mind = Environ.lookup_mind (fst ind1) env in - let cuniv = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - convert_instances ~flex:false u1 u2 cuniv - | Declarations.Cumulative_ind cumi -> - convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1) - u2 (CClosure.stack_args_size v2) cuniv - in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then + let cuniv = convert_instances ~flex:false u1 u2 cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + else + let mind = Environ.lookup_mind (fst ind1) env in + let cuniv = + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + convert_instances ~flex:false u1 u2 cuniv + | Declarations.Cumulative_ind cumi -> + convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1) + u2 (CClosure.stack_args_size v2) cuniv + in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> if Int.equal j1 j2 && eq_ind ind1 ind2 then - let mind = Environ.lookup_mind (fst ind1) env in - let cuniv = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - convert_instances ~flex:false u1 u2 cuniv - | Declarations.Cumulative_ind _ -> - convert_constructors - (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1) - u2 (CClosure.stack_args_size v2) cuniv - in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then + let cuniv = convert_instances ~flex:false u1 u2 cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + else + let mind = Environ.lookup_mind (fst ind1) env in + let cuniv = + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + convert_instances ~flex:false u1 u2 cuniv + | Declarations.Cumulative_ind _ -> + convert_constructors + (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1) + u2 (CClosure.stack_args_size v2) cuniv + in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Eta expansion of records *) -- cgit v1.2.3 From 5fb30d6c06d47a8e6c4200cdd0ba9067be7cfe2f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Mon, 12 Jun 2017 17:44:29 +0200 Subject: use map_constr more efficiently --- kernel/vars.ml | 42 ++++++++++++++++++++++++++++++------------ 1 file changed, 30 insertions(+), 12 deletions(-) (limited to 'kernel') diff --git a/kernel/vars.ml b/kernel/vars.ml index 89c17b850e..baf8fa31f6 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -316,18 +316,36 @@ let subst_univs_level_context s = Context.Rel.map (subst_univs_level_constr s) let subst_instance_constr subst c = - let f u = Univ.subst_instance_instance subst u in - let rec aux t = - match kind t with - | Const (c, u) -> mkConstU (c, f u) - | Ind (i, u) -> mkIndU (i, f u) - | Construct (c, u) -> mkConstructU (c, f u) - | Sort (Sorts.Type u) -> - let u' = Univ.subst_instance_universe subst u in - mkSort (Sorts.sort_of_univ u') - | _ -> Constr.map aux t - in - aux c + if Univ.Instance.is_empty subst then c + else + let f u = Univ.subst_instance_instance subst u in + let rec aux t = + match kind t with + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkConstU (c, u')) + | Ind (i, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkIndU (i, u')) + | Construct (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkConstructU (c, u')) + | Sort (Sorts.Type u) -> + let u' = Univ.subst_instance_universe subst u in + if u' == u then t else + (mkSort (Sorts.sort_of_univ u')) + | _ -> Constr.map aux t + in + aux c (* let substkey = Profile.declare_profile "subst_instance_constr";; *) (* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) -- cgit v1.2.3 From a4969591f391d857a9efd038338e1a80fc68950b Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 14 Jun 2017 16:32:47 +0200 Subject: A short cleanup --- kernel/declarations.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index f3b7ae2b24..21651b3e21 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -169,7 +169,7 @@ type one_inductive_body = { mind_reloc_tbl : Cbytecodes.reloc_table; } -type abstrac_inductive_universes = +type abstract_inductive_universes = | Monomorphic_ind of Univ.universe_context | Polymorphic_ind of Univ.abstract_universe_context | Cumulative_ind of Univ.abstract_cumulativity_info @@ -192,7 +192,7 @@ type mutual_inductive_body = { mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) - mind_universes : abstrac_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) -- cgit v1.2.3 From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 15 Jun 2017 16:50:05 +0200 Subject: Fix a bug in cumulativity --- kernel/reduction.ml | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a9e2ce78c7..605e9f314c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -679,12 +679,13 @@ let infer_check_conv_constructors infer_check_inductive_instances CONV cumi u1 u2 univs let check_inductive_instances cv_pb cumi u u' univs = - let ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + let length_ind_instance = + Univ.Instance.length + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) in let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && - (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + if not ((length_ind_instance = Univ.Instance.length u) && + (length_ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = @@ -765,13 +766,14 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = in (univs, cstrs') let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = - let ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.subtyp_context cumi) + let length_ind_instance = + Univ.Instance.length + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) in let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && - (Univ.Instance.length ind_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") + if not ((length_ind_instance = Univ.Instance.length u) && + (length_ind_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = let comp_subst = (Univ.Instance.append u u') in -- cgit v1.2.3