1 files changed, 51 insertions, 27 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 33ed25fe1..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 ())
+    | _ -> anomaly (str"Needed a product, but didn't find one")
 
+(* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *)
+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
 
 (* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
-let prod_appvect t nL = Array.fold_left prod_app t nL
+let prod_appvect c v = prod_applist c (Array.to_list v)
 
-(* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *)
-let prod_applist t nL = List.fold_left prod_app t nL
+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 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)
+let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v)
 
 (*********************************)
 (* Other term destructors        *)
@@ -616,25 +659,6 @@ let decompose_lam_n_decls n =
   in
   lamdec_rec empty_rel_context n
 
-(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
- * gives n (casts are ignored) *)
-let nb_lam =
-  let rec nbrec n c = match kind_of_term c with
-    | Lambda (_,_,c) -> nbrec (n+1) c
-    | Cast (c,_,_) -> nbrec n c
-    | _ -> n
-  in
-  nbrec 0
-
-(* similar to nb_lam, but gives the number of products instead *)
-let nb_prod =
-  let rec nbrec n c = match kind_of_term c with
-    | Prod (_,_,c) -> nbrec (n+1) c
-    | Cast (c,_,_) -> nbrec n c
-    | _ -> n
-  in
-  nbrec 0
-
 let prod_assum t = fst (decompose_prod_assum t)
 let prod_n_assum n t = fst (decompose_prod_n_assum n t)
 let strip_prod_assum t = snd (decompose_prod_assum t)