From e8c47b652a0b53f8d3f7eaa877e81910c8de55d0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Nov 2015 17:11:39 +0100 Subject: Unifying betazeta_applist and prod_applist into a clearer interface. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - prod_applist - prod_applist_assum - lambda_applist - lambda_applist_assum expect an instance matching the quantified context. They are now in term.ml, with "list" being possibly "vect". Names are a bit arbitrary. Better propositions are welcome. They are put in term.ml in that reduction is after all not needed, because the intent is not to do β or ι on the fly but rather to substitute a λΓ.c or ∀Γ.c (seen as internalization of a Γ⊢c) into one step, independently of the idea of reducing. On the other side: - beta_applist - beta_appvect are seen as optimizations of application doing reduction on the fly only if possible. They are then kept as functions relevant for reduction.ml. --- kernel/reduction.mli | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ef764f34f..7db7e57bb 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -96,15 +96,20 @@ val default_conv_leq : ?l2r:bool -> types conversion_function (************************************************************************) +(** Builds an application node, reducing beta redexes it may produce. *) +val beta_applist : constr -> constr list -> constr + (** 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. *) -val betazeta_appvect : int -> constr -> constr array -> constr +(** Builds an application node, reducing beta redexe it may produce. *) +val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** Compatibility alias for Term.lambda_appvect_assum *) +val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) -- cgit v1.2.3