X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Ftheory_explorer.ml;h=b17a32bdde6dfe5303df59b4c70958527f3a9271;hb=2231f2820190c8743854004a9efd902d3bb5baa4;hp=be1e107fb21081f8d62ea0bcc0bec192692f656f;hpb=99ca90bf28a25fcd1cd84596c37be43c97f74e6e;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml
index be1e107fb..b17a32bdd 100644
--- a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml
@@ -13,6 +13,8 @@ type compound_operator = op list
 let string_of_cop op =
  if op = [] then "id" else String.concat "" (List.map string_of_op op)
 
+let dot_of_cop op = "\"" ^ string_of_cop op ^ "\""
+
 let rec matita_of_cop v =
  function
   | [] -> v
@@ -40,12 +42,16 @@ let string_of_equivalence_class (repr,others,leq,_) =
 let dot_of_equivalence_class (repr,others,leq,_) =
  (if others <> [] then
    let eq = String.concat " = " (List.map string_of_cop (repr::others)) in
-    string_of_cop repr ^ "[label=\"" ^ eq ^ "\"];\n"
-  else "") ^
+    dot_of_cop repr ^ "[label=\"" ^ eq ^ "\"];" ^
+     if !leq = [] then "" else "\n"
+  else if !leq = [] then
+   dot_of_cop repr ^ ";"
+  else
+   "") ^
    String.concat "\n" 
     (List.map
       (function (repr',_,_,_) ->
-         string_of_cop repr' ^ " -> " ^ string_of_cop repr ^ ";") !leq)
+         dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ ";") !leq)
 
 (* set of equivalence classes *)
 type set = equivalence_class list
@@ -57,11 +63,12 @@ let ps_of_set ?processing s =
  let ch = open_out "xxx.dot" in
   output_string ch "digraph G {\n";
   output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s));
+  output_string ch "\n";
   (match processing with
       None -> ()
     | Some (repr,rel,repr') ->
        output_string ch
-        (string_of_cop repr' ^ " -> " ^ string_of_cop repr ^
+        (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^
          " [" ^
          (if rel="=" then "arrowhead=none " else "") ^
          "style=dashed];\n"));
@@ -140,9 +147,9 @@ let locate ((repr,_,leq,geq) as node) set =
   aux set
 ;;
 
-let analyze_one i repr hecandidate (news,set) =
+let analyze_one repr hecandidate (news,set) =
  let candidate = hecandidate::repr in
-  if List.length (List.filter ((=) M) candidate) > i then
+  if List.length (List.filter ((=) M) candidate) > 1 then
    news,set
   else
    try
@@ -158,31 +165,28 @@ let analyze_one i repr hecandidate (news,set) =
       candidate::news,set
 ;;
 
-let rec explore i j set news =
+let rec explore i set news =
  let rec aux news set =
   function
      [] -> news,set
    | repr::tl ->
       let news,set =
-       List.fold_right (analyze_one i repr) [I;C;M] (news,set)
+       List.fold_right (analyze_one repr) [I;C;M] (news,set)
       in
        aux news set tl
  in
   let news,set = aux [] set news in
    if news = [] then
     begin
-     print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i ^ " j=" ^ string_of_int j);
+     print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
      print_endline (string_of_set set ^ "\n----------------");
-     if i < 2 then
-      explore (i+1) 1 set (List.map (function (repr,_,_,_) -> repr) set)
-     else
-      ps_of_set set
+     ps_of_set set
     end
    else
     begin
-     print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i ^ " j=" ^ string_of_int j);
+     print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
      print_endline (string_of_set set ^ "\n----------------");
-     explore i (j+1) set news
+     explore (i+1) set news
     end
 in
  let id = [] in
@@ -191,5 +195,5 @@ in
   print_endline (string_of_set set ^ "\n----------------");
   ignore (Unix.system "rm -f log");
   ps_of_set set;
-  explore 0 1 set [id]
+  explore 1 set [id]
 ;;