From fc8408a10c29e472ec05e725a36da1f71d850937 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 2 Mar 2009 23:35:02 +0000
Subject: [PATCH] New version.

---
 .../contribs/formal_topology/bin/comb.ml      | 119 ++++++++----------
 1 file changed, 49 insertions(+), 70 deletions(-)

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index af5633ff3..922d39a7e 100755
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -95,92 +95,71 @@ let step (l : w list) =
  uniq
   (List.flatten
     (List.map
-     (function w -> List.map (fun x -> x@w) [[I];[C];[M];[]])
+     (function w -> List.map (fun x -> x@w) [[I];[C];(*[M];*)[]])
      l))
 ;;
 
-let classify (l : w list) =
- List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
-;;
-
-let print_graph =
- List.iter
-  (function (w,dir,w') ->
-    prerr_endline (string_of_w w ^ string_of_dir dir ^ string_of_w w'))
-;;
-
-print_graph (classify (step (step (step [[]]))));;
-
-(*
- let ns = ref [] in
-  List.iter (function eqc -> ns := eqc::!ns) s;
-  List.iter
-   (function eqc ->
-     List.iter
-      (function x ->
-        let eqc = simplify ([x] @@ eqc) in
-         if not (List.exists (fun eqc' -> eqc === eqc') !ns) then
-          ns := eqc::!ns
-      ) [I;C;M]
-   ) s;
-  combine_classes !ns
-;;
-
-
-
-let subseteq l1 l2 =
- List.for_all (fun x -> List.mem x l2) l1
+let leq rels x y =
+ let rec aux avoid x y =
+  x = y
+  || List.exists
+      (fun (x',dir,z) ->
+        x=x' && dir = Le && not (List.mem z avoid) && aux (z::avoid) z y) rels
+  || List.exists
+      (fun (z,dir,x') ->
+        x=x' && dir = Ge && not (List.mem z avoid) && aux (z::avoid) z y) rels
+ in
+  aux [x] x y
 ;;
 
-let (===) l1 l2 = subseteq l1 l2 && subseteq l2 l1;;
-
-let simplify eqc =
- let rec aux l =
-  let l' = uniq (List.flatten (List.map apply_rules l)) in
-  if l === l' then l else aux l'
- in
-  aux eqc
+let in_class rels eqc he =
+ match eqc with
+    [] -> assert false
+  | k::_ -> leq rels k he && leq rels he k
 ;;
 
-let combine_class_with_classes l1 =
- let rec aux =
+let add_class rels classes he =
+ let rec aux visited =
   function
-     [] -> [l1]
-   | l2::tl ->
-      if List.exists (fun x -> List.mem x l2) l1 then
-       uniq (l1 @ l2) :: tl
+     [] -> [he]::visited
+   | eqc::tl ->
+      if in_class rels eqc he then
+       (he::eqc)::tl@visited
       else
-       l2:: aux tl
+       aux (eqc::visited) tl
  in
-  aux
+  aux [] classes
 ;;
 
-let combine_classes l =
- let rec aux acc =
-  function
-     [] -> acc
-   | he::tl -> aux (combine_class_with_classes he acc) tl
+let classify (l : w list) =
+(*prerr_endline ("Classify: " ^ string_of_int (List.length l));*)
+ let rels =
+  List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
  in
-  aux [] l
+  let rec aux classes =
+   function
+      [] -> classes
+    | he::tl -> aux (add_class rels classes he) tl
+  in
+   aux [] l
 ;;
 
-let step (s : eqclass list) =
- let ns = ref [] in
-  List.iter (function eqc -> ns := eqc::!ns) s;
-  List.iter
-   (function eqc ->
-     List.iter
-      (function x ->
-        let eqc = simplify ([x] @@ eqc) in
-         if not (List.exists (fun eqc' -> eqc === eqc') !ns) then
-          ns := eqc::!ns
-      ) [I;C;M]
-   ) s;
-  combine_classes !ns
+let print_graph =
+ List.iter
+  (function (w,dir,w') ->
+    prerr_endline (string_of_w w ^ string_of_dir dir ^ string_of_w w'))
 ;;
 
-let classes = step (step (step (step [[[]]]))) in
+let print_graph' classes =
+ prerr_endline "=============================";
  prerr_endline ("Numero di classi trovate: " ^ string_of_int (List.length classes));
- print classes
+ List.iter (function eqc -> prerr_endline (string_of_eqclass eqc)) classes
+;;
+
+let rec iter n l =
+ print_graph' (classify l);
+ if n > 0 then
+  iter (n - 1) (step l)
+in
+ iter 4 [[]]
 ;;
-*)
-- 
2.39.2