From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 24 May 2007 13:07:34 +0000 (+0000)
Subject: It no longer generates double arcs between nodes.
X-Git-Tag: 0.4.95@7852~445
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0805587bed3189b59fa3ac54ceea6988eb738db0;p=helm.git

It no longer generates double arcs between nodes.
Bug: it does not put ii in the same equivalence class as i.
---

diff --git a/matita/contribs/formal_topology/bin/theory_explorer.ml b/matita/contribs/formal_topology/bin/theory_explorer.ml
index 5d3098d01..b803f5a10 100644
--- a/matita/contribs/formal_topology/bin/theory_explorer.ml
+++ b/matita/contribs/formal_topology/bin/theory_explorer.ml
@@ -217,6 +217,20 @@ let geq_transitive_closure node node' =
 
 let (@@) l1 e = if List.memq e l1 then l1 else l1@[e]
 
+let rec leq_reachable node =
+ function
+    [] -> false
+  | node'::_ when node == node' -> true
+  | (_,_,leq,_)::tl -> leq_reachable node (!leq@tl)
+;;
+
+let rec geq_reachable node =
+ function
+    [] -> false
+  | node'::_ when node == node' -> true
+  | (_,_,_,geq)::tl -> geq_reachable node (!geq@tl)
+;;
+
 let locate_using_leq to_be_considered_and_now ((repr,_,leq,_) as node)
  ((_,_,sup) as set)
 =
@@ -229,9 +243,9 @@ let locate_using_leq to_be_considered_and_now ((repr,_,leq,_) as node)
        set
    | (repr',_,_,geq') as node' :: tl ->
        if repr=repr' then aux is_sup set (!geq'@tl)
-       else if List.mem node' !leq
-            || test to_be_considered_and_now set SubsetEqual repr repr'
-       then
+       else if leq_reachable node' !leq then
+        aux is_sup set tl
+       else if test to_be_considered_and_now set SubsetEqual repr repr' then
         begin
          let inf = if !geq' = [] then (remove node' inf)@@node else inf in
           leq_transitive_closure node node';
@@ -258,9 +272,9 @@ let locate_using_geq to_be_considered_and_now ((repr,_,leq,geq) as node)
        set
    | (repr',_,leq',_) as node' :: tl ->
        if repr=repr' then aux is_inf set (!leq'@tl)
-       else if List.mem node' !geq
-            || test to_be_considered_and_now set SupersetEqual repr repr'
-       then
+       else if geq_reachable node' !geq then
+        aux is_inf set tl
+       else if test to_be_considered_and_now set SupersetEqual repr repr' then
         begin
          if List.mem node' !leq then
           (* We have found two equal nodes! *)