diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 390 |
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 (**************************************) |