From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- kernel/term.mli | 109 ++++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 86 insertions(+), 23 deletions(-) (limited to 'kernel/term.mli') diff --git a/kernel/term.mli b/kernel/term.mli index 3b5a2bc1..0de83166 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: term.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names @@ -42,7 +42,7 @@ type metavariable = int (*s Case annotation *) type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle type case_printing = - { ind_nargs : int; (* number of real args 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 *) type case_info = @@ -63,13 +63,13 @@ 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 {\em types} (i.e. terms of type a sort). + with {\em 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. - The following functions are intended to simplify and to uniform the + The following functions are intended to simplify and to uniform the manipulation of terms. Some of these functions may be overlapped with previous ones. *) @@ -96,9 +96,9 @@ val mkType : Univ.universe -> types (* This defines the strategy to use for verifiying a Cast *) -type cast_kind = VMcast | DEFAULTcast +type cast_kind = VMcast | DEFAULTcast -(* Constructs the term [t1::t2], i.e. the term $t_1$ casted with the +(* 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 @@ -122,7 +122,7 @@ val mkNamedLetIn : identifier -> constr -> types -> constr -> constr $(f~t_1~\dots~t_n)$. *) val mkApp : constr * constr array -> constr -(* Constructs a constant *) +(* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) val mkConst : constant -> constr @@ -132,7 +132,7 @@ val mkConst : constant -> constr (* 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 @@ -162,8 +162,8 @@ val mkFix : fixpoint -> constr [typarray = [|t1,...tn|]] [bodies = [b1,.....bn]] \par\noindent then [mkCoFix (i, (typsarray, funnames, bodies))] - constructs the ith function of the block - + constructs the ith function of the block + [CoFixpoint f1 = b1 with f2 = b2 ... @@ -208,11 +208,12 @@ type ('constr, 'types) kind_of_term = 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 *) type ('constr, 'types) kind_of_type = | SortType of sorts - | CastType of 'types * 'types + | CastType of 'types * 'types | ProdType of name * 'types * 'types | LetInType of name * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array @@ -226,6 +227,7 @@ val isVar : constr -> bool val isInd : constr -> bool val isEvar : constr -> bool val isMeta : constr -> bool +val isEvar_or_Meta : constr -> bool val isSort : constr -> bool val isCast : constr -> bool val isApp : constr -> bool @@ -245,7 +247,7 @@ val is_Type : constr -> bool val iskind : constr -> bool val is_small : sorts -> bool -(*s Term destructors. +(*s Term destructors. Destructor operations are partial functions and raise [invalid_arg "dest*"] if the term has not the expected form. *) @@ -258,7 +260,7 @@ val destMeta : constr -> metavariable (* Destructs a variable *) val destVar : constr -> identifier -(* Destructs a sort. [is_Prop] recognizes the sort \textsf{Prop}, whether +(* Destructs a sort. [is_Prop] recognizes the sort \textsf{Prop}, whether [isprop] recognizes both \textsf{Prop} and \textsf{Set}. *) val destSort : constr -> sorts @@ -298,7 +300,7 @@ val destConstruct : constr -> constructor (* Destructs a term

Case c of lc1 | lc2 .. | lcn end *) val destCase : constr -> case_info * constr * constr * constr array -(* Destructs the $i$th function of the block +(* 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 @@ -330,6 +332,18 @@ 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 *) + +(* 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 + +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] *) val mkProd_or_LetIn : rel_declaration -> types -> types val mkNamedProd_or_LetIn : named_declaration -> types -> types @@ -352,7 +366,7 @@ 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$ +(* [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]$ *) val prodn : int -> (name * constr) list -> constr -> constr @@ -367,15 +381,15 @@ 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)]$. - Inverse of [decompose_lam] *) + Inverse of [it_destLam] *) val compose_lam : (name * constr) list -> constr -> constr -(* [to_lambda n l] +(* [to_lambda n l] = $[x_1:T_1]...[x_n:T_n]T$ where $l = (x_1:T_1)...(x_n:T_n)T$ *) val to_lambda : int -> constr -> constr -(* [to_prod n l] +(* [to_prod n l] = $(x_1:T_1)...(x_n:T_n)T$ where $l = [x_1:T_1]...[x_n:T_n]T$ *) val to_prod : int -> constr -> constr @@ -386,6 +400,9 @@ val to_prod : int -> constr -> constr 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. *) (* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair @@ -397,22 +414,53 @@ val decompose_prod : constr -> (name*constr) list * constr $([(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 +(* 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 +(* 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 + "(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 *) +val decompose_lam_assum : constr -> rel_context * constr + +(* 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) *) 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) *) +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)*) +val prod_n_assum : int -> types -> rel_context +val lam_n_assum : int -> constr -> rel_context + +(* 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 *) +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) *) +val strip_prod_assum : types -> types +val strip_lam_assum : constr -> constr + (* flattens application lists *) val collapse_appl : constr -> constr @@ -427,6 +475,21 @@ val under_casts : (constr -> constr) -> constr -> constr (* 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. + 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 *) +val mkArity : arity -> types + +(* Destructs an "arity" into its canonical form *) +val destArity : types -> arity + +(* Tells if a term has the form of an arity *) +val isArity : types -> bool + (*s Occur checks *) (* [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *) @@ -532,11 +595,11 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool val hcons_constr: (constant -> constant) * - (kernel_name -> kernel_name) * + (mutual_inductive -> mutual_inductive) * (dir_path -> dir_path) * (name -> name) * (identifier -> identifier) * - (string -> string) + (string -> string) -> (constr -> constr) * (types -> types) -- cgit v1.2.3