diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-22 17:11:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:07:41 +0100 |
| commit | e8c47b652a0b53f8d3f7eaa877e81910c8de55d0 (patch) | |
| tree | 85e00c1bf5d9334a4381c38e950bd71ae5ecb7e6 /kernel/reduction.mli | |
| parent | e3cefca41b568b1e517313051a111b0416cd2594 (diff) | |
Unifying betazeta_applist and prod_applist into a clearer interface.
- 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.
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ef764f34f..7db7e57bb 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -97,14 +97,19 @@ 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 *) |