diff options
120 files changed, 3350 insertions, 743 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1de9e7f7c8..e1feabd064 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -253,6 +253,14 @@ ci-color: ci-compcert: <<: *ci-template +ci-coq-dpdgraph: + <<: *ci-template + variables: + <<: *ci-template-vars + EXTRA_OPAM: "ocamlgraph" + EXTRA_PACKAGES: "autoconf" + allow_failure: true + ci-coquelicot: <<: *ci-template variables: diff --git a/API/API.ml b/API/API.ml index 2b7bbd561b..515b152e42 100644 --- a/API/API.ml +++ b/API/API.ml @@ -138,6 +138,7 @@ module Typeclasses = Typeclasses module Pretype_errors = Pretype_errors module Notation = Notation module Declarations = Declarations +module Univops = Univops module Declareops = Declareops module Globnames = Globnames module Environ = Environ diff --git a/API/API.mli b/API/API.mli index 69278e7c9f..2fd3f27927 100644 --- a/API/API.mli +++ b/API/API.mli @@ -72,6 +72,7 @@ sig val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds end type 'a puniverses = 'a * Instance.t + val out_punivs : 'a puniverses -> 'a module Constraint : module type of struct include Univ.Constraint end @@ -84,7 +85,11 @@ sig end type universe_context = UContext.t - [@@ocaml.deprecated "alias of API.Names.UContext.t"] + [@@ocaml.deprecated "alias of API.Univ.UContext.t"] + + type abstract_universe_context = Univ.AUContext.t + type cumulativity_info = Univ.CumulativityInfo.t + type abstract_cumulativity_info = Univ.ACumulativityInfo.t module LSet : module type of struct include Univ.LSet end module ContextSet : @@ -1034,7 +1039,16 @@ sig | Undef of inline | Def of Term.constr Mod_subst.substituted | OpaqueDef of Opaqueproof.opaque - type constant_type = Declarations.constant_type + type template_arity = Declarations.template_arity = { + template_param_levels : Univ.Level.t option list; + template_level : Univ.Universe.t; + } + + type ('a, 'b) declaration_arity = ('a, 'b) Declarations.declaration_arity = + | RegularArity of 'a + | TemplateArity of 'b + + type constant_type = (Prelude.types, Context.Rel.t * template_arity) declaration_arity type constant_universes = Declarations.constant_universes type projection_body = Declarations.projection_body = { proj_ind : Names.MutInd.t; @@ -1045,12 +1059,12 @@ sig proj_body : Term.constr; } type typing_flags = Declarations.typing_flags + type constant_body = Declarations.constant_body = { const_hyps : Context.Named.t; const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; - const_polymorphic : bool; const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; @@ -1083,6 +1097,12 @@ sig | MEident of Names.ModPath.t | MEapply of module_alg_expr * Names.ModPath.t | MEwith of module_alg_expr * with_declaration + + type abstract_inductive_universes = Declarations.abstract_inductive_universes = + | Monomorphic_ind of Univ.UContext.t + | Polymorphic_ind of Univ.abstract_universe_context + | Cumulative_ind of Univ.abstract_cumulativity_info + type mutual_inductive_body = Declarations.mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : Declarations.record_body option; @@ -1092,8 +1112,7 @@ sig mind_nparams : int; mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; - mind_polymorphic : bool; - mind_universes : Univ.UContext.t; + mind_universes : Declarations.abstract_inductive_universes; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } @@ -1122,6 +1141,11 @@ sig | SFBmodtype of module_type_body end +module Univops : sig + val universes_of_constr : Term.constr -> Univ.LSet.t + val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t +end + module Environ : sig type env = Prelude.env @@ -1131,6 +1155,11 @@ sig uj_val : 'constr; uj_type : 'types } + type 'types punsafe_type_judgment = 'types Environ.punsafe_type_judgment = { + utj_val : 'types; + utj_type : Sorts.t } + + type unsafe_type_judgment = Term.types punsafe_type_judgment val empty_env : env val lookup_mind : Names.MutInd.t -> env -> Declarations.mutual_inductive_body val push_rel : Context.Rel.Declaration.t -> env -> env @@ -1156,6 +1185,7 @@ sig val fold_named_context_reverse : ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a val evaluable_named : Names.Id.t -> Environ.env -> bool + val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env end module UGraph : @@ -1219,6 +1249,7 @@ end module Typeops : sig + val infer_type : Environ.env -> Term.types -> Environ.unsafe_type_judgment val type_of_constant_type : Environ.env -> Declarations.constant_type -> Term.types val type_of_constant_in : Environ.env -> Term.pconstant -> Term.types end @@ -1900,6 +1931,7 @@ end module Decl_kinds : sig type polymorphic = bool + type cumulative_inductive_flag = bool type recursivity_kind = Decl_kinds.recursivity_kind = | Finite | CoFinite @@ -2381,7 +2413,7 @@ sig | VernacExactProof of Constrexpr.constr_expr | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * inline * (plident list * Constrexpr.constr_expr) with_coercion list - | VernacInductive of Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of @@ -2647,10 +2679,9 @@ sig type universe_opt_subst = Universes.universe_opt_subst val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set val new_Type : Names.DirPath.t -> Term.types + val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set val unsafe_type_of_global : Globnames.global_reference -> Term.types val constr_of_global : Prelude.global_reference -> Term.constr - val universes_of_constr : Term.constr -> Univ.LSet.t - val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t val new_univ_level : Names.DirPath.t -> Univ.Level.t val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context val new_sort_in_family : Sorts.family -> Sorts.t @@ -3476,6 +3507,7 @@ sig type ltac_constant = Names.KerName.t + val global : Libnames.reference -> Globnames.global_reference val global_of_path : Libnames.full_path -> Globnames.global_reference val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid val path_of_global : Globnames.global_reference -> Libnames.full_path @@ -4738,7 +4770,9 @@ sig type one_inductive_impls = Command.one_inductive_impls val do_mutual_inductive : - (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.polymorphic -> + (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> + Decl_kinds.cumulative_inductive_flag -> + Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.lident list option -> @@ -4762,7 +4796,9 @@ sig structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list val interp_mutual_inductive : - structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.polymorphic -> + structured_inductive_expr -> Vernacexpr.decl_notation list -> + Decl_kinds.cumulative_inductive_flag -> + Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list @@ -94,6 +94,12 @@ Build Infrastructure access to the same .cmi files. In short, use "make -j && make -j byte" instead of "make -j world byte". +Universes + +- Cumulative inductive types. see prefixes "Cumulative", "NonCumulative" + for inductive definitions and the option "Set Inductive Cumulativity" + in the reference manual. + Changes from V8.6beta1 to V8.6 ============================== diff --git a/checker/cic.mli b/checker/cic.mli index 3645587554..e298c41cf1 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -209,7 +209,9 @@ type constant_def = | Def of constr_substituted | OpaqueDef of lazy_constr -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 @@ -226,7 +228,6 @@ type constant_body = { const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; @@ -303,6 +304,11 @@ type one_inductive_body = { mind_reloc_tbl : 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 *) @@ -321,9 +327,7 @@ type mutual_inductive_body = { mind_params_ctxt : rel_context; (** 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; (** Local universe variables and constraints together with subtyping constraints *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) diff --git a/checker/closure.ml b/checker/closure.ml index b8294e7958..ac8388f6ed 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -328,6 +328,12 @@ let zshift n s = | (_,Zshift(k)::s) -> Zshift(n+k)::s | _ -> Zshift(n)::s +let rec stack_args_size = function + | Zapp v :: s -> Array.length v + stack_args_size s + | Zshift(_)::s -> stack_args_size s + | Zupdate(_)::s -> stack_args_size s + | _ -> 0 + (* Lifting. Preserves sharing (useful only for cell with norm=Red). lft_fconstr always create a new cell, while lift_fconstr avoids it when the lift is 0. *) diff --git a/checker/closure.mli b/checker/closure.mli index 8b1f246c28..8da9ad4ea5 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -125,6 +125,9 @@ type stack_member = and stack = stack_member list val append_stack : fconstr array -> stack -> stack + +val stack_args_size : stack -> int + val eta_expand_stack : stack -> stack val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> diff --git a/checker/declarations.ml b/checker/declarations.ml index ad93146d55..2eefe47816 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -521,6 +521,11 @@ let subst_template_cst_arity sub (ctx,s as arity) = let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s +let constant_is_polymorphic cb = + match cb.const_universes with + | Monomorphic_const _ -> false + | Polymorphic_const _ -> true + (* TODO: should be changed to non-coping after Term.subst_mps *) (* NB: we leave bytecode and native code fields untouched *) let subst_const_body sub cb = diff --git a/checker/declarations.mli b/checker/declarations.mli index 456df83699..6fc71bb942 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -14,6 +14,7 @@ val body_of_constant : constant_body -> constr option val constant_has_body : constant_body -> bool val is_opaque : constant_body -> bool val opaque_univ_context : constant_body -> Univ.ContextSet.t +val constant_is_polymorphic : constant_body -> bool (* Mutual inductives *) diff --git a/checker/environ.ml b/checker/environ.ml index 22d1eec178..11b8ea67cc 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -115,13 +115,15 @@ let add_constant kn cs env = env_constants = new_constants } in { env with env_globals = new_globals } -type const_evaluation_result = NoBody | Opaque +type const_evaluation_result = NoBody | Opaque | IsProj (* Constant types *) let constraints_of cb u = - let univs = cb.const_universes in - Univ.subst_instance_constraints u (Univ.UContext.constraints univs) + match cb.const_universes with + | Monomorphic_const _ -> Univ.Constraint.empty + | Polymorphic_const ctx -> + Univ.UContext.constraints (Univ.subst_instance_context u ctx) let map_regular_arity f = function | RegularArity a as ar -> @@ -132,23 +134,28 @@ let map_regular_arity f = function (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then - let csts = constraints_of cb u in - (map_regular_arity (subst_instance_constr u) cb.const_type, csts) - else cb.const_type, Univ.Constraint.empty + match cb.const_universes with + | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty + | Polymorphic_const ctx -> + let csts = constraints_of cb u in + (map_regular_arity (subst_instance_constr u) cb.const_type, csts) exception NotEvaluableConst of const_evaluation_result let constant_value env (kn,u) = let cb = lookup_constant kn env in + if cb.const_proj = None then match cb.const_body with | Def l_body -> let b = force_constr l_body in - if cb.const_polymorphic then - subst_instance_constr u (force_constr l_body) - else b + begin + match cb.const_universes with + | Monomorphic_const _ -> b + | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body) + end | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) + else raise (NotEvaluableConst IsProj) (* A global const is evaluable if it is defined and not opaque *) let evaluable_constant cst env = diff --git a/checker/environ.mli b/checker/environ.mli index 87f143d1bb..754c295d27 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -47,7 +47,7 @@ val check_constraints : Univ.constraints -> env -> bool val lookup_constant : constant -> env -> Cic.constant_body val add_constant : constant -> Cic.constant_body -> env -> env val constant_type : env -> constant puniverses -> constant_type Univ.constrained -type const_evaluation_result = NoBody | Opaque +type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant puniverses -> constr val evaluable_constant : constant -> env -> bool diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 6c38f38e29..54dec56b54 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -524,13 +524,67 @@ let check_positivity env_ar mind params nrecp inds = let wfp = Rtree.mk_rec irecargs in Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp +(* Check arities and constructors *) +let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : constr) 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 = fold_rel_context_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 = rel_context_nhyps paramsctxt in + let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in + let other_instnace = Univ.CumulativityInfo.subtyping_other_instance cumi in + let dosubst = subst_univs_level_constr sbsubst in + let uctx = Univ.CumulativityInfo.univ_context cumi in + let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in + let env = Environ.push_context uctx env_ar + in + let env = Environ.push_context uctx_other env + in + let env = Environ.push_context + (Univ.CumulativityInfo.subtyp_context cumi) env + in + (* process individual inductive types: *) + Array.iter (fun { mind_user_lc = lc; mind_arity = arity } -> + match arity with + | RegularArity { mind_user_arity = 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 + (************************************************************************) (************************************************************************) let check_inductive env kn mib = Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); (* check mind_constraints: should be consistent with env *) - let env = Environ.push_context (Univ.instantiate_univ_context mib.mind_universes) env in + let ind_ctx = + match mib.mind_universes with + | Monomorphic_ind ctx -> ctx + | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx + | Cumulative_ind cumi -> + Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) + in + let env = Environ.push_context ind_ctx env in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) (* check mind_ntypes *) @@ -547,6 +601,14 @@ let check_inductive env kn mib = let env_ar = typecheck_arity env params mib.mind_packets in (* - check constructor types *) Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; + (* check the inferred subtyping relation *) + let () = + match mib.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> () + | Cumulative_ind acumi -> + check_subtyping + (Univ.instantiate_cumulativity_info acumi) params env_ar mib.mind_packets + in (* check mind_nparams_rec: positivity condition *) check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets; (* check mind_equiv... *) diff --git a/checker/inductive.ml b/checker/inductive.ml index f890adba9a..e1860a23f0 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -54,10 +54,31 @@ let inductive_params (mib,_) = mib.mind_nparams (** Polymorphic inductives *) -let inductive_instance mib = - if mib.mind_polymorphic then - UContext.instance mib.mind_universes - else Instance.empty +let inductive_is_polymorphic mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> true + | Cumulative_ind cumi -> true + +let inductive_is_cumulative mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> false + | Cumulative_ind cumi -> true + +let inductive_polymorphic_instance mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind ctx -> Univ.AUContext.instance ctx + | Cumulative_ind cumi -> + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + +let inductive_polymorphic_context mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.UContext.empty + | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx + | Cumulative_ind cumi -> + Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) (************************************************************************) @@ -93,7 +114,7 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in - let t = mkArity (subst_instance_context u sign,dummy) in + let t = mkArity (Term.subst_instance_context u sign,dummy) in fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = @@ -199,7 +220,7 @@ let instantiate_universes env ctx ar argsorts = let type_of_inductive_gen env ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> - if not mib.mind_polymorphic then a.mind_user_arity + if not (inductive_is_polymorphic mib) then a.mind_user_arity else subst_instance_constr u a.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in diff --git a/checker/inductive.mli b/checker/inductive.mli index ed3a7b53ce..9a5541f39b 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -22,7 +22,13 @@ type mind_specif = mutual_inductive_body * one_inductive_body Raises [Not_found] if the inductive type is not found. *) val lookup_mind_specif : env -> inductive -> mind_specif -val inductive_instance : mutual_inductive_body -> Univ.universe_instance +val inductive_is_polymorphic : mutual_inductive_body -> bool + +val inductive_is_cumulative : mutual_inductive_body -> bool + +val inductive_polymorphic_instance : mutual_inductive_body -> Univ.universe_instance + +val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context val type_of_inductive : env -> mind_specif puniverses -> constr diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 7f93e15609..15e9ae2951 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -1,4 +1,3 @@ - open Pp open Util open Names @@ -26,21 +25,23 @@ let refresh_arity ar = | _ -> ar, Univ.ContextSet.empty let check_constant_declaration env kn cb = - Flags.if_verbose Feedback.msg_notice (str " checking cst: " ++ prcon kn); - let env' = - if cb.const_polymorphic then - let inst = Univ.make_abstract_instance cb.const_universes in - let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in - push_context ~strict:false ctx env - else push_context ~strict:true cb.const_universes env + Feedback.msg_notice (str " checking cst:" ++ prcon kn); + let env', u = + match cb.const_universes with + | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty + | Polymorphic_const auctx -> + let ctx = Univ.instantiate_univ_context auctx in + push_context ~strict:false ctx env, Univ.UContext.instance ctx in let envty, ty = match cb.const_type with RegularArity ty -> + let ty = subst_instance_constr u ty in let ty', cu = refresh_arity ty in let envty = push_context_set cu env' in let _ = infer_type envty ty' in envty, ty | TemplateArity(ctxt,par) -> + assert(Univ.Instance.is_empty u); let _ = check_ctxt env' ctxt in check_polymorphic_arity env' ctxt par; env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt @@ -48,6 +49,7 @@ let check_constant_declaration env kn cb = let () = match body_of_constant cb with | Some bd -> + let bd = subst_instance_constr u bd in (match cb.const_proj with | None -> let j = infer envty bd in conv_leq envty j ty @@ -57,7 +59,7 @@ let check_constant_declaration env kn cb = conv_leq envty j ty) | None -> () in - if cb.const_polymorphic then add_constant kn cb env + if constant_is_polymorphic cb then add_constant kn cb env else add_constant kn cb env' (** {6 Checking modules } *) diff --git a/checker/modops.ml b/checker/modops.ml index bed31143bf..be35c7e981 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -83,10 +83,10 @@ let strengthen_const mp_from l cb resolver = | Def _ -> cb | _ -> let con = Constant.make2 mp_from l in - let u = - if cb.const_polymorphic then - Univ.make_abstract_instance cb.const_universes - else Univ.Instance.empty + let u = + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const auctx -> Univ.make_abstract_instance auctx in { cb with const_body = Def (Declarations.from_val (Const (con,u))) } diff --git a/checker/reduction.ml b/checker/reduction.ml index ba0b017844..95dc93f5d2 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -117,6 +117,10 @@ let beta_appvect c v = (* Conversion *) (********************************************************************) +type conv_pb = + | CONV + | CUMUL + (* Conversion utility functions *) type 'a conversion_function = env -> 'a -> 'a -> unit @@ -152,11 +156,62 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) else raise NotConvertible -(* Convertibility of sorts *) +let convert_inductive_instances cv_pb cumi u u' univs = + let ind_instance = + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) in + let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in + if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && + (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.UContext.constraints + (Univ.subst_instance_context 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.UContext.constraints + (Univ.subst_instance_context comp_subst ind_subtypctx) + in + Univ.Constraint.union comp_cst comp_cst' + | CUMUL -> comp_cst + in + if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible + +let convert_inductives + cv_pb (mind, ind) u1 sv1 u2 sv2 univs = + match mind.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2 + | Cumulative_ind cumi -> + let num_param_arity = + mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs + in + if not (num_param_arity = sv1 && num_param_arity = sv2) then + convert_universes univs u1 u2 + else + convert_inductive_instances cv_pb cumi u1 u2 univs + +let convert_constructors + (mind, ind, cns) u1 sv1 u2 sv2 univs = + match mind.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2 + | Cumulative_ind cumi -> + let num_cnstr_args = + let nparamsctxt = + mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs + in + nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1) + in + if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then + convert_universes univs u1 u2 + else + convert_inductive_instances CONV cumi u1 u2 univs -type conv_pb = - | CONV - | CUMUL +(* Convertibility of sorts *) let sort_cmp env univ pb s0 s1 = match (s0,s1) with @@ -375,18 +430,37 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd (ind1,u1), FInd (ind2,u2)) -> - if mind_equiv_infos infos ind1 ind2 - then - (let () = convert_universes univ u1 u2 in - convert_stacks univ infos lft1 lft2 v1 v2) - else raise NotConvertible - - | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> - if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 - then - (let () = convert_universes univ u1 u2 in - convert_stacks univ infos lft1 lft2 v1 v2) - else raise NotConvertible + if mind_equiv_infos infos ind1 ind2 then + if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then + begin + convert_universes univ u1 u2; + convert_stacks univ infos lft1 lft2 v1 v2 + end + else + let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in + let () = + convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1) + u2 (stack_args_size v2) univ + in + convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible + + | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> + if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then + if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then + begin + convert_universes univ u1 u2; + convert_stacks univ infos lft1 lft2 v1 v2 + end + else + let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in + let () = + convert_constructors + (mind, snd ind1, j1) u1 (stack_args_size v1) + u2 (stack_args_size v2) univ + in + convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible (* Eta expansion of records *) | (FConstruct ((ind1,j1),u1), _) -> diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 2d04b77e46..bfe19584a7 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -88,18 +88,25 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let check_conv f = check_conv_error error f in let mib1 = match info1 with - | IndType ((_,0), mib) -> mib + | IndType ((_,0), mib) -> subst_mind subst1 mib | _ -> error () in let mib2 = subst_mind subst2 mib2 in let check eq f = if not (eq (f mib1) (f mib2)) then error () in - let bool_equal (x : bool) (y : bool) = x = y in - let u = - check bool_equal (fun x -> x.mind_polymorphic); - if mib1.mind_polymorphic then ( - check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes); - Univ.UContext.instance mib1.mind_universes) - else Univ.Instance.empty + let u = + let process inst inst' = + if Univ.Instance.equal inst inst' then inst else error () + in + match mib1.mind_universes, mib2.mind_universes with + | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx, Polymorphic_ind auctx' -> + process + (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx') + | Cumulative_ind cumi, Cumulative_ind cumi' -> + process + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi')) + | _ -> error () in let eq_projection_body p1 p2 = let check eq f = if not (eq (f p1) (f p2)) then error () in @@ -308,7 +315,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = "inductive type and give a definition to map the old name to the new " ^ "name."))); if constant_has_body cb2 then error () ; - let u = inductive_instance mind1 in + let u = inductive_polymorphic_instance mind1 in let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 @@ -319,7 +326,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = "constructor and give a definition to map the old name to the new " ^ "name."))); if constant_has_body cb2 then error () ; - let u1 = inductive_instance mind1 in + let u1 = inductive_polymorphic_instance mind1 in let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv env ty1 ty2 diff --git a/checker/term.ml b/checker/term.ml index 75c566aeb7..dea3d3e659 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -227,6 +227,8 @@ let rel_context_nhyps hyps = nhyps 0 hyps let fold_rel_context f l ~init = List.fold_right f l init +let fold_rel_context_outside f l ~init = List.fold_right f l init + let map_rel_decl f = function | LocalAssum (n, typ) as decl -> let typ' = f typ in @@ -414,6 +416,42 @@ 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 rec aux t = + match 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 (Const (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 (Ind (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 (Construct (c, u')) + | Sort (Type u) -> + let u' = Univ.subst_instance_universe subst u in + if u' == u then t else + (Sort (sort_of_univ u')) + | _ -> map_constr aux t + in + aux c + +let subst_instance_context s ctx = + if Univ.Instance.is_empty s then ctx + else map_rel_context (fun x -> subst_instance_constr s x) ctx + +let subst_univs_level_constr subst c = + if Univ.is_empty_level_subst subst then c + else + let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in let changed = ref false in let rec aux t = match t with @@ -436,14 +474,10 @@ let subst_instance_constr subst c = if u' == u then t else (changed := true; Construct (c, u')) | Sort (Type u) -> - let u' = Univ.subst_instance_universe subst u in + let u' = Univ.subst_univs_level_universe subst u in if u' == u then t else (changed := true; Sort (sort_of_univ u')) | _ -> map_constr aux t in let c' = aux c in if !changed then c' else c - -let subst_instance_context s ctx = - if Univ.Instance.is_empty s then ctx - else map_rel_context (fun x -> subst_instance_constr s x) ctx diff --git a/checker/term.mli b/checker/term.mli index 6b026d056f..ccf5b59e0c 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -33,6 +33,8 @@ val rel_context_length : rel_context -> int val rel_context_nhyps : rel_context -> int val fold_rel_context : (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a +val fold_rel_context_outside : + (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration val map_rel_context : (constr -> constr) -> rel_context -> rel_context val extended_rel_list : int -> rel_context -> constr list @@ -55,3 +57,4 @@ val eq_constr : constr -> constr -> bool (** Instance substitution for polymorphism. *) val subst_instance_constr : Univ.universe_instance -> constr -> constr val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context +val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr diff --git a/checker/typeops.ml b/checker/typeops.ml index 0163db3347..543f9acced 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -329,7 +329,6 @@ let rec execute env cstr = let pj = execute env p in let lfj = execute_array env lf in judge_of_case env ci (p,pj) (c,cj) lfj - | Fix ((_,i as vni),recdef) -> let fix_ty = execute_recdef env recdef i in let fix = (vni,recdef) in diff --git a/checker/univ.ml b/checker/univ.ml index 5717432315..0ee4686c1a 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -968,7 +968,23 @@ struct else Level.compare v v' end -module Constraint = Set.Make(UConstraintOrd) +let pr_constraint_type op = + let op_str = match op with + | Lt -> " < " + | Le -> " <= " + | Eq -> " = " + in str op_str + +module Constraint = +struct + module S = Set.Make(UConstraintOrd) + include S + + let pr prl c = + fold (fun (u1,op,u2) pp_std -> + pp_std ++ prl u1 ++ pr_constraint_type op ++ + prl u2 ++ fnl () ) c (str "") +end let empty_constraint = Constraint.empty let merge_constraints c g = @@ -1056,7 +1072,9 @@ module Instance : sig val subst_fn : universe_level_subst_fn -> t -> t val subst : universe_level_subst -> t -> t val pr : t -> Pp.std_ppcmds - val check_eq : t check_function + val check_eq : t check_function + val length : t -> int + val append : t -> t -> t end = struct type t = Level.t array @@ -1099,6 +1117,7 @@ struct (* [h] must be positive. *) let h = !accu land 0x3FFFFFFF in h + end module HInstance = Hashcons.Make(HInstancestruct) @@ -1135,6 +1154,10 @@ struct (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1)) in aux 0) + let length = Array.length + + let append = Array.append + end type universe_instance = Instance.t @@ -1152,10 +1175,63 @@ struct let make x = x let instance (univs, cst) = univs let constraints (univs, cst) = cst + + let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst + let pr prl (univs, cst as ctx) = + if is_empty ctx then mt() else + h 0 (Instance.pr univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) end type universe_context = UContext.t +module AUContext = UContext + +type abstract_universe_context = AUContext.t + +module CumulativityInfo = +struct + type t = universe_context * universe_context + + let make x = + if (Array.length (UContext.instance (snd x))) = + (Array.length (UContext.instance (fst x))) * 2 then x + else anomaly (Pp.str "Invalid subtyping information encountered!") + + let empty = (UContext.empty, UContext.empty) + + let halve_context ctx = + let len = Array.length ctx in + let halflen = len / 2 in + ((Array.sub ctx 0 halflen), (Array.sub ctx halflen halflen)) + + 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 ctx + + let from_universe_context univcst freshunivs = + let inst = (UContext.instance univcst) in + assert (Array.length freshunivs = Array.length inst); + (univcst, UContext.make (Array.append inst freshunivs, + create_trivial_subtyping inst freshunivs)) + + let subtyping_other_instance (univcst, subtypcst) = + let (_, ctx') = (halve_context (UContext.instance subtypcst)) in ctx' + + 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 + +module ACumulativityInfo = CumulativityInfo +type abstract_cumulativity_info = ACumulativityInfo.t + module ContextSet = struct type t = LSet.t constrained @@ -1166,6 +1242,8 @@ struct end type universe_context_set = ContextSet.t + + (** Substitutions. *) let is_empty_subst = LMap.is_empty @@ -1210,7 +1288,10 @@ let subst_instance_constraint s (u,d,v as c) = let subst_instance_constraints s csts = Constraint.fold (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) - csts Constraint.empty + csts Constraint.empty + +let subst_instance_context inst (inner_inst, inner_constr) = + (inner_inst, subst_instance_constraints inst inner_constr) let make_abstract_instance (ctx, _) = Array.mapi (fun i l -> Level.var i) ctx @@ -1219,8 +1300,8 @@ let make_abstract_instance (ctx, _) = let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) -let instantiate_univ_constraints u (_, csts) = - subst_instance_constraints u csts +let instantiate_cumulativity_info (ctx, ctx') = + (instantiate_univ_context ctx, instantiate_univ_context ctx') (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe @@ -1262,6 +1343,10 @@ let merge_context_set strict ctx g = (** Pretty-printing *) +let pr_constraints prl = Constraint.pr prl + +let pr_universe_context = UContext.pr + let pr_arc = function | _, Canonical {univ=u; lt=[]; le=[]} -> mt () diff --git a/checker/univ.mli b/checker/univ.mli index 7d4c629ab9..a503924708 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -18,6 +18,9 @@ sig (** Create a new universe level from a unique identifier and an associated module path. *) + val pr : t -> Pp.std_ppcmds + (** Pretty-printing *) + val equal : t -> t -> bool end @@ -71,6 +74,8 @@ type 'a check_function = universes -> 'a -> 'a -> bool val check_leq : universe check_function val check_eq : universe check_function + + (** The initial graph of universes: Prop < Set *) val initial_universes : universes @@ -170,6 +175,12 @@ sig val check_eq : t check_function (** Check equality of instances w.r.t. a universe graph *) + + val length : t -> int + (** Compute the length of the instance *) + + val append : t -> t -> t + (** Append two universe instances *) end type universe_instance = Instance.t @@ -187,9 +198,54 @@ sig val make : universe_instance constrained -> t val instance : t -> Instance.t val constraints : t -> constraints + val is_empty : t -> bool + +end + +type universe_context = UContext.t + +module AUContext : +sig + type t + + val instance : t -> Instance.t + +end + +type abstract_universe_context = AUContext.t + +module CumulativityInfo : +sig + type t + + val make : universe_context * universe_context -> t + + val empty : t + + val univ_context : t -> universe_context + val subtyp_context : t -> universe_context + + val from_universe_context : universe_context -> universe_instance -> t + + val subtyping_other_instance : t -> universe_instance + + 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 + module ContextSet : sig type t @@ -198,7 +254,6 @@ module ContextSet : val constraints : t -> constraints end -type universe_context = UContext.t type universe_context_set = ContextSet.t val merge_context : bool -> universe_context -> universes -> universes @@ -221,18 +276,22 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe (** Substitution of instances *) val subst_instance_instance : universe_instance -> universe_instance -> universe_instance val subst_instance_universe : universe_instance -> universe -> universe -val subst_instance_constraints : universe_instance -> constraints -> constraints +val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context (* val make_instance_subst : universe_instance -> universe_level_subst *) (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *) (** Get the instantiated graph. *) -val instantiate_univ_context : universe_context -> universe_context -val instantiate_univ_constraints : universe_instance -> universe_context -> constraints +val instantiate_univ_context : abstract_universe_context -> universe_context +val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info (** Build the relative instance corresponding to the context *) -val make_abstract_instance : universe_context -> universe_instance +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_universes : universes -> Pp.std_ppcmds diff --git a/checker/values.ml b/checker/values.ml index c175aed680..b8b395aaf7 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 6466d8cc443b5896cb905776df0cc49e checker/cic.mli +MD5 b132075590daf5e202de0d9cc34e6003 checker/cic.mli *) @@ -109,6 +109,8 @@ let v_cstrs = let v_instance = Annot ("instance", Array v_level) let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|] +let v_abs_context = v_context (* only for clarity *) +let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; v_context|] let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) @@ -215,13 +217,14 @@ let v_projbody = let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool|] +let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_context|]|] + let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; v_cst_type; Any; - v_bool; - v_context; + v_const_univs; Opt v_projbody; v_bool; v_typing_flags|] @@ -262,6 +265,10 @@ let v_finite = v_enum "recursivity_kind" 3 let v_mind_record = Annot ("mind_record", Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]))) +let v_ind_pack_univs = + v_sum "abstract_inductive_universes" 0 + [|[|v_context|]; [|v_abs_context|]; [|v_abs_cum_info|]|] + let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; v_mind_record; @@ -271,8 +278,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Int; Int; v_rctxt; - v_bool; - v_context; + v_ind_pack_univs; (* universes *) Opt v_bool; v_typing_flags|] diff --git a/dev/base_include b/dev/base_include index f9af0696b1..8ee1cceb23 100644 --- a/dev/base_include +++ b/dev/base_include @@ -58,8 +58,6 @@ (* Open main files *) -open API -open Grammar_API open Names open Term open Vars diff --git a/dev/include b/dev/include index 0f43f00729..31ae5da71a 100644 --- a/dev/include +++ b/dev/include @@ -41,6 +41,8 @@ #install_printer (* univ context *) ppuniverse_context;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; +#install_printer (* cumulativity info *) ppcumulativity_info;; +#install_printer (* abstract cumulativity info *) ppabstract_cumulativity_info;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; #install_printer (* univ subst *) ppuniverse_subst;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6ae5125f6d..ff575e432c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -8,7 +8,6 @@ (* Printers for the ocaml toplevel. *) -open API open Util open Pp open Names @@ -215,6 +214,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx +let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c) let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index be6b914b6b..afa94a63e0 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -1,4 +1,3 @@ -open API open Format open Term open Names diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index fdd2725810..96fb1eb752 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -461,6 +461,13 @@ recursively convertible to $u'_1$, or, symmetrically, $u_2$ is $\lb x:T\mto u'_2$ and $u_1\,x$ is recursively convertible to $u'_2$. We then write $\WTEGCONV{t_1}{t_2}$. +Apart from this we consider two instances of polymorphic and cumulative (see Chapter~\ref{Universes-full}) inductive types (see below) +convertible $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ if we have subtypings (see below) in both directions, i.e., +$\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ and $\WTEGLECONV{t\ w_1' \dots w_m'}{t\ w_1 \dots w_m}$. +Furthermore, we consider $\WTEGCONV{c\ v_1 \dots v_m}{c'\ v_1' \dots v_m'}$ convertible if $\WTEGCONV{v_i}{v_i'}$ +and we have that $c$ and $c'$ are the same constructors of different instances the same inductive types (differing only in universe levels) +such that $\WTEG{c\ v_1 \dots v_m}{t\ w_1 \dots w_m}$ and $\WTEG{c'\ v_1' \dots v_m'}{t'\ w_1' \dots w_m'}$ and we have $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$. + The convertibility relation allows introducing a new typing rule which says that two convertible well-formed types have the same inhabitants. @@ -480,6 +487,17 @@ convertibility into a {\em subtyping} relation inductively defined by: \item $\WTEGLECONV{\Prop}{\Set}$, hence, by transitivity, $\WTEGLECONV{\Prop}{\Type(i)}$, for any $i$ \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T, T'}{\forall~x:U, U'}$. +\item if $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ is a universe polymorphic and cumulative (see Chapter~\ref{Universes-full}) + inductive type (see below) and $(t : \forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort)\in\Gamma_I$ + and $(t' : \forall\Gamma_P',\forall\Gamma_{\mathit{Arr}(t)}', \Sort')\in\Gamma_I$ + are two different instances of \emph{the same} inductive type (differing only in universe levels) with constructors + \[[c_1: \forall\Gamma_P,\forall T_{1,1} \dots T_{1,n_1},t\ v_{1,1} \dots v_{1,m}; \dots; c_k: \forall\Gamma_P,\forall T_{k, 1} \dots T_{k,n_k},t\ v_{n,1}\dots v_{n,m}]\] + and + \[[c_1: \forall\Gamma_P',\forall T_{1,1}' \dots T_{1,n_1}',t'\ v_{1,1}' \dots v_{1,m}'; \dots; c_k: \forall\Gamma_P',\forall T_{k, 1}' \dots T_{k,n_k}',t\ v_{n,1}'\dots v_{n,m}']\] + respectively then $\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ (notice that $t$ and $t'$ are both fully applied, i.e., they have a sort as a type) + if $\WTEGCONV{w_i}{w_i'}$ for $1 \le i \le m$ and we have + \[ \WTEGLECONV{T_{i,j}}{T_{i,j}'} \text{ and } \WTEGLECONV{A_i}{A_i'}\] + where $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1; a_1 : A_l]$ and $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1'; a_1 : A_l']$. \end{enumerate} The conversion rule up to subtyping is now exactly: @@ -530,8 +548,12 @@ Formally, we can represent any {\em inductive definition\index{definition!induct These inductive definitions, together with global assumptions and global definitions, then form the global environment. % Additionally, for any $p$ there always exists $\Gamma_P=[a_1:A_1;\dots;a_p:A_p]$ -such that each $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as: +such that each $T$ in $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as: $\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of parameters\index{context of parameters}}. +Furthermore, we must have that each $T$ in $(t:T)\in\Gamma_I$ can be written as: +$\forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort$ where $\Gamma_{\mathit{Arr}(t)}$ is called the +{\em Arity} of the inductive type\index{arity of inductive type} $t$ and +$\Sort$ is called the sort of the inductive type $t$. \paragraph{Examples} diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 36518e6fae..2bb1301c79 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -131,6 +131,52 @@ producing global universe constraints, one can use the polymorphically, not at a single instance. \end{itemize} +\asection{{\tt Cumulative, NonCumulative}} +\comindex{Cumulative} +\comindex{NonCumulative} +\optindex{Inductive Cumulativity} + +Inductive types, coinductive types, variants and records can be +declared cumulative using the \texttt{Cumulative}. Alternatively, +there is an option \texttt{Set Inductive Cumulativity} which when set, +makes all subsequent inductive definitions cumulative. Consider the examples below. +\begin{coq_example*} +Polymorphic Cumulative Inductive list {A : Type} := +| nil : list +| cons : A -> list -> list. +\end{coq_example*} +\begin{coq_example} +Print list. +\end{coq_example} +When printing \texttt{list}, the part of the output of the form +\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff } +indicates the universe constraints in order to have the subtyping +$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ +(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$. +In the case of \texttt{list} there is no constraint! +This also means that any two instances of \texttt{list} are convertible: +$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and +furthermore their corresponding (when fully applied to convertible arguments) constructors. +See Chapter~\ref{Cic} for more details on convertibility and subtyping. +Also notice the subtyping constraints for the \emph{non-cumulative} version of list: +\begin{coq_example*} +Polymorphic NonCumulative Inductive list' {A : Type} := +| nil' : list' +| cons' : A -> list' -> list'. +\end{coq_example*} +\begin{coq_example} +Print list'. +\end{coq_example} +The following is an example of a record with non-trivial subtyping relation: +\begin{coq_example*} +Polymorphic Cumulative Record packType := {pk : Type}. +\end{coq_example*} +\begin{coq_example} +Print packType. +\end{coq_example} +Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}. + + \asection{Global and local universes} Each universe is declared in a global or local environment before it can diff --git a/engine/termops.ml b/engine/termops.ml index 92016d4af4..3eef71b2d0 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1173,6 +1173,9 @@ let compare_constr_univ sigma f cv_pb t1 t2 = Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2) | Prod (_,t1,c1), Prod (_,t2,c2) -> f Reduction.CONV t1 t2 && f cv_pb c1 c2 + | Const (c, u), Const (c', u') -> Constant.equal c c' + | Ind (i, _), Ind (i', _) -> eq_ind i i' + | Construct (i, _), Construct (i', _) -> eq_constructor i i' | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2 let constr_cmp sigma cv_pb t1 t2 = diff --git a/engine/uState.ml b/engine/uState.ml index acef901432..0973ca457f 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -284,7 +284,7 @@ let universe_context ?names ctx = in map, ctx let restrict ctx vars = - let uctx' = Universes.restrict_universe_context ctx.uctx_local vars in + let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } type rigid = diff --git a/engine/universes.ml b/engine/universes.ml index f201081862..bd4d75930c 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -283,11 +283,11 @@ let new_Type_sort dp = Type (new_univ dp) let fresh_universe_instance ctx = Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) - (UContext.instance ctx) + (AUContext.instance ctx) let fresh_instance_from_context ctx = let inst = fresh_universe_instance ctx in - let constraints = instantiate_univ_constraints inst ctx in + let constraints = UContext.constraints (subst_instance_context inst ctx) in inst, constraints let fresh_instance ctx = @@ -296,13 +296,13 @@ let fresh_instance ctx = Instance.subst_fn (fun v -> let u = new_univ_level (Global.current_dirpath ()) in ctx' := LSet.add u !ctx'; u) - (UContext.instance ctx) + (AUContext.instance ctx) in !ctx', inst let existing_instance ctx inst = let () = let a1 = Instance.to_array inst - and a2 = Instance.to_array (UContext.instance ctx) in + and a2 = Instance.to_array (AUContext.instance ctx) in let len1 = Array.length a1 and len2 = Array.length a2 in if not (len1 == len2) then CErrors.user_err ~hdr:"Universes" @@ -317,59 +317,75 @@ let fresh_instance_from ctx inst = | Some inst -> existing_instance ctx inst | None -> fresh_instance ctx in - let constraints = instantiate_univ_constraints inst ctx in + let constraints = UContext.constraints (subst_instance_context inst ctx) in inst, (ctx', constraints) let unsafe_instance_from ctx = - (Univ.UContext.instance ctx, ctx) + (Univ.AUContext.instance ctx, Univ.instantiate_univ_context ctx) (** Fresh universe polymorphic construction *) let fresh_constant_instance env c inst = let cb = lookup_constant c env in - if cb.Declarations.const_polymorphic then - let inst, ctx = - fresh_instance_from - (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst - in - ((c, inst), ctx) - else ((c,Instance.empty), ContextSet.empty) + match cb.Declarations.const_universes with + | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_const auctx -> + let inst, ctx = + fresh_instance_from auctx inst + in + ((c, inst), ctx) let fresh_inductive_instance env ind inst = let mib, mip = Inductive.lookup_mind_specif env ind in - if mib.Declarations.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in - ((ind,inst), ctx) - else ((ind,Instance.empty), ContextSet.empty) + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + ((ind,Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_ind uactx -> + let inst, ctx = (fresh_instance_from uactx) inst in + ((ind,inst), ctx) + | Declarations.Cumulative_ind acumi -> + let inst, ctx = + fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst + in ((ind,inst), ctx) let fresh_constructor_instance env (ind,i) inst = let mib, mip = Inductive.lookup_mind_specif env ind in - if mib.Declarations.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx inst in (((ind,i),inst), ctx) - else (((ind,i),Instance.empty), ContextSet.empty) + | Declarations.Cumulative_ind acumi -> + let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in + (((ind,i),inst), ctx) let unsafe_constant_instance env c = let cb = lookup_constant c env in - if cb.Declarations.const_polymorphic then - let inst, ctx = unsafe_instance_from - (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in - ((c, inst), ctx) - else ((c,Instance.empty), UContext.empty) + match cb.Declarations.const_universes with + | Declarations.Monomorphic_const _ -> + ((c,Instance.empty), UContext.empty) + | Declarations.Polymorphic_const auctx -> + let inst, ctx = unsafe_instance_from auctx in ((c, inst), ctx) let unsafe_inductive_instance env ind = let mib, mip = Inductive.lookup_mind_specif env ind in - if mib.Declarations.mind_polymorphic then - let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in - ((ind,inst), ctx) - else ((ind,Instance.empty), UContext.empty) + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> ((ind,Instance.empty), UContext.empty) + | Declarations.Polymorphic_ind auctx -> + let inst, ctx = unsafe_instance_from auctx in ((ind,inst), ctx) + | Declarations.Cumulative_ind acumi -> + let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in + ((ind,inst), ctx) let unsafe_constructor_instance env (ind,i) = let mib, mip = Inductive.lookup_mind_specif env ind in - if mib.Declarations.mind_polymorphic then - let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in - (((ind,i),inst), ctx) - else (((ind,i),Instance.empty), UContext.empty) + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> (((ind, i),Instance.empty), UContext.empty) + | Declarations.Polymorphic_ind auctx -> + let inst, ctx = unsafe_instance_from auctx in (((ind, i),inst), ctx) + | Declarations.Cumulative_ind acumi -> + let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in + (((ind, i),inst), ctx) open Globnames @@ -452,26 +468,49 @@ let type_of_reference env r = | ConstRef c -> let cb = Environ.lookup_constant c env in let ty = Typeops.type_of_constant_type env cb.const_type in - if cb.const_polymorphic then - let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in - Vars.subst_instance_constr inst ty, ctx - else ty, ContextSet.empty - + begin + match cb.const_universes with + | Monomorphic_const _ -> ty, ContextSet.empty + | Polymorphic_const auctx -> + let inst, ctx = fresh_instance_from auctx None in + Vars.subst_instance_constr inst ty, ctx + end | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - if mib.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.mind_universes None in + begin + match mib.mind_universes with + | Monomorphic_ind _ -> + let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in + ty, ContextSet.empty + | Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx None in let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - else - let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in - ty, ContextSet.empty + ty, ctx + | Cumulative_ind cumi -> + let inst, ctx = + fresh_instance_from (ACumulativityInfo.univ_context cumi) None + in + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + end + | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - if mib.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.mind_universes None in - Inductive.type_of_constructor (cstr,inst) specif, ctx - else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty + let (mib,oib as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + begin + match mib.mind_universes with + | Monomorphic_ind _ -> + Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty + | Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx None in + Inductive.type_of_constructor (cstr,inst) specif, ctx + | Cumulative_ind cumi -> + let inst, ctx = + fresh_instance_from (ACumulativityInfo.univ_context cumi) None + in + Inductive.type_of_constructor (cstr,inst) specif, ctx + end let type_of_global t = type_of_reference (Global.env ()) t @@ -976,36 +1015,6 @@ let normalize_context_set ctx us algs = (* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) (* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) -let universes_of_constr c = - let rec aux s c = - match kind_of_term c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> - let u = univ_of_sort u in - LSet.fold LSet.add (Universe.levels u) s - | _ -> fold_constr aux s c - in aux LSet.empty c - -let restrict_universe_context (univs,csts) s = - (* Universes that are not necessary to typecheck the term. - E.g. univs introduced by tactics and not used in the proof term. *) - let diff = LSet.diff univs s in - let rec aux diff candid univs ness = - let (diff', candid', univs', ness') = - Constraint.fold - (fun (l, d, r as c) (diff, candid, univs, csts) -> - if not (LSet.mem l diff) then - (LSet.remove r diff, candid, univs, Constraint.add c csts) - else if not (LSet.mem r diff) then - (LSet.remove l diff, candid, univs, Constraint.add c csts) - else (diff, Constraint.add c candid, univs, csts)) - candid (diff, Constraint.empty, univs, ness) - in - if ness' == ness then (LSet.diff univs diff', ness) - else aux diff' candid' univs' ness' - in aux diff csts univs Constraint.empty - let simplify_universe_context (univs,csts) = let uf = UF.create () in let noneqs = @@ -1118,3 +1127,14 @@ let solve_constraints_system levels level_bounds level_min = done; done; v + + +(** Operations for universe_info_ind *) + +(** Given a universe context representing constraints of an inductive + this function produces a UInfoInd.t that with the trivial subtyping relation. *) +let univ_inf_ind_from_universe_context univcst = + let freshunivs = Instance.of_array + (Array.map (fun _ -> new_univ_level ()) + (Instance.to_array (UContext.instance univcst))) + in CumulativityInfo.from_universe_context univcst freshunivs diff --git a/engine/universes.mli b/engine/universes.mli index 83ca1ea606..5ce5e4a42a 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -101,10 +101,10 @@ val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrai (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) -val fresh_instance_from_context : universe_context -> +val fresh_instance_from_context : abstract_universe_context -> universe_instance constrained -val fresh_instance_from : universe_context -> universe_instance option -> +val fresh_instance_from : abstract_universe_context -> universe_instance option -> universe_instance in_universe_context_set val fresh_sort_in_family : env -> sorts_family -> @@ -210,10 +210,6 @@ val unsafe_type_of_global : Globnames.global_reference -> types val nf_evars_and_universes_opt_subst : (existential -> constr option) -> universe_opt_subst -> constr -> constr -(** Shrink a universe context to a restricted set of variables *) - -val universes_of_constr : constr -> universe_set -val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set val simplify_universe_context : universe_context_set -> universe_context_set * universe_level_subst @@ -227,3 +223,9 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds val solve_constraints_system : universe option array -> universe array -> universe array -> universe array + +(** Operations for universe_info_ind *) + +(** Given a universe context representing constraints of an inductive + this function produces a UInfoInd.t that with the trivial subtyping relation. *) +val univ_inf_ind_from_universe_context : universe_context -> cumulativity_info diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 36b9d612a0..8aecf0e0c8 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -178,7 +178,7 @@ let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in let pr_rules = match pr with - | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> + | None -> <:expr< fun _ _ _ _ -> Pp.str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in declare_str_items loc [ <:str_item< diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml new file mode 100644 index 0000000000..8409c75218 --- /dev/null +++ b/ide/texmacspp.ml @@ -0,0 +1,769 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Xml_datatype +open Vernacexpr +open Constrexpr +open Names +open Misctypes +open Bigint +open Decl_kinds +open Extend +open Libnames +open Constrexpr_ops + +let unlock ?loc = + let start, stop = Option.cata Loc.unloc (0,0) loc in + (string_of_int start, string_of_int stop) + +let xmlWithLoc ?loc ename attr xml = + let start, stop = unlock ?loc in + Element(ename, [ "begin", start; "end", stop ] @ attr, xml) + +let get_fst_attr_in_xml_list attr xml_list = + let attrs_list = + List.map (function + | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs) + | _ -> []) + xml_list in + match List.flatten attrs_list with + | [] -> (attr, "") + | l -> (List.hd l) + +let backstep_loc xmllist = + let start_att = get_fst_attr_in_xml_list "begin" xmllist in + let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in + [start_att ; stop_att] + +let compare_begin_att xml1 xml2 = + let att1 = get_fst_attr_in_xml_list "begin" [xml1] in + let att2 = get_fst_attr_in_xml_list "begin" [xml2] in + match att1, att2 with + | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0 + | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1 + | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1 + | _ -> 0 + +let xmlBeginSection ?loc name = xmlWithLoc ?loc "beginsection" ["name", name] [] + +let xmlEndSegment ?loc name = xmlWithLoc ?loc "endsegment" ["name", name] [] + +let xmlThm ?loc typ name xml = + xmlWithLoc ?loc "theorem" ["type", typ; "name", name] xml + +let xmlDef ?loc typ name xml = + xmlWithLoc ?loc "definition" ["type", typ; "name", name] xml + +let xmlNotation ?loc attr name xml = + xmlWithLoc ?loc "notation" (("name", name) :: attr) xml + +let xmlReservedNotation ?loc attr name = + xmlWithLoc ?loc "reservednotation" (("name", name) :: attr) [] + +let xmlCst ?loc ?(attr=[]) name = + xmlWithLoc ?loc "constant" (("name", name) :: attr) [] + +let xmlOperator ?loc ?(attr=[]) ?(pprules=[]) name = + xmlWithLoc ?loc "operator" + (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) [] + +let xmlApply ?loc ?(attr=[]) xml = xmlWithLoc ?loc "apply" attr xml + +let xmlToken ?loc ?(attr=[]) xml = xmlWithLoc ?loc "token" attr xml + +let xmlTyped xml = Element("typed", (backstep_loc xml), xml) + +let xmlReturn ?(attr=[]) xml = Element("return", attr, xml) + +let xmlCase xml = Element("case", [], xml) + +let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml) + +let xmlWith xml = Element("with", [], xml) + +let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml]) + +let xmlInductive ?loc kind xml = xmlWithLoc ?loc "inductive" ["kind",kind] xml + +let xmlCoFixpoint xml = Element("cofixpoint", [], xml) + +let xmlFixpoint xml = Element("fixpoint", [], xml) + +let xmlCheck ?loc xml = xmlWithLoc ?loc "check" [] xml + +let xmlAssumption ?loc kind xml = xmlWithLoc ?loc "assumption" ["kind",kind] xml + +let xmlComment ?loc xml = xmlWithLoc ?loc "comment" [] xml + +let xmlCanonicalStructure ?loc attr = xmlWithLoc ?loc "canonicalstructure" attr [] + +let xmlQed ?loc ?(attr=[]) = xmlWithLoc ?loc "qed" attr [] + +let xmlPatvar ?loc id = xmlWithLoc ?loc "patvar" ["id", id] [] + +let xmlReference ref = + let name = Libnames.string_of_reference ref in + let i, j = Option.cata Loc.unloc (0,0) (Libnames.loc_of_reference ref) in + let b, e = string_of_int i, string_of_int j in + Element("reference",["name", name; "begin", b; "end", e] ,[]) + +let xmlRequire ?loc ?(attr=[]) xml = xmlWithLoc ?loc "require" attr xml +let xmlImport ?loc ?(attr=[]) xml = xmlWithLoc ?loc "import" attr xml + +let xmlAddLoadPath ?loc ?(attr=[]) xml = xmlWithLoc ?loc "addloadpath" attr xml +let xmlRemoveLoadPath ?loc ?(attr=[]) = xmlWithLoc ?loc "removeloadpath" attr +let xmlAddMLPath ?loc ?(attr=[]) = xmlWithLoc ?loc "addmlpath" attr + +let xmlExtend ?loc xml = xmlWithLoc ?loc "extend" [] xml + +let xmlScope ?loc ?(attr=[]) action name xml = + xmlWithLoc ?loc "scope" (["name",name;"action",action] @ attr) xml + +let xmlProofMode ?loc name = xmlWithLoc ?loc "proofmode" ["name",name] [] + +let xmlProof ?loc xml = xmlWithLoc ?loc "proof" [] xml + +let xmlSectionSubsetDescr name ssd = + Element("sectionsubsetdescr",["name",name], + [PCData (Proof_using.to_string ssd)]) + +let xmlDeclareMLModule ?loc s = + xmlWithLoc ?loc "declarexmlmodule" [] + (List.map (fun x -> Element("path",["value",x],[])) s) + +(* tactics *) +let xmlLtac ?loc xml = xmlWithLoc ?loc "ltac" [] xml + +(* toplevel commands *) +let xmlGallina ?loc xml = xmlWithLoc ?loc "gallina" [] xml + +let xmlTODO ?loc x = + xmlWithLoc ?loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + +let string_of_name n = + match n with + | Anonymous -> "_" + | Name id -> Id.to_string id + +let string_of_glob_sort s = + match s with + | GProp -> "Prop" + | GSet -> "Set" + | GType _ -> "Type" + +let string_of_cast_sort c = + match c with + | CastConv _ -> "CastConv" + | CastVM _ -> "CastVM" + | CastNative _ -> "CastNative" + | CastCoerce -> "CastCoerce" + +let string_of_case_style s = + match s with + | LetStyle -> "Let" + | IfStyle -> "If" + | LetPatternStyle -> "LetPattern" + | MatchStyle -> "Match" + | RegularStyle -> "Regular" + +let attribute_of_syntax_modifier sm = +match sm with + | SetItemLevel (sl, NumLevel n) -> + List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n] + | SetItemLevel (sl, NextLevel) -> + List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"] + | SetLevel i -> ["level", string_of_int i] + | SetAssoc a -> + begin match a with + | NonA -> ["",""] + | RightA -> ["associativity", "right"] + | LeftA -> ["associativity", "left"] + end + | SetEntryType (s, _) -> ["entrytype", s] + | SetOnlyPrinting -> ["onlyprinting", ""] + | SetOnlyParsing -> ["onlyparsing", ""] + | SetCompatVersion v -> ["compat", Flags.pr_version v] + | SetFormat (system, (loc, s)) -> + let start, stop = unlock ?loc in + ["format-"^system, s; "begin", start; "end", stop] + +let string_of_assumption_kind l a many = + match l, a, many with + | (Discharge, Logical, true) -> "Hypotheses" + | (Discharge, Logical, false) -> "Hypothesis" + | (Discharge, Definitional, true) -> "Variables" + | (Discharge, Definitional, false) -> "Variable" + | (Global, Logical, true) -> "Axioms" + | (Global, Logical, false) -> "Axiom" + | (Global, Definitional, true) -> "Parameters" + | (Global, Definitional, false) -> "Parameter" + | (Local, Logical, true) -> "Local Axioms" + | (Local, Logical, false) -> "Local Axiom" + | (Local, Definitional, true) -> "Local Parameters" + | (Local, Definitional, false) -> "Local Parameter" + | (Global, Conjectural, _) -> "Conjecture" + | ((Discharge | Local), Conjectural, _) -> assert false + +let rec pp_bindlist bl = + let tlist = + List.flatten + (List.map + (fun (loc_names, _, e) -> + let names = + (List.map + (fun (loc, name) -> + xmlCst ?loc (string_of_name name)) loc_names) in + match e.CAst.v with + | CHole _ -> names + | _ -> names @ [pp_expr e]) + bl) in + match tlist with + | [e] -> e + | l -> xmlTyped l +and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *) + Element ("decl_notation", ["name", s], [pp_expr ce]) +and pp_local_binder lb = (* don't know what it is for now *) + match lb with + | CLocalDef ((loc, nam), ce, ty) -> + let attrs = ["name", string_of_name nam] in + let value = match ty with + Some t -> CAst.make ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t) + | None -> ce in + pp_expr ~attr:attrs value + | CLocalAssum (namll, _, ce) -> + let ppl = + List.map (fun (loc, nam) -> (xmlCst ?loc (string_of_name nam))) namll in + xmlTyped (ppl @ [pp_expr ce]) + | CLocalPattern _ -> + assert false +and pp_local_decl_expr lde = (* don't know what it is for now *) + match lde with + | AssumExpr (_, ce) -> pp_expr ce + | DefExpr (_, ce, _) -> pp_expr ce +and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) = + (* inductive_expr *) + let b,e = Option.cata Loc.unloc (0,0) l in + let location = ["begin", string_of_int b; "end", string_of_int e] in + [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *) + begin match cl_or_rdexpr with + | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel + | RecordDecl (_, ldewwwl) -> + List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl + end @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end @ + (List.map pp_local_binder lbl) +and pp_recursion_order_expr optid roe = (* don't know what it is for now *) + let attrs = + match optid with + | None -> [] + | Some (loc, id) -> + let start, stop = unlock ?loc in + ["begin", start; "end", stop ; "name", Id.to_string id] in + let kind, expr = + match roe with + | CStructRec -> "struct", [] + | CWfRec e -> "rec", [pp_expr e] + | CMeasureRec (e, None) -> "mesrec", [pp_expr e] + | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in + Element ("recursion_order", ["kind", kind] @ attrs, expr) +and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) = + (* fixpoint_expr *) + let start, stop = unlock ?loc in + let id = Id.to_string id in + [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @ + (* fixpoint name *) + [pp_recursion_order_expr optid roe] @ + (List.map pp_local_binder lbl) @ + [pp_expr ce] @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end +and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *) + (* Nota: it is like fixpoint_expr without (optid, roe) + * so could be merged if there is no more differences *) + let start, stop = unlock ?loc in + let id = Id.to_string id in + [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @ + (* cofixpoint name *) + (List.map pp_local_binder lbl) @ + [pp_expr ce] @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end +and pp_lident (loc, id) = xmlCst ?loc (Id.to_string id) +and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce] +and pp_cases_pattern_expr {loc ; CAst.v = cpe} = + match cpe with + | CPatAlias (cpe, id) -> + xmlApply ?loc + (xmlOperator ?loc ~attr:["name", string_of_id id] "alias" :: + [pp_cases_pattern_expr cpe]) + | CPatCstr (ref, None, cpel2) -> + xmlApply ?loc + (xmlOperator ?loc "reference" + ~attr:["name", Libnames.string_of_reference ref] :: + [Element ("impargs", [], []); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatCstr (ref, Some cpel1, cpel2) -> + xmlApply ?loc + (xmlOperator ?loc "reference" + ~attr:["name", Libnames.string_of_reference ref] :: + [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1)); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatAtom optr -> + let attrs = match optr with + | None -> [] + | Some r -> ["name", Libnames.string_of_reference r] in + xmlApply ?loc (xmlOperator ?loc "atom" ~attr:attrs :: []) + | CPatOr cpel -> + xmlApply ?loc (xmlOperator ?loc "or" :: List.map pp_cases_pattern_expr cpel) + | CPatNotation (n, (subst_constr, subst_rec), cpel) -> + xmlApply ?loc + (xmlOperator ?loc "notation" :: + [xmlOperator ?loc n; + Element ("subst", [], + [Element ("subterms", [], + List.map pp_cases_pattern_expr subst_constr); + Element ("recsubterms", [], + List.map + (fun (cpel) -> + Element ("recsubterm", [], + List.map pp_cases_pattern_expr cpel)) + subst_rec)]); + Element ("args", [], (List.map pp_cases_pattern_expr cpel))]) + | CPatPrim tok -> pp_token ?loc tok + | CPatRecord rcl -> + xmlApply ?loc + (xmlOperator ?loc "record" :: + List.map (fun (r, cpe) -> + Element ("field", + ["reference", Libnames.string_of_reference r], + [pp_cases_pattern_expr cpe])) + rcl) + | CPatDelimiters (delim, cpe) -> + xmlApply ?loc + (xmlOperator ?loc "delimiter" ~attr:["name", delim] :: + [pp_cases_pattern_expr cpe]) + | CPatCast _ -> assert false +and pp_case_expr (e, name, pat) = + match name, pat with + | None, None -> xmlScrutinee [pp_expr e] + | Some (loc, name), None -> + let start, stop= unlock ?loc in + xmlScrutinee ~attr:["name", string_of_name name; + "begin", start; "end", stop] [pp_expr e] + | Some (loc, name), Some p -> + let start, stop= unlock ?loc in + xmlScrutinee ~attr:["name", string_of_name name; + "begin", start; "end", stop] + [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e] + | None, Some p -> + xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e] +and pp_branch_expr_list bel = + xmlWith + (List.map + (fun (_, (cpel, e)) -> + let ppcepl = + List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in + let ppe = [pp_expr e] in + xmlCase (ppcepl @ ppe)) + bel) +and pp_token ?loc tok = + let tokstr = + match tok with + | String s -> PCData s + | Numeral n -> PCData (to_string n) in + xmlToken ?loc [tokstr] +and pp_local_binder_list lbl = + let l = (List.map pp_local_binder lbl) in + Element ("recurse", (backstep_loc l), l) +and pp_const_expr_list cel = + let l = List.map pp_expr cel in + Element ("recurse", (backstep_loc l), l) +and pp_expr ?(attr=[]) { loc; CAst.v = e } = + match e with + | CRef (r, _) -> + xmlCst ?loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r) + | CProdN (bl, e) -> + xmlApply ?loc + (xmlOperator ?loc "forall" :: [pp_bindlist bl] @ [pp_expr e]) + | CApp ((_, hd), args) -> + xmlApply ?loc ~attr (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args) + | CAppExpl ((_, r, _), args) -> + xmlApply ?loc ~attr + (xmlCst ?loc:(Libnames.loc_of_reference r) (Libnames.string_of_reference r) + :: List.map pp_expr args) + | CNotation (notation, ([],[],[])) -> + xmlOperator ?loc notation + | CNotation (notation, (args, cell, lbll)) -> + let fmts = Notation.find_notation_extra_printing_rules notation in + let oper = xmlOperator ?loc notation ~pprules:fmts in + let cels = List.map pp_const_expr_list cell in + let lbls = List.map pp_local_binder_list lbll in + let args = List.map pp_expr args in + xmlApply ?loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls))) + | CSort(s) -> + xmlOperator ?loc (string_of_glob_sort s) + | CDelimiters (scope, ce) -> + xmlApply ?loc (xmlOperator ?loc "delimiter" ~attr:["name", scope] :: + [pp_expr ce]) + | CPrim tok -> pp_token ?loc tok + | CGeneralization (kind, _, e) -> + let kind= match kind with + | Explicit -> "explicit" + | Implicit -> "implicit" in + xmlApply ?loc + (xmlOperator ?loc ~attr:["kind", kind] "generalization" :: [pp_expr e]) + | CCast (e, tc) -> + begin match tc with + | CastConv t | CastVM t |CastNative t -> + xmlApply ?loc + (xmlOperator ?loc ":" ~attr:["kind", (string_of_cast_sort tc)] :: + [pp_expr e; pp_expr t]) + | CastCoerce -> + xmlApply ?loc + (xmlOperator ?loc ":" ~attr:["kind", "CastCoerce"] :: + [pp_expr e]) + end + | CEvar (ek, cel) -> + let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in + xmlApply ?loc + (xmlOperator ?loc "evar" ~attr:["id", string_of_id ek] :: + ppcel) + | CPatVar id -> xmlPatvar ?loc (string_of_id id) + | CHole (_, _, _) -> xmlCst ?loc ~attr "_" + | CIf (test, (_, ret), th, el) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc "if" :: + return @ [pp_expr th] @ [pp_expr el]) + | CLetTuple (names, (_, ret), value, body) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc "lettuple" :: + return @ + (List.map (fun (loc, var) -> xmlCst ?loc (string_of_name var)) names) @ + [pp_expr value; pp_expr body]) + | CCases (sty, ret, cel, bel) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc ~attr:["style", (string_of_case_style sty)] "match" :: + (return @ + [Element ("scrutinees", [], List.map pp_case_expr cel)] @ + [pp_branch_expr_list bel])) + | CRecord _ -> assert false + | CLetIn ((varloc, var), value, typ, body) -> + let value = match typ with + | Some t -> + CAst.make ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t)) + | None -> value in + xmlApply ?loc + (xmlOperator ?loc "let" :: + [xmlCst ?loc:varloc (string_of_name var) ; pp_expr value; pp_expr body]) + | CLambdaN (bl, e) -> + xmlApply ?loc + (xmlOperator ?loc "lambda" :: [pp_bindlist bl] @ [pp_expr e]) + | CCoFix (_, _) -> assert false + | CFix (lid, fel) -> + xmlApply ?loc + (xmlOperator ?loc "fix" :: + List.flatten (List.map + (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d)) + fel)) + +let pp_comment c = + match c with + | CommentConstr e -> [pp_expr e] + | CommentString s -> [Element ("string", [], [PCData s])] + | CommentInt i -> [PCData (string_of_int i)] + +let rec tmpp ?loc v = + match v with + (* Control *) + | VernacLoad (verbose,f) -> + xmlWithLoc ?loc "load" ["verbose",string_of_bool verbose;"file",f] [] + | VernacTime (loc,e) -> + xmlApply ?loc (Element("time",[],[]) :: + [tmpp ?loc e]) + | VernacRedirect (s, (loc,e)) -> + xmlApply ?loc (Element("redirect",["path", s],[]) :: + [tmpp ?loc e]) + | VernacTimeout (s,e) -> + xmlApply ?loc (Element("timeout",["val",string_of_int s],[]) :: + [tmpp ?loc e]) + | VernacFail e -> xmlApply ?loc (Element("fail",[],[]) :: [tmpp ?loc e]) + + (* Syntax *) + | VernacSyntaxExtension (_, ((_, name), sml)) -> + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + xmlReservedNotation ?loc attrs name + + | VernacOpenCloseScope (_,(true,name)) -> xmlScope ?loc "open" name [] + | VernacOpenCloseScope (_,(false,name)) -> xmlScope ?loc "close" name [] + | VernacDelimiters (name,Some tag) -> + xmlScope ?loc "delimit" name ~attr:["delimiter",tag] [] + | VernacDelimiters (name,None) -> + xmlScope ?loc "undelimit" name ~attr:[] [] + | VernacInfix (_,((_,name),sml),ce,sn) -> + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + let sc_attr = + match sn with + | Some scope -> ["scope", scope] + | None -> [] in + xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce] + | VernacNotation (_, ce, (lstr, sml), sn) -> + let name = snd lstr in + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + let sc_attr = + match sn with + | Some scope -> ["scope", scope] + | None -> [] in + xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce] + | VernacBindScope _ as x -> xmlTODO ?loc x + | VernacNotationAddFormat _ as x -> xmlTODO ?loc x + | VernacUniverse _ + | VernacConstraint _ + | VernacPolymorphic (_, _) as x -> xmlTODO ?loc x + (* Gallina *) + | VernacDefinition (ldk, ((_,id),_), de) -> + let l, dk = + match ldk with + | Some l, dk -> (l, dk) + | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *) + let e = + match de with + | ProveBody (_, ce) -> ce + | DefineBody (_, Some _, ce, None) -> ce + | DefineBody (_, None , ce, None) -> ce + | DefineBody (_, Some _, ce, Some _) -> ce + | DefineBody (_, None , ce, Some _) -> ce in + let str_dk = Kindops.string_of_definition_kind (l, false, dk) in + let str_id = Id.to_string id in + (xmlDef ?loc str_dk str_id [pp_expr e]) + | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) -> + let str_tk = Kindops.string_of_theorem_kind tk in + let str_id = Id.to_string id in + (xmlThm ?loc str_tk str_id [pp_expr statement]) + | VernacStartTheoremProof _ as x -> xmlTODO ?loc x + | VernacEndProof pe -> + begin + match pe with + | Admitted -> xmlQed ?loc ?attr:None + | Proved (_, Some ((_, id), Some tk)) -> + let nam = Id.to_string id in + let typ = Kindops.string_of_theorem_kind tk in + xmlQed ?loc ~attr:["name", nam; "type", typ] + | Proved (_, Some ((_, id), None)) -> + let nam = Id.to_string id in + xmlQed ?loc ~attr:["name", nam] + | Proved _ -> xmlQed ?loc ?attr:None + end + | VernacExactProof _ as x -> xmlTODO ?loc x + | VernacAssumption ((l, a), _, sbwcl) -> + let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in + let many = + List.length (List.flatten (List.map fst binders)) > 1 in + let exprs = + List.flatten (List.map pp_simple_binder binders) in + let l = match l with Some x -> x | None -> Decl_kinds.Global in + let kind = string_of_assumption_kind l a many in + xmlAssumption ?loc kind exprs + | VernacInductive (_, _, _, iednll) -> + let kind = + let (_, _, _, k, _), _ = List.hd iednll in + begin + match k with + | Record -> "Record" + | Structure -> "Structure" + | Inductive_kw -> "Inductive" + | CoInductive -> "CoInductive" + | Class _ -> "Class" + | Variant -> "Variant" + end in + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (ie, dnl) -> (pp_inductive_expr ie) @ + (List.map pp_decl_notation dnl)) iednll) in + xmlInductive ?loc kind exprs + | VernacFixpoint (_, fednll) -> + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (fe, dnl) -> (pp_fixpoint_expr fe) @ + (List.map pp_decl_notation dnl)) fednll) in + xmlFixpoint exprs + | VernacCoFixpoint (_, cfednll) -> + (* Nota: it is like VernacFixpoint without so could be merged *) + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @ + (List.map pp_decl_notation dnl)) cfednll) in + xmlCoFixpoint exprs + | VernacScheme _ as x -> xmlTODO ?loc x + | VernacCombinedScheme _ as x -> xmlTODO ?loc x + + (* Gallina extensions *) + | VernacBeginSection (_, id) -> xmlBeginSection ?loc (Id.to_string id) + | VernacEndSegment (_, id) -> xmlEndSegment ?loc (Id.to_string id) + | VernacNameSectionHypSet _ as x -> xmlTODO ?loc x + | VernacRequire (from, import, l) -> + let import = match import with + | None -> [] + | Some true -> ["export","true"] + | Some false -> ["import","true"] + in + let from = match from with + | None -> [] + | Some r -> ["from", Libnames.string_of_reference r] + in + xmlRequire ?loc ~attr:(from @ import) (List.map (fun ref -> + xmlReference ref) l) + | VernacImport (true,l) -> + xmlImport ?loc ~attr:["export","true"] (List.map (fun ref -> + xmlReference ref) l) + | VernacImport (false,l) -> + xmlImport ?loc (List.map (fun ref -> xmlReference ref) l) + | VernacCanonical r -> + let attr = + match r with + | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q] + | AN (Ident (_, id)) -> ["id", Id.to_string id] + | ByNotation (_, (s, _)) -> ["notation", s] in + xmlCanonicalStructure ?loc attr + | VernacCoercion _ as x -> xmlTODO ?loc x + | VernacIdentityCoercion _ as x -> xmlTODO ?loc x + + (* Type classes *) + | VernacInstance _ as x -> xmlTODO ?loc x + + | VernacContext _ as x -> xmlTODO ?loc x + + | VernacDeclareInstances _ as x -> xmlTODO ?loc x + + | VernacDeclareClass _ as x -> xmlTODO ?loc x + + (* Modules and Module Types *) + | VernacDeclareModule _ as x -> xmlTODO ?loc x + | VernacDefineModule _ as x -> xmlTODO ?loc x + | VernacDeclareModuleType _ as x -> xmlTODO ?loc x + | VernacInclude _ as x -> xmlTODO ?loc x + + (* Solving *) + + | (VernacSolveExistential _) as x -> + xmlLtac ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + + (* Auxiliary file and library management *) + | VernacAddLoadPath (recf,name,None) -> + xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] [] + | VernacAddLoadPath (recf,name,Some dp) -> + xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] + [PCData (Names.DirPath.to_string dp)] + | VernacRemoveLoadPath name -> xmlRemoveLoadPath ?loc ~attr:["path",name] [] + | VernacAddMLPath (recf,name) -> + xmlAddMLPath ?loc ~attr:["rec",string_of_bool recf;"path",name] [] + | VernacDeclareMLModule sl -> xmlDeclareMLModule ?loc sl + | VernacChdir _ as x -> xmlTODO ?loc x + + (* State management *) + | VernacWriteState _ as x -> xmlTODO ?loc x + | VernacRestoreState _ as x -> xmlTODO ?loc x + + (* Resetting *) + | VernacResetName _ as x -> xmlTODO ?loc x + | VernacResetInitial as x -> xmlTODO ?loc x + | VernacBack _ as x -> xmlTODO ?loc x + | VernacBackTo _ -> PCData "VernacBackTo" + + (* Commands *) + | VernacCreateHintDb _ as x -> xmlTODO ?loc x + | VernacRemoveHints _ as x -> xmlTODO ?loc x + | VernacHints _ as x -> xmlTODO ?loc x + | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) -> + let name = Id.to_string name in + let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in + xmlNotation ?loc attrs name [pp_expr ce] + | VernacDeclareImplicits _ as x -> xmlTODO ?loc x + | VernacArguments _ as x -> xmlTODO ?loc x + | VernacArgumentsScope _ as x -> xmlTODO ?loc x + | VernacReserve _ as x -> xmlTODO ?loc x + | VernacGeneralizable _ as x -> xmlTODO ?loc x + | VernacSetOpacity _ as x -> xmlTODO ?loc x + | VernacSetStrategy _ as x -> xmlTODO ?loc x + | VernacUnsetOption _ as x -> xmlTODO ?loc x + | VernacSetOption _ as x -> xmlTODO ?loc x + | VernacSetAppendOption _ as x -> xmlTODO ?loc x + | VernacAddOption _ as x -> xmlTODO ?loc x + | VernacRemoveOption _ as x -> xmlTODO ?loc x + | VernacMemOption _ as x -> xmlTODO ?loc x + | VernacPrintOption _ as x -> xmlTODO ?loc x + | VernacCheckMayEval (_,_,e) -> xmlCheck ?loc [pp_expr e] + | VernacGlobalCheck _ as x -> xmlTODO ?loc x + | VernacDeclareReduction _ as x -> xmlTODO ?loc x + | VernacPrint _ as x -> xmlTODO ?loc x + | VernacSearch _ as x -> xmlTODO ?loc x + | VernacLocate _ as x -> xmlTODO ?loc x + | VernacRegister _ as x -> xmlTODO ?loc x + | VernacComments (cl) -> + xmlComment ?loc (List.flatten (List.map pp_comment cl)) + + (* Stm backdoor *) + | VernacStm _ as x -> xmlTODO ?loc x + + (* Proof management *) + | VernacGoal _ as x -> xmlTODO ?loc x + | VernacAbort _ as x -> xmlTODO ?loc x + | VernacAbortAll -> PCData "VernacAbortAll" + | VernacRestart as x -> xmlTODO ?loc x + | VernacUndo _ as x -> xmlTODO ?loc x + | VernacUndoTo _ as x -> xmlTODO ?loc x + | VernacBacktrack _ as x -> xmlTODO ?loc x + | VernacFocus _ as x -> xmlTODO ?loc x + | VernacUnfocus as x -> xmlTODO ?loc x + | VernacUnfocused as x -> xmlTODO ?loc x + | VernacBullet _ as x -> xmlTODO ?loc x + | VernacSubproof _ as x -> xmlTODO ?loc x + | VernacEndSubproof as x -> xmlTODO ?loc x + | VernacShow _ as x -> xmlTODO ?loc x + | VernacCheckGuard as x -> xmlTODO ?loc x + | VernacProof (tac,using) -> + let tac = None (** FIXME *) in + let using = Option.map (xmlSectionSubsetDescr "using") using in + xmlProof ?loc (Option.List.(cons tac (cons using []))) + | VernacProofMode name -> xmlProofMode ?loc name + + (* Toplevel control *) + | VernacToplevelControl _ as x -> xmlTODO ?loc x + + (* For extension *) + | VernacExtend _ as x -> + xmlExtend ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + + (* Flags *) + | VernacProgram e -> xmlApply ?loc (Element("program",[],[]) :: [tmpp ?loc e]) + | VernacLocal (b,e) -> + xmlApply ?loc (Element("local",["flag",string_of_bool b],[]) :: + [tmpp ?loc e]) + +let tmpp ?loc v = + match tmpp ?loc v with + | Element("ltac",_,_) as x -> x + | xml -> xmlGallina ?loc [xml] diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml index 8254b1b802..c15c009887 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -14,7 +14,9 @@ type binding_kind = Explicit | Implicit type polymorphic = bool -type private_flag = bool +type private_flag = bool + +type cumulative_inductive_flag = bool type theorem_kind = | Theorem diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index cabd06735f..26a6db4ec9 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -336,7 +336,7 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * inline * (plident list * constr_expr) with_coercion list - | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 57b397e6f8..02c6a2c715 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -992,8 +992,8 @@ let compile_constant_body fail_on_error env univs = function let body = Mod_subst.force_constr sb in let instance_size = match univs with - | None -> 0 - | Some univ -> Univ.UContext.size univ + | Monomorphic_const _ -> 0 + | Polymorphic_const univ -> Univ.AUContext.size univ in match kind_of_term body with | Const (kn',u) when is_univ_copy instance_size u -> diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index c0f48641ce..48c2e45332 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -10,7 +10,7 @@ val compile : bool -> (* Fail on error with a nice user message, otherwise simpl (** init, fun, fv *) val compile_constant_body : bool -> - env -> constant_universes option -> constant_def -> body_code option + env -> constant_universes -> constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4deadff0a7..0008653644 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -153,8 +153,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * - bool * constant_universes * inline - * Context.Named.t option + constant_universes * inline * Context.Named.t option let on_body ml hy f = function | Undef _ as x -> x @@ -179,17 +178,21 @@ let cook_constr { Opaqueproof.modlist ; abstract } c = abstract_constant_body (expmod c) hyps let lift_univs cb subst = - if cb.const_polymorphic && not (Univ.LMap.is_empty subst) then - let inst = Univ.UContext.instance cb.const_universes in - let cstrs = Univ.UContext.constraints cb.const_universes in - let len = Univ.LMap.cardinal subst in - let subst = - Array.fold_left_i (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc) - subst (Univ.Instance.to_array inst) - in - let cstrs' = Univ.subst_univs_level_constraints subst cstrs in - subst, Univ.UContext.make (inst,cstrs') - else subst, cb.const_universes + match cb.const_universes with + | Monomorphic_const ctx -> subst, (Monomorphic_const ctx) + | Polymorphic_const auctx -> + if (Univ.LMap.is_empty subst) then + subst, (Polymorphic_const auctx) + else + let inst = Univ.AUContext.instance auctx in + let len = Univ.LMap.cardinal subst in + let subst = + Array.fold_left_i + (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc) + subst (Univ.Instance.to_array inst) + in + let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in + subst, (Polymorphic_const auctx') let cook_constant ~hcons env { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in @@ -243,15 +246,15 @@ let cook_constant ~hcons env { from = cb; info } = proj_eta = etab, etat; proj_type = ty'; proj_body = c' } in - let univs = - let abs' = - if cb.const_polymorphic then abs_ctx - else instantiate_univ_context abs_ctx - in - UContext.union abs' univs + let univs = + match univs with + | Monomorphic_const ctx -> + Monomorphic_const (UContext.union (instantiate_univ_context abs_ctx) ctx) + | Polymorphic_const auctx -> + Polymorphic_const (AUContext.union abs_ctx auctx) in (body, typ, Option.map projection cb.const_proj, - cb.const_polymorphic, univs, cb.const_inline_code, + univs, cb.const_inline_code, Some const_hyps) (* let cook_constant_key = Profile.declare_profile "cook_constant" *) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7d47eba23e..9db85a4a11 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -18,8 +18,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * - bool * constant_universes * inline - * Context.Named.t option + constant_universes * inline * Context.Named.t option val cook_constant : hcons:bool -> env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 71e228b19c..21651b3e21 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -64,7 +64,9 @@ type constant_def = | Def of constr Mod_subst.substituted (** or a transparent global definition *) | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) -type constant_universes = Univ.universe_context +type constant_universes = + | Monomorphic_const of Univ.universe_context + | Polymorphic_const of Univ.abstract_universe_context (** The [typing_flags] are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking @@ -83,7 +85,6 @@ type constant_body = { const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; - const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; @@ -168,6 +169,11 @@ type one_inductive_body = { mind_reloc_tbl : Cbytecodes.reloc_table; } +type abstract_inductive_universes = + | Monomorphic_ind of Univ.universe_context + | Polymorphic_ind of Univ.abstract_universe_context + | Cumulative_ind of Univ.abstract_cumulativity_info + type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) @@ -186,9 +192,7 @@ type mutual_inductive_body = { mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) - mind_polymorphic : bool; (** Is it polymorphic or not *) - - mind_universes : Univ.universe_context; (** Local universe variables and constraints *) + mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 0a822d6fad..72b4907680 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -45,9 +45,15 @@ let hcons_template_arity ar = (** {6 Constants } *) let instantiate cb c = - if cb.const_polymorphic then - Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c - else c + match cb.const_universes with + | Monomorphic_const _ -> c + | Polymorphic_const ctx -> + Vars.subst_instance_constr (Univ.AUContext.instance ctx) c + +let constant_is_polymorphic cb = + match cb.const_universes with + | Monomorphic_const _ -> false + | Polymorphic_const _ -> true let body_of_constant otab cb = match cb.const_body with | Undef _ -> None @@ -61,33 +67,56 @@ let type_of_constant cb = if t' == t then x else RegularArity t' | TemplateArity _ as x -> x -let constraints_of_constant otab cb = Univ.Constraint.union - (Univ.UContext.constraints cb.const_universes) - (match cb.const_body with - | Undef _ -> Univ.empty_constraint - | Def c -> Univ.empty_constraint - | OpaqueDef o -> - Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) +let constraints_of_constant otab cb = + match cb.const_universes with + | Polymorphic_const ctx -> + Univ.UContext.constraints (Univ.instantiate_univ_context ctx) + | Monomorphic_const ctx -> + Univ.Constraint.union + (Univ.UContext.constraints ctx) + (match cb.const_body with + | Undef _ -> Univ.empty_constraint + | Def c -> Univ.empty_constraint + | OpaqueDef o -> + Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) let universes_of_constant otab cb = match cb.const_body with - | Undef _ | Def _ -> cb.const_universes + | Undef _ | Def _ -> + begin + match cb.const_universes with + | Monomorphic_const ctx -> ctx + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + end | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints otab o in - assert(not cb.const_polymorphic || Univ.ContextSet.is_empty body_uctxs); - let uctxs = Univ.ContextSet.of_context cb.const_universes in - Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) + let body_uctxs = Opaqueproof.force_constraints otab o in + match cb.const_universes with + | Monomorphic_const ctx -> + let uctxs = Univ.ContextSet.of_context ctx in + Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) + | Polymorphic_const ctx -> + assert(Univ.ContextSet.is_empty body_uctxs); + Univ.instantiate_univ_context ctx let universes_of_polymorphic_constant otab cb = - if cb.const_polymorphic then - let univs = universes_of_constant otab cb in - Univ.instantiate_univ_context univs - else Univ.UContext.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.UContext.empty + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx let constant_has_body cb = match cb.const_body with | Undef _ -> false | Def _ | OpaqueDef _ -> true +let constant_polymorphic_instance cb = + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.AUContext.instance ctx + +let constant_polymorphic_context cb = + match cb.const_universes with + | Monomorphic_const _ -> Univ.UContext.empty + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Undef _ | Def _ -> false @@ -135,7 +164,6 @@ let subst_const_body sub cb = const_proj = proj'; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; - const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -166,11 +194,18 @@ let hcons_const_def = function Def (from_val (Term.hcons_constr constr)) | OpaqueDef _ as x -> x (* hashconsed when turned indirect *) +let hcons_const_universes cbu = + match cbu with + | Monomorphic_const ctx -> + Monomorphic_const (Univ.hcons_universe_context ctx) + | Polymorphic_const ctx -> + Polymorphic_const (Univ.hcons_abstract_universe_context ctx) + let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = hcons_const_type cb.const_type; - const_universes = Univ.hcons_universe_context cb.const_universes } + const_universes = hcons_const_universes cb.const_universes } (** {6 Inductive types } *) @@ -259,21 +294,36 @@ let subst_mind_body sub mib = mind_params_ctxt = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_polymorphic = mib.mind_polymorphic; mind_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_context mib = - if mib.mind_polymorphic then - Univ.instantiate_univ_context mib.mind_universes - else Univ.UContext.empty +let inductive_polymorphic_instance mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind ctx -> Univ.AUContext.instance ctx + | Cumulative_ind cumi -> + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + +let inductive_polymorphic_context mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.UContext.empty + | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx + | Cumulative_ind cumi -> + Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) + +let inductive_is_polymorphic mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> true + | Cumulative_ind cumi -> true + +let inductive_is_cumulative mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> false + | Cumulative_ind cumi -> true (** {6 Hash-consing of inductive declarations } *) @@ -301,11 +351,17 @@ let hcons_mind_packet oib = mind_user_lc = user; mind_nf_lc = nf } +let hcons_mind_universes miu = + match miu with + | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx) + | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx) + | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui) + let hcons_mind mib = { mib with mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; - mind_universes = Univ.hcons_universe_context mib.mind_universes } + mind_universes = hcons_mind_universes mib.mind_universes } (** {6 Stm machinery } *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 6650b6b7b0..811a28aa65 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -27,6 +27,12 @@ val subst_const_body : substitution -> constant_body -> constant_body val constant_has_body : constant_body -> bool +val constant_polymorphic_instance : constant_body -> universe_instance +val constant_polymorphic_context : constant_body -> universe_context + +(** Is the constant polymorphic? *) +val constant_is_polymorphic : constant_body -> bool + (** Accessing const_body, forcing access to opaque proof term if needed. Only use this function if you know what you're doing. *) @@ -66,8 +72,13 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body -val inductive_instance : mutual_inductive_body -> universe_instance -val inductive_context : mutual_inductive_body -> universe_context +val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance +val inductive_polymorphic_context : mutual_inductive_body -> universe_context + +(** Is the inductive polymorphic? *) +val inductive_is_polymorphic : mutual_inductive_body -> bool +(** Is the inductive cumulative? *) +val inductive_is_cumulative : mutual_inductive_body -> bool (** {6 Kernel flags} *) diff --git a/kernel/entries.mli b/kernel/entries.mli index 1e07c96909..f133587c16 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -34,6 +34,11 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; [mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]]. *) +type inductive_universes = + | Monomorphic_ind_entry of Univ.universe_context + | Polymorphic_ind_entry of Univ.universe_context + | Cumulative_ind_entry of Univ.cumulativity_info + type one_inductive_entry = { mind_entry_typename : Id.t; mind_entry_arity : constr; @@ -49,8 +54,9 @@ type mutual_inductive_entry = { mind_entry_finite : Decl_kinds.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; - mind_entry_polymorphic : bool; - mind_entry_universes : Univ.universe_context; + mind_entry_universes : inductive_universes; + (* universe constraints and the constraints for subtyping of + inductive types in the block. *) mind_entry_private : bool option; } diff --git a/kernel/environ.ml b/kernel/environ.ml index 5727bf2ea1..1ab5b7a8d1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -228,8 +228,10 @@ let add_constant kn cb env = add_constant_key kn cb no_link_info env let constraints_of cb u = - let univs = cb.const_universes in - Univ.subst_instance_constraints u (Univ.UContext.constraints univs) + match cb.const_universes with + | Monomorphic_const _ -> Univ.Constraint.empty + | Polymorphic_const ctx -> + Univ.UContext.constraints (Univ.subst_instance_context u ctx) let map_regular_arity f = function | RegularArity a as ar -> @@ -240,15 +242,23 @@ let map_regular_arity f = function (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then - let csts = constraints_of cb u in - (map_regular_arity (subst_instance_constr u) cb.const_type, csts) - else cb.const_type, Univ.Constraint.empty + match cb.const_universes with + | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty + | Polymorphic_const ctx -> + let csts = constraints_of cb u in + (map_regular_arity (subst_instance_constr u) cb.const_type, csts) + +let constant_instance env kn = + let cb = lookup_constant kn env in + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.AUContext.instance ctx let constant_context env kn = let cb = lookup_constant kn env in - if cb.const_polymorphic then cb.const_universes - else Univ.UContext.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.UContext.empty + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx type const_evaluation_result = NoBody | Opaque | IsProj @@ -259,10 +269,14 @@ let constant_value env (kn,u) = if cb.const_proj = None then match cb.const_body with | Def l_body -> - if cb.const_polymorphic then - let csts = constraints_of cb u in - (subst_instance_constr u (Mod_subst.force_constr l_body), csts) - else Mod_subst.force_constr l_body, Univ.Constraint.empty + begin + match cb.const_universes with + | Monomorphic_const _ -> + (Mod_subst.force_constr l_body, Univ.Constraint.empty) + | Polymorphic_const _ -> + let csts = constraints_of cb u in + (subst_instance_constr u (Mod_subst.force_constr l_body), csts) + end | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) else raise (NotEvaluableConst IsProj) @@ -273,7 +287,7 @@ let constant_opt_value env cst = let constant_value_and_type env (kn, u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then + if Declareops.constant_is_polymorphic cb then let cst = constraints_of cb u in let b' = match cb.const_body with | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body)) @@ -295,7 +309,7 @@ let constant_value_and_type env (kn, u) = (* constant_type gives the type of a constant *) let constant_type_in env (kn,u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then + if Declareops.constant_is_polymorphic cb then map_regular_arity (subst_instance_constr u) cb.const_type else cb.const_type @@ -321,7 +335,7 @@ let evaluable_constant kn env = | Undef _ -> false let polymorphic_constant cst env = - (lookup_constant cst env).const_polymorphic + Declareops.constant_is_polymorphic (lookup_constant cst env) let polymorphic_pconstant (cst,u) env = if Univ.Instance.is_empty u then false @@ -353,7 +367,7 @@ let is_projection cst env = let lookup_mind = lookup_mind let polymorphic_ind (mind,i) env = - (lookup_mind mind env).mind_polymorphic + Declareops.inductive_is_polymorphic (lookup_mind mind env) let polymorphic_pind (ind,u) env = if Univ.Instance.is_empty u then false diff --git a/kernel/environ.mli b/kernel/environ.mli index b7431dbe5f..ae3afcb355 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -161,6 +161,9 @@ val constant_value_and_type : env -> constant puniverses -> (** The universe context associated to the constant, empty if not polymorphic *) val constant_context : env -> constant -> Univ.universe_context +(** The universe isntance associated to the constant, empty if not + polymorphic *) +val constant_instance : env -> constant -> Univ.universe_instance (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant @@ -256,7 +259,7 @@ type unsafe_type_judgment = types punsafe_type_judgment (** {6 Compilation of global declaration } *) -val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option +val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option exception Hyp_not_found diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1e13239bfc..00fbe27a70 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -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,14 @@ 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 = + let process auctx = + subst_univs_level_instance substunivs (Univ.AUContext.instance auctx) + in + match aiu with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind acumi -> process (Univ.ACumulativityInfo.univ_context acumi) in let indsp = ((kn, 0), u) in let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in @@ -919,8 +990,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 +1005,6 @@ let check_inductive env kn mie = let chkpos = (Environ.typing_flags env).check_guarded in let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in (* Build the inductive packets *) - build_inductive env mie.mind_entry_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/inductive.ml b/kernel/inductive.ml index f3b03252db..e81a1cb587 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -54,9 +54,13 @@ let inductive_paramdecls (mib,u) = Vars.subst_instance_context u mib.mind_params_ctxt let instantiate_inductive_constraints mib u = - if mib.mind_polymorphic then - Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes) - else Univ.Constraint.empty + let process auctx = + Univ.UContext.constraints (Univ.subst_instance_context u auctx) + in + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Constraint.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) (************************************************************************) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 2f49982ce2..0813315b5b 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -41,5 +41,5 @@ Nativelibrary Safe_typing Vm Csymtable -Vconv Declarations +Vconv diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index ff44f0f540..79016735bc 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -74,12 +74,13 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = as long as they have the right type *) let uctx = Declareops.universes_of_constant (opaque_tables env) cb in let uctx = (* Context of the spec *) - if cb.const_polymorphic then - Univ.instantiate_univ_context uctx - else uctx + match cb.const_universes with + | Monomorphic_const _ -> uctx + | Polymorphic_const auctx -> + Univ.instantiate_univ_context auctx in let c', univs, ctx' = - if not cb.const_polymorphic then + if not (Declareops.constant_is_polymorphic cb) then let env' = Environ.push_context ~strict:true uctx env' in let env' = Environ.push_context ~strict:true ctx env' in let c',cst = match cb.const_body with @@ -92,7 +93,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = | Def cs -> let c' = Mod_subst.force_constr cs in c, Reduction.infer_conv env' (Environ.universes env') c c' - in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) + in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) else let cus, ccst = Univ.UContext.dest uctx in let newus, cst = Univ.UContext.dest ctx in @@ -122,21 +123,17 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = in if not (Univ.Constraint.is_empty cst) then error_incorrect_with_constraint lab; - let subst, ctx = Univ.abstract_universes true ctx in - Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty + let subst, ctx = Univ.abstract_universes ctx in + Vars.subst_univs_level_constr subst c, Polymorphic_const ctx, Univ.ContextSet.empty in let def = Def (Mod_subst.from_val c') in (* let ctx' = Univ.UContext.make (newus, cst) in *) - let univs = - if cb.const_polymorphic then Some cb.const_universes - else None - in let cb' = { cb with const_body = def; - const_universes = ctx ; + const_universes = univs ; const_body_code = Option.map Cemitcodes.from_val - (compile_constant_body env' univs def) } + (compile_constant_body env' cb.const_universes def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else diff --git a/kernel/modops.ml b/kernel/modops.ml index 1f8b97ae6a..33d13f1ba0 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -35,6 +35,7 @@ type signature_mismatch_error = | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField | NotConvertibleTypeField of env * types * types + | CumulativeStatusExpected of bool | PolymorphicStatusExpected of bool | NotSameConstructorNamesField | NotSameInductiveNameInBlockField @@ -327,12 +328,10 @@ let strengthen_const mp_from l cb resolver = |_ -> let kn = KerName.make2 mp_from l in let con = constant_of_delta_kn resolver kn in - let u = - if cb.const_polymorphic then - let u = Univ.UContext.instance cb.const_universes in - let s = Univ.make_instance_subst u in - Univ.subst_univs_level_instance s u - else Univ.Instance.empty + let u = + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.make_abstract_instance ctx in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); diff --git a/kernel/modops.mli b/kernel/modops.mli index e9f3db6e91..4b533c7efd 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -94,6 +94,7 @@ type signature_mismatch_error = | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField | NotConvertibleTypeField of env * types * types + | CumulativeStatusExpected of bool | PolymorphicStatusExpected of bool | NotSameConstructorNamesField | NotSameInductiveNameInBlockField diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d3cd6b62a5..4941d64d82 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1863,8 +1863,9 @@ let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with | None -> let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes - else Univ.Instance.empty + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.AUContext.instance ctx in begin match cb.const_body with | Def t -> @@ -1960,7 +1961,7 @@ let param_name = Name (id_of_string "params") let arg_name = Name (id_of_string "arg") let compile_mind prefix ~interactive mb mind stack = - let u = Declareops.inductive_instance mb in + let u = Declareops.inductive_polymorphic_instance mb in let f i stack ob = let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in let j = push_symbol (SymbInd (mind,i)) in diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 59e90ca2e9..3e15ff7401 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } + abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } type proofterm = (constr * Univ.universe_context_set) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 3897d5e51e..be1f4b13f0 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } + abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } (* The type has two caveats: 1) cook_constr is defined after diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b6786c045c..605e9f314c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -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,88 @@ 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.Instance.length + (Univ.AUContext.instance (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.UContext.constraints + (Univ.subst_instance_context 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.UContext.constraints + (Univ.subst_instance_context 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 +758,58 @@ 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.Instance.length + (Univ.AUContext.instance (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.UContext.constraints + (Univ.subst_instance_context 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.UContext.constraints + (Univ.subst_instance_context 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..b6d88c2b9b 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -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/safe_typing.ml b/kernel/safe_typing.ml index f5e8e86530..946222ef2f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -237,20 +237,29 @@ let private_con_of_scheme ~kind env cl = let universes_of_private eff = let open Declarations in - List.fold_left (fun acc { Entries.eff } -> - match eff with - | Entries.SEscheme (l,s) -> - List.fold_left (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (_, ctx) -> ctx :: acc in - if cb.const_polymorphic then acc - else (Univ.ContextSet.of_context cb.const_universes) :: acc) - acc l - | Entries.SEsubproof (c, cb, e) -> - if cb.const_polymorphic then acc - else Univ.ContextSet.of_context cb.const_universes :: acc) - [] (Term_typing.uniq_seff eff) + List.fold_left + (fun acc { Entries.eff } -> + match eff with + | Entries.SEscheme (l,s) -> + List.fold_left + (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc + in + match cb.const_universes with + | Monomorphic_const ctx -> + (Univ.ContextSet.of_context ctx) :: acc + | Polymorphic_const _ -> acc + ) + acc l + | Entries.SEsubproof (c, cb, e) -> + match cb.const_universes with + | Monomorphic_const ctx -> + (Univ.ContextSet.of_context ctx) :: acc + | Polymorphic_const _ -> acc + ) + [] (Term_typing.uniq_seff eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -373,7 +382,11 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in + let c,typ,univs = + match Term_typing.translate_local_def senv.revstruct senv.env id de with + | c, typ, Monomorphic_const ctx -> c, typ, ctx + | _, _, Polymorphic_const _ -> assert false + in let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with @@ -410,26 +423,28 @@ let labels_of_mib mib = get () let globalize_constant_universes env cb = - if cb.const_polymorphic then - [Now (true, Univ.ContextSet.empty)] - else - let cstrs = Univ.ContextSet.of_context cb.const_universes in - Now (false, cstrs) :: - (match cb.const_body with - | (Undef _ | Def _) -> [] - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with - | None -> [] - | Some fc -> + match cb.const_universes with + | Monomorphic_const ctx -> + let cstrs = Univ.ContextSet.of_context ctx in + Now (false, cstrs) :: + (match cb.const_body with + | (Undef _ | Def _) -> [] + | OpaqueDef lc -> + match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with + | None -> [] + | Some fc -> match Future.peek_val fc with - | None -> [Later fc] - | Some c -> [Now (false, c)]) + | None -> [Later fc] + | Some c -> [Now (false, c)]) + | Polymorphic_const _ -> + [Now (true, Univ.ContextSet.empty)] let globalize_mind_universes mb = - if mb.mind_polymorphic then - [Now (true, Univ.ContextSet.empty)] - else - [Now (false, Univ.ContextSet.of_context mb.mind_universes)] + match mb.mind_universes with + | Monomorphic_ind ctx -> + [Now (false, Univ.ContextSet.of_context ctx)] + | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)] + | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)] let constraints_of_sfb env sfb = match sfb with diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index f779f68be4..1bd9d6e495 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -90,6 +90,7 @@ let check_conv_error error why cst poly u f env a1 a2 = else error (IncompatiblePolymorphism (env, a1, a2)) else Constraint.union cst cst' with NotConvertible -> error why + | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e) (* for now we do not allow reorderings *) @@ -103,15 +104,21 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib | _ -> error (InductiveFieldExpected mib2) in - let poly = - if not (mib1.mind_polymorphic == mib2.mind_polymorphic) then - error (PolymorphicStatusExpected mib2.mind_polymorphic) - else mib2.mind_polymorphic - in - let u = - if poly then - CErrors.user_err Pp.(str "Checking of subtyping of polymorphic inductive types not implemented") - else Instance.empty + let u = + let process inst inst' = + if Univ.Instance.equal inst inst' then inst else error IncompatibleInstances + in + match mib1.mind_universes, mib2.mind_universes with + | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx, Polymorphic_ind auctx' -> + process + (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx') + | Cumulative_ind cumi, Cumulative_ind cumi' -> + process + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi')) + | _ -> error + (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2)) in let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name env t1 t2 = @@ -147,7 +154,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 error (NotConvertibleInductiveField name) | _ -> (s1, s2) in check_conv (NotConvertibleInductiveField name) - cst poly u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) + cst (inductive_is_polymorphic mib1) u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) in let check_packet cst p1 p2 = @@ -175,7 +182,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let check_cons_types i cst p1 p2 = Array.fold_left3 (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst - poly u infer_conv env t1 t2) + (inductive_is_polymorphic mib1) u infer_conv env t1 t2) cst p2.mind_consnames (arities_of_specif (mind,u) (mib1,p1)) @@ -292,37 +299,42 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let cb2 = Declareops.subst_const_body subst2 cb2 in (* Start by checking universes *) let poly = - if not (cb1.const_polymorphic == cb2.const_polymorphic) then - error (PolymorphicStatusExpected cb2.const_polymorphic) - else cb2.const_polymorphic + if not (Declareops.constant_is_polymorphic cb1 + == Declareops.constant_is_polymorphic cb2) then + error (PolymorphicStatusExpected (Declareops.constant_is_polymorphic cb2)) + else Declareops.constant_is_polymorphic cb2 in - let cst', env', u = - if poly then - let ctx1 = Univ.instantiate_univ_context cb1.const_universes in - let ctx2 = Univ.instantiate_univ_context cb2.const_universes in - let inst1, ctx1 = Univ.UContext.dest ctx1 in - let inst2, ctx2 = Univ.UContext.dest ctx2 in + let cst', env', u = + match cb1.const_universes, cb2.const_universes with + | Monomorphic_const _, Monomorphic_const _ -> + cst, env, Univ.Instance.empty + | Polymorphic_const auctx1, Polymorphic_const auctx2 -> + begin + let ctx1 = Univ.instantiate_univ_context auctx1 in + let ctx2 = Univ.instantiate_univ_context auctx2 in + let inst1, ctx1 = Univ.UContext.dest ctx1 in + let inst2, ctx2 = Univ.UContext.dest ctx2 in if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then error IncompatibleInstances else let cstrs = Univ.enforce_eq_instances inst1 inst2 cst in let cstrs = Univ.Constraint.union cstrs ctx2 in - try - (* The environment with the expected universes plus equality - of the body instances with the expected instance *) - let ctxi = Univ.Instance.append inst1 inst2 in - let ctx = Univ.UContext.make (ctxi, cstrs) in - let env = Environ.push_context ctx env in - (* Check that the given definition does not add any constraint over - the expected ones, so that it can be used in place of - the original. *) - if UGraph.check_constraints ctx1 (Environ.universes env) then - cstrs, env, inst2 - else error (IncompatibleConstraints ctx1) - with Univ.UniverseInconsistency incon -> - error (IncompatibleUniverses incon) - else - cst, env, Univ.Instance.empty + try + (* The environment with the expected universes plus equality + of the body instances with the expected instance *) + let ctxi = Univ.Instance.append inst1 inst2 in + let ctx = Univ.UContext.make (ctxi, cstrs) in + let env = Environ.push_context ctx env in + (* Check that the given definition does not add any constraint over + the expected ones, so that it can be used in place of + the original. *) + if UGraph.check_constraints ctx1 (Environ.universes env) then + cstrs, env, inst2 + else error (IncompatibleConstraints ctx1) + with Univ.UniverseInconsistency incon -> + error (IncompatibleUniverses incon) + end + | _ -> assert false in (* Now check types *) let typ1 = Typeops.type_of_constant_type env' cb1.const_type in @@ -353,7 +365,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "name.")); let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; - let u1 = inductive_instance mind1 in + let u1 = inductive_polymorphic_instance mind1 in let arity1,cst1 = constrained_type_of_inductive env ((mind1,mind1.mind_packets.(i)),u1) in let cst2 = @@ -370,7 +382,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "name.")); let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; - let u1 = inductive_instance mind1 in + let u1 = inductive_polymorphic_instance mind1 in let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in let cst2 = Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index bdfd00a8d3..5370bcea43 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -121,18 +121,19 @@ let inline_side_effects env body ctx side_eff = | OpaqueDef _, `Opaque (b,_) -> (b, true) | _ -> assert false in - if cb.const_polymorphic then - (** Inline the term to emulate universe polymorphism *) - let data = (Univ.UContext.instance cb.const_universes, b) in - let subst = Cmap_env.add c (Inl data) subst in - (subst, var, ctx, args) - else + match cb.const_universes with + | Monomorphic_const cnstctx -> (** Abstract over the term at the top of the proof *) let ty = Typeops.type_of_constant_type env cb.const_type in let subst = Cmap_env.add c (Inr var) subst in - let univs = Univ.ContextSet.of_context cb.const_universes in + let univs = Univ.ContextSet.of_context cnstctx in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) + | Polymorphic_const auctx -> + (** Inline the term to emulate universe polymorphism *) + let data = (Univ.AUContext.instance auctx, b) in + let subst = Cmap_env.add c (Inl data) subst in + (subst, var, ctx, args) in let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in (** Third step: inline the definitions *) @@ -225,16 +226,25 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:state_id Feedback.Complete) +let abstract_constant_universes abstract uctx = + if not abstract then + Univ.empty_level_subst, Monomorphic_const uctx + else + let sbst, auctx = Univ.abstract_universes uctx in + sbst, Polymorphic_const auctx + let infer_declaration ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in let j = infer env t in let abstract = poly && not (Option.is_empty kn) in - let usubst, univs = Univ.abstract_universes abstract uctx in + let usubst, univs = + abstract_constant_universes abstract uctx + in let c = Typeops.assumption_of_judgment env j in let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in - Undef nl, RegularArity t, None, poly, univs, false, ctx + Undef nl, RegularArity t, None, univs, false, ctx (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. @@ -264,9 +274,9 @@ let infer_declaration ~trust env kn dcl = feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in - def, RegularArity typ, None, c.const_entry_polymorphic, - c.const_entry_universes, - c.const_entry_inline_code, c.const_entry_secctx + def, RegularArity typ, None, + (Monomorphic_const c.const_entry_universes), + c.const_entry_inline_code, c.const_entry_secctx (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> @@ -279,7 +289,8 @@ let infer_declaration ~trust env kn dcl = let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = - Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in + abstract_constant_universes abstract (Univ.ContextSet.to_context ctx) + in let j = infer env body in let typ = match typ with | None -> @@ -298,8 +309,7 @@ let infer_declaration ~trust env kn dcl = else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; - def, typ, None, c.const_entry_polymorphic, - univs, c.const_entry_inline_code, c.const_entry_secctx + def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> let mib, _ = Inductive.lookup_mind_specif env (ind,0) in @@ -311,9 +321,16 @@ let infer_declaration ~trust env kn dcl = else assert false | _ -> assert false in + let univs = + match mib.mind_universes with + | Monomorphic_ind ctx -> Monomorphic_const ctx + | Polymorphic_ind auctx -> Polymorphic_const auctx + | Cumulative_ind acumi -> + Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) + in let term, typ = pb.proj_eta in Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, - mib.mind_polymorphic, mib.mind_universes, false, None + univs, false, None let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t @@ -337,7 +354,7 @@ let record_aux env s_ty s_bo suggested_expr = let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = +let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -409,9 +426,8 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) check declared inferred) lc) in let tps = let res = - let comp_univs = if poly then Some univs else None in match proj with - | None -> compile_constant_body env comp_univs def + | None -> compile_constant_body env univs def | Some pb -> (* The compilation of primitive projections is a bit tricky, because they refer to themselves (the body of p looks like fun c => @@ -425,14 +441,13 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_type = typ; const_proj = proj; const_body_code = None; - const_polymorphic = poly; const_universes = univs; const_inline_code = inline_code; const_typing_flags = Environ.typing_flags env; } in let env = add_constant kn cb env in - compile_constant_body env comp_univs def + compile_constant_body env univs def in Option.map Cemitcodes.from_val res in { const_hyps = hyps; @@ -440,7 +455,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_type = typ; const_proj = proj; const_body_code = tps; - const_polymorphic = poly; const_universes = univs; const_inline_code = inline_code; const_typing_flags = Environ.typing_flags env } @@ -452,6 +466,12 @@ let translate_constant mb env kn ce = (infer_declaration ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = + let poly, univs = + match cb.const_universes with + | Monomorphic_const ctx -> false, ctx + | Polymorphic_const auctx -> + true, Univ.instantiate_univ_context auctx + in let pt = match cb.const_body, u with | OpaqueDef _, `Opaque (b, c) -> b, c @@ -463,8 +483,8 @@ let constant_entry_of_side_effect cb u = const_entry_feedback = None; const_entry_type = (match cb.const_type with RegularArity t -> Some t | _ -> None); - const_entry_polymorphic = cb.const_polymorphic; - const_entry_universes = cb.const_universes; + const_entry_polymorphic = poly; + const_entry_universes = univs; const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } ;; @@ -508,16 +528,23 @@ let export_side_effects mb env ce = let trusted = check_signatures mb signatures in let push_seff env = function | kn, cb, `Nothing, _ -> - let env = Environ.add_constant kn cb env in - if not cb.const_polymorphic then - Environ.push_context ~strict:true cb.const_universes env - else env - | kn, cb, `Opaque(_, ctx), _ -> - let env = Environ.add_constant kn cb env in - if not cb.const_polymorphic then - let env = Environ.push_context ~strict:true cb.const_universes env in - Environ.push_context_set ~strict:true ctx env - else env in + begin + let env = Environ.add_constant kn cb env in + match cb.const_universes with + | Monomorphic_const ctx -> + Environ.push_context ~strict:true ctx env + | Polymorphic_const _ -> env + end + | kn, cb, `Opaque(_, ctx), _ -> + begin + let env = Environ.add_constant kn cb env in + match cb.const_universes with + | Monomorphic_const cstctx -> + let env = Environ.push_context ~strict:true cstctx env in + Environ.push_context_set ~strict:true ctx env + | Polymorphic_const _ -> env + end + in let rec translate_seff sl seff acc env = match sl, seff with | _, [] -> List.rev acc, ce @@ -553,7 +580,7 @@ let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) let translate_local_def mb env id centry = - let def,typ,proj,poly,univs,inline_code,ctx = + let def,typ,proj,univs,inline_code,ctx = infer_declaration ~trust:mb env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1a07bb2fc6..e08f3362db 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -555,7 +555,7 @@ let type_of_projection_constant env (p,u) = let cb = lookup_constant cst env in match cb.const_proj with | Some pb -> - if cb.const_polymorphic then + if Declareops.constant_is_polymorphic cb then Vars.subst_instance_constr u pb.proj_type else pb.proj_type | None -> raise (Invalid_argument "type_of_projection: not a projection") diff --git a/kernel/univ.ml b/kernel/univ.ml index d53dd8e733..8cbb20a051 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -725,8 +725,11 @@ struct pp_std ++ prl u1 ++ pr_constraint_type op ++ prl u2 ++ fnl () ) c (str "") + let universes_of c = + fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty end +let universes_of_constraints = Constraint.universes_of let empty_constraint = Constraint.empty let union_constraint = Constraint.union let eq_constraint = Constraint.equal @@ -1028,6 +1031,82 @@ end type universe_context = UContext.t let hcons_universe_context = UContext.hcons +module AUContext = UContext + +type abstract_universe_context = AUContext.t +let hcons_abstract_universe_context = AUContext.hcons + +(** Universe info for cumulative inductive types: + A context of universe levels + with universe constraints, representing local universe variables + and constraints, together with a context of universe levels with + universe constraints, representing conditions for subtyping used + 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 +1211,9 @@ let subst_univs_level_constraints subst csts = (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c)) csts Constraint.empty +let subst_univs_level_abstract_universe_context subst (inst, csts) = + inst, subst_univs_level_constraints subst csts + (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe @@ -1203,8 +1285,9 @@ let subst_instance_constraints s csts = let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) -let instantiate_univ_constraints u (_, csts) = - subst_instance_constraints u csts +(** Substitute instance inst for ctx in universe constraints and subtyping constraints *) +let instantiate_cumulativity_info (univcst, subtpcst) = + (instantiate_univ_context univcst, instantiate_univ_context subtpcst) let make_instance_subst i = let arr = Instance.to_array i in @@ -1218,16 +1301,22 @@ let make_inverse_instance_subst i = LMap.add (Level.var i) l acc) LMap.empty arr -let abstract_universes poly ctx = +let make_abstract_instance (ctx, _) = + Array.mapi (fun i l -> Level.var i) ctx + +let abstract_universes ctx = let instance = UContext.instance ctx in - if poly then - let subst = make_instance_subst instance in - let cstrs = subst_univs_level_constraints subst - (UContext.constraints ctx) - in - let ctx = UContext.make (instance, cstrs) in - subst, ctx - else empty_level_subst, ctx + let subst = make_instance_subst instance in + let cstrs = subst_univs_level_constraints subst + (UContext.constraints ctx) + in + let ctx = UContext.make (instance, cstrs) in + subst, ctx + +let abstract_cumulativity_info (univcst, substcst) = + let instance, univcst = abstract_universes univcst in + let _, substcst = abstract_universes substcst in + (instance, (univcst, substcst)) (** Pretty-printing *) @@ -1235,6 +1324,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 = @@ -1290,3 +1385,12 @@ let subst_instance_constraints = let key = Profile.declare_profile "subst_instance_constraints" in Profile.profile2 key subst_instance_constraints else subst_instance_constraints + +let subst_instance_context = + let subst_instance_context_body inst (inner_inst, inner_constr) = + (inner_inst, subst_instance_constraints inst inner_constr) + in + if Flags.profile then + let key = Profile.declare_profile "subst_instance_constraints" in + Profile.profile2 key subst_instance_context_body + else subst_instance_context_body diff --git a/kernel/univ.mli b/kernel/univ.mli index 1ccdebd501..ecc72701d4 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -315,6 +315,67 @@ end type universe_context = UContext.t +module AUContext : +sig + type t + + val empty : t + + val instance : t -> Instance.t + + val size : t -> int + + (** Keeps the order of the instances *) + val union : t -> t -> t + +end + +type abstract_universe_context = AUContext.t + +(** Universe info for inductive types: A context of universe levels + with universe constraints, representing local universe variables + and constraints, together with a context of universe levels with + 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 +426,8 @@ val is_empty_level_subst : universe_level_subst -> bool val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level val subst_univs_level_universe : universe_level_subst -> universe -> universe val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints +val subst_univs_level_abstract_universe_context : + universe_level_subst -> abstract_universe_context -> abstract_universe_context val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance (** Level to universe substitutions. *) @@ -379,23 +442,31 @@ val subst_univs_constraints : universe_subst_fn -> constraints -> constraints (** Substitution of instances *) val subst_instance_instance : universe_instance -> universe_instance -> universe_instance val subst_instance_universe : universe_instance -> universe -> universe -val subst_instance_constraints : universe_instance -> constraints -> constraints +val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context val make_instance_subst : universe_instance -> universe_level_subst val make_inverse_instance_subst : universe_instance -> universe_level_subst -val abstract_universes : bool -> universe_context -> universe_level_subst * universe_context +val abstract_universes : universe_context -> universe_level_subst * abstract_universe_context + +val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abstract_cumulativity_info + +val make_abstract_instance : abstract_universe_context -> universe_instance (** Get the instantiated graph. *) -val instantiate_univ_context : universe_context -> universe_context +val instantiate_univ_context : abstract_universe_context -> universe_context -val instantiate_univ_constraints : universe_instance -> universe_context -> constraints +(** Get the instantiated graphs for both universe constraints and subtyping constraints. *) +val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info (** {6 Pretty-printing of universes. } *) val pr_constraint_type : constraint_type -> Pp.std_ppcmds val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds +val pr_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> cumulativity_info -> Pp.std_ppcmds +val pr_abstract_universe_context : (Level.t -> Pp.std_ppcmds) -> abstract_universe_context -> Pp.std_ppcmds +val pr_abstract_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> abstract_cumulativity_info -> Pp.std_ppcmds val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> univ_inconsistency -> Pp.std_ppcmds @@ -409,7 +480,10 @@ val hcons_univ : universe -> universe val hcons_constraints : constraints -> constraints val hcons_universe_set : universe_set -> universe_set val hcons_universe_context : universe_context -> universe_context +val hcons_abstract_universe_context : abstract_universe_context -> abstract_universe_context val hcons_universe_context_set : universe_context_set -> universe_context_set +val hcons_cumulativity_info : cumulativity_info -> cumulativity_info +val hcons_abstract_cumulativity_info : abstract_cumulativity_info -> abstract_cumulativity_info (******) @@ -419,3 +493,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..baf8fa31f6 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -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/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/lib/envars.mli b/lib/envars.mli index edd13447fc..18b7676ce7 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -53,7 +53,7 @@ val coqroot : string the order it gets added to the search path. *) val coqpath : string list -(** [camlbin ()] is the path to the ocamlfind binary. *) +(** [camlfind ()] is the path to the ocamlfind binary. *) val ocamlfind : unit -> string (** [camlp4bin ()] is the path to the camlp4 binary. *) diff --git a/lib/flags.ml b/lib/flags.ml index 13539bced3..46bbba8e55 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -163,6 +163,10 @@ let use_polymorphic_flag () = let make_polymorphic_flag b = local_polymorphic_flag := Some b +let inductive_cumulativity = ref false +let make_inductive_cumulativity b = inductive_cumulativity := b +let is_inductive_cumulativity () = !inductive_cumulativity + (** [program_mode] tells that Program mode has been activated, either globally via [Set Program] or locally via the Program command prefix. *) diff --git a/lib/flags.mli b/lib/flags.mli index 0026aba2e3..5e78f0a041 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -119,6 +119,10 @@ val is_universe_polymorphism : unit -> bool val make_polymorphic_flag : bool -> unit val use_polymorphic_flag : unit -> bool +(** Global inductive cumulativity flag. *) +val make_inductive_cumulativity : bool -> unit +val is_inductive_cumulativity : unit -> bool + val warn : bool ref val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit diff --git a/library/declare.ml b/library/declare.ml index 7d0edbc8b3..db3dbcbd92 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -158,7 +158,7 @@ let cache_constant ((sp,kn), obj) = assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); let cst = Global.lookup_constant kn' in - add_section_constant cst.const_polymorphic kn' cst.const_hyps; + add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (constant_of_kn kn) obj.cst_kind @@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let kn' = Global.add_mind dir id mie in assert (eq_mind kn' (mind_of_kn kn)); let mind = Global.lookup_mind kn' in - add_section_kn mind.mind_polymorphic kn' mind.mind_hyps; + add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names @@ -351,11 +351,27 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_record = None; mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_polymorphic = false; - mind_entry_universes = Univ.UContext.empty; + mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty; mind_entry_private = None; }) +(* reinfer subtyping constraints for inductive after section is dischared. *) +let infer_inductive_subtyping (pth, mind_ent) = + match mind_ent.mind_entry_universes with + | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> + (pth, mind_ent) + | Cumulative_ind_entry cumi -> + begin + let env = Global.env () in + let env' = + Environ.push_context + (Univ.CumulativityInfo.univ_context cumi) env + in + (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) + let evd = Evd.from_env env' in + (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent) + end + type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry let inInductive : inductive_obj -> obj = @@ -365,7 +381,8 @@ let inInductive : inductive_obj -> obj = open_function = open_inductive; classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; - discharge_function = discharge_inductive } + discharge_function = discharge_inductive; + rebuild_function = infer_inductive_subtyping } let declare_projections mind = let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in diff --git a/library/global.ml b/library/global.ml index 1ba86699d3..6d80012f47 100644 --- a/library/global.ml +++ b/library/global.ml @@ -176,19 +176,14 @@ let type_of_global_unsafe r = Vars.subst_instance_constr (Univ.UContext.instance univs) ty | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let inst = - if mib.Declarations.mind_polymorphic then - Univ.UContext.instance mib.Declarations.mind_universes - else Univ.Instance.empty - in + let inst = Declareops.inductive_polymorphic_instance mib in Inductive.type_of_inductive env (specif, inst) | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let inst = Univ.UContext.instance mib.Declarations.mind_universes in - Inductive.type_of_constructor (cstr,inst) specif + let inst = Declareops.inductive_polymorphic_instance mib in + Inductive.type_of_constructor (cstr,inst) specif let type_of_global_in_context env r = - let open Declarations in match r with | VarRef id -> Environ.named_type id env, Univ.UContext.empty | ConstRef c -> @@ -199,21 +194,17 @@ let type_of_global_in_context env r = Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let univs = - if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes - else Univ.UContext.empty - in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs + let univs = Declareops.inductive_polymorphic_context mib in + Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let univs = - if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes - else Univ.UContext.empty - in - let inst = Univ.UContext.instance univs in - Inductive.type_of_constructor (cstr,inst) specif, univs + let (mib,oib as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + let univs = Declareops.inductive_polymorphic_context mib in + let inst = Univ.UContext.instance univs in + Inductive.type_of_constructor (cstr,inst) specif, univs let universes_of_global env r = - let open Declarations in match r with | VarRef id -> Univ.UContext.empty | ConstRef c -> @@ -222,10 +213,11 @@ let universes_of_global env r = (Environ.opaque_tables env) cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in - Univ.instantiate_univ_context mib.mind_universes + Declareops.inductive_polymorphic_context mib | ConstructRef cstr -> - let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Univ.instantiate_univ_context mib.mind_universes + let (mib,oib) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + Declareops.inductive_polymorphic_context mib let universes_of_global gr = universes_of_global (env ()) gr diff --git a/library/lib.ml b/library/lib.ml index f22f53eadf..8127316d73 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -402,7 +402,7 @@ let find_opening_node id = type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t +type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t @@ -465,9 +465,9 @@ let add_section_replacement f g poly hyps = let () = check_same_poly poly vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in - let subst, ctx = Univ.abstract_universes true ctx in + let subst, ctx = Univ.abstract_universes ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.UContext.instance ctx,args) exps, + sectab := (vars,f (Univ.AUContext.instance ctx,args) exps, g (sechyps,subst,ctx) abs)::sl let add_section_kn poly kn = diff --git a/library/lib.mli b/library/lib.mli index f47d6e1a58..284d339801 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -157,7 +157,7 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t +type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t val instance_from_variable_context : variable_context -> Names.Id.t array val named_of_variable_context : variable_context -> Context.Named.t diff --git a/library/library.mllib b/library/library.mllib index 6f433b77d1..d94fc22919 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,3 +1,4 @@ +Univops Nameops Libnames Globnames diff --git a/library/univops.ml b/library/univops.ml new file mode 100644 index 0000000000..60c12f0d81 --- /dev/null +++ b/library/univops.ml @@ -0,0 +1,79 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Term +open Univ +open Declarations + +let universes_of_constr c = + let rec aux s c = + match kind_of_term c with + | Const (_, u) | Ind (_, u) | Construct (_, u) -> + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> fold_constr aux s c + in aux LSet.empty c + +let universes_of_inductive mind = + let process auctx = + let u = Univ.AUContext.instance auctx in + let univ_of_one_ind oind = + let arity_univs = + Context.Rel.fold_outside + (fun decl unvs -> + Univ.LSet.union + (Context.Rel.Declaration.fold_constr + (fun cnstr unvs -> + let cnstr = Vars.subst_instance_constr u cnstr in + Univ.LSet.union + (universes_of_constr cnstr) unvs) + decl Univ.LSet.empty) unvs) + oind.mind_arity_ctxt ~init:Univ.LSet.empty + in + Array.fold_left (fun unvs cns -> + let cns = Vars.subst_instance_constr u cns in + Univ.LSet.union (universes_of_constr cns) unvs) arity_univs + oind.mind_nf_lc + in + let univs = + Array.fold_left + (fun unvs pk -> + Univ.LSet.union + (univ_of_one_ind pk) unvs + ) + Univ.LSet.empty mind.mind_packets + in + let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context auctx) in + let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in + univs + in + match mind.mind_universes with + | Monomorphic_ind _ -> LSet.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) + +let restrict_universe_context (univs,csts) s = + (* Universes that are not necessary to typecheck the term. + E.g. univs introduced by tactics and not used in the proof term. *) + let diff = LSet.diff univs s in + let rec aux diff candid univs ness = + let (diff', candid', univs', ness') = + Constraint.fold + (fun (l, d, r as c) (diff, candid, univs, csts) -> + if not (LSet.mem l diff) then + (LSet.remove r diff, candid, univs, Constraint.add c csts) + else if not (LSet.mem r diff) then + (LSet.remove l diff, candid, univs, Constraint.add c csts) + else (diff, Constraint.add c candid, univs, csts)) + candid (diff, Constraint.empty, univs, ness) + in + if ness' == ness then (LSet.diff univs diff', ness) + else aux diff' candid' univs' ness' + in aux diff csts univs Constraint.empty diff --git a/library/univops.mli b/library/univops.mli new file mode 100644 index 0000000000..5b499c75bc --- /dev/null +++ b/library/univops.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Term +open Univ +open Declarations + +(** Shrink a universe context to a restricted set of variables *) + +val universes_of_constr : constr -> universe_set +val universes_of_inductive : mutual_inductive_body -> universe_set +val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b605a44c87..dbd2fc4016 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -162,11 +162,16 @@ GEXTEND Gram | IDENT "Let"; id = identref; b = def_body -> VernacDefinition ((Some Discharge, Definition), (id, None), b) (* Gallina inductive declarations *) - | priv = private_token; f = finite_token; + | cum = cumulativity_token; priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in - let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (priv,f,indl) + let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in + let cum = + match cum with + Some b -> b + | None -> Flags.is_inductive_cumulativity () + in + VernacInductive (cum, priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -227,13 +232,16 @@ GEXTEND Gram r = universe_level -> (l, ord, r) ] ] ; finite_token: - [ [ "Inductive" -> (Inductive_kw,Finite) - | "CoInductive" -> (CoInductive,CoFinite) - | "Variant" -> (Variant,BiFinite) + [ [ IDENT "Inductive" -> (Inductive_kw,Finite) + | IDENT "CoInductive" -> (CoInductive,CoFinite) + | IDENT "Variant" -> (Variant,BiFinite) | IDENT "Record" -> (Record,BiFinite) | IDENT "Structure" -> (Structure,BiFinite) | IDENT "Class" -> (Class true,BiFinite) ] ] ; + cumulativity_token: + [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ] + ; private_token: [ [ IDENT "Private" -> true | -> false ] ] ; diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 0e2ca49000..db2af2be53 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1459,7 +1459,9 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite + with_full_print + (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1470,7 +1472,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1485,7 +1487,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index c75f7f868c..ba88563d3b 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -880,7 +880,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,pl,impls = Command.interp_mutual_inductive indl [] - false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in + false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index ee75d2908e..da21f64ab1 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -153,8 +153,8 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na ctx c = let open Term in - let vars = Universes.universes_of_constr c in - let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in + let vars = Univops.universes_of_constr c in + let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in mkConst(declare_constant (Id.of_string na) (DefinitionEntry (definition_entry ~opaque:true ~univs:(Univ.ContextSet.to_context ctx) c), diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 1bd03491a7..c7b37aba5c 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -43,7 +43,7 @@ let section_segment_of_reference = function | ConstRef con -> Lib.section_segment_of_constant con | IndRef (kn,_) | ConstructRef ((kn,_),_) -> Lib.section_segment_of_mutual_inductive kn - | _ -> [], Univ.LMap.empty, Univ.UContext.empty + | _ -> [], Univ.LMap.empty, Univ.AUContext.empty let discharge_rename_args = function | _, (ReqGlobal (c, names), _ as req) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3757ba7e6d..d84363089d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -350,6 +350,26 @@ let exact_ise_stack2 env evd f sk1 sk2 = ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) +let check_leq_inductives evd cumi u u' = + let u = EConstr.EInstance.kind evd u in + let u' = EConstr.EInstance.kind evd u' in + let length_ind_instance = + Univ.Instance.length + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + in + let ind_sbcst = 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 + begin + let comp_subst = (Univ.Instance.append u u') in + let comp_cst = + Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst) + in + Evd.add_constraints evd comp_cst + end + let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in @@ -439,16 +459,102 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let univs = EConstr.eq_constr_universes evd term term' in - match univs with - | Some univs -> - ise_and evd [(fun i -> - let cstrs = Universes.to_constraints (Evd.universes i) univs in - try Success (Evd.add_constraints i cstrs) - with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] - | None -> - UnifFailure (evd,NotSameHead) + let check_strict () = + let univs = EConstr.eq_constr_universes evd term term' in + match univs with + | Some univs -> + begin + let cstrs = Universes.to_constraints (Evd.universes evd) univs in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + end + | None -> + UnifFailure (evd, NotSameHead) + in + let first_try_strict_check cond u u' try_subtyping_constraints = + if cond then + let univs = EConstr.eq_constr_universes evd term term' in + match univs with + | Some univs -> + begin + let cstrs = Universes.to_constraints (Evd.universes evd) univs in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> try_subtyping_constraints () + end + | None -> + UnifFailure (evd, NotSameHead) + else + UnifFailure (evd, NotSameHead) + in + let compare_heads evd = + match EConstr.kind evd term, EConstr.kind evd term' with + | Const (c, u), Const (c', u') -> + check_strict () + | Ind (ind, u), Ind (ind', u') -> + let check_subtyping_constraints () = + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + begin + let mind = Environ.lookup_mind (fst ind) env in + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + UnifFailure (evd, NotSameHead) + | Declarations.Cumulative_ind cumi -> + begin + let num_param_arity = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + in + if not (num_param_arity = nparamsaplied + && num_param_arity = nparamsaplied') then + UnifFailure (evd, NotSameHead) + else + begin + let evd' = check_leq_inductives evd cumi u u' in + Success (check_leq_inductives evd' cumi u' u) + end + end + end + in + first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints + | Construct (cons, u), Construct (cons', u') -> + let check_subtyping_constraints () = + let ind, ind' = fst cons, fst cons' in + let j, j' = snd cons, snd cons' in + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + let mind = Environ.lookup_mind (fst ind) env in + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + UnifFailure (evd, NotSameHead) + | Declarations.Cumulative_ind cumi -> + begin + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + in + nparamsctxt + + mind.Declarations.mind_packets.(snd ind). + Declarations.mind_consnrealargs.(j - 1) + in + if not (num_cnstr_args = nparamsaplied + && num_cnstr_args = nparamsaplied') then + UnifFailure (evd, NotSameHead) + else + begin + let evd' = check_leq_inductives evd cumi u u' in + Success (check_leq_inductives evd' cumi u' u) + end + end + in + first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints + | _, _ -> anomaly (Pp.str "") + in + ise_and evd [(fun i -> + try compare_heads i + with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] in let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = let switch f a b = if on_left then f a b else f b a in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d8252ea9bb..2ae7c0f809 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -655,3 +655,93 @@ let control_only_guard env c = iter_constr_with_full_binders push_rel iter env c in iter env c + +(* inference of subtyping condition for inductive types *) + +let infer_inductive_subtyping_arity_constructor + (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) = + let numchecked = ref 0 in + let numparams = Context.Rel.nhyps params in + let update_contexts (env, evd, csts) csts' = + (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts') + in + let basic_check (env, evd, csts) tp = + let result = + if !numchecked >= numparams then + let csts' = + Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp) + in update_contexts (env, evd, csts) csts' + else + (env, evd, csts) + in + numchecked := !numchecked + 1; result + in + let infer_typ typ ctxs = + match typ with + | LocalAssum (_, typ') -> + begin + try + let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts) + with Reduction.NotConvertible -> + anomaly ~label:"inference of record/inductive subtyping relation failed" + (Pp.str "Can't infer subtyping for record/inductive type") + end + | _ -> anomaly (Pp.str "") + in + let arcn' = Term.it_mkProd_or_LetIn arcn params in + let typs, codom = Reduction.dest_prod env arcn' in + let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in + if not is_arity then basic_check last_contexts codom else last_contexts + +let infer_inductive_subtyping env evd mind_ent = + let { Entries.mind_entry_params = params; + Entries.mind_entry_inds = entries; + Entries.mind_entry_universes = ground_univs; + } = mind_ent + in + let uinfind = + match ground_univs with + | Entries.Monomorphic_ind_entry _ + | Entries.Polymorphic_ind_entry _ -> ground_univs + | Entries.Cumulative_ind_entry cumi -> + begin + let uctx = Univ.CumulativityInfo.univ_context cumi in + let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in + let dosubst = subst_univs_level_constr sbsubst 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 in + let env = Environ.push_context uctx_other env in + let evd = + Evd.merge_universe_context + evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) + in + let (_, _, subtyp_constraints) = + List.fold_left + (fun ctxs indentry -> + let _, params = Typeops.infer_local_decls env params in + let ctxs' = infer_inductive_subtyping_arity_constructor + ctxs dosubst indentry.Entries.mind_entry_arity true params + in + List.fold_left + (fun ctxs cons -> + infer_inductive_subtyping_arity_constructor + ctxs dosubst cons false params + ) + ctxs' indentry.Entries.mind_entry_lc + ) (env, evd, Univ.Constraint.empty) entries + in + Entries.Cumulative_ind_entry + (Univ.CumulativityInfo.make + (Univ.CumulativityInfo.univ_context cumi, + Univ.UContext.make + (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi), + subtyp_constraints))) + end + in {mind_ent with Entries.mind_entry_universes = uinfind;} diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index bdb6f996b9..811f47f39a 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -199,3 +199,12 @@ val type_of_inductive_knowing_conclusion : (********************) val control_only_guard : env -> types -> unit + +(* inference of subtyping condition for inductive types *) +(* for debugging purposes only to be removed *) +val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t -> +(Term.constr -> Term.constr) -> +Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t + +val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index bc9e3a1f46..283a1dcd18 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -197,7 +197,7 @@ let warn_projection_no_head_constant = (* Intended to always succeed *) let compute_canonical_projections warn (con,ind) = let env = Global.env () in - let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in + let ctx = Environ.constant_context env con in let u = Univ.UContext.instance ctx in let v = (mkConstU (con,u)) in let ctx = Univ.ContextSet.of_context ctx in @@ -298,8 +298,7 @@ let error_not_structure ref = let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in let env = Global.env () in - let ctx = Environ.constant_context env sp in - let u = Univ.UContext.instance ctx in + let u = Environ.constant_instance env sp in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c2a6483012..123c610166 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1313,8 +1313,8 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV -let report_anomaly _ = - let e = UserError (None, Pp.str "Conversion test raised an anomaly") in +let report_anomaly e = + let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in let e = CErrors.push e in iraise e @@ -1361,9 +1361,81 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible +let sigma_check_inductive_instances cv_pb uinfind u u' sigma = + let ind_instance = + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) + in + let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in + if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && + (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx) + in + let comp_cst = + match cv_pb with + Reduction.CONV -> + let comp_subst = (Univ.Instance.append u' u) in + let comp_cst' = + Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx) + in + Univ.Constraint.union comp_cst comp_cst' + | Reduction.CUMUL -> comp_cst + in + try Evd.add_constraints sigma comp_cst + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible + +let sigma_conv_inductives + cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Polymorphic_ind _ -> + raise Reduction.NotConvertible + | 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 + raise Reduction.NotConvertible + else + sigma_check_inductive_instances cv_pb cumi u1 u2 sigma + +let sigma_conv_constructors + (mind, ind, cns) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Polymorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Cumulative_ind cumi -> + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + nparamsctxt + + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) + in + if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then + raise Reduction.NotConvertible + else + sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma + let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances } + Reduction.compare_instances = sigma_compare_instances; + Reduction.conv_inductives = sigma_conv_inductives; + Reduction.conv_constructors = sigma_conv_constructors} let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index af4ea3ac53..a4da19de75 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -66,7 +66,6 @@ module Cst_stack : sig val pr : t -> Pp.std_ppcmds end - module Stack : sig type 'a app_node diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d7b4842810..f883e647b5 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -111,20 +111,16 @@ let new_instance cl info glob poly impl = let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes" let instances : instances ref = Summary.ref Refmap.empty ~name:"instances" -open Declarations - let typeclass_univ_instance (cl,u') = let subst = let u = match cl.cl_impl with | ConstRef c -> let cb = Global.lookup_constant c in - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes - else Univ.Instance.empty + Declareops.constant_polymorphic_instance cb | IndRef c -> let mib,oib = Global.lookup_inductive c in - if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes - else Univ.Instance.empty + Declareops.inductive_polymorphic_instance mib | _ -> Univ.Instance.empty in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b08666483e..9e151fea25 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -174,8 +174,7 @@ and nf_whd env sigma whd typ = | Vatom_stk(Aind ((mi,i) as ind), stk) -> let mib = Environ.lookup_mind mi env in let nb_univs = - if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes - else 0 + Univ.Instance.length (Declareops.inductive_polymorphic_instance mib) in let mk u = let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) @@ -204,8 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = | ConstKey cst -> let cbody = Environ.lookup_constant cst env in let nb_univs = - if cbody.const_polymorphic then Univ.UContext.size cbody.const_universes - else 0 + Univ.Instance.length (Declareops.constant_polymorphic_instance cbody) in let mk u = let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 9d28bc4f84..4a5cfe6301 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -727,7 +727,7 @@ open Decl_kinds let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in return (hov 2 (pr_assumption_token (n > 1) stre ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) - | VernacInductive (p,f,l) -> + | VernacInductive (cum, p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -754,13 +754,19 @@ open Decl_kinds in let key = let (_,_,_,k,_),_ = List.hd l in - match k with Record -> "Record" | Structure -> "Structure" - | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" | Variant -> "Variant" + let kind = + match k with Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class _ -> "Class" | Variant -> "Variant" + in + if p then + let cm = if cum then "Cumulative" else "NonCumulative" in + cm ^ " " ^ kind + else kind in return ( hov 1 (pr_oneind key (List.hd l)) ++ - (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) + (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) | VernacFixpoint (local, recs) -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 3ae7da8fc1..6d2bf6b73a 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -502,8 +502,8 @@ let ungeneralized_type_of_constant_type t = Typeops.type_of_constant_type (Global.env ()) t let print_instance sigma cb = - if cb.const_polymorphic then - pr_universe_instance sigma cb.const_universes + if Declareops.constant_is_polymorphic cb then + pr_universe_instance sigma (Declareops.constant_polymorphic_context cb) else mt() let print_constant with_values sep sp = @@ -511,16 +511,14 @@ let print_constant with_values sep sp = let val_0 = Global.body_of_constant_body cb in let typ = Declareops.type_of_constant cb in let typ = ungeneralized_type_of_constant_type typ in - let univs = Univ.instantiate_univ_context - (Global.universes_of_constant_body cb) - in + let univs = Global.universes_of_constant_body cb in let ctx = Evd.evar_universe_context_of_binders (Universes.universe_binders_of_global (ConstRef sp)) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in - hov 0 (pr_polymorphic cb.const_polymorphic ++ + hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++ match val_0 with | None -> str"*** [ " ++ diff --git a/printing/printer.ml b/printing/printer.ml index d6f0778f75..3b0b6d5d23 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -261,6 +261,14 @@ let pr_universe_ctx sigma c = else mt() +let pr_cumulativity_info sigma cumi = + if !Detyping.print_universes + && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi + else + mt() + (**********************************************************************) (* Global references *) @@ -991,6 +999,11 @@ let pr_assumptionset env s = let xor a b = (a && not b) || (not a && b) +let pr_cumulative poly cum = + if poly then + if cum then str "Cumulative " else str "NonCumulative " + else mt () + let pr_polymorphic b = let print = xor (Flags.is_universe_polymorphism ()) b in if print then diff --git a/printing/printer.mli b/printing/printer.mli index 3fce065613..f0a32bbbdf 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -95,8 +95,10 @@ val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds +val pr_cumulative : bool -> bool -> std_ppcmds val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds +val pr_cumulativity_info : evar_map -> Univ.cumulativity_info -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index c4affd4acd..08d177f53e 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -88,8 +88,8 @@ let build_ind_type env mip = Inductive.type_of_inductive env mip let print_one_inductive env sigma mib ((_,i) as ind) = - let u = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + let u = if Declareops.inductive_is_polymorphic mib then + Declareops.inductive_polymorphic_instance mib else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in @@ -99,8 +99,8 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in let inst = - if mib.mind_polymorphic then - Printer.pr_universe_instance sigma mib.mind_universes + if Declareops.inductive_is_polymorphic mib then + Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib) else mt () in hov 0 ( @@ -120,11 +120,18 @@ let print_mutual_inductive env mind mib = in let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in - hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ - def keyword ++ spc () ++ - prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env sigma mib) inds ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ + Printer.pr_cumulative + (Declareops.inductive_is_polymorphic mib) + (Declareops.inductive_is_cumulative mib) ++ + def keyword ++ spc () ++ + prlist_with_sep (fun () -> fnl () ++ str" with ") + (print_one_inductive env sigma mib) inds ++ + match mib.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> str "" + | Cumulative_ind cumi -> + Printer.pr_cumulativity_info + sigma (Univ.instantiate_cumulativity_info cumi)) let get_fields = let rec prodec_rec l subst c = @@ -141,8 +148,8 @@ let get_fields = let print_record env mind mib = let u = - if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + if Declareops.inductive_is_polymorphic mib then + Declareops.inductive_polymorphic_instance mib else Univ.Instance.empty in let mip = mib.mind_packets.(0) in @@ -164,7 +171,10 @@ let print_record env mind mib = in hov 0 ( hov 0 ( - Printer.pr_polymorphic mib.mind_polymorphic ++ + Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ + Printer.pr_cumulative + (Declareops.inductive_is_polymorphic mib) + (Declareops.inductive_is_cumulative mib) ++ def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ @@ -175,7 +185,12 @@ let print_record env mind mib = (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + match mib.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> str "" + | Cumulative_ind cumi -> + Printer.pr_cumulativity_info + sigma (Univ.instantiate_cumulativity_info cumi) + ) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then @@ -278,7 +293,8 @@ let print_body is_impl env mp (l,body) = | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + if Declareops.constant_is_polymorphic cb then + Declareops.constant_polymorphic_instance cb else Univ.Instance.empty in let sigma = Evd.empty in @@ -300,7 +316,8 @@ let print_body is_impl env mp (l,body) = Printer.pr_lconstr_env env sigma (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes)) + Printer.pr_universe_ctx sigma + (Declareops.constant_polymorphic_context cb)) | SFBmind mib -> try let env = Option.get env in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5ec34a6387..d5fbdbb830 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -336,15 +336,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let make_body = if poly || now then let make_body t (c, eff) = - let open Universes in let body = c in let typ = if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then nf t else t in - let used_univs_body = Universes.universes_of_constr body in - let used_univs_typ = Universes.universes_of_constr typ in + let used_univs_body = Univops.universes_of_constr body in + let used_univs_typ = Univops.universes_of_constr typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in @@ -353,7 +352,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx_body = restrict_universe_context ctx used_univs in + let ctx_body = Univops.restrict_universe_context ctx used_univs in (initunivs, typ), ((body, ctx_body), eff) else let initunivs = Univ.UContext.empty in @@ -362,7 +361,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now * constraints in which we merge the ones for the body and the ones * for the typ *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = restrict_universe_context ctx used_univs in + let ctx = Univops.restrict_universe_context ctx used_univs in let univs = Univ.ContextSet.to_context ctx in (univs, typ), ((body, Univ.ContextSet.empty), eff) in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 471e05e458..87d9e411a7 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -142,7 +142,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in VtSideff ids, VtLater | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,l) -> + | VernacInductive (_, _,_,l) -> let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2faf1e0ecb..5fbf59b815 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -649,8 +649,9 @@ module V85 = struct Goal.V82.hyps gls.Evd.sigma (sig_it gls) let make_autogoal_hints = - let cache = ref (true, Environ.empty_named_context_val, - Hint_db.empty full_transparent_state true) + let cache = Summary.ref ~name:"make_autogoal_hints_cache" + (true, Environ.empty_named_context_val, + Hint_db.empty full_transparent_state true) in fun only_classes ?(st=full_transparent_state) g -> let sign = pf_filtered_hyps g in @@ -979,8 +980,9 @@ module Search = struct search_hints : hint_db; } (** Local hints *) - let autogoal_cache = ref (DirPath.empty, true, Context.Named.empty, - Hint_db.empty full_transparent_state true) + let autogoal_cache = Summary.ref ~name:"autogoal_cache" + (DirPath.empty, true, Context.Named.empty, + Hint_db.empty full_transparent_state true) let make_autogoal_hints only_classes ?(st=full_transparent_state) g = let open Proofview in diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 466b1350d9..99761437eb 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -47,7 +47,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = (nf c', Evd.evar_universe_context sigma), eff else let mib,mip = Inductive.lookup_mind_specif env ind in - let ctx = Declareops.inductive_context mib in + let ctx = Declareops.inductive_polymorphic_context mib in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in @@ -60,7 +60,7 @@ let build_induction_scheme_in_type dep sort ind = let sigma = Evd.from_env env in let ctx = let mib,mip = Inductive.lookup_mind_specif env ind in - Declareops.inductive_context mib + Declareops.inductive_polymorphic_context mib in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in @@ -80,30 +80,30 @@ let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants) -let ind_scheme_kind_from_type = - declare_individual_scheme_object "_ind_nodep" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp) - -let ind_scheme_kind_from_prop = - declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" - (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp) - -let ind_dep_scheme_kind_from_type = - declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp) +let rec_scheme_kind_from_type = + declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) -let rec_scheme_kind_from_type = - declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) - let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) +let ind_scheme_kind_from_type = + declare_individual_scheme_object "_ind_nodep" + (optimize_non_type_induction_scheme rec_scheme_kind_from_type false InProp) + +let ind_dep_scheme_kind_from_type = + declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" + (optimize_non_type_induction_scheme rec_dep_scheme_kind_from_type true InProp) + +let ind_scheme_kind_from_prop = + declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" + (optimize_non_type_induction_scheme rec_scheme_kind_from_prop false InProp) + (* Case analysis *) let build_case_analysis_scheme_in_type dep sort ind = diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index 77f927f2df..da432beadc 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -10,6 +10,14 @@ open Ind_tables (** Induction/recursion schemes *) +val optimize_non_type_induction_scheme : + 'a Ind_tables.scheme_kind -> + Indrec.dep_flag -> + Term.sorts_family -> + 'b -> + Names.inductive -> + (Constr.constr * Evd.evar_universe_context) * Safe_typing.private_constants + val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind val rec_scheme_kind_from_prop : individual scheme_kind diff --git a/tactics/hints.ml b/tactics/hints.ml index 681db5d08e..2fc8baa895 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1306,7 +1306,8 @@ let interp_hints poly = List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in - empty_hint_info, mib.Declarations.mind_polymorphic, true, + empty_hint_info, + (Declareops.inductive_is_polymorphic mib), true, PathHints [gr], IsGlobRef gr) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index e3b5e94356..672fb3f131 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -41,6 +41,8 @@ Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function Open Scope function_scope. +Set Printing Universes. Set Printing All. + Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. @@ -156,7 +158,8 @@ Delimit Scope morphism_scope with morphism. Delimit Scope category_scope with category. Delimit Scope object_scope with object. - +Set Printing Universes. +Set Printing All. Record PreCategory := Build_PreCategory' { object :> Type; @@ -1069,7 +1072,7 @@ Section Adjunction. Variable F : Functor C D. Variable G : Functor D C. - Let Adjunction_Type := + Let Adjunction_Type := Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G). Record AdjunctionHom := diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v index 6a5e9a4023..403c2d2026 100644 --- a/test-suite/bugs/closed/4366.v +++ b/test-suite/bugs/closed/4366.v @@ -10,6 +10,6 @@ end. Goal True. Proof. pose (v := stupid 24). -Timeout 2 vm_compute in v. +Timeout 4 vm_compute in v. exact I. Qed. diff --git a/test-suite/bugs/closed/5578.v b/test-suite/bugs/closed/5578.v new file mode 100644 index 0000000000..5bcdaa2f18 --- /dev/null +++ b/test-suite/bugs/closed/5578.v @@ -0,0 +1,57 @@ +(* File reduced by coq-bug-finder from original input, then from 1549 lines to 298 lines, then from 277 lines to 133 lines, then from 985 lines to 138 lines, then from 206 lines to 139 lines, then from 203 lines to 142 lines, then from 262 lines to 152 lines, then from 567 lines to 151 lines, then from 3746 lines to 151 lines, then from 577 lines to 151 lines, then from 187 lines to 151 lines, thenfrom 981 lines to 940 lines, then from 938 lines to 175 lines, then from 589 lines to 205 lines, then from 3797 lines to 205 lines, then from 628 lines to 206 lines, then from 238 lines to 205 lines, then from 1346 lines to 213 lines, then from 633 lines to 214 lines, then from 243 lines to 213 lines, then from 5656 lines to 245 lines, then from 661 lines to 272 lines, then from 3856 lines to 352 lines, then from 1266 lines to 407 lines, then from 421 lines to 406 lines, then from 424 lines to 91 lines, then from 105 lines to 91 lines, then from 85 lines to 55 lines, then from 69 lines to 55 lines *) +(* coqc version trunk (May 2017) compiled on May 30 2017 13:28:59 with OCaml +4.02.3 + coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-trunk,trunk (fd36c0451c26e44b1b7e93299d3367ad2d35fee3) *) + +Class Proper {A} (R : A -> A -> Prop) (m : A) := mkp : R m m. +Definition respectful {A B} (R : A -> A -> Prop) (R' : B -> B -> Prop) (f g : A -> B) := forall x y, R x y -> R' (f x) (g y). +Set Implicit Arguments. + +Class EqDec (A : Set) := { + eqb : A -> A -> bool ; + eqb_leibniz : forall x y, eqb x y = true <-> x = y +}. + +Infix "?=" := eqb (at level 70) : eq_scope. + +Inductive Comp : Set -> Type := +| Bind : forall (A B : Set), Comp B -> (B -> Comp A) -> Comp A. + +Open Scope eq_scope. + +Goal forall (Rat : Set) (PositiveMap_t : Set -> Set) + type (t : type) (interp_type_list_message interp_type_rand interp_type_message : nat -> Set), + (forall eta : nat, PositiveMap_t (interp_type_rand eta) -> interp_type_list_message eta -> interp_type_message eta) -> + ((nat -> Rat) -> Prop) -> + forall (interp_type_sbool : nat -> Set) (interp_type0 : type -> nat -> Set), + (forall eta : nat, + (interp_type_list_message eta -> interp_type_message eta) -> PositiveMap_t (interp_type_rand eta) -> interp_type0 t eta) + -> (forall (t0 : type) (eta : nat), EqDec (interp_type0 t0 eta)) + -> (bool -> Comp bool) -> False. + clear. + intros Rat PositiveMap_t type t interp_type_list_message interp_type_rand interp_type_message adv negligible interp_type_sbool + interp_type interp_term_fixed_t_x + EqDec_interp_type ret_bool. + assert (forall f adv' k + (lem : forall (eta : nat) (evil_rands rands : PositiveMap_t +(interp_type_rand eta)), + (interp_term_fixed_t_x eta (adv eta evil_rands) rands + ?= interp_term_fixed_t_x eta (adv eta evil_rands) rands) = true), + (forall (eta : nat), Proper (respectful eq eq) (f eta)) + -> negligible + (fun eta : nat => + f eta ( + (Bind (k eta) (fun rands => + ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))). + Undo. + assert (forall f adv' k + (lem : forall (eta : nat) (rands : PositiveMap_t +(interp_type_rand eta)), + (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands) = true), + (forall (eta : nat), Proper (respectful eq eq) (f eta)) + -> negligible + (fun eta : nat => + f eta ( + (Bind (k eta) (fun rands => + ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))). + (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *)
\ No newline at end of file diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v new file mode 100644 index 0000000000..a978f6b901 --- /dev/null +++ b/test-suite/coqchk/cumulativity.v @@ -0,0 +1,67 @@ +Set Universe Polymorphism. +Set Inductive Cumulativity. +Set Printing Universes. + +Inductive List (A: Type) := nil | cons : A -> List A -> List A. + +Section ListLift. + Universe i j. + + Constraint i < j. + + Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. + +End ListLift. + +Lemma LiftL_Lem A (l : List A) : l = LiftL l. +Proof. reflexivity. Qed. + +Section ListLower. + Universe i j. + + Constraint i < j. + + Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. + +End ListLower. + +Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. +Proof. reflexivity. Qed. +(* +I disable these tests because cqochk can't process them when compiled with + ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis! + + I have added this file (including the commented parts below) in + test-suite/success/cumulativity.v which doesn't run coqchk on them. +*) +(* Inductive Tp := tp : Type -> Tp. *) + +(* Section TpLift. *) +(* Universe i j. *) + +(* Constraint i < j. *) + +(* Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. *) + +(* End TpLift. *) + +(* Lemma LiftC_Lem (t : Tp) : LiftTp t = t. *) +(* Proof. reflexivity. Qed. *) + +(* Section TpLower. *) +(* Universe i j. *) + +(* Constraint i < j. *) + +(* Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. *) + +(* End TpLower. *) + + +(* Section subtyping_test. *) +(* Universe i j. *) +(* Constraint i < j. *) + +(* Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *) + +(* End subtyping_test. *)
\ No newline at end of file diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v new file mode 100644 index 0000000000..ebf817cfc5 --- /dev/null +++ b/test-suite/success/cumulativity.v @@ -0,0 +1,65 @@ +Set Universe Polymorphism. +Set Inductive Cumulativity. +Set Printing Universes. + +Inductive List (A: Type) := nil | cons : A -> List A -> List A. + +Section ListLift. + Universe i j. + + Constraint i < j. + + Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. + +End ListLift. + +Lemma LiftL_Lem A (l : List A) : l = LiftL l. +Proof. reflexivity. Qed. + +Section ListLower. + Universe i j. + + Constraint i < j. + + Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. + +End ListLower. + +Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. +Proof. reflexivity. Qed. + +Inductive Tp := tp : Type -> Tp. + +Section TpLift. + Universe i j. + + Constraint i < j. + + Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. + +End TpLift. + +Lemma LiftC_Lem (t : Tp) : LiftTp t = t. +Proof. reflexivity. Qed. + +Section TpLower. + Universe i j. + + Constraint i < j. + + Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. + +End TpLower. + + +Section subtyping_test. + Universe i j. + Constraint i < j. + + Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. + +End subtyping_test. + +Record A : Type := { a :> Type; }. + +Record B (X : A) : Type := { b : X; }.
\ No newline at end of file diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 66ff55edcb..ecc988507c 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -352,3 +352,35 @@ Module Anonymous. Check collapsethemiddle@{_ _}. End Anonymous. + +Module F. + Context {A B : Type}. + Definition foo : Type := B. +End F. + +Set Universe Polymorphism. + +Cumulative Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }. + +Section test_letin_subtyping. + Universe i j k i' j' k'. + Constraint j < j'. + + Context (W : Type) (X : box@{i j k} W). + Definition Y := X : box@{i' j' k'} W. + + Universe i1 j1 k1 i2 j2 k2. + Constraint i1 < i2. + Constraint k2 < k1. + Context (V : Type). + + Definition Z : box@{i1 j1 k1} V := {| unwrap := V |}. + Definition Z' : box@{i2 j2 k2} V := {| unwrap := V |}. + Lemma ZZ' : @eq (box@{i2 j2 k2} V) Z Z'. + Proof. + Set Printing All. Set Printing Universes. + cbv. + reflexivity. + Qed. + +End test_letin_subtyping. diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 92730c14d0..74c7663ca5 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -286,7 +286,12 @@ let ensure_exists f = let compile verbosely f = let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in - if not (List.is_empty pfs) then vernac_error (str "There are pending proofs") + if not (List.is_empty pfs) then + vernac_error (str "There are pending proofs: " + ++ (pfs + |> List.rev + |> prlist_with_sep pr_comma Names.Id.print) + ++ str ".") in match !Flags.compilation_mode with | BuildVo -> diff --git a/vernac/classes.ml b/vernac/classes.ml index aba61146c7..007b70bc0f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -114,8 +114,8 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id pl poly evm term termtype = let kind = IsDefinition Instance in let evm = - let levels = Univ.LSet.union (Universes.universes_of_constr termtype) - (Universes.universes_of_constr term) in + let levels = Univ.LSet.union (Univops.universes_of_constr termtype) + (Univops.universes_of_constr term) in Evd.restrict_universe_context evm levels in let pl, uctx = Evd.universe_context ?names:pl evm in @@ -420,6 +420,8 @@ let context poly l = let _ = Command.declare_definition id decl entry [] [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in - let () = uctx := Univ.ContextSet.empty in status && nstatus - in List.fold_left fn true (List.rev ctx) + in + if Lib.sections_are_opened () then + Declare.declare_universe_context poly !uctx; + List.fold_left fn true (List.rev ctx) diff --git a/vernac/command.ml b/vernac/command.ml index 998e7803e1..4064773561 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -106,7 +106,7 @@ let interp_definition pl bl p red_option c ctypopt = let c = EConstr.Unsafe.to_constr c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = Universes.universes_of_constr body in + let vars = Univops.universes_of_constr body in let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in imps1@(Impargs.lift_implicits nb_args imps2), pl, @@ -131,8 +131,8 @@ let interp_definition pl bl p red_option c ctypopt = in if not (try List.for_all chk imps2 with Not_found -> false) then warn_implicits_in_term (); - let vars = Univ.LSet.union (Universes.universes_of_constr body) - (Universes.universes_of_constr typ) in + let vars = Univ.LSet.union (Univops.universes_of_constr body) + (Univops.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl ctx in imps1@(Impargs.lift_implicits nb_args impsty), pl, @@ -329,7 +329,7 @@ let do_assumptions_bound_univs coe kind nl id pl c = let nf, subst = Evarutil.e_nf_evars_and_universes evdref in let ty = EConstr.Unsafe.to_constr ty in let ty = nf ty in - let vars = Universes.universes_of_constr ty in + let vars = Univops.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in let uctx = Univ.ContextSet.of_context uctx in @@ -573,7 +573,7 @@ let check_param = function | CLocalAssum (nas, Generalized _, _) -> () | CLocalPattern _ -> assert false -let interp_mutual_inductive (paramsl,indl) notations poly prv finite = +let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = check_all_names_different indl; List.iter check_param paramsl; let env0 = Global.env() in @@ -649,16 +649,27 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in + let univs = + if poly then + if cum then + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) + else Polymorphic_ind_entry uctx + else + Monomorphic_ind_entry uctx + in (* Build the mutual inductive entry *) - { mind_entry_params = List.map prepare_param ctx_params; - mind_entry_record = None; - mind_entry_finite = finite; - mind_entry_inds = entries; - mind_entry_polymorphic = poly; - mind_entry_private = if prv then Some false else None; - mind_entry_universes = uctx; - }, - pl, impls + let mind_ent = + { mind_entry_params = List.map prepare_param ctx_params; + mind_entry_record = None; + mind_entry_finite = finite; + mind_entry_inds = entries; + mind_entry_private = if prv then Some false else None; + mind_entry_universes = univs; + } + in + (if poly && cum then + Inductiveops.infer_inductive_subtyping env_ar evd mind_ent + else mind_ent), pl, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -742,10 +753,10 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -let do_mutual_inductive indl poly prv finite = +let do_mutual_inductive indl cum poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in + let mie,pl,impls = interp_mutual_inductive indl ntns cum poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) @@ -1208,7 +1219,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in + let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in @@ -1240,7 +1251,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Universes.universes_of_constr (List.hd fixdecls) in + let vars = Univops.universes_of_constr (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in diff --git a/vernac/command.mli b/vernac/command.mli index 2a52d9bcb5..a636bc03c5 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -90,9 +90,9 @@ type one_inductive_impls = Impargs.manual_implicits list (** for constrs *) val interp_mutual_inductive : - structured_inductive_expr -> decl_notation list -> polymorphic -> - private_flag -> Decl_kinds.recursivity_kind -> - mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list + structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> + polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> + mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list (** Registering a mutual inductive definition together with its associated schemes *) @@ -104,8 +104,8 @@ val declare_mutual_inductive_with_eliminations : (** Entry points for the vernacular commands Inductive and CoInductive *) val do_mutual_inductive : - (one_inductive_expr * decl_notation list) list -> polymorphic -> - private_flag -> Decl_kinds.recursivity_kind -> unit + (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> + polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit (** {6 Fixpoints and cofixpoints} *) diff --git a/vernac/discharge.ml b/vernac/discharge.ml index 65ade78876..18f93334b1 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -79,12 +79,14 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let process_inductive (sechyps,abs_ctx) modlist mib = let nparams = mib.mind_nparams in - let subst, univs = - if mib.mind_polymorphic then - let inst = Univ.UContext.instance mib.mind_universes in - let cstrs = Univ.UContext.constraints mib.mind_universes in - inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) - else Univ.Instance.empty, mib.mind_universes + let subst, univs = + match mib.mind_universes with + | Monomorphic_ind ctx -> Univ.Instance.empty, ctx + | Polymorphic_ind auctx -> + Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx + | Cumulative_ind cumi -> + let auctx = Univ.ACumulativityInfo.univ_context cumi in + Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx in let inds = Array.map_to_list @@ -105,6 +107,12 @@ let process_inductive (sechyps,abs_ctx) modlist mib = let (params',inds') = abstract_inductive sechyps' nparams inds in let abs_ctx = Univ.instantiate_univ_context abs_ctx in let univs = Univ.UContext.union abs_ctx univs in + let ind_univs = + match mib.mind_universes with + | Monomorphic_ind _ -> Monomorphic_ind_entry univs + | Polymorphic_ind _ -> Polymorphic_ind_entry univs + | Cumulative_ind _ -> + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) in let record = match mib.mind_record with | Some (Some (id, _, _)) -> Some (Some id) | Some None -> Some None @@ -114,7 +122,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_finite = mib.mind_finite; mind_entry_params = params'; mind_entry_inds = inds'; - mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; - mind_entry_universes = univs; + mind_entry_universes = ind_univs } + diff --git a/vernac/discharge.mli b/vernac/discharge.mli index 18d1b67766..3845c04a11 100644 --- a/vernac/discharge.mli +++ b/vernac/discharge.mli @@ -11,4 +11,5 @@ open Entries open Opaqueproof val process_inductive : - Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry + ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context) + -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 6d8dd82ac6..ce91e1a09f 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -889,6 +889,10 @@ let explain_not_match_error = function | NoTypeConstraintExpected -> strbrk "a definition whose type is constrained can only be subtype " ++ strbrk "of a definition whose type is itself constrained" + | CumulativeStatusExpected b -> + let status b = if b then str"cumulative" else str"non-cumulative" in + str "a " ++ status b ++ str" declaration was expected, but a " ++ + status (not b) ++ str" declaration was found" | PolymorphicStatusExpected b -> let status b = if b then str"polymorphic" else str"monomorphic" in str "a " ++ status b ++ str" declaration was expected, but a " ++ diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml index f3259f1f3b..65d42b6267 100644 --- a/vernac/ind_tables.ml +++ b/vernac/ind_tables.ml @@ -148,7 +148,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define mode id c mib.mind_polymorphic ctx in + let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in declare_scheme kind [|ind,const|]; const, Safe_typing.add_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff @@ -166,7 +166,7 @@ let define_mutual_scheme_base kind suff f mode names mind = try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in let consts = Array.map2 (fun id cl -> - define mode id cl mib.mind_polymorphic ctx) ids cl in + define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e03e9b8039..135e4c63ab 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -365,8 +365,8 @@ let get_body obl = match obl.obl_body with | None -> None | Some (DefinedObl c) -> - let ctx = Environ.constant_context (Global.env ()) c in - let pc = (c, Univ.UContext.instance ctx) in + let u = Environ.constant_instance (Global.env ()) c in + let pc = (c, u) in Some (DefinedObl pc) | Some (TermObl c) -> Some (TermObl c) diff --git a/vernac/record.ml b/vernac/record.ml index 2400fa6814..7dd70d0133 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -265,10 +265,16 @@ let warn_non_primitive_record = let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in - let u = Declareops.inductive_instance mib in + let u = Declareops.inductive_polymorphic_instance mib in let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let poly = mib.mind_polymorphic in - let ctx = Univ.instantiate_univ_context mib.mind_universes in + let poly = Declareops.inductive_is_polymorphic mib in + let ctx = + match mib.mind_universes with + | Monomorphic_ind ctx -> ctx + | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx + | Cumulative_ind cumi -> + Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) + in let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in @@ -377,12 +383,18 @@ let structure_signature ctx = open Typeclasses -let declare_structure finite poly ctx id idbuild paramimpls params arity template +let declare_structure finite univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in + let poly, ctx = + match univs with + | Monomorphic_ind_entry ctx -> false, ctx + | Polymorphic_ind_entry ctx -> true, ctx + | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi) + in let binder_name = match name with | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) @@ -400,11 +412,22 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat mind_entry_record = Some (if !primitive_flag then Some binder_name else None); mind_entry_finite = finite; mind_entry_inds = [mie_ind]; - mind_entry_polymorphic = poly; mind_entry_private = None; - mind_entry_universes = ctx; + mind_entry_universes = univs; } in + let mie = + if poly then + begin + let env = Global.env () in + let env' = Environ.push_context ctx env in + (* let env'' = Environ.push_rel_context params env' in *) + let evd = Evd.from_env env' in + Inductiveops.infer_inductive_subtyping env' evd mie + end + else + mie + in let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in @@ -423,7 +446,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def poly ctx id idbuild paramimpls params arity +let declare_class finite def cum poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -466,7 +489,16 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls + let univs = + if poly then + if cum then + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + else + Polymorphic_ind_entry ctx + else + Monomorphic_ind_entry ctx + in + let ind = declare_structure BiFinite univs (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -515,7 +547,7 @@ let add_inductive_class ind = let mind, oneind = Global.lookup_inductive ind in let k = let ctx = oneind.mind_arity_ctxt in - let inst = Univ.UContext.instance mind.mind_universes in + let inst = Declareops.inductive_polymorphic_instance mind in let ty = Inductive.type_of_inductive (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) @@ -540,7 +572,7 @@ open Vernacexpr (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions or subinstances. *) -let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) = +let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let cfs,priorities = List.split cfs in let coers,fs = List.split cfs in @@ -564,14 +596,24 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id let gr = match kind with | Class def -> let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - let gr = declare_class finite def poly ctx (loc,idstruc) idbuild + let gr = declare_class finite def cum poly ctx (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> - let implfs = List.map + let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits - (succ (List.length params)) impls) implfs in - let ind = declare_structure finite poly ctx idstruc + (succ (List.length params)) impls) implfs + in + let univs = + if poly then + if cum then + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + else + Polymorphic_ind_entry ctx + else + Monomorphic_ind_entry ctx + in + let ind = declare_structure finite univs idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind diff --git a/vernac/record.mli b/vernac/record.mli index 3fd651db90..aa530fd61a 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -26,7 +26,7 @@ val declare_projections : val declare_structure : Decl_kinds.recursivity_kind -> - bool (** polymorphic?*) -> Univ.universe_context -> + Entries.inductive_universes -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) bool (** template arity ? *) -> @@ -38,8 +38,8 @@ val declare_structure : inductive val definition_structure : - inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * - plident with_coercion * local_binder_expr list * + inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * + Decl_kinds.recursivity_kind * plident with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference diff --git a/vernac/search.ml b/vernac/search.ml index 0ff78f439d..5e56ada8ad 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -85,7 +85,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = let mib = Global.lookup_mind mind in let iter_packet i mip = let ind = (mind, i) in - let u = Declareops.inductive_instance mib in + let u = Declareops.inductive_polymorphic_instance mib in let i = (ind, u) in let typ = Inductiveops.type_of_inductive env i in let () = fn (IndRef ind) env typ in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d0f9c7de74..21f053fb9b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -526,7 +526,7 @@ let vernac_assumption locality poly (local, kind) l nl = let status = do_assumptions kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom -let vernac_record k poly finite struc binders sort nameopt cfs = +let vernac_record cum k poly finite struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (fst (snd struc))) | Some (_,id as lid) -> @@ -537,13 +537,13 @@ let vernac_record k poly finite struc binders sort nameopt cfs = match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); - ignore(Record.definition_structure (k,poly,finite,struc,binders,cfs,const,sort)) + ignore(Record.definition_structure (k,cum,poly,finite,struc,binders,cfs,const,sort)) (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) -let vernac_inductive poly lo finite indl = +let vernac_inductive cum poly lo finite indl = if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -559,14 +559,14 @@ let vernac_inductive poly lo finite indl = | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> user_err Pp.(str "The Variant keyword does not support syntax { ... }.") | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> - vernac_record (match b with Class _ -> Class false | _ -> b) + vernac_record cum (match b with Class _ -> Class false | _ -> b) poly finite id bl c oc fs | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> let f = let (coe, ((loc, id), ce)) = l in let coe' = if coe then Some true else None in (((coe', AssumExpr ((loc, Name id), ce)), None), []) - in vernac_record (Class true) poly finite id bl c None [f] + in vernac_record cum (Class true) poly finite id bl c None [f] | [ ( _ , _, _, Class _, Constructors _), [] ] -> user_err Pp.(str "Inductive classes not supported") | [ ( id , bl , c , Class _, _), _ :: _ ] -> @@ -580,7 +580,7 @@ let vernac_inductive poly lo finite indl = | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in - do_mutual_inductive indl poly lo finite + do_mutual_inductive indl cum poly lo finite let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in @@ -1365,6 +1365,14 @@ let _ = optwrite = Flags.make_universe_polymorphism } let _ = + declare_bool_option + { optdepr = false; + optname = "inductive cumulativity"; + optkey = ["Inductive"; "Cumulativity"]; + optread = Flags.is_inductive_cumulativity; + optwrite = Flags.make_inductive_cumulativity } + +let _ = declare_int_option { optdepr = false; optname = "the level of inlining during functor application"; @@ -1933,7 +1941,7 @@ let interp ?proof ?loc locality poly c = | VernacEndProof e -> vernac_end_proof ?proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl - | VernacInductive (priv,finite,l) -> vernac_inductive poly priv finite l + | VernacInductive (cum, priv,finite,l) -> vernac_inductive cum poly priv finite l | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l | VernacScheme l -> vernac_scheme l |