summaryrefslogtreecommitdiff
path: root/kernel/term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.mli')
-rw-r--r--kernel/term.mli390
1 files changed, 207 insertions, 183 deletions
diff --git a/kernel/term.mli b/kernel/term.mli
index c9a97bbe..d5899f18 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -1,169 +1,176 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: term.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Names
-(*i*)
-(*s The sorts of CCI. *)
+(** {6 The sorts of CCI. } *)
type contents = Pos | Null
type sorts =
- | Prop of contents (* Prop and Set *)
- | Type of Univ.universe (* Type *)
+ | Prop of contents (** Prop and Set *)
+ | Type of Univ.universe (** Type *)
val set_sort : sorts
val prop_sort : sorts
val type1_sort : sorts
-(*s The sorts family of CCI. *)
+(** {6 The sorts family of CCI. } *)
type sorts_family = InProp | InSet | InType
val family_of_sort : sorts -> sorts_family
-(*s Useful types *)
+(** {6 Useful types } *)
-(*s Existential variables *)
+(** {6 Existential variables } *)
type existential_key = int
-(*s Existential variables *)
+(** {6 Existential variables } *)
type metavariable = int
-(*s Case annotation *)
-type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
+(** {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 *)
+ { ind_nargs : int; (** length of the arity of the inductive type *)
style : case_style }
-(* the integer is the number of real args, needed for reduction *)
+
+(** the integer is the number of real args, needed for reduction *)
type case_info =
{ ci_ind : inductive;
ci_npar : int;
- ci_cstr_nargs : int array; (* number of real args of each constructor *)
- ci_pp_info : case_printing (* not interpreted by the kernel *)
+ ci_cstr_ndecls : int array; (** number of real args of each constructor *)
+ ci_pp_info : case_printing (** not interpreted by the kernel *)
}
-(*s*******************************************************************)
-(* The type of constructions *)
+(** {6 The type of constructions } *)
type constr
-(* [eq_constr a b] is true if [a] equals [b] modulo alpha, casts,
+(** [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
+(** [types] is the same as [constr] but is intended to be used for
documentation to indicate that such or such function specifically works
- with {\em types} (i.e. terms of type a sort).
+ with {e types} (i.e. terms of type a sort).
(Rem:plurial form since [type] is a reserved ML keyword) *)
type types = constr
-(*s Functions for dealing with constr terms.
+(** {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. *)
-(*s Term constructors. *)
+(** {6 Term constructors. } *)
-(* Constructs a DeBrujin index (DB indices begin at 1) *)
+(** Constructs a DeBrujin index (DB indices begin at 1) *)
val mkRel : int -> constr
-(* Constructs a Variable *)
+(** Constructs a Variable *)
val mkVar : identifier -> constr
-(* Constructs an patvar named "?n" *)
+(** Constructs an patvar named "?n" *)
val mkMeta : metavariable -> constr
-(* Constructs an existential variable *)
+(** Constructs an existential variable *)
type existential = existential_key * constr array
val mkEvar : existential -> constr
-(* Construct a sort *)
+(** 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
+(** 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). *)
+(** 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] *)
+(** Constructs the product [(x:t1)t2] *)
val mkProd : name * types * types -> types
val mkNamedProd : identifier -> types -> types -> types
-(* non-dependant product $t_1 \rightarrow t_2$, an alias for
- [(_:t1)t2]. Beware $t_2$ is NOT lifted.
- Eg: A |- A->A is built by [(mkArrow (mkRel 0) (mkRel 1))] *)
+
+(** 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$ *)
+(** 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] *)
+(** 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)$. *)
+(** [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 *)
+(** Constructs a constant
+ The array of terms correspond to the variables introduced in the section *)
val mkConst : constant -> constr
-(* Inductive types *)
+(** 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 *)
+(** 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
+(** 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 the term <p>Case c of c1 | c2 .. | cn end *)
+(** 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|]]
+(** 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)
+ 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.]
- \noindent where the length of the $j$th context is $ij$.
+ 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|]]
+(** If [funnames = [|f1,.....fn|]]
[typarray = [|t1,...tn|]]
- [bodies = [b1,.....bn]] \par\noindent
- then [mkCoFix (i, (typsarray, funnames, bodies))]
+ [bodies = [b1,.....bn]]
+ then [mkCoFix (i, (funnames, typarray, bodies))]
constructs the ith function of the block
-
+
[CoFixpoint f1 = b1
with f2 = b2
...
@@ -173,9 +180,9 @@ type cofixpoint = int * rec_declaration
val mkCoFix : cofixpoint -> constr
-(*s Concrete type for making pattern-matching. *)
+(** {6 Concrete type for making pattern-matching. } *)
-(* [constr array] is an instance matching definitional [named_context] in
+(** [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 ('constr, 'types) prec_declaration =
@@ -203,14 +210,13 @@ type ('constr, 'types) kind_of_term =
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
-(* User view of [constr]. For [App], it is ensured there is at
+(** User view of [constr]. For [App], it is ensured there is at
least one argument and the function is not itself an applicative
term *)
val kind_of_term : constr -> (constr, types) kind_of_term
-val kind_of_term2 : constr -> ((constr,types) kind_of_term,constr) kind_of_term
-(* Experimental *)
+(** Experimental, used in Presburger contrib *)
type ('constr, 'types) kind_of_type =
| SortType of sorts
| CastType of 'types * 'types
@@ -220,10 +226,11 @@ type ('constr, 'types) kind_of_type =
val kind_of_type : types -> (constr, types) kind_of_type
-(*s Simple term case analysis. *)
+(** {6 Simple term case analysis. } *)
val isRel : constr -> bool
val isVar : constr -> bool
+val isVarId : identifier -> constr -> bool
val isInd : constr -> bool
val isEvar : constr -> bool
val isMeta : constr -> bool
@@ -247,77 +254,83 @@ val is_Type : constr -> bool
val iskind : constr -> bool
val is_small : sorts -> bool
-(*s Term destructors.
- Destructor operations are partial functions and
- raise [invalid_arg "dest*"] if the term has not the expected form. *)
-(* Destructs a DeBrujin index *)
+(** {6 Term destructors } *)
+(** Destructor operations are partial functions and
+ @raise Invalid_argument "dest*" if the term has not the expected form. *)
+
+(** Destructs a DeBrujin index *)
val destRel : constr -> int
-(* Destructs an existential variable *)
+(** Destructs an existential variable *)
val destMeta : constr -> metavariable
-(* Destructs a variable *)
+(** Destructs a variable *)
val destVar : constr -> identifier
-(* Destructs a sort. [is_Prop] recognizes the sort \textsf{Prop}, whether
- [isprop] recognizes both \textsf{Prop} and \textsf{Set}. *)
+(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether
+ [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *)
val destSort : constr -> sorts
-(* Destructs a casted term *)
+(** Destructs a casted term *)
val destCast : constr -> constr * cast_kind * constr
-(* Destructs the product $(x:t_1)t_2$ *)
+(** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *)
val destProd : types -> name * types * types
-(* Destructs the abstraction $[x:t_1]t_2$ *)
+(** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)
val destLambda : constr -> name * types * constr
-(* Destructs the let $[x:=b:t_1]t_2$ *)
+(** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *)
val destLetIn : constr -> name * constr * types * constr
-(* Destructs an application *)
+(** Destructs an application *)
val destApp : constr -> constr * constr array
-(* Obsolete synonym of destApp *)
+(** Obsolete synonym of destApp *)
val destApplication : constr -> constr * constr array
-(* Decompose any term as an applicative term; the list of args can be empty *)
+(** Decompose any term as an applicative term; the list of args can be empty *)
val decompose_app : constr -> constr * constr list
-(* Destructs a constant *)
+(** Destructs a constant *)
val destConst : constr -> constant
-(* Destructs an existential variable *)
+(** Destructs an existential variable *)
val destEvar : constr -> existential
-(* Destructs a (co)inductive type *)
+(** Destructs a (co)inductive type *)
val destInd : constr -> inductive
-(* Destructs a constructor *)
+(** Destructs a constructor *)
val destConstruct : constr -> constructor
-(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
+(** 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
+return P in t1], or [if c then t1 else t2])
+@return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])]
+where [info] is pretty-printing information *)
val destCase : constr -> case_info * constr * constr * constr array
-(* Destructs the $i$th function of the block
- $\mathit{Fixpoint} ~ f_1 ~ [ctx_1] = b_1
- \mathit{with} ~ f_2 ~ [ctx_2] = b_2
- \dots
- \mathit{with} ~ f_n ~ [ctx_n] = b_n$,
- where the lenght of the $j$th context is $ij$.
+(** Destructs the {% $ %}i{% $ %}th function of the block
+ [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
+ with f{_ 2} ctx{_ 2} = b{_ 2}
+ ...
+ with f{_ n} ctx{_ n} = b{_ n}],
+ where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
*)
val destFix : constr -> fixpoint
val destCoFix : constr -> cofixpoint
-(*s A {\em declaration} has the form (name,body,type). It is either an
- {\em assumption} if [body=None] or a {\em definition} if
- [body=Some actualbody]. It is referred by {\em name} if [na] is an
- identifier or by {\em relative index} if [na] is not an identifier
+(** {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 *)
+ purpose) *)
type named_declaration = identifier * constr option * types
type rel_declaration = name * constr option * types
@@ -332,9 +345,25 @@ val fold_named_declaration :
val fold_rel_declaration :
(constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
-(*s Contexts of declarations referred to by de Bruijn indices *)
+val exists_named_declaration :
+ (constr -> bool) -> named_declaration -> bool
+val exists_rel_declaration :
+ (constr -> bool) -> rel_declaration -> bool
-(* In [rel_context], more recent declaration is on top *)
+val for_all_named_declaration :
+ (constr -> bool) -> named_declaration -> bool
+val for_all_rel_declaration :
+ (constr -> bool) -> rel_declaration -> bool
+
+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
@@ -344,185 +373,186 @@ val lookup_rel : int -> rel_context -> rel_declaration
val rel_context_length : rel_context -> int
val rel_context_nhyps : rel_context -> int
-(* Constructs either [(x:t)c] or [[x=b:t]c] *)
+(** Constructs either [(x:t)c] or [[x=b:t]c] *)
val mkProd_or_LetIn : rel_declaration -> types -> types
+val mkProd_wo_LetIn : rel_declaration -> types -> types
val mkNamedProd_or_LetIn : named_declaration -> types -> types
val mkNamedProd_wo_LetIn : named_declaration -> types -> types
-(* Constructs either [[x:t]c] or [[x=b:t]c] *)
+(** Constructs either [[x:t]c] or [[x=b:t]c] *)
val mkLambda_or_LetIn : rel_declaration -> constr -> constr
val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr
-(*s Other term constructors. *)
+(** {6 Other term constructors. } *)
-val abs_implicit : constr -> constr
-val lambda_implicit : constr -> constr
-val lambda_implicit_lift : int -> constr -> constr
-
-(* [applist (f,args)] and co work as [mkApp] *)
+(** [applist (f,args)] and its variants work as [mkApp] *)
val applist : constr * constr list -> constr
val applistc : constr -> constr list -> constr
val appvect : constr * constr array -> constr
val appvectc : constr -> constr array -> constr
-(* [prodn n l b] = $(x_1:T_1)..(x_n:T_n)b$
- where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *)
+(** [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
-(* [compose_prod l b] = $(x_1:T_1)..(x_n:T_n)b$
- where $l = [(x_n,T_n);\dots;(x_1,T_1)]$.
+(** [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
-(* [lamn n l b] = $[x_1:T_1]..[x_n:T_n]b$
- where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *)
+(** [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
-(* [compose_lam l b] = $[x_1:T_1]..[x_n:T_n]b$
- where $l = [(x_n,T_n);\dots;(x_1,T_1)]$.
+(** [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
-(* [to_lambda n l]
- = $[x_1:T_1]...[x_n:T_n]T$
- where $l = (x_1:T_1)...(x_n:T_n)T$ *)
+(** [to_lambda n l]
+ @return [fun (x_1:T_1)...(x_n:T_n) => T]
+ where [l] is [forall (x_1:T_1)...(x_n:T_n), T] *)
val to_lambda : int -> constr -> constr
-(* [to_prod n l]
- = $(x_1:T_1)...(x_n:T_n)T$
- where $l = [x_1:T_1]...[x_n:T_n]T$ *)
+(** [to_prod n l]
+ @return [forall (x_1:T_1)...(x_n:T_n), T]
+ where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *)
val to_prod : int -> constr -> constr
-(* pseudo-reduction rule *)
+(** pseudo-reduction rule *)
-(* [prod_appvect] $(x1:B1;...;xn:Bn)B a1...an \rightarrow B[a1...an]$ *)
+(** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *)
val prod_appvect : constr -> constr array -> constr
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
-(*s Other term destructors. *)
+(** {6 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.
+(** 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.
It includes also local definitions *)
val decompose_prod : constr -> (name*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. *)
+(** 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
-(* 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)$. *)
+(** 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
-(* 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)$ *)
+(** 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
-(* Extract the premisses and the conclusion of a term of the form
+(** 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 *)
val decompose_prod_assum : types -> rel_context * types
-(* Idem with lambda's *)
+(** Idem with lambda's *)
val decompose_lam_assum : constr -> rel_context * constr
-(* Idem but extract the first [n] premisses *)
+(** Idem but extract the first [n] premisses *)
val decompose_prod_n_assum : int -> types -> rel_context * types
val decompose_lam_n_assum : int -> constr -> rel_context * constr
-(* [nb_lam] $[x_1:T_1]...[x_n:T_n]c$ where $c$ is not an abstraction
- gives $n$ (casts are ignored) *)
+(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
+ gives {% $ %}n{% $ %} (casts are ignored) *)
val nb_lam : constr -> int
-(* Similar to [nb_lam], but gives the number of products instead *)
+(** Similar to [nb_lam], but gives the number of products instead *)
val nb_prod : constr -> int
-(* Returns the premisses/parameters of a type/term (let-in included) *)
+(** Returns the premisses/parameters of a type/term (let-in included) *)
val prod_assum : types -> rel_context
val lam_assum : constr -> rel_context
-(* Returns the first n-th premisses/parameters of a type/term (let included)*)
+(** Returns the first n-th premisses/parameters of a type/term (let included)*)
val prod_n_assum : int -> types -> rel_context
val lam_n_assum : int -> constr -> rel_context
-(* Remove the premisses/parameters of a type/term *)
+(** Remove the premisses/parameters of a type/term *)
val strip_prod : types -> types
val strip_lam : constr -> constr
-(* Remove the first n-th premisses/parameters of a type/term *)
+(** Remove the first n-th premisses/parameters of a type/term *)
val strip_prod_n : int -> types -> types
val strip_lam_n : int -> constr -> constr
-(* Remove the premisses/parameters of a type/term (including let-in) *)
+(** Remove the premisses/parameters of a type/term (including let-in) *)
val strip_prod_assum : types -> types
val strip_lam_assum : constr -> constr
-(* flattens application lists *)
+(** flattens application lists *)
val collapse_appl : constr -> constr
-(* Removes recursively the casts around a term i.e.
- [strip_outer_cast] (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
+(** Removes recursively the casts around a term i.e.
+ [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
val strip_outer_cast : constr -> constr
-(* Apply a function letting Casted types in place *)
+(** Apply a function letting Casted types in place *)
val under_casts : (constr -> constr) -> constr -> constr
-(* Apply a function under components of Cast if any *)
+(** Apply a function under components of Cast if any *)
val under_outer_cast : (constr -> constr) -> constr -> constr
-(*s An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
+(** {6 ... } *)
+(** 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 *)
type arity = rel_context * sorts
-(* Build an "arity" from its canonical form *)
+(** Build an "arity" from its canonical form *)
val mkArity : arity -> types
-(* Destructs an "arity" into its canonical form *)
+(** Destructs an "arity" into its canonical form *)
val destArity : types -> arity
-(* Tells if a term has the form of an arity *)
+(** Tells if a term has the form of an arity *)
val isArity : types -> bool
-(*s Occur checks *)
+(** {6 Occur checks } *)
-(* [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
+(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
val closedn : int -> constr -> bool
-(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(** [closed0 M] is true iff [M] is a (deBruijn) closed term *)
val closed0 : constr -> bool
-(* [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *)
+(** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *)
val noccurn : int -> constr -> bool
-(* [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M]
+(** [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
-(* Checking function for terms containing existential- or
+(** 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
-(*s Relocation and substitution *)
+(** {6 Relocation and substitution } *)
-(* [exliftn el c] lifts [c] with lifting [el] *)
+(** [exliftn el c] lifts [c] with lifting [el] *)
val exliftn : Esubst.lift -> constr -> constr
-(* [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
+(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
val liftn : int -> int -> constr -> constr
-(* [lift n c] lifts by [n] the positive indexes in [c] *)
+(** [lift n c] lifts by [n] the positive indexes in [c] *)
val lift : int -> constr -> constr
-(* [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an]
+(** [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
@@ -539,29 +569,30 @@ val substl_named_decl : constr list -> named_declaration -> named_declaration
val replace_vars : (identifier * constr) list -> constr -> constr
val subst_var : identifier -> constr -> constr
-(* [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t]
+(** [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
-(* [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
+
+(** [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
-(*s Functionals working on the immediate subterm of a construction *)
+(** {6 Functionals working on the immediate subterm of a construction } *)
-(* [fold_constr f acc c] folds [f] on the immediate subterms of [c]
+(** [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 fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
-(* [map_constr f c] maps [f] on the immediate subterms of [c]; it is
+(** [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 *)
val map_constr : (constr -> constr) -> constr -> constr
-(* [map_constr_with_binders g f n c] maps [f n] on the immediate
+(** [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
@@ -570,13 +601,13 @@ val map_constr : (constr -> constr) -> constr -> constr
val map_constr_with_binders :
('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
-(* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
+(** [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 iter_constr : (constr -> unit) -> constr -> unit
-(* [iter_constr_with_binders g f n c] iters [f n] on the immediate
+(** [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
@@ -585,27 +616,20 @@ val iter_constr : (constr -> unit) -> constr -> unit
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
+(** [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 *)
val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+val constr_ord : constr -> constr -> int
+val hash_constr : constr -> int
+
(*********************************************************************)
-val hcons_constr:
- (constant -> constant) *
- (mutual_inductive -> mutual_inductive) *
- (dir_path -> dir_path) *
- (name -> name) *
- (identifier -> identifier) *
- (string -> string)
- ->
- (constr -> constr) *
- (types -> types)
-
-val hcons1_constr : constr -> constr
-val hcons1_types : types -> types
+val hcons_sorts : sorts -> sorts
+val hcons_constr : constr -> constr
+val hcons_types : types -> types
(**************************************)