Moving unused code out of the kernel into Termops.

Strangely enough, the checker seems to rely on an outdated decompose_app
function which is not the same as the kernel, as the latter is sensitive
to casts. Cast-manipulating functions from the kernel are only used on
upper layers, and thus was moved there.

2 files changed, 22 insertions, 0 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 04f55f2c3..35917b368 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -678,6 +678,21 @@ let rec subst_meta bl c =
     | Meta i -> (try Int.List.assoc i bl with Not_found -> c)
     | _ -> map_constr (subst_meta bl) c
 
+let rec strip_outer_cast c = match kind_of_term c with
+  | Cast (c,_,_) -> strip_outer_cast c
+  | _ -> c
+
+(* flattens application lists throwing casts in-between *)
+let collapse_appl c = match kind_of_term c with
+  | App (f,cl) ->
+      let rec collapse_rec f cl2 =
+        match kind_of_term (strip_outer_cast f) with
+        | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+        | _ -> mkApp (f,cl2)
+      in
+      collapse_rec f cl
+  | _ -> c
+
 (* First utilities for avoiding telescope computation for subst_term *)
 
 let prefix_application eq_fun (k,c) (t : constr) =
diff --git a/engine/termops.mli b/engine/termops.mli
index c58e3728c..78826f79a 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -164,6 +164,13 @@ val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*)
 
 val eta_reduce_head : constr -> constr
 
+(** Flattens application lists *)
+val collapse_appl : constr -> constr
+
+(** Remove recursively the casts around a term i.e.
+   [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
+val strip_outer_cast : constr -> constr
+
 exception CannotFilter
 
 (** Lightweight first-order filtering procedure. Unification