diff options
Diffstat (limited to 'kernel')
87 files changed, 1374 insertions, 978 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/primitives.ml b/kernel/cPrimitives.ml index 27732c00cb..14c11bf107 100644 --- a/kernel/primitives.ml +++ b/kernel/cPrimitives.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/cPrimitives.mli index 86e86a5e5a..8cdffb6702 100644 --- a/kernel/primitives.mli +++ b/kernel/cPrimitives.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..718917ab35 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 *) @@ -34,7 +34,7 @@ type structured_constant = | Const_univ_level of Univ.universe_level | Const_type of Univ.universe -val pp_struct_const : structured_constant -> Pp.std_ppcmds +val pp_struct_const : structured_constant -> Pp.t type reloc_table = (tag * int) array @@ -163,8 +163,8 @@ type comp_env = { in_env : vm_env ref (** the variables that are accessed *) } -val pp_bytecodes : bytecodes -> Pp.std_ppcmds -val pp_fv_elem : fv_elem -> Pp.std_ppcmds +val pp_bytecodes : bytecodes -> Pp.t +val pp_fv_elem : fv_elem -> Pp.t (*spiwack: moved this here because I needed it for retroknowledge *) type block = 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..80d41847cd 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 *) @@ -18,7 +18,6 @@ open Util open Names open Term open Declarations -open Environ open Univ module NamedDecl = Context.Named.Declaration @@ -151,10 +150,14 @@ let abstract_constant_body = type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = - constant_def * constant_type * projection_body option * - bool * constant_universes * inline - * Context.Named.t option +type result = { + cook_body : constant_def; + cook_type : types; + cook_proj : projection_body option; + cook_universes : constant_universes; + cook_inline : inline; + cook_context : Context.Named.t option; +} let on_body ml hy f = function | Undef _ as x -> x @@ -163,11 +166,6 @@ let on_body ml hy f = function OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f { Opaqueproof.modlist = ml; abstract = hy } o) -let constr_of_def otab = function - | Undef _ -> assert false - | Def cs -> Mod_subst.force_constr cs - | OpaqueDef lc -> Opaqueproof.force_proof otab lc - let expmod_constr_subst cache modlist subst c = let c = expmod_constr cache modlist c in Vars.subst_univs_level_constr subst c @@ -179,17 +177,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 @@ -211,17 +214,7 @@ let cook_constant ~hcons env { from = cb; info } = List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) hyps ~init:cb.const_hyps in - let typ = match cb.const_type with - | RegularArity t -> - let typ = - abstract_constant_type (expmod t) hyps in - RegularArity typ - | TemplateArity (ctx,s) -> - let t = mkArity (ctx,Type s.template_level) in - let typ = abstract_constant_type (expmod t) hyps in - let j = make_judge (constr_of_def (opaque_tables env) body) typ in - Typeops.make_polymorphic_if_constant_for_ind env j - in + let typ = abstract_constant_type (expmod cb.const_type) hyps in let projection pb = let c' = abstract_constant_body (expmod pb.proj_body) hyps in let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in @@ -235,24 +228,26 @@ let cook_constant ~hcons env { from = cb; info } = | _ -> assert false with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0) in - let typ = (* By invariant, a regular arity *) - match typ with RegularArity t -> t | TemplateArity _ -> assert false - in let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; 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, - Some const_hyps) + { + cook_body = body; + cook_type = typ; + cook_proj = Option.map projection cb.const_proj; + cook_universes = univs; + cook_inline = cb.const_inline_code; + cook_context = Some const_hyps; + } (* let cook_constant_key = Profile.declare_profile "cook_constant" *) (* let cook_constant = Profile.profile2 cook_constant_key cook_constant *) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7d47eba23e..6d1b776c05 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 *) @@ -16,10 +16,14 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = - constant_def * constant_type * projection_body option * - bool * constant_universes * inline - * Context.Named.t option +type result = { + cook_body : constant_def; + cook_type : types; + cook_proj : projection_body option; + cook_universes : constant_universes; + cook_inline : inline; + cook_context : 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..e17fb1c38f 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 *) @@ -36,8 +36,6 @@ type ('a, 'b) declaration_arity = | RegularArity of 'a | TemplateArity of 'b -type constant_type = (types, Context.Rel.t * template_arity) declaration_arity - (** Inlining level of parameters at functor applications. None means no inlining *) @@ -64,7 +62,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 @@ -81,9 +81,8 @@ type typing_flags = { type constant_body = { const_hyps : Context.Named.t; (** New: younger hyp at top *) const_body : constant_def; - const_type : constant_type; + const_type : types; 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 +167,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 +190,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 *) @@ -248,16 +250,16 @@ and module_implementation = | Struct of module_signature (** interactive body *) | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) -and module_body = +and 'a generic_module_body = { mod_mp : module_path; (** absolute path of the module *) - mod_expr : module_implementation; (** implementation *) + mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) mod_type_alg : module_expression option; (** algebraic type *) mod_constraints : Univ.ContextSet.t; (** set of all universes constraints in the module *) mod_delta : Mod_subst.delta_resolver; (** quotiented set of equivalent constants and inductive names *) - mod_retroknowledge : Retroknowledge.action list } + mod_retroknowledge : 'a module_retroknowledge } (** For a module, there are five possible situations: - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T] @@ -267,13 +269,19 @@ and module_body = - [Module M : T. ... End M] then [mod_expr = Struct; mod_type_alg = Some T] And of course, all these situations may be functors or not. *) -(** A [module_type_body] is just a [module_body] with no - implementation ([mod_expr] always [Abstract]) and also - an empty [mod_retroknowledge]. Its [mod_type_alg] contains +and module_body = module_implementation generic_module_body + +(** A [module_type_body] is just a [module_body] with no implementation and + also an empty [mod_retroknowledge]. Its [mod_type_alg] contains the algebraic definition of this module type, or [None] if it has been built interactively. *) -and module_type_body = module_body +and module_type_body = unit generic_module_body + +and _ module_retroknowledge = +| ModBodyRK : + Retroknowledge.action list -> module_implementation module_retroknowledge +| ModTypeRK : unit module_retroknowledge (** Extra invariants : diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 0a822d6fad..66d66c7d09 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 @@ -99,10 +69,6 @@ let subst_rel_declaration sub = let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -let subst_template_cst_arity sub (ctx,s as arity) = - let ctx' = subst_rel_context sub ctx in - if ctx==ctx' then arity else (ctx',s) - let subst_const_type sub arity = if is_empty_subst sub then arity else subst_mps sub arity @@ -124,7 +90,7 @@ let subst_const_body sub cb = if is_empty_subst sub then cb else let body' = subst_const_def sub cb.const_body in - let type' = subst_decl_arity subst_const_type subst_template_cst_arity sub cb.const_type in + let type' = subst_const_type sub cb.const_type in let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type && proj' == cb.const_proj then cb @@ -135,7 +101,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 } @@ -151,14 +116,6 @@ let hcons_rel_decl = let hcons_rel_context l = List.smartmap hcons_rel_decl l -let hcons_regular_const_arity t = Term.hcons_constr t - -let hcons_template_const_arity (ctx, ar) = - (hcons_rel_context ctx, hcons_template_arity ar) - -let hcons_const_type = - map_decl_arity hcons_regular_const_arity hcons_template_const_arity - let hcons_const_def = function | Undef inl -> Undef inl | Def l_constr -> @@ -166,11 +123,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_type = Term.hcons_constr cb.const_type; + const_universes = hcons_const_universes cb.const_universes } (** {6 Inductive types } *) @@ -259,21 +223,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_is_polymorphic mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> true + | Cumulative_ind cumi -> true -let inductive_context mib = - if mib.mind_polymorphic then - Univ.instantiate_univ_context mib.mind_universes - else Univ.UContext.empty +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 +272,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 } *) @@ -341,7 +318,7 @@ let rec hcons_structure_field_body sb = match sb with let mb' = hcons_module_body mb in if mb == mb' then sb else SFBmodule mb' | SFBmodtype mb -> - let mb' = hcons_module_body mb in + let mb' = hcons_module_type mb in if mb == mb' then sb else SFBmodtype mb' and hcons_structure_body sb = @@ -354,10 +331,10 @@ and hcons_structure_body sb = List.smartmap map sb and hcons_module_signature ms = - hcons_functorize hcons_module_body hcons_structure_body hcons_module_signature ms + hcons_functorize hcons_module_type hcons_structure_body hcons_module_signature ms and hcons_module_expression me = - hcons_functorize hcons_module_body hcons_module_alg_expr hcons_module_expression me + hcons_functorize hcons_module_type hcons_module_alg_expr hcons_module_expression me and hcons_module_implementation mip = match mip with | Abstract -> Abstract @@ -369,9 +346,11 @@ and hcons_module_implementation mip = match mip with if ms == ms' then mip else Struct ms | FullStruct -> FullStruct -and hcons_module_body mb = +and hcons_generic_module_body : + 'a. ('a -> 'a) -> 'a generic_module_body -> 'a generic_module_body = + fun hcons_impl mb -> let mp' = mb.mod_mp in - let expr' = hcons_module_implementation mb.mod_expr in + let expr' = hcons_impl mb.mod_expr in let type' = hcons_module_signature mb.mod_type in let type_alg' = mb.mod_type_alg in let constraints' = Univ.hcons_universe_context_set mb.mod_constraints in @@ -396,3 +375,9 @@ and hcons_module_body mb = mod_delta = delta'; mod_retroknowledge = retroknowledge'; } + +and hcons_module_body mb = + hcons_generic_module_body hcons_module_implementation mb + +and hcons_module_type mb = + hcons_generic_module_body (fun () -> ()) mb diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 6650b6b7b0..b2d29759da 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} *) @@ -83,3 +78,4 @@ val safe_flags : typing_flags val hcons_const_body : constant_body -> constant_body val hcons_mind : mutual_inductive_body -> mutual_inductive_body val hcons_module_body : module_body -> module_body +val hcons_module_type : module_type_body -> module_type_body diff --git a/kernel/entries.mli b/kernel/entries.ml index 1e07c96909..a1ccbdbc1b 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; } @@ -58,6 +64,10 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation +type constant_universes_entry = + | Monomorphic_const_entry of Univ.universe_context + | Polymorphic_const_entry of Univ.universe_context + type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -65,8 +75,7 @@ type 'a definition_entry = { (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; - const_entry_polymorphic : bool; - const_entry_universes : Univ.universe_context; + const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } diff --git a/kernel/environ.ml b/kernel/environ.ml index 5727bf2ea1..621a9931de 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,27 +228,24 @@ 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) - -let map_regular_arity f = function - | RegularArity a as ar -> - let a' = f a in - if a' == a then ar else RegularArity a' - | TemplateArity _ -> assert false + match cb.const_universes with + | Monomorphic_const _ -> Univ.Constraint.empty + | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx (* 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 + (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 +256,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,14 +274,14 @@ 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)) | OpaqueDef _ -> None | Undef _ -> None in - b', map_regular_arity (subst_instance_constr u) cb.const_type, cst + b', subst_instance_constr u cb.const_type, cst else let b' = match cb.const_body with | Def l_body -> Some (Mod_subst.force_constr l_body) @@ -295,8 +296,8 @@ 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 - map_regular_arity (subst_instance_constr u) cb.const_type + if Declareops.constant_is_polymorphic cb then + subst_instance_constr u cb.const_type else cb.const_type let constant_value_in env (kn,u) = @@ -321,7 +322,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 @@ -330,15 +331,6 @@ let polymorphic_pconstant (cst,u) env = let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes -let template_polymorphic_constant cst env = - match (lookup_constant cst env).const_type with - | TemplateArity _ -> true - | RegularArity _ -> false - -let template_polymorphic_pconstant (cst,u) env = - if not (Univ.Instance.is_empty u) then false - else template_polymorphic_constant cst env - let lookup_projection cst env = match (lookup_constant (Projection.constant cst) env).const_proj with | Some pb -> pb @@ -353,7 +345,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 @@ -632,39 +624,39 @@ fun rk value field -> native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; } | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 - Primitives.Int31add + CPrimitives.Int31add | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 - Primitives.Int31addc + CPrimitives.Int31addc | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 - Primitives.Int31addcarryc + CPrimitives.Int31addcarryc | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 - Primitives.Int31sub + CPrimitives.Int31sub | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 - Primitives.Int31subc + CPrimitives.Int31subc | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const - Cbytecodes.Ksubcarrycint31 Primitives.Int31subcarryc + Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 - Primitives.Int31mul + CPrimitives.Int31mul | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 - Primitives.Int31mulc + CPrimitives.Int31mulc | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 - Primitives.Int31div21 + CPrimitives.Int31div21 | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 - Primitives.Int31diveucl + CPrimitives.Int31diveucl | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 - Primitives.Int31addmuldiv + CPrimitives.Int31addmuldiv | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 - Primitives.Int31compare + CPrimitives.Int31compare | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 - Primitives.Int31head0 + CPrimitives.Int31head0 | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 - Primitives.Int31tail0 + CPrimitives.Int31tail0 | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 - Primitives.Int31lor + CPrimitives.Int31lor | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 - Primitives.Int31land + CPrimitives.Int31land | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 - Primitives.Int31lxor + CPrimitives.Int31lxor | _ -> empty_reactive_info let _ = Hook.set Retroknowledge.dispatch_hook dispatch diff --git a/kernel/environ.mli b/kernel/environ.mli index b7431dbe5f..377c61de2c 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 *) @@ -139,10 +139,6 @@ val polymorphic_constant : constant -> env -> bool val polymorphic_pconstant : pconstant -> env -> bool val type_in_type_constant : constant -> env -> bool -(** Old-style polymorphism *) -val template_polymorphic_constant : constant -> env -> bool -val template_polymorphic_pconstant : pconstant -> env -> bool - (** {6 ... } *) (** [constant_value env c] raises [NotEvaluableConst Opaque] if [c] is opaque and [NotEvaluableConst NoBody] if it has no @@ -153,20 +149,20 @@ type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant puniverses -> constr constrained -val constant_type : env -> constant puniverses -> constant_type constrained +val constant_type : env -> constant puniverses -> types constrained val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option val constant_value_and_type : env -> constant puniverses -> - constr option * constant_type * Univ.constraints + constr option * types * 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 application. *) val constant_value_in : env -> constant puniverses -> constr -val constant_type_in : env -> constant puniverses -> constant_type +val constant_type_in : env -> constant puniverses -> types val constant_opt_value_in : env -> constant puniverses -> constr option (** {6 Primitive projections} *) @@ -256,7 +252,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..917e4f6f14 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -13,9 +13,11 @@ Mod_subst Cbytecodes Copcodes Cemitcodes -Nativevalues -Primitives Opaqueproof +Declarations +Entries +Nativevalues +CPrimitives 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..f1d0e42796 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 *) @@ -107,9 +107,9 @@ val subst_substituted : substitution -> 'a substituted -> 'a substituted (**/**) (* debugging *) val debug_string_of_subst : substitution -> string -val debug_pr_subst : substitution -> Pp.std_ppcmds +val debug_pr_subst : substitution -> Pp.t val debug_string_of_delta : delta_resolver -> string -val debug_pr_delta : delta_resolver -> Pp.std_ppcmds +val debug_pr_delta : delta_resolver -> Pp.t (**/**) (** [subst_mp sub mp] guarantees that whenever the result of the diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index ff44f0f540..d2b41aae98 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,71 +72,58 @@ 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 _ -> let j = Typeops.infer env' c in - let typ = Typeops.type_of_constant_type env' cb.const_type in + let typ = cb.const_type in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in j.uj_val, cst' | Def cs -> let c' = Mod_subst.force_constr cs in c, Reduction.infer_conv env' (Environ.universes env') c c' - in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) - else - let cus, ccst = Univ.UContext.dest uctx in - let newus, cst = Univ.UContext.dest ctx in - let () = - if not (Univ.Instance.length cus == Univ.Instance.length newus) then - error_incorrect_with_constraint lab - in - let inst = Univ.Instance.append cus newus in - let csti = Univ.enforce_eq_instances cus newus cst in - let csta = Univ.Constraint.union csti ccst in - let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in - let () = if not (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 typ = cb.const_type 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 @@ -277,7 +264,9 @@ let rec translate_mse env mpo inl = function |MEident mp1 as me -> let mb = match mpo with |Some mp -> strengthen_and_subst_mb (lookup_module mp1 env) mp false - |None -> lookup_modtype mp1 env + |None -> + let mt = lookup_modtype mp1 env in + module_body_of_type mt.mod_mp mt in mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty |MEapply (fe,mp1) -> @@ -294,9 +283,11 @@ let mk_mod mp e ty cst reso = mod_type_alg = None; mod_constraints = cst; mod_delta = reso; - mod_retroknowledge = [] } + mod_retroknowledge = ModBodyRK []; } -let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso +let mk_modtype mp ty cst reso = + let mb = mk_mod mp Abstract ty cst reso in + { mb with mod_expr = (); mod_retroknowledge = ModTypeRK } let rec translate_mse_funct env mpo inl mse = function |[] -> @@ -332,6 +323,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with { res_mtb with mod_mp = mp; mod_expr = impl; + mod_retroknowledge = ModBodyRK []; (** cst from module body typing, cst' from subtyping, constraints from module type. *) 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..76915e917a 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 @@ -142,11 +143,12 @@ let rec functor_iter fty f0 = function (** {6 Misc operations } *) let module_type_of_module mb = - { mb with mod_expr = Abstract; mod_type_alg = None } + { mb with mod_expr = (); mod_type_alg = None; + mod_retroknowledge = ModTypeRK; } let module_body_of_type mp mtb = - assert (mtb.mod_expr == Abstract); - { mtb with mod_mp = mp } + { mtb with mod_expr = Abstract; mod_mp = mp; + mod_retroknowledge = ModBodyRK []; } let check_modpath_equiv env mp1 mp2 = if ModPath.equal mp1 mp2 then () @@ -195,7 +197,8 @@ let rec subst_structure sub do_delta sign = in List.smartmap subst_body sign -and subst_body is_mod sub do_delta mb = +and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = + fun is_mod sub subst_impl do_delta mb -> let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in let mp' = subst_mp sub mp in let sub = @@ -204,10 +207,7 @@ and subst_body is_mod sub do_delta mb = else add_mp mp mp' empty_delta_resolver sub in let ty' = subst_signature sub do_delta ty in - let me' = - implem_smartmap - (subst_signature sub id_delta) (subst_expression sub id_delta) me - in + let me' = subst_impl sub me in let aty' = Option.smartmap (subst_expression sub id_delta) aty in let delta' = do_delta mb.mod_delta sub in if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta @@ -220,9 +220,14 @@ and subst_body is_mod sub do_delta mb = mod_type_alg = aty'; mod_delta = delta' } -and subst_module sub do_delta mb = subst_body true sub do_delta mb +and subst_module sub do_delta mb = + subst_body true sub subst_impl do_delta mb + +and subst_impl sub me = + implem_smartmap + (subst_signature sub id_delta) (subst_expression sub id_delta) me -and subst_modtype sub do_delta mtb = subst_body false sub do_delta mtb +and subst_modtype sub do_delta mtb = subst_body false sub (fun _ () -> ()) do_delta mtb and subst_expr sub do_delta seb = match seb with |MEident mp -> @@ -267,7 +272,7 @@ let add_retroknowledge mp = CErrors.anomaly ~label:"Modops.add_retroknowledge" (Pp.str "had to import an unsupported kind of term.") in - fun lclrk env -> + fun (ModBodyRK lclrk) env -> (* The order of the declaration matters, for instance (and it's at the time this comment is being written, the only relevent instance) the int31 type registration absolutely needs int31 bits to be registered. @@ -327,12 +332,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))); @@ -568,7 +571,7 @@ let rec is_bounded_expr l = function is_bounded_expr l (MEident mp) || is_bounded_expr l fexpr | _ -> false -let rec clean_module l mb = +let rec clean_module_body l mb = let impl, typ = mb.mod_expr, mb.mod_type in let typ' = clean_signature l typ in let impl' = match impl with @@ -578,19 +581,25 @@ let rec clean_module l mb = if typ==typ' && impl==impl' then mb else { mb with mod_type=typ'; mod_expr=impl' } +and clean_module_type l mb = + let (), typ = mb.mod_expr, mb.mod_type in + let typ' = clean_signature l typ in + if typ==typ' then mb + else { mb with mod_type=typ' } + and clean_field l field = match field with |(lab,SFBmodule mb) -> - let mb' = clean_module l mb in + let mb' = clean_module_body l mb in if mb==mb' then field else (lab,SFBmodule mb') |_ -> field and clean_structure l = List.smartmap (clean_field l) and clean_signature l = - functor_smartmap (clean_module l) (clean_structure l) + functor_smartmap (clean_module_type l) (clean_structure l) and clean_expression l = - functor_smartmap (clean_module l) (fun me -> me) + functor_smartmap (clean_module_type l) (fun me -> me) let rec collect_mbid l sign = match sign with |MoreFunctor (mbid,ty,m) -> @@ -614,14 +623,16 @@ let join_constant_body except otab cb = | _ -> () let join_structure except otab s = - let rec join_module mb = - implem_iter join_signature join_expression mb.mod_expr; + let rec join_module : 'a. 'a generic_module_body -> unit = fun mb -> Option.iter join_expression mb.mod_type_alg; join_signature mb.mod_type and join_field (l,body) = match body with |SFBconst sb -> join_constant_body except otab sb |SFBmind _ -> () - |SFBmodule m |SFBmodtype m -> join_module m + |SFBmodule m -> + implem_iter join_signature join_expression m.mod_expr; + join_module m + |SFBmodtype m -> join_module m and join_structure struc = List.iter join_field struc and join_signature sign = functor_iter join_module join_structure sign 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..d111dd3c06 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 *) @@ -57,7 +57,7 @@ sig val to_string : t -> string (** Converts a identifier into an string. *) - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t (** Pretty-printer. *) module Set : Set.S with type elt = t @@ -105,7 +105,7 @@ sig val hcons : t -> t (** Hashconsing over names. *) - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t (** Pretty-printer (print "_" for [Anonymous]. *) end @@ -187,7 +187,7 @@ sig val to_id : t -> Id.t (** Conversion to an identifier. *) - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t (** Pretty-printer. *) module Set : Set.S with type elt = t @@ -286,7 +286,7 @@ sig val debug_to_string : t -> string (** Same as [to_string], but outputs information related to debug. *) - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t (** Comparisons *) val compare : t -> t -> int @@ -365,9 +365,9 @@ sig (** Displaying *) val to_string : t -> string - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t val debug_to_string : t -> string - val debug_print : t -> Pp.std_ppcmds + val debug_print : t -> Pp.t end @@ -447,9 +447,9 @@ sig (** Displaying *) val to_string : t -> string - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t val debug_to_string : t -> string - val debug_print : t -> Pp.std_ppcmds + val debug_print : t -> Pp.t end @@ -609,7 +609,7 @@ val mk_label : string -> label val string_of_label : label -> string (** @deprecated Same as [Label.to_string]. *) -val pr_label : label -> Pp.std_ppcmds +val pr_label : label -> Pp.t (** @deprecated Same as [Label.print]. *) val label_of_id : Id.t -> label @@ -695,7 +695,7 @@ val label : kernel_name -> Label.t val string_of_kn : kernel_name -> string (** @deprecated Same as [KerName.to_string]. *) -val pr_kn : kernel_name -> Pp.std_ppcmds +val pr_kn : kernel_name -> Pp.t (** @deprecated Same as [KerName.print]. *) val kn_ord : kernel_name -> kernel_name -> int @@ -731,7 +731,7 @@ module Projection : sig val map : (constant -> constant) -> t -> t val to_string : t -> string - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t end @@ -776,10 +776,10 @@ val con_with_label : constant -> Label.t -> constant val string_of_con : constant -> string (** @deprecated Same as [Constant.to_string] *) -val pr_con : constant -> Pp.std_ppcmds +val pr_con : constant -> Pp.t (** @deprecated Same as [Constant.print] *) -val debug_pr_con : constant -> Pp.std_ppcmds +val debug_pr_con : constant -> Pp.t (** @deprecated Same as [Constant.debug_print] *) val debug_string_of_con : constant -> string @@ -826,10 +826,10 @@ val mind_modpath : mutual_inductive -> ModPath.t val string_of_mind : mutual_inductive -> string (** @deprecated Same as [MutInd.to_string] *) -val pr_mind : mutual_inductive -> Pp.std_ppcmds +val pr_mind : mutual_inductive -> Pp.t (** @deprecated Same as [MutInd.print] *) -val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds +val debug_pr_mind : mutual_inductive -> Pp.t (** @deprecated Same as [MutInd.debug_print] *) val debug_string_of_mind : mutual_inductive -> string diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d3cd6b62a5..e08d913bc6 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)) @@ -296,7 +296,7 @@ type primitive = | MLmagic | MLarrayget | Mk_empty_instance - | Coq_primitive of Primitives.t * (prefix * constant) option + | Coq_primitive of CPrimitives.t * (prefix * constant) option let eq_primitive p1 p2 = match p1, p2 with @@ -361,9 +361,9 @@ let primitive_hash = function | MLsub -> 33 | MLmul -> 34 | MLmagic -> 35 - | Coq_primitive (prim, None) -> combinesmall 36 (Primitives.hash prim) + | Coq_primitive (prim, None) -> combinesmall 36 (CPrimitives.hash prim) | Coq_primitive (prim, Some (prefix,kn)) -> - combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim)) + combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim)) | Mk_proj -> 38 | MLarrayget -> 39 | Mk_empty_instance -> 40 @@ -921,7 +921,7 @@ let merge_branches t = type prim_aux = - | PAprim of string * constant * Primitives.t * prim_aux array + | PAprim of string * constant * CPrimitives.t * prim_aux array | PAml of mllambda let add_check cond args = @@ -988,11 +988,11 @@ let compile_prim decl cond paux = | Int31lt -> if Sys.word_size = 64 then app_prim Mk_bool [|(app_prim MLlt (args_to_int args))|] - else app_prim (Coq_primitive (Primitives.Int31lt,None)) args + else app_prim (Coq_primitive (CPrimitives.Int31lt,None)) args | Int31le -> if Sys.word_size = 64 then app_prim Mk_bool [|(app_prim MLle (args_to_int args))|] - else app_prim (Coq_primitive (Primitives.Int31le, None)) args + else app_prim (Coq_primitive (CPrimitives.Int31le, None)) args | Int31lsl -> of_int (mk_lsl (args_to_int args)) | Int31lsr -> of_int (mk_lsr (args_to_int args)) | Int31land -> of_int (mk_land (args_to_int args)) @@ -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) @@ -1752,11 +1752,10 @@ let pp_mllam fmt l = | MLarrayget -> Format.fprintf fmt "Array.get" | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty" | Coq_primitive (op,None) -> - Format.fprintf fmt "no_check_%s" (Primitives.to_string op) + Format.fprintf fmt "no_check_%s" (CPrimitives.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)))) + Format.fprintf fmt "%s %a" (CPrimitives.to_string op) + 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..a62a079da9 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 *) @@ -132,7 +132,7 @@ let native_conv_gen pb sigma env univs t1 t2 = let penv = Environ.pre_env env in let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code penv sigma prefix t1 t2 in - match compile ml_filename code with + match compile ml_filename code ~profile:false with | (true, fn) -> begin if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); 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..2353470f01 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 *) @@ -30,7 +30,7 @@ and lambda = | Lapp of lambda * lambda array | Lconst of prefix * pconstant | Lproj of prefix * constant (* prefix, projection name *) - | Lprim of prefix * constant * Primitives.t * lambda array + | Lprim of prefix * constant * CPrimitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda 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..156e4f834a 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 *) @@ -38,5 +38,5 @@ val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array -> val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda -> lambda -val compile_prim : Primitives.t -> constant -> bool -> prefix -> lambda array -> +val compile_prim : CPrimitives.t -> constant -> bool -> prefix -> lambda array -> lambda diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index f6c94158f8..665ddf7a65 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 *) @@ -64,7 +64,7 @@ let warn_native_compiler_failed = in CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print -let call_compiler ml_filename = +let call_compiler ?profile:(profile=false) ml_filename = let load_path = !get_load_paths () in let load_path = List.map (fun dn -> dn / output_dir) load_path in let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in @@ -74,14 +74,26 @@ let call_compiler ml_filename = let remove f = if Sys.file_exists f then Sys.remove f in remove link_filename; remove (f ^ ".cmi"); + let initial_args = + if Dynlink.is_native then + ["opt"; "-shared"] + else + ["ocamlc"; "-c"] + in + let profile_args = + if profile then + ["-g"] + else + [] + in let args = - (if Dynlink.is_native then "opt" else "ocamlc") - ::(if Dynlink.is_native then "-shared" else "-c") - ::"-o"::link_filename - ::"-rectypes" - ::"-w"::"a" - ::include_dirs - @ ["-impl"; ml_filename] in + initial_args @ + profile_args @ + ("-o"::link_filename + ::"-rectypes" + ::"-w"::"a" + ::include_dirs) @ + ["-impl"; ml_filename] in if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args))); try let res = CUnix.sys_command (ocamlfind ()) args in @@ -95,9 +107,9 @@ let call_compiler ml_filename = warn_native_compiler_failed (Inr e); false, link_filename -let compile fn code = +let compile fn code ~profile:profile = write_ml_code fn code; - let r = call_compiler fn in + let r = call_compiler ~profile fn in if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn; r diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 12ad3cf2f7..a262a9f58a 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 *) @@ -19,7 +19,7 @@ val load_obj : (string -> unit) ref val get_ml_filename : unit -> string * string -val compile : string -> global list -> bool * string +val compile : string -> global list -> profile:bool -> bool * string val compile_library : Names.dir_path -> global list -> string -> bool 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..94738d6186 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 *) @@ -156,7 +156,7 @@ let map_named_val f ctxt = in (accu, d') in - let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in + let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in if map == ctxt.env_named_map then ctxt else { env_named_ctx = ctx; env_named_map = map } 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/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..ad622b07d8 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,8 +382,13 @@ 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 poly = de.Entries.const_entry_polymorphic in + let open Entries in + let trust = Term_typing.SideEffects senv.revstruct in + let c,typ,univs = Term_typing.translate_local_def trust senv.env id de in + let poly = match de.Entries.const_entry_universes with + | Monomorphic_const_entry _ -> false + | Polymorphic_const_entry _ -> true + in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with | Def c -> Mod_subst.force_constr c, univs @@ -410,26 +424,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 @@ -477,12 +493,16 @@ let add_field ((l,sfb) as field) gn senv = let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) +type 'a effect_entry = +| EffectEntry : private_constants effect_entry +| PureEntry : unit effect_entry + type global_declaration = - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constants Entries.constant_entry * private_constant_role + constant * private_constant_role let add_constant_aux no_section senv (kn, cb) = let l = pi3 (Constant.repr3 kn) in @@ -506,30 +526,29 @@ let add_constant_aux no_section senv (kn, cb) = in senv'' +let export_private_constants ~in_section ce senv = + let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in + let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in + let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in + let no_section = not in_section in + let senv = List.fold_left (add_constant_aux no_section) senv bodies in + (ce, exported), senv + let add_constant dir l decl senv = let kn = make_con senv.modpath dir l in let no_section = DirPath.is_empty dir in - let seff_to_export, decl = - match decl with - | ConstantEntry (true, ce) -> - let exports, ce = - Term_typing.export_side_effects senv.revstruct senv.env ce in - exports, ConstantEntry (false, ce) - | _ -> [], decl - in - let senv = - List.fold_left (add_constant_aux no_section) senv - (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in let senv = let cb = match decl with - | ConstantEntry (export_seff,ce) -> - Term_typing.translate_constant senv.revstruct senv.env kn ce + | ConstantEntry (EffectEntry, ce) -> + Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce + | ConstantEntry (PureEntry, ce) -> + Term_typing.translate_constant Term_typing.Pure senv.env kn ce | GlobalRecipe r -> let cb = Term_typing.translate_recipe senv.env kn r in if no_section then Declareops.hcons_const_body cb else cb in add_constant_aux no_section senv (kn, cb) in - (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv + kn, senv (** Insertion of inductive types *) @@ -555,7 +574,7 @@ let add_mind dir l mie senv = let add_modtype l params_mte inl senv = let mp = MPdot(senv.modpath, l) in let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte in - let mtb = Declareops.hcons_module_body mtb in + let mtb = Declareops.hcons_module_type mtb in let senv' = add_field (l,SFBmodtype mtb) MT senv in mp, senv' @@ -658,7 +677,7 @@ let build_module_body params restype senv = (struc,None,senv.modresolver,senv.univ) restype' in let mb' = functorize_module params mb in - { mb' with mod_retroknowledge = senv.local_retroknowledge } + { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge } (** Returning back to the old pre-interactive-module environment, with one extra component and some updated fields @@ -713,12 +732,12 @@ let end_module l restype senv = let build_mtb mp sign cst delta = { mod_mp = mp; - mod_expr = Abstract; + mod_expr = (); mod_type = sign; mod_type_alg = None; mod_constraints = cst; mod_delta = delta; - mod_retroknowledge = [] } + mod_retroknowledge = ModTypeRK } let end_modtype l senv = let mp = senv.modpath in @@ -834,7 +853,7 @@ let export ?except senv dir = mod_type_alg = None; mod_constraints = senv.univ; mod_delta = senv.modresolver; - mod_retroknowledge = senv.local_retroknowledge + mod_retroknowledge = ModBodyRK senv.local_retroknowledge } in let ast, symbols = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index efeb98bd25..752fdd793e 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 *) @@ -67,7 +67,7 @@ val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : Environ.env -> Constr.constr -> private_constants -> Constr.constr val inline_private_constants_in_definition_entry : - Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry + Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry val universes_of_private : private_constants -> Univ.universe_context_set list @@ -94,19 +94,26 @@ val push_named_def : (** Insertion of global axioms or definitions *) +type 'a effect_entry = +| EffectEntry : private_constants effect_entry +| PureEntry : unit effect_entry + type global_declaration = - (* bool: export private constants *) - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constants Entries.constant_entry * private_constant_role + constant * private_constant_role + +val export_private_constants : in_section:bool -> + private_constants Entries.constant_entry -> + (unit Entries.constant_entry * exported_private_constant list) safe_transformer (** returns the main constant plus a list of auxiliary constants (empty unless one requires the side effects to be exported) *) val add_constant : DirPath.t -> Label.t -> global_declaration -> - (constant * exported_private_constant list) safe_transformer + constant safe_transformer (** Adding an inductive type *) 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..b564b2a8c1 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 = cb1.const_type in + let typ2 = 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 @@ -449,7 +416,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = mod_type = subst_signature subst1 body_t1; mod_type_alg = None; mod_constraints = mtb1.mod_constraints; - mod_retroknowledge = []; + mod_retroknowledge = ModBodyRK []; mod_delta = mtb1.mod_delta} env in check_structure cst env body_t1 body_t2 equiv subst1 subst2 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..3f42c348fc 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 *) @@ -21,7 +21,6 @@ open Environ open Entries open Typeops -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) @@ -77,6 +76,10 @@ end type side_effects = SideEffects.t +type _ trust = +| Pure : unit trust +| SideEffects : structure_body -> side_effects trust + let uniq_seff_rev = SideEffects.repr let uniq_seff l = List.rev (SideEffects.repr l) @@ -121,18 +124,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 ty = 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 +144,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 +228,32 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:state_id Feedback.Complete) -let infer_declaration ~trust env kn dcl = +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 (type a) ~(trust : a trust) env kn (dcl : a constant_entry) = 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 + { + Cooking.cook_body = Undef nl; + cook_type = t; + cook_proj = None; + cook_universes = univs; + cook_inline = false; + cook_context = ctx; + } (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. @@ -242,55 +261,69 @@ let infer_declaration ~trust env kn dcl = delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_polymorphic = false} as c) -> - let env = push_context ~strict:true c.const_entry_universes env in + const_entry_universes = Monomorphic_const_entry univs } as c) -> + let env = push_context ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> - let body, uctx, signatures = - inline_side_effects env body uctx side_eff in - let valid_signatures = check_signatures trust signatures in - let env = push_context_set uctx env in - let j = + let j, uctx = match trust with + | Pure -> + let env = push_context_set uctx env in + let j = infer env body in + let _ = judge_of_cast env j DEFAULTcast tyj in + j, uctx + | SideEffects mb -> + let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in + let valid_signatures = check_signatures mb signatures in + let env = push_context_set uctx env in 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 j = unzip ectx j in + let _ = judge_of_cast env j DEFAULTcast tyj in + j, uctx + in 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 + { + Cooking.cook_body = def; + cook_type = typ; + cook_proj = None; + cook_universes = Monomorphic_const univs; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let univsctx = Univ.ContextSet.of_context c.const_entry_universes in - let body, ctx, _ = inline_side_effects env body - (Univ.ContextSet.union univsctx ctx) side_eff in - let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in - let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in + let poly, univs = match c.const_entry_universes with + | Monomorphic_const_entry univs -> false, univs + | Polymorphic_const_entry univs -> true, univs + in + let univsctx = Univ.ContextSet.of_context univs in + let ctx = Univ.ContextSet.union univsctx ctx in + let body, ctx, _ = match trust with + | Pure -> body, ctx, [] + | SideEffects _ -> inline_side_effects env body ctx side_eff + in + let env = push_context_set ~strict:(not poly) ctx env in + let abstract = poly && 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 -> - if not c.const_entry_polymorphic then (* Old-style polymorphism *) - make_polymorphic_if_constant_for_ind env j - else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type) + Vars.subst_univs_level_constr usubst j.uj_type | 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) + Vars.subst_univs_level_constr usubst t in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in let def = @@ -298,8 +331,14 @@ 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 + { + Cooking.cook_body = def; + cook_type = typ; + cook_proj = None; + cook_universes = univs; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> let mib, _ = Inductive.lookup_mind_specif env (ind,0) in @@ -311,17 +350,22 @@ 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 - -let global_vars_set_constant_type env = function - | RegularArity t -> global_vars_set env t - | TemplateArity (ctx,_) -> - Context.Rel.fold_outside - (RelDecl.fold_constr - (fun t c -> Id.Set.union (global_vars_set env t) c)) - ctx ~init:Id.Set.empty + { + Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term)); + cook_type = typ; + cook_proj = Some pb; + cook_universes = univs; + cook_inline = false; + cook_context = None; + } let record_aux env s_ty s_bo suggested_expr = let in_ty = keep_hyps env s_ty in @@ -337,7 +381,9 @@ 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 result = + let open Cooking in + let typ = result.cook_type in 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 @@ -364,11 +410,12 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map NamedDecl.get_id (named_context env) in - match ctx with + let def = result.cook_body in + match result.cook_context with | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) - let ids_typ = global_vars_set_constant_type env typ in + let ids_typ = global_vars_set env typ in let ids_def = match def with | Undef _ -> Idset.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) @@ -396,22 +443,22 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) match def with | Undef _ as x -> x (* nothing to check *) | Def cs as x -> - let ids_typ = global_vars_set_constant_type env typ in + let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Mod_subst.force_constr cs) in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) OpaqueDef (Opaqueproof.iter_direct_opaque (fun c -> - let ids_typ = global_vars_set_constant_type env typ in + let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env c in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred) lc) in + let univs = result.cook_universes 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 + match result.cook_proj with + | 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 => @@ -423,26 +470,24 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = proj; + const_proj = result.cook_proj; const_body_code = None; - const_polymorphic = poly; const_universes = univs; - const_inline_code = inline_code; + const_inline_code = result.cook_inline; 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; const_body = def; const_type = typ; - const_proj = proj; + const_proj = result.cook_proj; const_body_code = tps; - const_polymorphic = poly; const_universes = univs; - const_inline_code = inline_code; + const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } (*s Global and local constant declaration. *) @@ -452,19 +497,24 @@ let translate_constant mb env kn ce = (infer_declaration ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = + let univs = + match cb.const_universes with + | Monomorphic_const uctx -> + Monomorphic_const_entry uctx + | Polymorphic_const auctx -> + Polymorphic_const_entry (Univ.AUContext.repr auctx) + in let pt = match cb.const_body, u with | OpaqueDef _, `Opaque (b, c) -> b, c | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty | _ -> assert false in DefinitionEntry { - const_entry_body = Future.from_val (pt, empty_seff); + const_entry_body = Future.from_val (pt, ()); const_entry_secctx = None; 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_type = Some cb.const_type; + const_entry_universes = univs; const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } ;; @@ -482,17 +532,18 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects constant_entry * side_effect_role + constant * constant_body * side_effect_role let export_side_effects mb env ce = match ce with - | ParameterEntry _ | ProjectionEntry _ -> [], ce + | ParameterEntry e -> [], ParameterEntry e + | ProjectionEntry e -> [], ProjectionEntry e | DefinitionEntry c -> let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with const_entry_body = Future.chain ~pure:true body - (fun (b_ctx, _) -> b_ctx, empty_seff) } in + (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in @@ -508,16 +559,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 @@ -525,8 +583,8 @@ let export_side_effects mb env ce = let env, cbs = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in - let cb = translate_constant mb env kn ce in - (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + let cb = translate_constant Pure env kn ce in + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) (env,[]) cbs in translate_seff sl rest (cbs @ acc) env | Some sl, cbs :: rest -> @@ -534,7 +592,7 @@ let export_side_effects mb env ce = let cbs = List.map turn_direct cbs in let env = List.fold_left push_seff env cbs in let ecbs = List.map (fun (kn,cb,u,r) -> - kn, cb, constant_entry_of_side_effect cb u, r) cbs in + kn, cb, r) cbs in translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env in translate_seff trusted seff [] env @@ -553,11 +611,11 @@ 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 = - 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 - match def with + let open Cooking in + let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in + let typ = decl.cook_type in + if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin + match decl.cook_body with | Undef _ -> () | Def _ -> () | OpaqueDef lc -> @@ -570,7 +628,11 @@ let translate_local_def mb env id centry = env ids_def ids_typ context_ids in record_aux env ids_typ ids_def expr end; - def, typ, univs + let univs = match decl.cook_universes with + | Monomorphic_const ctx -> ctx + | Polymorphic_const _ -> assert false + in + decl.cook_body, typ, univs (* Insertion of inductive types. *) @@ -580,7 +642,7 @@ let inline_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in - (body, ctx'), empty_seff); + (body, ctx'), ()); } let inline_side_effects env body side_eff = diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 075389ea53..24153343e7 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 *) @@ -14,8 +14,12 @@ open Entries type side_effects -val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> - constant_def * types * constant_universes +type _ trust = +| Pure : unit trust +| SideEffects : structure_body -> side_effects trust + +val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry -> + constant_def * types * Univ.universe_context val translate_local_assum : env -> types -> types @@ -26,7 +30,7 @@ val inline_side_effects : env -> constr -> side_effects -> constr redexes. *) val inline_entry_side_effects : - env -> side_effects definition_entry -> side_effects definition_entry + env -> side_effects definition_entry -> unit definition_entry (** Same as {!inline_side_effects} but applied to entries. Only modifies the {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) @@ -43,7 +47,7 @@ val uniq_seff : side_effects -> side_effect list val equal_eff : side_effect -> side_effect -> bool val translate_constant : - structure_body -> env -> constant -> side_effects constant_entry -> + 'a trust -> env -> constant -> 'a constant_entry -> constant_body type side_effect_role = @@ -51,7 +55,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects constant_entry * side_effect_role + constant * constant_body * side_effect_role (* Given a constant entry containing side effects it exports them (either * by re-checking them or trusting them). Returns the constant bodies to @@ -59,10 +63,7 @@ type exported_side_effect = * needs to be translated as usual after this step. *) val export_side_effects : structure_body -> env -> side_effects constant_entry -> - exported_side_effect list * side_effects constant_entry - -val constant_entry_of_side_effect : - constant_body -> seff_env -> side_effects constant_entry + exported_side_effect list * unit constant_entry val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -71,8 +72,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:structure_body -> env -> constant option -> - side_effects constant_entry -> Cooking.result +val infer_declaration : trust:'a trust -> env -> constant option -> + 'a constant_entry -> Cooking.result val build_constant_declaration : constant -> env -> Cooking.result -> constant_body 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..044877e82a 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 *) @@ -111,36 +111,17 @@ let check_hyps_inclusion env f c sign = (* Type of constants *) -let type_of_constant_type_knowing_parameters env t paramtyps = - match t with - | RegularArity t -> t - | TemplateArity (sign,ar) -> - let ctx = List.rev sign in - let ctx,s = instantiate_universes env ctx ar paramtyps in - mkArity (List.rev ctx,s) - -let type_of_constant_knowing_parameters env (kn,u as cst) args = +let type_of_constant env (kn,u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in - let ty = type_of_constant_type_knowing_parameters env ty args in let () = check_constraints cu env in ty -let type_of_constant_knowing_parameters_in env (kn,u as cst) args = +let type_of_constant_in env (kn,u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ty args - -let type_of_constant env cst = - type_of_constant_knowing_parameters env cst [||] - -let type_of_constant_in env cst = - type_of_constant_knowing_parameters_in env cst [||] - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] + constant_type_in env cst (* Type of a lambda-abstraction. *) @@ -369,9 +350,6 @@ let rec execute env cstr = | Ind ind when Environ.template_polymorphic_pind ind env -> let args = Array.map (fun t -> lazy t) argst in type_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - let args = Array.map (fun t -> lazy t) argst in - type_of_constant_knowing_parameters env cst args | _ -> (* No template polymorphism *) execute env f @@ -509,8 +487,6 @@ let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) -let judge_of_constant_knowing_parameters env cst args = - make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) let judge_of_projection env p cj = make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) @@ -555,38 +531,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") - -(* Instantiation of terms on real arguments. *) - -(* Make a type polymorphic if an arity *) - -let extract_level env p = - let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None - -let extract_context_levels env l = - let fold l = function - | RelDecl.LocalAssum (_,p) -> extract_level env p :: l - | RelDecl.LocalDef _ -> l - in - List.fold_left fold [] l - -let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = - let params, ccl = dest_prod_assum env t in - match kind_of_term ccl with - | Sort (Type u) -> - let ind, l = decompose_app (whd_all env c) in - if isInd ind && List.is_empty l then - let mis = lookup_mind_specif env (fst (destInd ind)) in - let nparams = Inductive.inductive_params mis in - let paramsl = CList.lastn nparams params in - let param_ccls = extract_context_levels env paramsl in - let s = { template_param_levels = param_ccls; template_level = u} in - TemplateArity (params,s) - else RegularArity t - | _ -> - RegularArity t diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 007acae604..a8f7fba9a0 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 *) @@ -11,7 +11,6 @@ open Univ open Term open Environ open Entries -open Declarations (** {6 Typing functions (not yet tagged as safe) } @@ -53,9 +52,6 @@ val judge_of_variable : env -> variable -> unsafe_judgment val judge_of_constant : env -> pconstant -> unsafe_judgment -val judge_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> unsafe_judgment - (** {6 type of an applied projection } *) val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment @@ -98,21 +94,9 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_constant_type : env -> constant_type -> types - val type_of_projection_constant : env -> Names.projection puniverses -> types val type_of_constant_in : env -> pconstant -> types -val type_of_constant_type_knowing_parameters : - env -> constant_type -> types Lazy.t array -> types - -val type_of_constant_knowing_parameters_in : - env -> pconstant -> types Lazy.t array -> types - -(** Make a type polymorphic if an arity *) -val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> - constant_type - (** Check that hyps are included in env and fails with error otherwise *) val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit 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..2fe5550184 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -53,9 +53,13 @@ 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 +val pr_universes : (Level.t -> Pp.t) -> universes -> Pp.t (** {6 Dumping to a file } *) diff --git a/kernel/univ.ml b/kernel/univ.ml index d53dd8e733..d915fb8c98 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 @@ -889,7 +892,7 @@ module Instance : sig val subst_fn : universe_level_subst_fn -> t -> t - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> t -> Pp.t val levels : t -> LSet.t end = struct @@ -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..a4f2e26b63 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 *) @@ -37,7 +37,7 @@ sig (** Create a new universe level from a unique identifier and an associated module path. *) - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t (** Pretty-printing *) val to_string : t -> string @@ -56,7 +56,7 @@ module LSet : sig include CSig.SetS with type elt = universe_level - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> t -> Pp.t (** Pretty-printing *) end @@ -86,10 +86,10 @@ sig val make : Level.t -> t (** Create a universe representing the given level. *) - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t (** Pretty-printing *) - val pr_with : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr_with : (Level.t -> Pp.t) -> t -> Pp.t val is_level : t -> bool (** Test if the universe is a level or an algebraic universe. *) @@ -127,7 +127,7 @@ type universe = Universe.t (** Alias name. *) -val pr_uni : universe -> Pp.std_ppcmds +val pr_uni : universe -> Pp.t (** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *) @@ -218,7 +218,7 @@ sig (** [subst_union x y] favors the bindings of the first map that are [Some], otherwise takes y's bindings. *) - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t (** Pretty-printing *) end @@ -270,7 +270,7 @@ sig val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> t -> Pp.t (** Pretty-printing, no comments *) val levels : t -> LSet.t @@ -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,29 +451,30 @@ 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_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 +val pr_constraint_type : constraint_type -> Pp.t +val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t +val pr_universe_context : (Level.t -> Pp.t) -> universe_context -> Pp.t +val pr_cumulativity_info : (Level.t -> Pp.t) -> cumulativity_info -> Pp.t +val pr_abstract_universe_context : (Level.t -> Pp.t) -> abstract_universe_context -> Pp.t +val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> abstract_cumulativity_info -> Pp.t +val pr_universe_context_set : (Level.t -> Pp.t) -> universe_context_set -> Pp.t +val explain_universe_inconsistency : (Level.t -> Pp.t) -> + univ_inconsistency -> Pp.t -val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds -val pr_universe_subst : universe_subst -> Pp.std_ppcmds +val pr_universe_level_subst : universe_level_subst -> Pp.t +val pr_universe_subst : universe_subst -> Pp.t (** {6 Hash-consing } *) @@ -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 *) diff --git a/kernel/vm.mli b/kernel/vm.mli index 6e9579aa46..df638acc1f 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -50,9 +50,9 @@ type whd = (** For debugging purposes only *) -val pr_atom : atom -> Pp.std_ppcmds -val pr_whd : whd -> Pp.std_ppcmds -val pr_stack : stack -> Pp.std_ppcmds +val pr_atom : atom -> Pp.t +val pr_whd : whd -> Pp.t +val pr_stack : stack -> Pp.t (** Constructors *) |