diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 51 |
1 files changed, 45 insertions, 6 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index f2f5e8495..2d3df6e1e 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -24,6 +24,13 @@ type sorts = Sorts.t = type sorts_family = Sorts.family = InProp | InSet | InType +type 'a puniverses = 'a Univ.puniverses + +(** Simply type aliases *) +type pconstant = constant puniverses +type pinductive = inductive puniverses +type pconstructor = constructor puniverses + type constr = Constr.constr (** Alias types, for compatibility. *) @@ -73,12 +80,13 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of constant - | Ind of inductive - | Construct of constructor + | Const of constant puniverses + | Ind of inductive puniverses + | Construct of constructor puniverses | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint + | Proj of constant * 'constr type values = Constr.values @@ -157,16 +165,16 @@ val decompose_app : constr -> constr * constr list val decompose_appvect : constr -> constr * constr array (** Destructs a constant *) -val destConst : constr -> constant +val destConst : constr -> constant puniverses (** Destructs an existential variable *) val destEvar : constr -> existential (** Destructs a (co)inductive type *) -val destInd : constr -> inductive +val destInd : constr -> inductive puniverses (** Destructs a constructor *) -val destConstruct : constr -> constructor +val destConstruct : constr -> constructor 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 @@ -397,8 +405,13 @@ val mkLambda : Name.t * types * constr -> constr val mkLetIn : Name.t * constr * types * constr -> constr val mkApp : constr * constr array -> constr val mkConst : constant -> constr +val mkProj : (constant * constr) -> constr val mkInd : inductive -> constr val mkConstruct : constructor -> constr +val mkConstU : constant puniverses -> constr +val mkIndU : inductive puniverses -> constr +val mkConstructU : constructor puniverses -> constr +val mkConstructUi : (pinductive * int) -> constr val mkCase : case_info * constr * constr * constr array -> constr val mkFix : fixpoint -> constr val mkCoFix : cofixpoint -> constr @@ -408,6 +421,26 @@ val mkCoFix : cofixpoint -> constr val eq_constr : constr -> constr -> bool (** Alias for [Constr.equal] *) +(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and the universe equalities in [c]. *) +val eq_constr_univs : constr Univ.check_function + +(** [leq_constr_univs a b] [true, c] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe inequalities in [c]. *) +val leq_constr_univs : constr Univ.check_function + +(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and the universe equalities in [c]. *) +val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained + +(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe inequalities in [c]. *) +val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained + +(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and ignoring universe instances. *) +val eq_constr_nounivs : constr -> constr -> bool + val kind_of_term : constr -> (constr, types) kind_of_term (** Alias for [Constr.kind] *) @@ -424,6 +457,10 @@ val map_constr_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr (** Alias for [Constr.map_with_binders] *) +val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses +val univ_of_sort : sorts -> Univ.universe +val sort_of_univ : Univ.universe -> sorts + val iter_constr : (constr -> unit) -> constr -> unit (** Alias for [Constr.iter] *) @@ -437,6 +474,8 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool val hash_constr : constr -> int (** Alias for [Constr.hash] *) +(*********************************************************************) + val hcons_sorts : sorts -> sorts (** Alias for [Constr.hashcons_sorts] *) |