diff options
| author | Maxime Dénès | 2017-06-19 17:43:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-19 17:43:19 +0200 |
| commit | 414890675cb72fd9286e19521a746677c06e784e (patch) | |
| tree | 14599a23215356ac472ac483ad564c11eb53c1fc | |
| parent | 396c77feb0cced3965f90f65c681e48c528636d5 (diff) | |
| parent | 15b1856edd593b39d63d23584a4f5acec0eeb592 (diff) | |
Merge PR#613: Cumulativity for inductive types
113 files changed, 3250 insertions, 734 deletions
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 0d7094359b..2fd3f27927 100644 --- a/API/API.mli +++ b/API/API.mli @@ -85,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 : @@ -1055,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; @@ -1093,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; @@ -1102,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; } @@ -1132,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 @@ -1917,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 @@ -2398,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 @@ -2667,8 +2682,6 @@ sig 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 @@ -4757,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 -> @@ -4781,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/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/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/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/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/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 |
