RELATIONAL: new undecomposable definition of NLE

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

diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml
index 4cfd47e5abcac8309337f7f808b87c37f750bd50..6fd8a5e60597adb67540b4219ea20d1677d9e442 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralClassify.ml
+++ b/helm/software/components/acic_procedural/proceduralClassify.ml
@@ -26,19 +26,15 @@
 module C = Cic
 module R = CicReduction
 module D = Deannotate
-module Int = struct
-   type t = int
-   let compare = compare 
-end
-module S = Set.Make (Int) 
+module I = CicInspect
 
 type conclusion = (int * int) option
 
 (* debugging ****************************************************************)
 
 let string_of_entry inverse =
-   if S.mem 0 inverse then "C" else
-   if S.is_empty inverse then "I" else "P"
+   if I.S.mem 0 inverse then "C" else
+   if I.S.is_empty inverse then "I" else "P"
 
 let to_string (classes, rc) =
    let linearize = String.concat " " (List.map string_of_entry classes) in
@@ -49,7 +45,7 @@ let to_string (classes, rc) =
 let out_table b =
    let map i (_, inverse) =
       let map i tl = Printf.sprintf "%2u" i :: tl in 
-      let iset = String.concat " " (S.fold map inverse []) in
+      let iset = String.concat " " (I.S.fold map inverse []) in
       Printf.eprintf "%2u|%s\n" i iset
    in
    Array.iteri map b;
@@ -59,47 +55,6 @@ let out_table b =
 
 let id x = x
 
-let rec list_fold_left g map = function
-  | []       -> g
-  | hd :: tl -> map (list_fold_left g map tl) hd
-
-let get_rels h t = 
-   let rec aux d g = function
-      | C.Sort _
-      | C.Implicit _       -> g
-      | C.Rel i            -> 
-         if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
-      | C.Appl ss          -> list_fold_left g (aux d) ss
-      | C.Const (_, ss)
-      | C.MutInd (_, _, ss)
-      | C.MutConstruct (_, _, _, ss)
-      | C.Var (_, ss)      -> 
-         let map g (_, t) = aux d g t in 
-        list_fold_left g map ss
-      | C.Meta (_, ss)     ->
-         let map g = function 
-           | None   -> g
-           | Some t -> aux d g t
-        in
-        list_fold_left g map ss
-      | C.Cast (t1, t2)    -> aux d (aux d g t2) t1
-      | C.LetIn (_, t1, t2)
-      | C.Lambda (_, t1, t2)
-      | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
-      | C.MutCase (_, _, t1, t2, ss) ->
-        aux d (aux d (list_fold_left g (aux d) ss) t2) t1
-      | C.Fix (_, ss) ->
-         let k = List.length ss in
-        let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
-        list_fold_left g map ss
-      | C.CoFix (_, ss) ->
-         let k = List.length ss in
-        let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
-        list_fold_left g map ss
-   in
-   let g a = a in
-   aux 1 g t S.empty
-
 let split c t =
    let add s v c = Some (s, C.Decl v) :: c in
    let rec aux whd a n c = function
@@ -118,32 +73,28 @@ let classify c t =
 try   
    let vs, h = split c t in
    let rc = classify_conclusion (List.hd vs) in
-   let map (b, h) v = (get_rels h v, S.empty) :: b, succ h 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
    let b = Array.of_list (List.rev l) in
    let mk_closure b h =
-      let map j = if j < h then S.union (fst b.(j)) else id in 
+      let map j = if j < h then I.S.union (fst b.(j)) else id in 
       for i = pred h downto 0 do
          let direct, unused = b.(i) in
-        b.(i) <- S.fold map direct direct, unused 
+        b.(i) <- I.S.fold map direct direct, unused 
       done; b
    in
    let b = mk_closure b h in
    let rec mk_inverse i direct =
-      if S.is_empty direct then () else
-      let j = S.choose direct in
+      if I.S.is_empty direct then () else
+      let j = I.S.choose direct in
       if j < h then
          let unused, inverse = b.(j) in 
-         b.(j) <- unused, S.add i inverse
+         b.(j) <- unused, I.S.add i inverse
        else ();
-       mk_inverse i (S.remove j direct)
+       mk_inverse i (I.S.remove j direct)
    in
    let map i (direct, _) = mk_inverse i direct in
    Array.iteri map b;
 (*   out_table b; *)
    List.rev_map snd (List.tl (Array.to_list b)), rc
 with Invalid_argument _ -> failwith "Classify.classify"
-
-let overlaps s1 s2 =
-   let predicate x = S.mem x s1 in
-   S.exists predicate s2