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.

1 files changed, 17 insertions, 19 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 110555011..33beca28a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -120,24 +120,6 @@ let whd_betadeltaiota_nolet env t =
        Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
     | _ -> whd_val (create_clos_infos betadeltaiotanolet env) (inject t)
 
-(* Beta *)
-
-let beta_appvect c v =
-  let rec stacklam env t stack =
-    match kind_of_term t, stack with
-        Lambda(_,_,c), arg::stacktl -> stacklam (arg::env) c stacktl
-      | _ -> applist (substl env t, stack) in
-  stacklam [] c (Array.to_list v)
-    
-let betazeta_appvect n c v =
-  let rec stacklam n env t stack =
-    if Int.equal n 0 then applist (substl env t, stack) else
-    match kind_of_term t, stack with
-        Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
-      | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
-      | _ -> anomaly (Pp.str "Not enough lambda/let's") in
-  stacklam n [] c (Array.to_list v)
-
 (********************************************************************)
 (*                         Conversion                               *)
 (********************************************************************)
@@ -733,12 +715,28 @@ let conv env t1 t2 =
   Profile.profile4 convleqkey conv env t1 t2;;
 *)
 
+(* Application with on-the-fly reduction *)
+
+let beta_applist c l =
+  let rec app subst c l =
+    match kind_of_term c, l with
+    | Lambda(_,_,c), arg::l -> app (arg::subst) c l
+    | _ -> applist (substl subst c, l) in
+  app [] c l
+
+let beta_appvect c v = beta_applist c (Array.to_list v)
+
+let beta_app c a = beta_applist c [a]
+
+(* Compatibility *)
+let betazeta_appvect = lambda_appvect_assum
+
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
 
 (* pseudo-reduction rule:
- * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
+ * [hnf_prod_app env (Prod(_,B)) N --> B[N]
  * with an HNF on the first argument to produce a product.
  * if this does not work, then we use the string S as part of our
  * error message. *)