X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Ftheory_explorer.ml;h=2ea4abf37c994e603616b7208096d343b5091ef5;hb=e1f0bb910f75b8b21f2c5e394ebb4c5a63ef4945;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..2ea4abf37 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
@@ -53,15 +59,24 @@ type set = equivalence_class list
 let string_of_set s =
  String.concat "\n" (List.map string_of_equivalence_class s)
 
-let ps_of_set ?processing s =
+let ps_of_set (to_be_considered,under_consideration) ?processing s =
  let ch = open_out "xxx.dot" in
   output_string ch "digraph G {\n";
+  (match under_consideration with
+      None -> ()
+    | Some repr ->
+       output_string ch (dot_of_cop repr ^ " [color=yellow];"));
+  List.iter
+   (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];")
+   ) to_be_considered ;
   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 (dot_of_cop repr ^ " [color=red];");
        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"));
@@ -69,8 +84,8 @@ let ps_of_set ?processing s =
   close_out ch;
   ignore (Unix.system "dot -Tps xxx.dot > xxx.ps")
 
-let test set rel candidate repr =
- ps_of_set ~processing:(candidate,rel,repr) set;
+let test to_be_considered_and_now set rel candidate repr =
+ ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;
  print_string
   (string_of_cop candidate ^ " " ^ rel ^ " " ^ string_of_cop repr ^ "? ");
  flush stdout;
@@ -106,12 +121,12 @@ let test set rel candidate repr =
    print_endline (if res then "y" else "n");
    res
 
-let normalize candidate set =
+let normalize to_be_considered_and_now candidate set =
  let rec aux =
   function
      [] -> raise Not_found
    | (repr,others,leq,geq) as eqclass :: tl ->
-       if test set "=" candidate repr then
+       if test to_be_considered_and_now set "=" candidate repr then
         (repr,others@[candidate],leq,geq)::tl
        else
         eqclass::(aux tl) 
@@ -119,18 +134,18 @@ let normalize candidate set =
   aux set
 ;;
 
-let locate ((repr,_,leq,geq) as node) set =
+let locate to_be_considered_and_now ((repr,_,leq,geq) as node) set =
  let rec aux =
   function
      [] -> ()
    | (repr',_,leq',geq') as node' :: tl ->
        if repr = repr' then ()
-       else if test set "⊆" repr repr' then
+       else if test to_be_considered_and_now set "⊆" repr repr' then
         begin
          leq  := node' :: !leq;
          geq' := node  :: !geq'
         end
-       else if test set "⊆" repr' repr then
+       else if test to_be_considered_and_now set "⊆" repr' repr then
         begin
          geq  := node' :: !geq;
          leq' := node  :: !leq'
@@ -140,13 +155,13 @@ let locate ((repr,_,leq,geq) as node) set =
   aux set
 ;;
 
-let analyze_one i repr hecandidate (news,set) =
+let analyze_one to_be_considered 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
-    let set = normalize candidate set in
+    let set = normalize (to_be_considered,Some repr) candidate set in
      news,set
    with
     Not_found ->
@@ -154,35 +169,32 @@ let analyze_one i repr hecandidate (news,set) =
      let geq = ref [] in
      let node = candidate,[],leq,geq in
      let set = node::set in
-      locate node set;
+      locate (to_be_considered,Some repr) node 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 tl 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 ([],None) 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
@@ -190,6 +202,6 @@ in
   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
   print_endline (string_of_set set ^ "\n----------------");
   ignore (Unix.system "rm -f log");
-  ps_of_set set;
-  explore 0 1 set [id]
+  ps_of_set ([id],None) set;
+  explore 1 set [id]
 ;;