diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 1 | ||||
| -rw-r--r-- | API/API.mli | 61 | ||||
| -rw-r--r-- | API/grammar_API.mli | 2 |
3 files changed, 51 insertions, 13 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 68fbda7c73..2fd3f27927 100644 --- a/API/API.mli +++ b/API/API.mli @@ -72,6 +72,7 @@ sig val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds end type 'a puniverses = 'a * Instance.t + val out_punivs : 'a puniverses -> 'a module Constraint : module type of struct include Univ.Constraint end @@ -84,7 +85,11 @@ sig end type universe_context = UContext.t - [@@ocaml.deprecated "alias of API.Names.UContext.t"] + [@@ocaml.deprecated "alias of API.Univ.UContext.t"] + + type abstract_universe_context = Univ.AUContext.t + type cumulativity_info = Univ.CumulativityInfo.t + type abstract_cumulativity_info = Univ.ACumulativityInfo.t module LSet : module type of struct include Univ.LSet end module ContextSet : @@ -1034,7 +1039,16 @@ sig | Undef of inline | Def of Term.constr Mod_subst.substituted | OpaqueDef of Opaqueproof.opaque - type constant_type = Declarations.constant_type + type template_arity = Declarations.template_arity = { + template_param_levels : Univ.Level.t option list; + template_level : Univ.Universe.t; + } + + type ('a, 'b) declaration_arity = ('a, 'b) Declarations.declaration_arity = + | RegularArity of 'a + | TemplateArity of 'b + + type constant_type = (Prelude.types, Context.Rel.t * template_arity) declaration_arity type constant_universes = Declarations.constant_universes type projection_body = Declarations.projection_body = { proj_ind : Names.MutInd.t; @@ -1045,12 +1059,12 @@ sig proj_body : Term.constr; } type typing_flags = Declarations.typing_flags + type constant_body = Declarations.constant_body = { const_hyps : Context.Named.t; const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; - const_polymorphic : bool; const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; @@ -1083,6 +1097,12 @@ sig | MEident of Names.ModPath.t | MEapply of module_alg_expr * Names.ModPath.t | MEwith of module_alg_expr * with_declaration + + type abstract_inductive_universes = Declarations.abstract_inductive_universes = + | Monomorphic_ind of Univ.UContext.t + | Polymorphic_ind of Univ.abstract_universe_context + | Cumulative_ind of Univ.abstract_cumulativity_info + type mutual_inductive_body = Declarations.mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : Declarations.record_body option; @@ -1092,8 +1112,7 @@ sig mind_nparams : int; mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; - mind_polymorphic : bool; - mind_universes : Univ.UContext.t; + mind_universes : Declarations.abstract_inductive_universes; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } @@ -1122,6 +1141,11 @@ sig | SFBmodtype of module_type_body end +module Univops : sig + val universes_of_constr : Term.constr -> Univ.LSet.t + val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t +end + module Environ : sig type env = Prelude.env @@ -1131,6 +1155,11 @@ sig uj_val : 'constr; uj_type : 'types } + type 'types punsafe_type_judgment = 'types Environ.punsafe_type_judgment = { + utj_val : 'types; + utj_type : Sorts.t } + + type unsafe_type_judgment = Term.types punsafe_type_judgment val empty_env : env val lookup_mind : Names.MutInd.t -> env -> Declarations.mutual_inductive_body val push_rel : Context.Rel.Declaration.t -> env -> env @@ -1156,6 +1185,7 @@ sig val fold_named_context_reverse : ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a val evaluable_named : Names.Id.t -> Environ.env -> bool + val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env end module UGraph : @@ -1219,6 +1249,7 @@ end module Typeops : sig + val infer_type : Environ.env -> Term.types -> Environ.unsafe_type_judgment val type_of_constant_type : Environ.env -> Declarations.constant_type -> Term.types val type_of_constant_in : Environ.env -> Term.pconstant -> Term.types end @@ -1900,6 +1931,7 @@ end module Decl_kinds : sig type polymorphic = bool + type cumulative_inductive_flag = bool type recursivity_kind = Decl_kinds.recursivity_kind = | Finite | CoFinite @@ -2055,8 +2087,10 @@ sig type explicitation = Constrexpr.explicitation = | ExplByPos of int * Names.Id.t option | ExplByName of Names.Id.t + type sign = bool + type raw_natural_number = string type prim_token = Constrexpr.prim_token = - | Numeral of Bigint.bigint + | Numeral of raw_natural_number * sign | String of string type notation = string type instance_expr = Misctypes.glob_level list @@ -2379,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 @@ -2645,10 +2679,9 @@ sig type universe_opt_subst = Universes.universe_opt_subst val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set val new_Type : Names.DirPath.t -> Term.types + val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set val unsafe_type_of_global : Globnames.global_reference -> Term.types val constr_of_global : Prelude.global_reference -> Term.constr - val universes_of_constr : Term.constr -> Univ.LSet.t - val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t val new_univ_level : Names.DirPath.t -> Univ.Level.t val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context val new_sort_in_family : Sorts.family -> Sorts.t @@ -2694,7 +2727,6 @@ module Lib : sig | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_segment = (Libnames.object_name * node) list @@ -3475,6 +3507,7 @@ sig type ltac_constant = Names.KerName.t + val global : Libnames.reference -> Globnames.global_reference val global_of_path : Libnames.full_path -> Globnames.global_reference val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid val path_of_global : Globnames.global_reference -> Libnames.full_path @@ -4737,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 -> @@ -4761,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 diff --git a/API/grammar_API.mli b/API/grammar_API.mli index 4da5b380fe..c643f09086 100644 --- a/API/grammar_API.mli +++ b/API/grammar_API.mli @@ -116,7 +116,7 @@ sig val pattern_identref : Names.Id.t located Gram.Entry.e val base_ident : Names.Id.t Gram.Entry.e val natural : int Gram.Entry.e - val bigint : Bigint.bigint Gram.Entry.e + val bigint : Constrexpr.raw_natural_number Gram.Entry.e val integer : int Gram.Entry.e val string : string Gram.Entry.e val qualid : API.Libnames.qualid located Gram.Entry.e |