Procedural : cic object preprocessor added

[helm.git] / components / acic_procedural / proceduralClassify.ml

diff --git a/components/acic_procedural/proceduralClassify.ml b/components/acic_procedural/proceduralClassify.ml
index 6fd8a5e60597adb67540b4219ea20d1677d9e442..2fd2d979d7053abecb185562b9567858df3e6b8c 100644 (file)
--- a/components/acic_procedural/proceduralClassify.ml
+++ b/components/acic_procedural/proceduralClassify.ml
@@ -24,10 +24,11 @@
  *)
 
 module C = Cic
-module R = CicReduction
 module D = Deannotate
 module I = CicInspect
 
+module P = ProceduralPreprocess
+
 type conclusion = (int * int) option
 
 (* debugging ****************************************************************)
@@ -55,15 +56,6 @@ let out_table b =
 
 let id x = x
 
-let split c t =
-   let add s v c = Some (s, C.Decl v) :: c in
-   let rec aux whd a n c = function
-      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
-      | v when whd        -> v :: a, n
-      | v                 -> aux true a n c (R.whd ~delta:true c v)
-    in
-    aux false [] 0 c t
-
 let classify_conclusion = function
    | C.Rel i                -> Some (i, 0)
    | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
@@ -71,7 +63,7 @@ let classify_conclusion = function
 
 let classify c t =
 try   
-   let vs, h = split c t in
+   let vs, h = P.split c t in
    let rc = classify_conclusion (List.hd vs) in
    let map (b, h) v = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in
    let l, h = List.fold_left map ([], 0) vs in