diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 97 |
1 files changed, 59 insertions, 38 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 501aaf741e..32267f6c4c 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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} @@ -203,7 +202,7 @@ val destCoFix : constr -> cofixpoint (** 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))] + Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 1) (mkRel 2))] *) val mkArrow : types -> types -> constr @@ -213,14 +212,14 @@ 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 -val mkProd_wo_LetIn : rel_declaration -> types -> types -val mkNamedProd_or_LetIn : named_declaration -> types -> types -val mkNamedProd_wo_LetIn : named_declaration -> types -> types +val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types +val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types +val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types +val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types (** 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 +val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr +val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr (** {5 Other term constructors. } *) @@ -262,14 +261,34 @@ val to_lambda : int -> constr -> constr where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr +val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr +val it_mkProd_or_LetIn : types -> Context.Rel.t -> types + +(** In [lambda_applist c args], [c] is supposed to have the form + [λΓ.c] with [Γ] without let-in; it returns [c] with the variables + of [Γ] instantiated by [args]. *) +val lambda_applist : constr -> constr list -> constr +val lambda_appvect : constr -> constr array -> constr + +(** In [lambda_applist_assum n c args], [c] is supposed to have the + form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it + returns [c] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val lambda_applist_assum : int -> constr -> constr list -> constr +val lambda_appvect_assum : int -> constr -> constr array -> constr + (** pseudo-reduction rule *) (** [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 +(** In [prod_appvect_assum n c args], [c] is supposed to have the + form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it + returns [c] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val prod_appvect_assum : int -> constr -> constr array -> constr +val prod_applist_assum : int -> constr -> constr list -> constr (** {5 Other term destructors. } *) @@ -281,40 +300,42 @@ val decompose_prod : constr -> (Name.t*constr) list * constr {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *) val decompose_lam : constr -> (Name.t*constr) list * constr -(** Given a positive integer n, transforms a product term +(** Given a positive integer n, decompose a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} - into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *) + into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. + Raise a user error if not enough products. *) 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){% $ %} *) +(** Given a positive integer {% $ %}n{% $ %}, decompose a lambda term + {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}. + Raise a user error if not enough lambdas. *) 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 *) -val decompose_prod_assum : types -> rel_context * types +val decompose_prod_assum : types -> Context.Rel.t * types (** Idem with lambda's *) -val decompose_lam_assum : constr -> rel_context * constr +val decompose_lam_assum : constr -> Context.Rel.t * constr + +(** Idem but extract the first [n] premisses, counting let-ins. *) +val decompose_prod_n_assum : int -> types -> Context.Rel.t * types -(** 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 +(** Idem for lambdas, _not_ counting let-ins *) +val decompose_lam_n_assum : int -> constr -> Context.Rel.t * 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 +(** Idem, counting let-ins *) +val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr -(** Similar to [nb_lam], but gives the number of products instead *) -val nb_prod : constr -> int +(** Return the premisses/parameters of a type/term (let-in included) *) +val prod_assum : types -> Context.Rel.t +val lam_assum : constr -> Context.Rel.t -(** Returns the premisses/parameters of a type/term (let-in included) *) -val prod_assum : types -> rel_context -val lam_assum : constr -> rel_context +(** Return the first n-th premisses/parameters of a type (let included and counted) *) +val prod_n_assum : int -> types -> Context.Rel.t -(** 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 +(** Return the first n-th premisses/parameters of a term (let included but not counted) *) +val lam_n_assum : int -> constr -> Context.Rel.t (** Remove the premisses/parameters of a type/term *) val strip_prod : types -> types @@ -328,11 +349,11 @@ val strip_lam_n : int -> constr -> constr 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. +(** Remove recursively the casts around a term i.e. [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) val strip_outer_cast : constr -> constr @@ -347,15 +368,15 @@ val under_outer_cast : (constr -> constr) -> constr -> constr Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = rel_context * sorts +type arity = Context.Rel.t * sorts (** Build an "arity" from its canonical form *) val mkArity : arity -> types -(** Destructs an "arity" into its canonical form *) +(** Destruct an "arity" into its canonical form *) val destArity : types -> arity -(** Tells if a term has the form of an arity *) +(** Tell if a term has the form of an arity *) val isArity : types -> bool (** {5 Kind of type} *) @@ -427,11 +448,11 @@ val eq_constr : constr -> constr -> bool (** [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 +val eq_constr_univs : constr UGraph.check_function (** [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 +val leq_constr_univs : constr UGraph.check_function (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and ignoring universe instances. *) |