diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 50 |
1 files changed, 24 insertions, 26 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 4a3e4cd5..aa78fbda 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,21 +1,17 @@ (************************************************************************) (* 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: reduction.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Term open Environ open Closure -(*i*) -(************************************************************************) -(*s Reduction functions *) +(*********************************************************************** + s Reduction functions *) val whd_betaiotazeta : constr -> constr val whd_betadeltaiota : env -> constr -> constr @@ -24,8 +20,8 @@ val whd_betadeltaiota_nolet : env -> constr -> constr val whd_betaiota : constr -> constr val nf_betaiota : constr -> constr -(************************************************************************) -(*s conversion functions *) +(*********************************************************************** + s conversion functions *) exception NotConvertible exception NotConvertibleVect of int @@ -40,45 +36,47 @@ val sort_cmp : val conv_sort : sorts conversion_function val conv_sort_leq : sorts conversion_function -val trans_conv_cmp : conv_pb -> constr trans_conversion_function +val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function val trans_conv : - ?evars:(existential->constr option) -> constr trans_conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function val trans_conv_leq : - ?evars:(existential->constr option) -> types trans_conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function -val conv_cmp : conv_pb -> constr conversion_function +val conv_cmp : ?l2r:bool -> conv_pb -> constr conversion_function val conv : - ?evars:(existential->constr option) -> constr conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function val conv_leq : - ?evars:(existential->constr option) -> types conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function val conv_leq_vecti : - ?evars:(existential->constr option) -> types array conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function -(* option for conversion *) +(** option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function -val set_default_conv : (conv_pb -> types conversion_function) -> unit -val default_conv : conv_pb -> types conversion_function -val default_conv_leq : types conversion_function +val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit +val default_conv : conv_pb -> ?l2r:bool -> types conversion_function +val default_conv_leq : ?l2r:bool -> types conversion_function (************************************************************************) -(* Builds an application node, reducing beta redexes it may produce. *) +(** Builds an application node, reducing beta redexes it may produce. *) val beta_appvect : constr -> constr array -> constr -(* Builds an application node, reducing the [n] first beta-zeta redexes. *) +(** Builds an application node, reducing the [n] first beta-zeta redexes. *) val betazeta_appvect : int -> constr -> constr array -> constr -(* Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) +(** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types -(************************************************************************) -(*s Recognizing products and arities modulo reduction *) +(*********************************************************************** + s Recognizing products and arities modulo reduction *) val dest_prod : env -> types -> rel_context * types val dest_prod_assum : env -> types -> rel_context * types -val dest_arity : env -> types -> arity +exception NotArity + +val dest_arity : env -> types -> arity (* raises NotArity if not an arity *) val is_arity : env -> types -> bool |