Moving three related small half-general half-ad-hoc utility functions

next to each other, waiting for possible integration into a more
uniform API.

2 files changed, 38 insertions, 0 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index ebd9d939aa..5716a19dd1 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -846,6 +846,34 @@ let decompose_prod_letin : constr -> int * rel_context * constr =
     | _               -> i,l,c in
   prodec_rec 0 []
 
+(* (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 nb_prod_modulo_zeta x =
+  let rec count n c =
+    match kind_of_term c with
+        Prod(_,_,t) -> count (n+1) t
+      | LetIn(_,a,_,t) -> count n (subst1 a t)
+      | Cast(c,_,_) -> count n c
+      | _ -> n
+  in count 0 x
+
 let align_prod_letin c a : rel_context * constr =
   let (lc,_,_) = decompose_prod_letin c in
   let (la,l,a) = decompose_prod_letin a in
diff --git a/engine/termops.mli b/engine/termops.mli
index 6c680005db..5d812131ed 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -174,6 +174,16 @@ val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
 val decompose_prod_letin : constr -> int * rel_context * constr
 val align_prod_letin : constr -> constr -> rel_context * constr
 
+(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
+   gives {% $ %}n{% $ %} (casts are ignored) *)
+val nb_lam : constr -> int
+
+(** Similar to [nb_lam], but gives the number of products instead *)
+val nb_prod : constr -> int
+
+(** Similar to [nb_prod], but zeta-contracts let-in on the way *)
+val nb_prod_modulo_zeta : constr -> int
+
 (** Get the last arg of a constr intended to be an application *)
 val last_arg : constr -> constr