diff options
Diffstat (limited to 'kernel/term.mli')
-rw-r--r-- | kernel/term.mli | 501 |
1 files changed, 173 insertions, 328 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 33d3daaf..501aaf74 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,237 +1,101 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Names +open Context +(** {5 Redeclaration of types from module Constr and Sorts} -(** {6 The sorts of CCI. } *) + This reexports constructors of inductive types defined in module [Constr], + for compatibility purposes. Refer to this module for further info. -type contents = Pos | Null +*) + +type contents = Sorts.contents = Pos | Null -type sorts = +type sorts = Sorts.t = | Prop of contents (** Prop and Set *) | Type of Univ.universe (** Type *) -val set_sort : sorts -val prop_sort : sorts -val type1_sort : sorts +type sorts_family = Sorts.family = InProp | InSet | InType -(** {6 The sorts family of CCI. } *) +type 'a puniverses = 'a Univ.puniverses -type sorts_family = InProp | InSet | InType +(** Simply type aliases *) +type pconstant = constant puniverses +type pinductive = inductive puniverses +type pconstructor = constructor puniverses -val family_of_sort : sorts -> sorts_family +type constr = Constr.constr +(** Alias types, for compatibility. *) + +type types = Constr.types +(** Same as [constr], for documentation purposes. *) -(** {6 Useful types } *) +type existential_key = Constr.existential_key -(** {6 Existential variables } *) -type existential_key = int +type existential = Constr.existential -(** {6 Existential variables } *) -type metavariable = int +type metavariable = Constr.metavariable -(** {6 Case annotation } *) -type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle - | RegularStyle (** infer printing form from number of constructor *) -type case_printing = - { ind_nargs : int; (** length of the arity of the inductive type *) - style : case_style } +type case_style = Constr.case_style = + LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle -(** the integer is the number of real args, needed for reduction *) -type case_info = +type case_printing = Constr.case_printing = + { ind_tags : bool list; cstr_tags : bool list array; style : case_style } + +type case_info = Constr.case_info = { ci_ind : inductive; ci_npar : int; - ci_cstr_ndecls : int array; (** number of real args of each constructor *) - ci_pp_info : case_printing (** not interpreted by the kernel *) + ci_cstr_ndecls : int array; + ci_cstr_nargs : int array; + ci_pp_info : case_printing } -(** {6 The type of constructions } *) - -type constr - -(** [eq_constr a b] is true if [a] equals [b] modulo alpha, casts, - and application grouping *) -val eq_constr : constr -> constr -> bool - -(** [types] is the same as [constr] but is intended to be used for - documentation to indicate that such or such function specifically works - with {e types} (i.e. terms of type a sort). - (Rem:plurial form since [type] is a reserved ML keyword) *) - -type types = constr - -(** {5 Functions for dealing with constr terms. } - The following functions are intended to simplify and to uniform the - manipulation of terms. Some of these functions may be overlapped with - previous ones. *) - -(** {6 Term constructors. } *) - -(** Constructs a DeBrujin index (DB indices begin at 1) *) -val mkRel : int -> constr - -(** Constructs a Variable *) -val mkVar : identifier -> constr - -(** Constructs an patvar named "?n" *) -val mkMeta : metavariable -> constr - -(** Constructs an existential variable *) -type existential = existential_key * constr array -val mkEvar : existential -> constr - -(** Construct a sort *) -val mkSort : sorts -> types -val mkProp : types -val mkSet : types -val mkType : Univ.universe -> types - - -(** This defines the strategy to use for verifiying a Cast *) -type cast_kind = VMcast | DEFAULTcast | REVERTcast - -(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the - type t{_ 2} (that means t2 is declared as the type of t1). *) -val mkCast : constr * cast_kind * constr -> constr - -(** Constructs the product [(x:t1)t2] *) -val mkProd : name * types * types -> types -val mkNamedProd : identifier -> types -> types -> types +type cast_kind = Constr.cast_kind = + VMcast | NATIVEcast | DEFAULTcast | REVERTcast -(** non-dependent product [t1 -> t2], an alias for - [forall (_:t1), t2]. Beware [t_2] is NOT lifted. - Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))] -*) -val mkArrow : types -> types -> constr - -(** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *) -val mkLambda : name * types * constr -> constr -val mkNamedLambda : identifier -> types -> constr -> constr - -(** Constructs the product [let x = t1 : t2 in t3] *) -val mkLetIn : name * constr * types * constr -> constr -val mkNamedLetIn : identifier -> constr -> types -> constr -> constr - -(** [mkApp (f,[| t_1; ...; t_n |]] constructs the application - {% $(f~t_1~\dots~t_n)$ %}. *) -val mkApp : constr * constr array -> constr - -(** Constructs a constant - The array of terms correspond to the variables introduced in the section *) -val mkConst : constant -> constr - -(** Inductive types *) - -(** Constructs the ith (co)inductive type of the block named kn - The array of terms correspond to the variables introduced in the section *) -val mkInd : inductive -> constr - -(** Constructs the jth constructor of the ith (co)inductive type of the - block named kn. The array of terms correspond to the variables - introduced in the section *) -val mkConstruct : constructor -> constr - -(** Constructs a destructor of inductive type. - - [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] - presented as describe in [ci]. - - [p] stucture is [fun args x -> "return clause"] - - [ac]{^ ith} element is ith constructor case presented as - {e lambda construct_args (without params). case_term } *) -val mkCase : case_info * constr * constr * constr array -> constr - -(** If [recindxs = [|i1,...in|]] - [funnames = [|f1,.....fn|]] - [typarray = [|t1,...tn|]] - [bodies = [|b1,.....bn|]] - then [mkFix ((recindxs,i), funnames, typarray, bodies) ] - constructs the {% $ %}i{% $ %}th function of the block (counting from 0) - - [Fixpoint f1 [ctx1] = b1 - with f2 [ctx2] = b2 - ... - with fn [ctxn] = bn.] - - where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. -*) -type rec_declaration = name array * types array * constr array -type fixpoint = (int array * int) * rec_declaration -val mkFix : fixpoint -> constr - -(** If [funnames = [|f1,.....fn|]] - [typarray = [|t1,...tn|]] - [bodies = [b1,.....bn]] - then [mkCoFix (i, (funnames, typarray, bodies))] - constructs the ith function of the block - - [CoFixpoint f1 = b1 - with f2 = b2 - ... - with fn = bn.] - *) -type cofixpoint = int * rec_declaration -val mkCoFix : cofixpoint -> constr - - -(** {6 Concrete type for making pattern-matching. } *) - -(** [constr array] is an instance matching definitional [named_context] in - the same order (i.e. last argument first) *) -type 'constr pexistential = existential_key * 'constr array +type rec_declaration = Constr.rec_declaration +type fixpoint = Constr.fixpoint +type cofixpoint = Constr.cofixpoint +type 'constr pexistential = 'constr Constr.pexistential type ('constr, 'types) prec_declaration = - name array * 'types array * 'constr array -type ('constr, 'types) pfixpoint = - (int array * int) * ('constr, 'types) prec_declaration -type ('constr, 'types) pcofixpoint = - int * ('constr, 'types) prec_declaration + ('constr, 'types) Constr.prec_declaration +type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint +type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -type ('constr, 'types) kind_of_term = +type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = | Rel of int - | Var of identifier + | Var of Id.t | Meta of metavariable | Evar of 'constr pexistential | Sort of sorts | Cast of 'constr * cast_kind * 'types - | Prod of name * 'types * 'types - | Lambda of name * 'types * 'constr - | LetIn of name * 'constr * 'types * 'constr + | Prod of Name.t * 'types * 'types + | 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 projection * 'constr -(** User view of [constr]. For [App], it is ensured there is at - least one argument and the function is not itself an applicative - term *) +type values = Constr.values -val kind_of_term : constr -> (constr, types) kind_of_term - -(** Experimental, used in Presburger contrib *) -type ('constr, 'types) kind_of_type = - | SortType of sorts - | CastType of 'types * 'types - | ProdType of name * 'types * 'types - | LetInType of name * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array - -val kind_of_type : types -> (constr, types) kind_of_type - -(** {6 Simple term case analysis. } *) +(** {5 Simple term case analysis. } *) val isRel : constr -> bool val isRelN : int -> constr -> bool val isVar : constr -> bool -val isVarId : identifier -> constr -> bool +val isVarId : Id.t -> constr -> bool val isInd : constr -> bool val isEvar : constr -> bool val isMeta : constr -> bool @@ -248,6 +112,7 @@ val isConstruct : constr -> bool val isFix : constr -> bool val isCoFix : constr -> bool val isCase : constr -> bool +val isProj : constr -> bool val is_Prop : constr -> bool val is_Set : constr -> bool @@ -257,9 +122,11 @@ val iskind : constr -> bool val is_small : sorts -> bool -(** {6 Term destructors } *) +(** {5 Term destructors } *) (** Destructor operations are partial functions and - @raise Invalid_argument "dest*" if the term has not the expected form. *) + @raise DestKO if the term has not the expected form. *) + +exception DestKO (** Destructs a DeBrujin index *) val destRel : constr -> int @@ -268,7 +135,7 @@ val destRel : constr -> int val destMeta : constr -> metavariable (** Destructs a variable *) -val destVar : constr -> identifier +val destVar : constr -> Id.t (** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) @@ -278,13 +145,13 @@ val destSort : constr -> sorts val destCast : constr -> constr * cast_kind * constr (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) -val destProd : types -> name * types * types +val destProd : types -> Name.t * types * types (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) -val destLambda : constr -> name * types * constr +val destLambda : constr -> Name.t * types * constr (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) -val destLetIn : constr -> name * constr * types * constr +val destLetIn : constr -> Name.t * constr * types * constr (** Destructs an application *) val destApp : constr -> constr * constr array @@ -295,17 +162,20 @@ val destApplication : constr -> constr * constr array (** Decompose any term as an applicative term; the list of args can be empty *) val decompose_app : constr -> constr * constr list +(** Same as [decompose_app], but returns an array. *) +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 @@ -314,6 +184,9 @@ return P in t1], or [if c then t1 else t2]) where [info] is pretty-printing information *) val destCase : constr -> case_info * constr * constr * constr array +(** Destructs a projection *) +val destProj : constr -> projection * constr + (** Destructs the {% $ %}i{% $ %}th function of the block [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} with f{_ 2} ctx{_ 2} = b{_ 2} @@ -326,54 +199,18 @@ val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint -(** {6 Local } *) -(** A {e declaration} has the form [(name,body,type)]. It is either an - {e assumption} if [body=None] or a {e definition} if - [body=Some actualbody]. It is referred by {e name} if [na] is an - identifier or by {e relative index} if [na] is not an identifier - (in the latter case, [na] is of type [name] but just for printing - purpose) *) - -type named_declaration = identifier * constr option * types -type rel_declaration = name * constr option * types - -val map_named_declaration : - (constr -> constr) -> named_declaration -> named_declaration -val map_rel_declaration : - (constr -> constr) -> rel_declaration -> rel_declaration - -val fold_named_declaration : - (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a -val fold_rel_declaration : - (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a - -val exists_named_declaration : - (constr -> bool) -> named_declaration -> bool -val exists_rel_declaration : - (constr -> bool) -> rel_declaration -> bool - -val for_all_named_declaration : - (constr -> bool) -> named_declaration -> bool -val for_all_rel_declaration : - (constr -> bool) -> rel_declaration -> bool +(** {5 Derived constructors} *) -val eq_named_declaration : - named_declaration -> named_declaration -> bool - -val eq_rel_declaration : - rel_declaration -> rel_declaration -> bool - -(** {6 Contexts of declarations referred to by de Bruijn indices } *) - -(** In [rel_context], more recent declaration is on top *) -type rel_context = rel_declaration list - -val empty_rel_context : rel_context -val add_rel_decl : rel_declaration -> rel_context -> rel_context +(** non-dependent product [t1 -> t2], an alias for + [forall (_:t1), t2]. Beware [t_2] is NOT lifted. + Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))] +*) +val mkArrow : types -> types -> constr -val lookup_rel : int -> rel_context -> rel_declaration -val rel_context_length : rel_context -> int -val rel_context_nhyps : rel_context -> int +(** Named version of the functions from [Term]. *) +val mkNamedLambda : Id.t -> types -> constr -> constr +val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr +val mkNamedProd : Id.t -> types -> types -> types (** Constructs either [(x:t)c] or [[x=b:t]c] *) val mkProd_or_LetIn : rel_declaration -> types -> types @@ -385,7 +222,7 @@ val mkNamedProd_wo_LetIn : named_declaration -> types -> types val mkLambda_or_LetIn : rel_declaration -> constr -> constr val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr -(** {6 Other term constructors. } *) +(** {5 Other term constructors. } *) (** [applist (f,args)] and its variants work as [mkApp] *) @@ -396,24 +233,24 @@ val appvectc : constr -> constr array -> constr (** [prodn n l b] = [forall (x_1:T_1)...(x_n:T_n), b] where [l] is [(x_n,T_n)...(x_1,T_1)...]. *) -val prodn : int -> (name * constr) list -> constr -> constr +val prodn : int -> (Name.t * constr) list -> constr -> constr (** [compose_prod l b] @return [forall (x_1:T_1)...(x_n:T_n), b] where [l] is [(x_n,T_n)...(x_1,T_1)]. Inverse of [decompose_prod]. *) -val compose_prod : (name * constr) list -> constr -> constr +val compose_prod : (Name.t * constr) list -> constr -> constr (** [lamn n l b] @return [fun (x_1:T_1)...(x_n:T_n) => b] where [l] is [(x_n,T_n)...(x_1,T_1)...]. *) -val lamn : int -> (name * constr) list -> constr -> constr +val lamn : int -> (Name.t * constr) list -> constr -> constr (** [compose_lam l b] @return [fun (x_1:T_1)...(x_n:T_n) => b] where [l] is [(x_n,T_n)...(x_1,T_1)]. Inverse of [it_destLam] *) -val compose_lam : (name * constr) list -> constr -> constr +val compose_lam : (Name.t * constr) list -> constr -> constr (** [to_lambda n l] @return [fun (x_1:T_1)...(x_n:T_n) => T] @@ -434,24 +271,24 @@ val prod_applist : constr -> constr list -> constr val it_mkLambda_or_LetIn : constr -> rel_context -> constr val it_mkProd_or_LetIn : types -> rel_context -> types -(** {6 Other term destructors. } *) +(** {5 Other term destructors. } *) (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *) -val decompose_prod : constr -> (name*constr) list * constr +val decompose_prod : constr -> (Name.t*constr) list * constr (** Transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *) -val decompose_lam : constr -> (name*constr) list * constr +val decompose_lam : constr -> (Name.t*constr) list * constr (** Given a positive integer n, transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *) -val decompose_prod_n : int -> constr -> (name * constr) list * constr +val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr (** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *) -val decompose_lam_n : int -> constr -> (name * constr) list * constr +val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr (** Extract the premisses and the conclusion of a term of the form "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *) @@ -505,7 +342,7 @@ val under_casts : (constr -> constr) -> constr -> constr (** Apply a function under components of Cast if any *) val under_outer_cast : (constr -> constr) -> constr -> constr -(** {6 ... } *) +(** {5 ... } *) (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. Such a term can canonically be seen as the pair of a context of types and of a sort *) @@ -521,117 +358,125 @@ val destArity : types -> arity (** Tells if a term has the form of an arity *) val isArity : types -> bool -(** {6 Occur checks } *) +(** {5 Kind of type} *) + +type ('constr, 'types) kind_of_type = + | SortType of sorts + | CastType of 'types * 'types + | ProdType of Name.t * 'types * 'types + | LetInType of Name.t * 'constr * 'types * 'types + | AtomicType of 'constr * 'constr array + +val kind_of_type : types -> (constr, types) kind_of_type -(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *) -val closedn : int -> constr -> bool +(** {5 Redeclaration of stuff from module [Sorts]} *) -(** [closed0 M] is true iff [M] is a (deBruijn) closed term *) -val closed0 : constr -> bool +val set_sort : sorts +(** Alias for Sorts.set *) -(** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *) -val noccurn : int -> constr -> bool +val prop_sort : sorts +(** Alias for Sorts.prop *) -(** [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M] - for n <= p < n+m *) -val noccur_between : int -> int -> constr -> bool +val type1_sort : sorts +(** Alias for Sorts.type1 *) -(** Checking function for terms containing existential- or - meta-variables. The function [noccur_with_meta] does not consider - meta-variables applied to some terms (intended to be its local - context) (for existential variables, it is necessarily the case) *) -val noccur_with_meta : int -> int -> constr -> bool +val sorts_ord : sorts -> sorts -> int +(** Alias for Sorts.compare *) -(** {6 Relocation and substitution } *) +val is_prop_sort : sorts -> bool +(** Alias for Sorts.is_prop *) -(** [exliftn el c] lifts [c] with lifting [el] *) -val exliftn : Esubst.lift -> constr -> constr +val family_of_sort : sorts -> sorts_family +(** Alias for Sorts.family *) -(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *) -val liftn : int -> int -> constr -> constr +(** {5 Redeclaration of stuff from module [Constr]} -(** [lift n c] lifts by [n] the positive indexes in [c] *) -val lift : int -> constr -> constr + See module [Constr] for further info. *) -(** [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an] - for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates - accordingly indexes in [a1],...,[an] *) -val substnl : constr list -> int -> constr -> constr -val substl : constr list -> constr -> constr -val subst1 : constr -> constr -> constr +(** {6 Term constructors. } *) -val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration -val substl_decl : constr list -> rel_declaration -> rel_declaration -val subst1_decl : constr -> rel_declaration -> rel_declaration +val mkRel : int -> constr +val mkVar : Id.t -> constr +val mkMeta : metavariable -> constr +val mkEvar : existential -> constr +val mkSort : sorts -> types +val mkProp : types +val mkSet : types +val mkType : Univ.universe -> types +val mkCast : constr * cast_kind * constr -> constr +val mkProd : Name.t * types * types -> types +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 : projection * 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 -val subst1_named_decl : constr -> named_declaration -> named_declaration -val substl_named_decl : constr list -> named_declaration -> named_declaration +(** {6 Aliases} *) -val replace_vars : (identifier * constr) list -> constr -> constr -val subst_var : identifier -> constr -> constr +val eq_constr : constr -> constr -> bool +(** Alias for [Constr.equal] *) -(** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t] - if two names are identical, the one of least indice is kept *) -val subst_vars : identifier list -> constr -> constr +(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, + application grouping and the universe constraints in [u]. *) +val eq_constr_univs : constr Univ.check_function -(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t] - if two names are identical, the one of least indice is kept *) -val substn_vars : int -> identifier list -> constr -> constr +(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe constraints in [u]. *) +val leq_constr_univs : constr Univ.check_function +(** [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 -(** {6 Functionals working on the immediate subterm of a construction } *) +val kind_of_term : constr -> (constr, types) kind_of_term +(** Alias for [Constr.kind] *) -(** [fold_constr f acc c] folds [f] on the immediate subterms of [c] - starting from [acc] and proceeding from left to right according to - the usual representation of the constructions; it is not recursive *) +val constr_ord : constr -> constr -> int +(** Alias for [Constr.compare] *) val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a - -(** [map_constr f c] maps [f] on the immediate subterms of [c]; it is - not recursive and the order with which subterms are processed is - not specified *) +(** Alias for [Constr.fold] *) val map_constr : (constr -> constr) -> constr -> constr - -(** [map_constr_with_binders g f n c] maps [f n] on the immediate - subterms of [c]; it carries an extra data [n] (typically a lift - index) which is processed by [g] (which typically add 1 to [n]) at - each binder traversal; it is not recursive and the order with which - subterms are processed is not specified *) +(** Alias for [Constr.map] *) val map_constr_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr +(** Alias for [Constr.map_with_binders] *) -(** [iter_constr f c] iters [f] on the immediate subterms of [c]; it is - not recursive and the order with which subterms are processed is - not specified *) +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 - -(** [iter_constr_with_binders g f n c] iters [f n] on the immediate - subterms of [c]; it carries an extra data [n] (typically a lift - index) which is processed by [g] (which typically add 1 to [n]) at - each binder traversal; it is not recursive and the order with which - subterms are processed is not specified *) +(** Alias for [Constr.iter] *) val iter_constr_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit - -(** [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare - the immediate subterms of [c1] of [c2] if needed; Cast's, binders - name and Cases annotations are not taken into account *) +(** Alias for [Constr.iter_with_binders] *) val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool +(** Alias for [Constr.compare_head] *) -val constr_ord : constr -> constr -> int val hash_constr : constr -> int +(** Alias for [Constr.hash] *) (*********************************************************************) val hcons_sorts : sorts -> sorts -val hcons_constr : constr -> constr -val hcons_types : types -> types +(** Alias for [Constr.hashcons_sorts] *) -(**************************************) +val hcons_constr : constr -> constr +(** Alias for [Constr.hashcons] *) -type values +val hcons_types : types -> types +(** Alias for [Constr.hashcons] *) |