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.

5 files changed, 101 insertions, 35 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 466d48715..632b4daea 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -357,14 +357,14 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
       let cstr = ith_constructor_of_inductive ind (i+1) in
       let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in
       vargs @ [dep_cstr] in
-    let base = betazeta_appvect (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in
+    let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in
     it_mkProd_or_LetIn base cstrsign in
   Array.mapi build_one_branch mip.mind_nf_lc
 
 (* [p] is the predicate, [c] is the match object, [realargs] is the
    list of real args of the inductive type *)
 let build_case_type env n p c realargs =
-  whd_betaiota env (betazeta_appvect (n+1) p (Array.of_list (realargs@[c])))
+  whd_betaiota env (lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c])))
 
 let type_case_branches env (pind,largs) pj c =
   let specif = lookup_mind_specif env (fst pind) in
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. *)
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 *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 7d47c4609..455248dd5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -471,6 +471,36 @@ let rec to_prod n lam =
       | Cast (c,_,_) -> to_prod n c
       | _   -> errorlabstrm "to_prod" (mt ())
 
+let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
+let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
+
+(* Application with expected on-the-fly reduction *)
+
+let lambda_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
+    | _, [] -> substl subst c
+    | _ -> anomaly (Pp.str "Not enough lambda's") in
+  app [] c l
+
+let lambda_appvect c v = lambda_applist c (Array.to_list v)
+
+let lambda_app c a = lambda_applist c [a]
+
+let lambda_applist_assum n c l =
+  let rec app n subst t l =
+    if Int.equal n 0 then
+      if l == [] then substl subst t
+      else anomaly (Pp.str "Not enough arguments")
+    else match kind_of_term t, l with
+    | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+    | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+  app n [] c l
+
+let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v)
+
 (* pseudo-reduction rule:
  * [prod_app  s (Prod(_,B)) N --> B[N]
  * with an strip_outer_cast on the first argument to produce a product *)
@@ -478,19 +508,32 @@ let rec to_prod n lam =
 let prod_app t n =
   match kind_of_term (strip_outer_cast t) with
     | Prod (_,_,b) -> subst1 n b
-    | _ ->
-        errorlabstrm "prod_app"
-          (str"Needed a product, but didn't find one" ++ fnl ())
-
-
-(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
-let prod_appvect t nL = Array.fold_left prod_app t nL
+    | _ -> anomaly (str"Needed a product, but didn't find one")
 
 (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *)
-let prod_applist t nL = List.fold_left prod_app t nL
+let prod_applist c l =
+  let rec app subst c l =
+    match kind_of_term c, l with
+    | Prod(_,_,c), arg::l -> app (arg::subst) c l
+    | _, [] -> substl subst c
+    | _ -> anomaly (Pp.str "Not enough prod's") in
+  app [] c l
 
-let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
-let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
+(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
+let prod_appvect c v = prod_applist c (Array.to_list v)
+
+let prod_applist_assum n c l =
+  let rec app n subst t l =
+    if Int.equal n 0 then
+      if l == [] then substl subst t
+      else anomaly (Pp.str "Not enough arguments")
+    else match kind_of_term t, l with
+    | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+    | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+    | _ -> anomaly (Pp.str "Not enough prod/let's") in
+  app n [] c l
+
+let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v)
 
 (*********************************)
 (* Other term destructors        *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 69adb517a..972a67ebe 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -262,14 +262,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 -> rel_context -> constr
+val it_mkProd_or_LetIn : types -> rel_context -> 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. } *)