diff options
Diffstat (limited to 'kernel')
86 files changed, 1031 insertions, 626 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 8bd4b5bfe1..7e193ef829 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 69a5e79b45..9e5cb48a49 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 94ca4c72dd..25f61c7aa9 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index b8de7619cf..8f38e9d34e 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 57b397e6f8..d63fcffa2c 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/cemitcodes.ml b/kernel/cemitcodes.ml index 40c1e027d4..092bcecc38 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/constr.ml b/kernel/constr.ml index eecceb32a7..c3e6095363 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/constr.mli b/kernel/constr.mli index e0954160f9..76dbf55309 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/context.ml b/kernel/context.ml index abb284f226..929324efec 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/context.mli b/kernel/context.mli index 24e69ebd6e..c3ecd8d4ea 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 4533169804..ca568fc6ec 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 70f02b54d7..248cd2b30e 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4deadff0a7..95822fac68 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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,22 @@ 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 len = Univ.LMap.cardinal subst in + let rec gen_subst i acc = + if i < 0 then acc + else + let acc = Univ.LMap.add (Level.var i) (Level.var (i + len)) acc in + gen_subst (pred i) acc + in + let subst = gen_subst (Univ.AUContext.size auctx - 1) subst 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 +247,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 -> + assert (AUContext.is_empty abs_ctx); univs + | 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..79a028d760 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/csymtable.ml b/kernel/csymtable.ml index 40595f944c..d21ea9670f 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index cd561148bf..633cf0abdd 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 71e228b19c..f35438dfc4 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 abstract_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,9 +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_universes : Univ.universe_context; (** Local universe variables and constraints *) + 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 *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 0a822d6fad..efce219826 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -44,50 +44,20 @@ 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 - -let body_of_constant otab cb = match cb.const_body with - | Undef _ -> None - | Def c -> Some (instantiate cb (force_constr c)) - | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o)) - -let type_of_constant cb = - match cb.const_type with - | RegularArity t as x -> - let t' = instantiate cb t in - 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 universes_of_constant otab cb = - match cb.const_body with - | Undef _ | Def _ -> cb.const_universes - | 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 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 +let constant_is_polymorphic cb = + match cb.const_universes with + | Monomorphic_const _ -> false + | Polymorphic_const _ -> true let constant_has_body cb = match cb.const_body with | Undef _ -> false | Def _ | OpaqueDef _ -> true +let constant_polymorphic_context cb = + match cb.const_universes with + | Monomorphic_const _ -> Univ.AUContext.empty + | Polymorphic_const ctx -> ctx + let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Undef _ | Def _ -> false @@ -135,7 +105,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 } @@ -166,11 +135,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 } *) @@ -259,21 +235,28 @@ 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_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 mib.mind_universes - else Univ.Instance.empty +let inductive_polymorphic_context mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.AUContext.empty + | Polymorphic_ind ctx -> ctx + | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi -let inductive_context mib = - if mib.mind_polymorphic then - Univ.instantiate_univ_context mib.mind_universes - else Univ.UContext.empty +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 } *) @@ -301,11 +284,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_context 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..a8ba5fa392 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -27,23 +27,14 @@ val subst_const_body : substitution -> constant_body -> constant_body val constant_has_body : 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. *) +val constant_polymorphic_context : constant_body -> abstract_universe_context -val body_of_constant : - Opaqueproof.opaquetab -> constant_body -> Term.constr option -val type_of_constant : constant_body -> constant_type -val constraints_of_constant : - Opaqueproof.opaquetab -> constant_body -> Univ.constraints -val universes_of_constant : - Opaqueproof.opaquetab -> constant_body -> Univ.universe_context +(** Is the constant polymorphic? *) +val constant_is_polymorphic : constant_body -> bool (** Return the universe context, in case the definition is polymorphic, otherwise the context is empty. *) -val universes_of_polymorphic_constant : - Opaqueproof.opaquetab -> constant_body -> Univ.universe_context - val is_opaque : constant_body -> bool (** Side effects *) @@ -66,8 +57,12 @@ 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_context : mutual_inductive_body -> abstract_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.ml index 1e07c96909..3fa25c142a 100644 --- a/kernel/entries.mli +++ b/kernel/entries.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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,8 +54,9 @@ 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_universes : Univ.universe_context; + 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..b01b652001 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -228,8 +228,9 @@ 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.AUContext.instantiate u ctx let map_regular_arity f = function | RegularArity a as ar -> @@ -240,15 +241,17 @@ 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_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.AUContext.empty + | Polymorphic_const ctx -> ctx type const_evaluation_result = NoBody | Opaque | IsProj @@ -259,10 +262,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 +280,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 +302,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 +328,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 +360,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..cd7a9d2791 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -160,7 +160,7 @@ val constant_value_and_type : env -> constant puniverses -> constr option * constant_type * Univ.constraints (** The universe context associated to the constant, empty if not polymorphic *) -val constant_context : env -> constant -> Univ.universe_context +val constant_context : env -> constant -> Univ.abstract_universe_context (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant @@ -256,7 +256,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/esubst.ml b/kernel/esubst.ml index 1dc389c649..ac2b3f9d59 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/esubst.mli b/kernel/esubst.mli index 533d1c68c3..95a2e71c2c 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/evar.ml b/kernel/evar.ml index b972fc1147..e63665f519 100644 --- a/kernel/evar.ml +++ b/kernel/evar.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/evar.mli b/kernel/evar.mli index f28a13640f..eee6680fb8 100644 --- a/kernel/evar.mli +++ b/kernel/evar.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1e13239bfc..e248436ec4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -207,6 +207,50 @@ 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) 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') -> + 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 cumi paramsctxt env_ar inds = + let numparams = Context.Rel.nhyps paramsctxt in + let sbsubst = CumulativityInfo.subtyping_susbst cumi in + let dosubst = subst_univs_level_constr sbsubst 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 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 env dosubst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor env 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 @@ -220,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 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 *) @@ -339,12 +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 () = + 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) (************************************************************************) @@ -816,23 +875,31 @@ 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 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 subst, ctx = Univ.abstract_universes p ctx in - let paramsctxt = Vars.subst_univs_level_context subst 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 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 + 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 = @@ -851,8 +918,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 +938,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; @@ -893,10 +960,11 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm && 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 subst (Univ.UContext.instance ctx) - else Univ.Instance.empty + let u = + match aiu with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx + | Cumulative_ind acumi -> Univ.make_abstract_instance (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 @@ -919,8 +987,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_nparams_rec = nmr; mind_params_ctxt = paramsctxt; mind_packets = packets; - mind_polymorphic = p; - mind_universes = ctx; + mind_universes = aiu; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -935,7 +1002,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_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 5b4615399d..e4b7c086af 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f3b03252db..1eaba49aa9 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -54,9 +54,11 @@ 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 mib.mind_universes) - else Univ.Constraint.empty + let process auctx = Univ.AUContext.instantiate 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/inductive.mli b/kernel/inductive.mli index 521ee3c7b7..0dfa8db00e 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 2f49982ce2..9946348541 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -13,9 +13,11 @@ Mod_subst Cbytecodes Copcodes Cemitcodes +Opaqueproof +Declarations +Entries Nativevalues Primitives -Opaqueproof Declareops Retroknowledge Conv_oracle @@ -42,4 +44,3 @@ Safe_typing Vm Csymtable Vconv -Declarations diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 95990bea6a..7b660939b5 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 6d86b94167..3cd02fb9f8 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index ff44f0f540..c7f3e5c51b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -72,15 +72,13 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = (* In the spirit of subtyping.check_constant, we accept any implementations of parameters and opaques terms, as long as they have the right type *) - let uctx = Declareops.universes_of_constant (opaque_tables env) cb in - let uctx = (* Context of the spec *) - if cb.const_polymorphic then - Univ.instantiate_univ_context uctx - else uctx - in - let c', univs, ctx' = - if not cb.const_polymorphic then - let env' = Environ.push_context ~strict:true uctx env' in + let c', univs, ctx' = + match cb.const_universes with + | Monomorphic_const _ -> + (** We do not add the deferred constraints of the body in the + environment, because they do not appear in the type of the + definition. Any inconsistency will be raised at a later stage + when joining the environment. *) let env' = Environ.push_context ~strict:true ctx env' in let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> @@ -92,51 +90,40 @@ 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) - else - let cus, ccst = Univ.UContext.dest uctx in - let newus, cst = Univ.UContext.dest ctx in - let () = - if not (Univ.Instance.length cus == Univ.Instance.length newus) then - error_incorrect_with_constraint lab - in - let inst = Univ.Instance.append cus newus in - let csti = Univ.enforce_eq_instances cus newus cst in - let csta = Univ.Constraint.union csti ccst in - let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in - let () = if not (UGraph.check_constraints cst (Environ.universes env')) then - error_incorrect_with_constraint lab - in + in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) + | Polymorphic_const uctx -> + let subst, ctx = Univ.abstract_universes ctx in + let c = Vars.subst_univs_level_constr subst c in + let () = + if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then + error_incorrect_with_constraint lab + in + (** Terms are compared in a context with De Bruijn universe indices *) + let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env in let cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in let typ = Typeops.type_of_constant_type env' cb.const_type in - let typ = Vars.subst_instance_constr cus typ in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in cst' | Def cs -> - let c' = Vars.subst_instance_constr cus (Mod_subst.force_constr cs) in + let c' = Mod_subst.force_constr cs in let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in cst' 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 + 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/mod_typing.mli b/kernel/mod_typing.mli index 5949dad08c..dcabb13346 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 1f8b97ae6a..a079bc8931 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 @@ -48,7 +49,7 @@ type signature_mismatch_error = | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types - | IncompatibleConstraints of Univ.constraints + | IncompatibleConstraints of Univ.AUContext.t type module_typing_error = | SignatureMismatch of @@ -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..e2a94b6919 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 @@ -107,7 +108,7 @@ type signature_mismatch_error = | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types - | IncompatibleConstraints of Univ.constraints + | IncompatibleConstraints of Univ.AUContext.t type module_typing_error = | SignatureMismatch of diff --git a/kernel/names.ml b/kernel/names.ml index d7c0a5e980..e524f4258d 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/names.mli b/kernel/names.mli index 004d52d4b3..74d63c0cea 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d3cd6b62a5..da7fcd6f23 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -48,9 +48,9 @@ let fresh_lname n = (** Global names **) type gname = - | Gind of string * pinductive (* prefix, inductive name *) - | Gconstruct of string * pconstructor (* prefix, constructor name *) - | Gconstant of string * pconstant (* prefix, constant name *) + | Gind of string * inductive (* prefix, inductive name *) + | Gconstruct of string * constructor (* prefix, constructor name *) + | Gconstant of string * constant (* prefix, constant name *) | Gproj of string * constant (* prefix, constant name *) | Gcase of label option * int | Gpred of label option * int @@ -64,11 +64,11 @@ type gname = let eq_gname gn1 gn2 = match gn1, gn2 with | Gind (s1, ind1), Gind (s2, ind2) -> - String.equal s1 s2 && Univ.eq_puniverses eq_ind ind1 ind2 + String.equal s1 s2 && eq_ind ind1 ind2 | Gconstruct (s1, c1), Gconstruct (s2, c2) -> - String.equal s1 s2 && Univ.eq_puniverses eq_constructor c1 c2 + String.equal s1 s2 && eq_constructor c1 c2 | Gconstant (s1, c1), Gconstant (s2, c2) -> - String.equal s1 s2 && Univ.eq_puniverses Constant.equal c1 c2 + String.equal s1 s2 && Constant.equal c1 c2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -92,12 +92,12 @@ let dummy_gname = open Hashset.Combine let gname_hash gn = match gn with -| Gind (s, (ind,u)) -> - combinesmall 1 (combine3 (String.hash s) (ind_hash ind) (Univ.Instance.hash u)) -| Gconstruct (s, (c,u)) -> - combinesmall 2 (combine3 (String.hash s) (constructor_hash c) (Univ.Instance.hash u)) -| Gconstant (s, (c,u)) -> - combinesmall 3 (combine3 (String.hash s) (Constant.hash c) (Univ.Instance.hash u)) +| Gind (s, ind) -> + combinesmall 1 (combine (String.hash s) (ind_hash ind)) +| Gconstruct (s, c) -> + combinesmall 2 (combine (String.hash s) (constructor_hash c)) +| Gconstant (s, c) -> + combinesmall 3 (combine (String.hash s) (Constant.hash c)) | Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i)) | Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i)) | Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i)) @@ -1068,9 +1068,9 @@ let ml_of_instance instance u = MLlet(lname,def,body) | Lapp(f,args) -> MLapp(ml_of_lam env l f, Array.map (ml_of_lam env l) args) - | Lconst (prefix,c) -> - let args = ml_of_instance env.env_univ (snd c) in - mkMLapp (MLglobal(Gconstant (prefix,c))) args + | Lconst (prefix, (c, u)) -> + let args = ml_of_instance env.env_univ u in + mkMLapp (MLglobal(Gconstant (prefix, c))) args | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c)) | Lprim _ -> let decl,cond,paux = extract_prim (ml_of_lam env l) t in @@ -1281,17 +1281,17 @@ let ml_of_instance instance u = MLconstruct(prefix,cn,args) | Lconstruct (prefix, (cn,u)) -> let uargs = ml_of_instance env.env_univ u in - mkMLapp (MLglobal (Gconstruct (prefix, (cn,u)))) uargs + mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs | Luint v -> (match v with | UintVal i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) | UintDigits (prefix,cn,ds) -> - let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in + let c = MLglobal (Gconstruct (prefix, cn)) in let ds = Array.map (ml_of_lam env l) ds in let i31 = MLapp (MLprimitive Mk_I31_accu, [|c|]) in MLapp(i31, ds) | UintDecomp (prefix,cn,t) -> - let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in + let c = MLglobal (Gconstruct (prefix, cn)) in let t = ml_of_lam env l t in MLapp (MLprimitive Decomp_uint, [|c;t|])) | Lval v -> @@ -1304,9 +1304,9 @@ let ml_of_instance instance u = in let uarg = MLapp(MLprimitive MLmagic, [|uarg|]) in MLapp(MLprimitive Mk_sort, [|get_sort_code i; uarg|]) - | Lind (prefix, pind) -> - let uargs = ml_of_instance env.env_univ (snd pind) in - mkMLapp (MLglobal (Gind (prefix, pind))) uargs + | Lind (prefix, (ind, u)) -> + let uargs = ml_of_instance env.env_univ u in + mkMLapp (MLglobal (Gind (prefix, ind))) uargs | Llazy -> MLglobal (Ginternal "lazy") | Lforce -> MLglobal (Ginternal "Lazy.force") @@ -1539,11 +1539,11 @@ let string_of_mind mind = string_of_kn (user_mind mind) let string_of_gname g = match g with - | Gind (prefix, ((mind,i), _)) -> + | Gind (prefix, (mind, i)) -> Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i - | Gconstruct (prefix, (((mind, i), j), _)) -> + | Gconstruct (prefix, ((mind, i), j)) -> Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1) - | Gconstant (prefix, (c,_)) -> + | Gconstant (prefix, c) -> Format.sprintf "%sconst_%s" prefix (string_of_con c) | Gproj (prefix, c) -> Format.sprintf "%sproj_%s" prefix (string_of_con c) @@ -1754,9 +1754,8 @@ let pp_mllam fmt l = | Coq_primitive (op,None) -> Format.fprintf fmt "no_check_%s" (Primitives.to_string op) | Coq_primitive (op, Some (prefix,kn)) -> - let u = Univ.Instance.empty in Format.fprintf fmt "%s %a" (Primitives.to_string op) - pp_mllam (MLglobal (Gconstant (prefix,(kn,u)))) + pp_mllam (MLglobal (Gconstant (prefix, kn))) in Format.fprintf fmt "@[%a@]" pp_mllam l @@ -1862,9 +1861,10 @@ and compile_named env sigma univ auxdefs id = 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 + let no_univs = + match cb.const_universes with + | Monomorphic_const _ -> true + | Polymorphic_const ctx -> Int.equal (Univ.AUContext.size ctx) 0 in begin match cb.const_body with | Def t -> @@ -1879,7 +1879,7 @@ let compile_constant env sigma prefix ~interactive con cb = in let l = con_label con in let auxdefs,code = - if Univ.Instance.is_empty u then compile_with_fv env sigma None [] (Some l) code + if no_univs then compile_with_fv env sigma None [] (Some l) code else let univ = fresh_univ () in let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in @@ -1887,25 +1887,24 @@ let compile_constant env sigma prefix ~interactive con cb = in if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code"); let code = - optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs) + optimize_stk (Glet(Gconstant ("", con),code)::auxdefs) in if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code"); code, name | _ -> let i = push_symbol (SymbConst con) in let args = - if Univ.Instance.is_empty u then [|get_const_code i; MLarray [||]|] + if no_univs then [|get_const_code i; MLarray [||]|] else [|get_const_code i|] in (* let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const) *) - [Glet(Gconstant ("",(con,u)), mkMLapp (MLprimitive Mk_const) args)], + [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)], if interactive then LinkedInteractive prefix else Linked prefix end | Some pb -> - let u = Univ.Instance.empty in let mind = pb.proj_ind in let ind = (mind,0) in let mib = lookup_mind mind env in @@ -1932,7 +1931,7 @@ let compile_constant env sigma prefix ~interactive con cb = let gn = Gproj ("",con) in let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in let arg = fargs.(pb.proj_npars) in - Glet(Gconstant ("",(con,u)), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal + Glet(Gconstant ("", con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal arg|]))):: [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix @@ -1960,14 +1959,14 @@ 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_context 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 - let name = Gind ("", ((mind, i), u)) in + let name = Gind ("", (mind, i)) in let accu = let args = - if Univ.Instance.is_empty u then + if Int.equal (Univ.AUContext.size u) 0 then [|get_ind_code j; MLarray [||]|] else [|get_ind_code j|] in @@ -1979,7 +1978,7 @@ let compile_mind prefix ~interactive mb mind stack = let add_construct j acc (_,arity) = let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in let c = (mind,i), (j+1) in - Glet(Gconstruct ("",(c,u)), + Glet(Gconstruct ("", c), mkMLlam (Array.append params args) (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 77d9c33f8d..ae6fb1bd6b 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index fe9f393f63..d2f050d3bc 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 63b1eb0586..fbbcce7449 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 41e79a5355..cb79877e8b 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 72d9c48513..508112b35d 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index c33574408b..bfa3bf9418 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index f6c94158f8..02e02b031a 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 12ad3cf2f7..e8b51dc366 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 246b00da40..3e273dde20 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index 7d01640b29..f327ba224a 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 7ffb48221b..7463a30feb 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index f4396659ec..49b1e122d5 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 59e90ca2e9..5e20c1b514 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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..a0418a022f 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/pre_env.ml b/kernel/pre_env.ml index 48d7ee9ec3..7b4fb4e869 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 866790367d..f2a009b868 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/primitives.ml b/kernel/primitives.ml index 27732c00cb..14c11bf107 100644 --- a/kernel/primitives.ml +++ b/kernel/primitives.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/primitives.mli b/kernel/primitives.mli index 86e86a5e5a..8cdffb6702 100644 --- a/kernel/primitives.mli +++ b/kernel/primitives.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b6786c045c..2bf9f43a5a 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -191,6 +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; + 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 @@ -206,6 +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 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 @@ -299,11 +309,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 +338,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 +352,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 +379,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 +387,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 +434,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 +452,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,66 +461,88 @@ 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) (* Inductive types: MutInd MutConstruct Fix Cofix *) - | (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) - else raise NotConvertible + if eq_ind ind1 ind2 then + 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 cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) - else raise NotConvertible + if Int.equal j1 j2 && eq_ind ind1 ind2 then + 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 *) | (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) | (_, 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 +553,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 +568,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 +583,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 +597,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 +605,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 +642,85 @@ let check_convert_instances ~flex u u' univs = if UGraph.check_eq_instances univs u u' then univs else raise NotConvertible +(* 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 = + 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 + 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 = + 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 + (* 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 + infer_check_inductive_instances CONV cumi u1 u2 univs + +let check_inductive_instances cv_pb cumi u u' univs = + let length_ind_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) + in + let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in + 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 + Univ.AUContext.instantiate comp_subst ind_subtypctx + in + let comp_cst = + match cv_pb with + CONV -> + let comp_cst' = + let comp_subst = (Univ.Instance.append u' u) in + Univ.AUContext.instantiate comp_subst ind_subtypctx + 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 } + compare_instances = check_convert_instances; + 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 @@ -647,11 +755,56 @@ 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_inductive_instances cv_pb cumi u u' (univs, cstrs) = + let length_ind_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) + in + let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in + 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 + Univ.AUContext.instantiate comp_subst ind_subtypctx + in + let comp_cst = + match cv_pb with + CONV -> + let comp_cst' = + let comp_subst = (Univ.Instance.append u' u) in + Univ.AUContext.instantiate comp_subst ind_subtypctx + 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 } + compare_instances = infer_convert_instances; + 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 8a2b2469d6..253c0874f2 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -36,10 +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; + 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 diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index ea53d00d7b..5fbd914f3f 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 905a05fe53..18a12a4ef1 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f5e8e86530..ed4c7d57ad 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 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/safe_typing.mli b/kernel/safe_typing.mli index efeb98bd25..5bb8ceb1a5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 62013b38f1..cf5207e8dc 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/sorts.mli b/kernel/sorts.mli index eb4697ad6d..3426d6fd3c 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index f779f68be4..bd82dd465b 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -80,16 +80,23 @@ let make_labmap mp list = List.fold_right add_one list empty_labmap -let check_conv_error error why cst poly u f env a1 a2 = +let check_conv_error error why cst poly f env a1 a2 = try - let a1 = Vars.subst_instance_constr u a1 in - let a2 = Vars.subst_instance_constr u a2 in let cst' = f env (Environ.universes env) a1 a2 in if poly then if Constraint.is_empty cst' then cst else error (IncompatiblePolymorphism (env, a1, a2)) else Constraint.union cst cst' with NotConvertible -> error why + | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e) + +let check_polymorphic_instance error env auctx1 auctx2 = + if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then + error IncompatibleInstances + else if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then + error (IncompatibleConstraints auctx1) + else + Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env (* for now we do not allow reorderings *) @@ -97,24 +104,28 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let kn1 = KerName.make2 mp1 l in let kn2 = KerName.make2 mp2 l in let error why = error_signature_mismatch l spec2 why in - let check_conv why cst poly u f = check_conv_error error why cst poly u f in + let check_conv why cst poly f = check_conv_error error why cst poly f in let mib1 = match info1 with | 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 env, inst = + match mib1.mind_universes, mib2.mind_universes with + | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty + | Polymorphic_ind auctx, Polymorphic_ind auctx' -> + let env = check_polymorphic_instance error env auctx auctx' in + env, Univ.make_abstract_instance auctx' + | Cumulative_ind cumi, Cumulative_ind cumi' -> + let auctx = Univ.ACumulativityInfo.univ_context cumi in + let auctx' = Univ.ACumulativityInfo.univ_context cumi' in + let env = check_polymorphic_instance error env auctx auctx' in + env, Univ.make_abstract_instance auctx' + | _ -> 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 = + let check_inductive_type cst name t1 t2 = (* Due to template polymorphism, the conclusions of t1 and t2, if in Type, are generated as the least upper bounds @@ -147,7 +158,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) infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) in let check_packet cst p1 p2 = @@ -165,21 +176,20 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* nparams done *) (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let ty1, cst1 = constrained_type_of_inductive env ((mib1,p1),u) in - let ty2, cst2 = constrained_type_of_inductive env ((mib2,p2),u) in - let cst = Constraint.union cst1 (Constraint.union cst2 cst) in - let cst = check_inductive_type cst p2.mind_typename env ty1 ty2 in + let ty1 = type_of_inductive env ((mib1, p1), inst) in + let ty2 = type_of_inductive env ((mib2, p2), inst) in + let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in cst in let mind = mind_of_kn kn1 in 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) infer_conv env t1 t2) cst p2.mind_consnames - (arities_of_specif (mind,u) (mib1,p1)) - (arities_of_specif (mind,u) (mib2,p2)) + (arities_of_specif (mind, inst) (mib1, p1)) + (arities_of_specif (mind, inst) (mib2, p2)) in let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x); @@ -235,8 +245,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error why = error_signature_mismatch l spec2 why in - let check_conv cst poly u f = check_conv_error error cst poly u f in - let check_type poly u cst env t1 t2 = + let check_conv cst poly f = check_conv_error error cst poly f in + let check_type poly cst env t1 t2 = let err = NotConvertibleTypeField (env, t1, t2) in @@ -283,7 +293,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = t1,t2 else (t1,t2) in - check_conv err cst poly u infer_conv_leq env t1 t2 + check_conv err cst poly infer_conv_leq env t1 t2 in match info1 with | Constant cb1 -> @@ -291,43 +301,21 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let cb1 = Declareops.subst_const_body subst1 cb1 in 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 - 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 - 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 + let poly, env = + match cb1.const_universes, cb2.const_universes with + | Monomorphic_const _, Monomorphic_const _ -> + false, env + | Polymorphic_const auctx1, Polymorphic_const auctx2 -> + true, check_polymorphic_instance error env auctx1 auctx2 + | Monomorphic_const _, Polymorphic_const _ -> + error (PolymorphicStatusExpected true) + | Polymorphic_const _, Monomorphic_const _ -> + error (PolymorphicStatusExpected false) in (* Now check types *) - let typ1 = Typeops.type_of_constant_type env' cb1.const_type in - let typ2 = Typeops.type_of_constant_type env' cb2.const_type in - let cst = check_type poly u cst env' typ1 typ2 in + let typ1 = Typeops.type_of_constant_type env cb1.const_type in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + let cst = check_type poly cst env typ1 typ2 in (* Now we check the bodies: - A transparent constant can only be implemented by a compatible transparent constant. @@ -344,40 +332,19 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = Anyway [check_conv] will handle that afterwards. *) let c1 = Mod_subst.force_constr lc1 in let c2 = Mod_subst.force_constr lc2 in - check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2)) + check_conv NotConvertibleBodyField cst poly infer_conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (CErrors.user_err Pp.(str @@ + CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ - "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 arity1,cst1 = constrained_type_of_inductive env - ((mind1,mind1.mind_packets.(i)),u1) in - let cst2 = - Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in - let typ2 = Typeops.type_of_constant_type env cb2.const_type in - let cst = Constraint.union cst (Constraint.union cst1 cst2) in - let error = NotConvertibleTypeField (env, arity1, typ2) in - check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2 - | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (CErrors.user_err Pp.(str @@ + "name.") + | IndConstr (((kn,i),j),mind1) -> + CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ - "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 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 - let ty2 = Typeops.type_of_constant_type env cb2.const_type in - let cst = Constraint.union cst (Constraint.union cst1 cst2) in - let error = NotConvertibleTypeField (env, ty1, ty2) in - check_conv error cst false Univ.Instance.empty infer_conv env ty1 ty2 + "name.") let rec check_modules cst env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module msb1 in diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index a00eb87329..b24c20aa02 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,5 +11,3 @@ open Declarations open Environ val check_subtypes : env -> module_type_body -> module_type_body -> constraints - - diff --git a/kernel/term.ml b/kernel/term.ml index b90718358e..0e0af2f59d 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/term.mli b/kernel/term.mli index e729439f01..d5aaf6ad06 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index bdfd00a8d3..cf82d54ec1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -121,18 +121,18 @@ 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 subst = Cmap_env.add c (Inl b) 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 *) @@ -141,7 +141,7 @@ let inline_side_effects env body ctx side_eff = let data = try Some (Cmap_env.find c subst) with Not_found -> None in begin match data with | None -> t - | Some (Inl (inst, b)) -> + | Some (Inl b) -> (** [b] is closed but may refer to other constants *) subst_const i k (Vars.subst_instance_constr u b) | Some (Inr n) -> @@ -225,16 +225,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. @@ -256,17 +265,14 @@ let infer_declaration ~trust env kn dcl = let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in unzip ectx j in - let subst = Univ.LMap.empty in let _ = judge_of_cast env j DEFAULTcast tyj in - assert (eq_constr typ tyj.utj_val); let c = hcons_constr j.uj_val in - let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in 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 +285,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 -> @@ -289,7 +296,6 @@ let infer_declaration ~trust env kn dcl = | Some t -> let tj = infer_type env t in let _ = judge_of_cast env j DEFAULTcast tj in - assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr usubst t) in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in @@ -298,8 +304,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 +316,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, 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 +349,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 +421,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 +436,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 +450,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 +461,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.AUContext.repr auctx + in let pt = match cb.const_body, u with | OpaqueDef _, `Opaque (b, c) -> b, c @@ -463,8 +478,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 +523,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 +575,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/term_typing.mli b/kernel/term_typing.mli index 075389ea53..77d126074f 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 5e17638152..bbaf569d39 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index bd6032716f..1b2ccf8f82 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1a07bb2fc6..b814deb6eb 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/typeops.mli b/kernel/typeops.mli index 007acae604..24521070e2 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 487257a776..9793dd881d 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -830,6 +830,18 @@ let sort_universes g = in normalize_universes g +(** Subtyping of polymorphic contexts *) + +let check_subtype univs ctxT ctx = + if AUContext.size ctx == AUContext.size ctx then + let (inst, cst) = UContext.dest (AUContext.repr ctx) in + let cstT = UContext.constraints (AUContext.repr ctxT) in + let push accu v = add_universe v false accu in + let univs = Array.fold_left push univs (Instance.to_array inst) in + let univs = merge_constraints cstT univs in + check_constraints cst univs + else false + (** Instances *) let check_eq_instances g t1 t2 = diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 935a3cab4a..4de373eb4c 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -53,6 +53,10 @@ val check_constraints : constraints -> universes -> bool val check_eq_instances : Instance.t check_function (** Check equality of instances w.r.t. a universe graph *) +val check_subtype : AUContext.t check_function +(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of + [ctx1]. *) + (** {6 Pretty-printing of universes. } *) val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds diff --git a/kernel/univ.ml b/kernel/univ.ml index d53dd8e733..02b02db893 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 @@ -985,6 +988,31 @@ let enforce_eq_instances x y = (Pp.str " instances of different lengths.")); CArray.fold_right2 enforce_eq_level ax ay +let subst_instance_level s l = + match l.Level.data with + | Level.Var n -> s.(n) + | _ -> l + +let subst_instance_instance s i = + Array.smartmap (fun l -> subst_instance_level s l) i + +let subst_instance_universe s u = + let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in + let u' = Universe.smartmap f u in + if u == u' then u + else Universe.sort u' + +let subst_instance_constraint s (u,d,v as c) = + let u' = subst_instance_level s u in + let v' = subst_instance_level s v in + if u' == u && v' == v then c + else (u',d,v') + +let subst_instance_constraints s csts = + Constraint.fold + (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) + csts Constraint.empty + type universe_instance = Instance.t type 'a puniverses = 'a * Instance.t @@ -1028,6 +1056,93 @@ end type universe_context = UContext.t let hcons_universe_context = UContext.hcons +module AUContext = +struct + include UContext + + let repr (inst, cst) = + (Array.mapi (fun i l -> Level.var i) inst, cst) + + let instantiate inst (u, cst) = + assert (Array.length u = Array.length inst); + subst_instance_constraints inst cst + +end + +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 + 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 CumulativityInfo = +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 = + 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 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) ++ 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) + + 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)) + + 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' + +end + +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. Beware, representation could change. @@ -1132,6 +1247,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 @@ -1174,38 +1292,6 @@ let subst_univs_constraints subst csts = (fun c cstrs -> subst_univs_constraint subst c cstrs) csts Constraint.empty -let subst_instance_level s l = - match l.Level.data with - | Level.Var n -> s.(n) - | _ -> l - -let subst_instance_instance s i = - Array.smartmap (fun l -> subst_instance_level s l) i - -let subst_instance_universe s u = - let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in - let u' = Universe.smartmap f u in - if u == u' then u - else Universe.sort u' - -let subst_instance_constraint s (u,d,v as c) = - let u' = subst_instance_level s u in - let v' = subst_instance_level s v in - if u' == u && v' == v then c - else (u',d,v') - -let subst_instance_constraints s csts = - Constraint.fold - (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) - csts Constraint.empty - -(** Substitute instance inst for ctx in csts *) -let instantiate_univ_context (ctx, csts) = - (ctx, subst_instance_constraints ctx csts) - -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 -> @@ -1218,16 +1304,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 *) @@ -1235,6 +1327,12 @@ let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.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 let pr_universe_subst = @@ -1283,10 +1381,3 @@ let explain_universe_inconsistency prl (o,u,v,p) = let compare_levels = Level.compare let eq_levels = Level.equal let equal_universes = Universe.equal - - -let subst_instance_constraints = - if Flags.profile then - let key = Profile.declare_profile "subst_instance_constraints" in - Profile.profile2 key subst_instance_constraints - else subst_instance_constraints diff --git a/kernel/univ.mli b/kernel/univ.mli index 1ccdebd501..99092a543e 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -315,6 +315,76 @@ end type universe_context = UContext.t +module AUContext : +sig + type t + + val repr : t -> UContext.t + (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of + the context and [cstr] the abstracted constraints. *) + + val empty : t + val is_empty : t -> bool + + (** Don't use. *) + val instance : t -> Instance.t + + val size : t -> int + + (** Keeps the order of the instances *) + val union : t -> t -> t + + val instantiate : Instance.t -> t -> Constraint.t + (** Generate the set of instantiated constraints **) + +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 + 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 CumulativityInfo : +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 + + (** 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 + + val subtyping_susbst : t -> universe_level_subst + +end + +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) *) module ContextSet : @@ -365,6 +435,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. *) @@ -379,23 +451,24 @@ 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 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 -(** Get the instantiated graph. *) -val instantiate_univ_context : universe_context -> universe_context +val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abstract_cumulativity_info -val instantiate_univ_constraints : universe_instance -> universe_context -> constraints +val make_abstract_instance : abstract_universe_context -> universe_instance (** {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_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 @@ -409,7 +482,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_cumulativity_info : cumulativity_info -> cumulativity_info +val hcons_abstract_cumulativity_info : abstract_cumulativity_info -> abstract_cumulativity_info (******) @@ -419,3 +495,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/vars.ml b/kernel/vars.ml index 629de80f7c..d0dad02ece 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -319,35 +319,33 @@ 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 = + 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')) + | 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 (changed := true; mkIndU (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 (changed := true; mkConstructU (c, u')) - | Sort (Sorts.Type 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 - (changed := true; mkSort (Sorts.sort_of_univ u')) + if u' == u then t else + (mkSort (Sorts.sort_of_univ u')) | _ -> Constr.map aux t in - let c' = aux c in - if !changed then c' else c + aux c (* let substkey = Profile.declare_profile "subst_instance_constr";; *) (* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) diff --git a/kernel/vars.mli b/kernel/vars.mli index df5c55118f..59dc09a75d 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 74d956bef0..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 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 diff --git a/kernel/vconv.mli b/kernel/vconv.mli index ff01735c0b..f4e680c690 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/vm.ml b/kernel/vm.ml index 21c1225cc4..6b7a86d6f9 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |