diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 94 |
1 files changed, 55 insertions, 39 deletions
diff --git a/API/API.mli b/API/API.mli index ec6a68ebb0..1a84600ec9 100644 --- a/API/API.mli +++ b/API/API.mli @@ -491,6 +491,8 @@ sig val equal : t -> t -> bool + val print : t -> Pp.t + (** a set of unique identifiers of some {i evars} *) module Set : Set.S with type elt = t module Map : CMap.ExtS with type key = t and module Set := Set @@ -516,12 +518,16 @@ sig type metavariable = int type existential_key = Evar.t - type 'constr pexistential = existential_key * 'constr array + [@@ocaml.deprecated "use Evar.t"] + + type 'constr pexistential = Evar.t * 'constr array type 'a puniverses = 'a Univ.puniverses - type pconstant = Constant.t puniverses - type pinductive = inductive puniverses - type pconstructor = constructor puniverses + [@@ocaml.deprecated "use Univ.puniverses"] + + type pconstant = Constant.t Univ.puniverses + type pinductive = inductive Univ.puniverses + type pconstructor = constructor Univ.puniverses type ('constr, 'types) prec_declaration = Name.t array * 'types array * 'constr array @@ -594,7 +600,7 @@ sig val mkRel : int -> t val mkVar : Id.t -> t val mkMeta : metavariable -> t - type existential = existential_key * constr array + type existential = Evar.t * constr array val mkEvar : existential -> t val mkSort : Sorts.t -> t val mkProp : t @@ -605,7 +611,7 @@ sig val mkLambda : Name.t * types * t -> t val mkLetIn : Name.t * t * types * t -> t val mkApp : t * t array -> t - val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses + val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses type rec_declaration = Name.t array * types array * constr array type fixpoint = (int array * int) * rec_declaration @@ -695,16 +701,16 @@ sig val decompose_appvect : constr -> constr * constr array (** Destructs a constant *) - val destConst : constr -> Constant.t puniverses + val destConst : constr -> Constant.t Univ.puniverses (** Destructs an existential variable *) val destEvar : constr -> existential (** Destructs a (co)inductive type *) - val destInd : constr -> inductive puniverses + val destInd : constr -> inductive Univ.puniverses (** Destructs a constructor *) - val destConstruct : constr -> constructor puniverses + val destConstruct : constr -> constructor Univ.puniverses (** Destructs a [match c as x in I args return P with ... | Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args @@ -988,11 +994,11 @@ sig type 'a puniverses = 'a Univ.puniverses [@@ocaml.deprecated "Alias of Constr.puniverses"] - type pconstant = Names.Constant.t Constr.puniverses + type pconstant = Names.Constant.t Univ.puniverses [@@ocaml.deprecated "Alias of Constr.pconstant"] - type pinductive = Names.inductive Constr.puniverses + type pinductive = Names.inductive Univ.puniverses [@@ocaml.deprecated "Alias of Constr.pinductive"] - type pconstructor = Names.constructor Constr.puniverses + type pconstructor = Names.constructor Univ.puniverses [@@ocaml.deprecated "Alias of Constr.pconstructor"] type case_style = Constr.case_style = | LetStyle @@ -1045,7 +1051,7 @@ sig | CoFix of ('constr, 'types) Constr.pcofixpoint | Proj of Names.Projection.t * 'constr [@@ocaml.deprecated "Alias of Constr.kind_of_term"] - type existential = Constr.existential_key * Constr.constr array + type existential = Evar.t * Constr.constr array [@@ocaml.deprecated "Alias of Constr.existential"] type rec_declaration = Names.Name.t array * Constr.constr array * Constr.constr array [@@ocaml.deprecated "Alias of Constr.rec_declaration"] @@ -1093,7 +1099,7 @@ sig [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkConstruct : Names.constructor -> constr [@@ocaml.deprecated "Alias of similarly named Constr function"] - val mkConstructU : Names.constructor Constr.puniverses -> constr + val mkConstructU : Names.constructor Univ.puniverses -> constr [@@ocaml.deprecated "Alias of similarly named Constr function"] val mkConstructUi : (Constr.pinductive * int) -> constr [@@ocaml.deprecated "Alias of similarly named Constr function"] @@ -1135,7 +1141,7 @@ sig [@@ocaml.deprecated "Alias for the function in [Constr]"] val destRel : constr -> int [@@ocaml.deprecated "Alias for the function in [Constr]"] - val destConst : constr -> Names.Constant.t Constr.puniverses + val destConst : constr -> Names.Constant.t Univ.puniverses [@@ocaml.deprecated "Alias for the function in [Constr]"] val destCast : constr -> constr * Constr.cast_kind * constr [@@ocaml.deprecated "Alias for the function in [Constr]"] @@ -1208,7 +1214,7 @@ sig val is_prop_sort : Sorts.t -> bool [@@ocaml.deprecated "alias of API.Sorts.is_prop"] - type existential_key = Constr.existential_key + type existential_key = Evar.t [@@ocaml.deprecated "Alias of Constr.existential_key"] val family_of_sort : Sorts.t -> Sorts.family @@ -1220,7 +1226,7 @@ sig val constr_ord : constr -> constr -> int [@@ocaml.deprecated "alias of Term.compare"] - val destInd : constr -> Names.inductive Constr.puniverses + val destInd : constr -> Names.inductive Univ.puniverses [@@ocaml.deprecated "Alias for the function in [Constr]"] val univ_of_sort : Sorts.t -> Univ.Universe.t [@@ocaml.deprecated "Alias for the function in [Constr]"] @@ -1417,7 +1423,7 @@ sig | TemplateArity of 'b type constant_universes = - | Monomorphic_const of Univ.UContext.t + | Monomorphic_const of Univ.ContextSet.t | Polymorphic_const of Univ.AUContext.t type projection_body = { @@ -1484,7 +1490,7 @@ sig | MEwith of module_alg_expr * with_declaration type abstract_inductive_universes = - | Monomorphic_ind of Univ.UContext.t + | Monomorphic_ind of Univ.ContextSet.t | Polymorphic_ind of Univ.AUContext.t | Cumulative_ind of Univ.ACumulativityInfo.t @@ -1551,7 +1557,7 @@ sig | LocalAssumEntry of constr type inductive_universes = - | Monomorphic_ind_entry of Univ.UContext.t + | Monomorphic_ind_entry of Univ.ContextSet.t | Polymorphic_ind_entry of Univ.UContext.t | Cumulative_ind_entry of Univ.CumulativityInfo.t @@ -1580,8 +1586,9 @@ sig type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation type constant_universes_entry = - | Monomorphic_const_entry of Univ.UContext.t + | Monomorphic_const_entry of Univ.ContextSet.t | Polymorphic_const_entry of Univ.UContext.t + type 'a in_constant_universes_entry = 'a * constant_universes_entry type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -1592,7 +1599,7 @@ sig const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } - type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline + type parameter_entry = Context.Named.t option * Constr.types in_constant_universes_entry * inline type projection_entry = { proj_entry_ind : MutInd.t; @@ -2186,7 +2193,7 @@ sig | ImpossibleCase | MatchingVar of matching_var_kind | VarInstance of Names.Id.t - | SubEvar of Constr.existential_key + | SubEvar of Evar.t end module Glob_term : @@ -2763,6 +2770,9 @@ sig val context_set : t -> Univ.ContextSet.t val of_context_set : Univ.ContextSet.t -> t + val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry + val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes + type rigid = | UnivRigid | UnivFlexible of bool @@ -2772,9 +2782,12 @@ end module Evd : sig - type evar = Constr.existential_key + type evar = Evar.t + [@@ocaml.deprecated "use Evar.t"] val string_of_existential : Evar.t -> string + [@@ocaml.deprecated "use Evar.print"] + type evar_constraint = Reduction.conv_pb * Environ.env * Constr.t * Constr.t (* --------------------------------- *) @@ -2851,7 +2864,7 @@ sig val empty : evar_map val from_env : Environ.env -> evar_map val find : evar_map -> Evar.t -> evar_info - val find_undefined : evar_map -> evar -> evar_info + val find_undefined : evar_map -> Evar.t -> evar_info val is_defined : evar_map -> Evar.t -> bool val mem : evar_map -> Evar.t -> bool val add : evar_map -> Evar.t -> evar_info -> evar_map @@ -2869,7 +2882,7 @@ sig val clear_metas : evar_map -> evar_map (** Allocates a new evar that represents a {i sort}. *) - val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t + val new_sort_variable : ?loc:Loc.t -> ?name:Names.Id.t -> rigid -> evar_map -> evar_map * Sorts.t val remove : evar_map -> Evar.t -> evar_map val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> Environ.env -> @@ -2879,13 +2892,16 @@ sig val fold_undefined : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a val universe_context_set : evar_map -> Univ.ContextSet.t - val evar_ident : evar -> evar_map -> Names.Id.t option + val evar_ident : Evar.t -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list - val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> - (Names.Id.t * Univ.Level.t) list * Univ.UContext.t + val universe_binders : evar_map -> Universes.universe_binders val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map + val to_universe_context : evar_map -> Univ.UContext.t + val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry + val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes + val meta_list : evar_map -> (Constr.metavariable * clbinding) list val meta_defined : evar_map -> Constr.metavariable -> bool @@ -3312,7 +3328,7 @@ sig val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t val read_line : string t end - val proofview : proofview -> Evd.evar list * Evd.evar_map + val proofview : proofview -> Evar.t list * Evd.evar_map val cycle : int -> unit tactic val swap : int -> int -> unit tactic val revgoals : unit tactic @@ -3339,20 +3355,20 @@ sig val shelve_unifiable : unit tactic val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview - * (bool * Evd.evar list * Evd.evar list) + * (bool * Evar.t list * Evar.t list) * Proofview_monad.Info.tree val numgoals : int tactic - val with_shelf : 'a tactic -> (Evd.evar list * 'a) tactic + val with_shelf : 'a tactic -> (Evar.t list * 'a) tactic module Unsafe : sig val tclEVARS : Evd.evar_map -> unit tactic - val tclGETGOALS : Evd.evar list tactic + val tclGETGOALS : Evar.t list tactic - val tclSETGOALS : Evd.evar list -> unit tactic + val tclSETGOALS : Evar.t list -> unit tactic - val tclNEWGOALS : Evd.evar list -> unit tactic + val tclNEWGOALS : Evar.t list -> unit tactic end module Goal : @@ -3668,7 +3684,7 @@ sig val nconstructors : Names.inductive -> int val find_rectype : Environ.env -> Evd.evar_map -> EConstr.types -> inductive_type val get_constructors : Environ.env -> inductive_family -> constructor_summary array - val dest_ind_family : inductive_family -> Names.inductive Constr.puniverses * Constr.t list + val dest_ind_family : inductive_family -> Names.inductive Univ.puniverses * Constr.t list val find_inductive : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * Constr.t list val type_of_inductive : Environ.env -> Constr.pinductive -> Constr.types end @@ -4668,11 +4684,11 @@ sig val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:Decl_kinds.definition_object_kind -> - ?local:bool -> ?poly:Decl_kinds.polymorphic -> Names.Id.t -> ?types:Constr.t -> - Constr.t Univ.in_universe_context_set -> Names.Constant.t + ?local:bool -> Names.Id.t -> ?types:Constr.t -> + Constr.t Entries.in_constant_universes_entry -> Names.Constant.t val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:Constr.types -> - ?poly:Decl_kinds.polymorphic -> ?univs:Univ.UContext.t -> + ?univs:Entries.constant_universes_entry -> ?eff:Safe_typing.private_constants -> Constr.t -> Safe_typing.private_constants Entries.definition_entry val definition_message : Names.Id.t -> unit val declare_variable : Names.Id.t -> variable_declaration -> Libnames.object_name |