matita/contribs/formal_topology/bin/theory_explorer.ml

   1 (**** PROFILING ****)
   2 let ok_time = ref 0.0;;
   3 let ko_time = ref 0.0;;
   4
   5 let profile f x =
   6  let before = Unix.gettimeofday () in
   7  let res = f x in
   8  let after = Unix.gettimeofday () in
   9  let delta = after -. before in
  10   if res then
  11    ok_time := !ok_time +. delta
  12   else
  13    ko_time := !ko_time +. delta;
  14   res
  15 ;;
  16
  17 let _ =
  18  Sys.catch_break true;
  19  at_exit
  20   (function () ->
  21     prerr_endline
  22      ("\nTIME SPENT IN CHECKING GOOD CONJECTURES: " ^ string_of_float !ok_time);
  23     prerr_endline
  24      ("TIME SPENT IN CHECKING BAD CONJECTURES: " ^ string_of_float !ko_time);)
  25 ;;
  26
  27 (**** END PROFILING ****)
  28
  29 type rel = Equal | SubsetEqual | SupersetEqual
  30
  31 let string_of_rel =
  32  function
  33     Equal -> "="
  34   | SubsetEqual -> "⊆"
  35   | SupersetEqual -> "⊇"
  36
  37 (* operator *)
  38 type op = I | C | M
  39
  40 let string_of_op = function I -> "i" | C -> "c" | M -> "-"
  41 let matita_of_op = function I -> "i" | C -> "c" | M -> "m"
  42
  43 (* compound operator *)
  44 type compound_operator = op list
  45
  46 let string_of_cop op =
  47  if op = [] then "id" else String.concat "" (List.map string_of_op op)
  48
  49 let dot_of_cop op = "\"" ^ string_of_cop op ^ "\""
  50
  51 let matita_of_cop v =
  52  let rec aux =
  53   function
  54    | [] -> v
  55    | [op] -> matita_of_op op ^ " " ^ v
  56    | op::tl -> matita_of_op op ^ " (" ^ aux tl ^ ")"
  57  in
  58   aux
  59
  60 let name_of_theorem cop rel cop' =
  61  let cop,rel,cop' =
  62   match rel with
  63      Equal -> cop,"eq",cop'
  64    | SubsetEqual -> cop,"leq",cop'
  65    | SupersetEqual -> cop',"leq",cop
  66  in
  67   rel ^ "_" ^
  68    String.concat "" (List.map matita_of_op cop) ^ "_" ^
  69    String.concat "" (List.map matita_of_op cop')
  70 ;;
  71
  72 (* representative, other elements in the equivalence class,
  73    leq classes, geq classes *)
  74 type equivalence_class =
  75  compound_operator * compound_operator list *
  76   equivalence_class list ref * equivalence_class list ref
  77
  78 let (===) (repr,_,_,_) (repr',_,_,_) = repr = repr';;
  79 let (<=>) (repr,_,_,_) (repr',_,_,_) = repr <> repr';;
  80
  81 let string_of_equivalence_class (repr,others,leq,_) =
  82  String.concat " = " (List.map string_of_cop (repr::others)) ^
  83   (if !leq <> [] then
  84     "\n" ^
  85      String.concat "\n"
  86       (List.map
  87         (function (repr',_,_,_) ->
  88            string_of_cop repr ^ " ⊆ " ^ string_of_cop repr') !leq)
  89    else
  90     "")
  91
  92 let dot_of_equivalence_class (repr,others,leq,_) =
  93  (if others <> [] then
  94    let eq = String.concat " = " (List.map string_of_cop (repr::others)) in
  95     dot_of_cop repr ^ "[label=\"" ^ eq ^ "\"];" ^
  96      if !leq = [] then "" else "\n"
  97   else if !leq = [] then
  98    dot_of_cop repr ^ ";"
  99   else
 100    "") ^
 101    String.concat "\n"
 102     (List.map
 103       (function (repr',_,_,_) ->
 104          dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ ";") !leq)
 105
 106 (* set of equivalence classes, infima, suprema *)
 107 type set =
 108  equivalence_class list * equivalence_class list * equivalence_class list
 109
 110 let string_of_set (s,_,_) =
 111  String.concat "\n" (List.map string_of_equivalence_class s)
 112
 113 let ps_of_set (to_be_considered,under_consideration,news) ?processing (s,inf,sup) =
 114  let ch = open_out "xxx.dot" in
 115   output_string ch "digraph G {\n";
 116   (match under_consideration with
 117       None -> ()
 118     | Some repr ->
 119        output_string ch (dot_of_cop repr ^ " [color=yellow];"));
 120   List.iter
 121    (function (repr,_,_,_) ->
 122      if List.exists (function (repr',_,_,_) -> repr=repr') sup then
 123       output_string ch (dot_of_cop repr ^ " [shape=Mdiamond];")
 124      else
 125       output_string ch (dot_of_cop repr ^ " [shape=diamond];")
 126    ) inf ;
 127   List.iter
 128    (function (repr,_,_,_) ->
 129      if not (List.exists (function (repr',_,_,_) -> repr=repr') inf) then
 130       output_string ch (dot_of_cop repr ^ " [shape=polygon];")
 131    ) sup ;
 132   List.iter
 133    (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];")
 134    ) to_be_considered ;
 135   List.iter
 136    (function repr -> output_string ch (dot_of_cop repr ^ " [color=navy];")
 137    ) news ;
 138   output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s));
 139   output_string ch "\n";
 140   (match processing with
 141       None -> ()
 142     | Some (repr,rel,repr') ->
 143        output_string ch (dot_of_cop repr ^ " [color=red];");
 144        let repr,repr' =
 145         match rel with
 146            SupersetEqual -> repr',repr
 147          | Equal
 148          | SubsetEqual -> repr,repr'
 149        in
 150         output_string ch
 151          (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^
 152           " [" ^
 153           (match rel with Equal -> "arrowhead=none " | _ -> "") ^
 154           "style=dashed];\n"));
 155   output_string ch "}\n";
 156   close_out ch;
 157   (*ignore (Unix.system "tred xxx.dot > yyy.dot && dot -Tps yyy.dot > xxx.ps")*)
 158   ignore (Unix.system "cp xxx.ps xxx_old.ps && dot -Tps xxx.dot > xxx.ps");
 159   (*ignore (read_line ())*)
 160 ;;
 161
 162 (******** communication with matitawiki ************)
 163 let min_ch,mout_ch = Unix.open_process "../../../matitawiki.opt 2> /dev/null";;
 164
 165 let exec_cmd ?(undo=false) s =
 166  let un = if undo then "un" else "" in
 167 (*prerr_endline ("<pgip><" ^ un ^ "doitem>" ^ s ^ "</" ^ un ^ "doitem></pgip>\n");*)
 168  output_string mout_ch ("<pgip><" ^ un ^ "doitem>" ^ s ^ "</" ^ un ^ "doitem></pgip>\n");
 169  flush mout_ch;
 170  let rec aux v =
 171   let l = input_line min_ch in
 172   let last = String.length l - 1 in
 173    assert (last > 0);
 174    if l.[last] = Char.chr 249 then
 175     int_of_string (String.sub l 0 last)
 176    else
 177     aux l
 178  in
 179   aux "x"
 180 ;;
 181
 182 let exec_cmds =
 183  let rec aux undopos =
 184   function
 185      [] -> true
 186    | he::tl ->
 187       let pos = exec_cmd he in
 188        if pos = -1 then
 189         begin
 190          match undopos with
 191             None -> assert false
 192           | Some undopos ->
 193              assert (exec_cmd ~undo:true (string_of_int (undopos - 1)) <> -1);
 194              false
 195         end
 196        else
 197         match undopos with
 198            None -> aux (Some pos) tl
 199          | _ -> aux undopos tl
 200  in
 201   aux None
 202
 203 let _ =
 204  assert (exec_cmd "set \"baseuri\" \"cic:/matita/theory_former\"." <> -1);
 205  assert (exec_cmd "include \"formal_topology.ma\"." <> -1);
 206 ;;
 207
 208 (********* testing a conjecture *******************)
 209
 210 let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr =
 211  ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;
 212  print_string
 213   (string_of_cop candidate ^ " " ^ string_of_rel rel ^ " " ^ string_of_cop repr ^ "? ");
 214  flush stdout;
 215 (*
 216  assert (Unix.system "cat log.ma | sed s/^theorem/axiom/g | sed 's/\\. intros.*qed\\././g' > xxx.ma" = Unix.WEXITED 0);
 217  let ch = open_out_gen [Open_append] 0 "xxx.ma" in
 218 *)
 219 (*
 220  let i = ref 0 in
 221   List.iter
 222    (function (repr,others,leq,_) ->
 223      List.iter
 224       (function repr' ->
 225         incr i;
 226         output_string ch
 227          ("axiom ax" ^ string_of_int !i ^
 228           ": \\forall A." ^
 229            matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n");
 230       ) others;
 231      List.iter
 232       (function (repr',_,_,_) ->
 233         incr i;
 234         output_string ch
 235          ("axiom ax" ^ string_of_int !i ^
 236           ": \\forall A." ^
 237            matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n");
 238       ) !leq;
 239    ) s;
 240 *)
 241   let candidate',rel',repr' =
 242    match rel with
 243       SupersetEqual -> repr,SubsetEqual,candidate
 244     | Equal
 245     | SubsetEqual -> candidate,rel,repr in
 246   let query1 =
 247    let name = name_of_theorem candidate' rel' repr' in
 248    ("theorem " ^ name ^ ": \\forall A." ^ matita_of_cop "A" candidate' ^
 249       " " ^ string_of_rel rel' ^ " " ^
 250       matita_of_cop "A" repr' ^ ".") in
 251   let query2 = "intros;" in
 252   let query3 = "autobatch size=8 depth=3 width=2." in
 253   let query4 = "qed." in
 254   let query = query1 ^ query2 ^ query3 ^ query4 in
 255 (*
 256   output_string ch (query ^ "\n");
 257   close_out ch;
 258 *)
 259   let res = profile exec_cmds [query1; query2; query3; query4] in
 260 (*
 261   let res =
 262    (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*)
 263    profile Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0
 264   in
 265 *)
 266    ignore (Unix.system "echo '(*' >> log.ma && cat xxx.dot >> log.ma && echo '*)' >> log.ma");
 267    let ch = open_out_gen [Open_append] 0o0600 "log.ma" in
 268    if res then
 269     output_string ch (query ^ "\n")
 270    else
 271     output_string ch ("(* " ^ query ^ "*)\n");
 272    close_out ch;
 273    print_endline (if res then "y" else "n");
 274    res
 275
 276 let remove node = List.filter (fun node' -> node <=> node');;
 277
 278 let add_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
 279  leq := node' :: !leq;
 280  geq' := node :: !geq'
 281 ;;
 282
 283 let add_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
 284  geq := node' :: !geq;
 285  leq' := node :: !leq'
 286 ;;
 287
 288 let remove_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
 289  leq := remove node' !leq;
 290  geq' := remove node !geq'
 291 ;;
 292
 293 let remove_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
 294  geq := remove node' !geq;
 295  leq' := remove node !leq'
 296 ;;
 297
 298 let leq_transitive_closure node node' =
 299  add_leq_arc node node';
 300  let rec remove_transitive_arcs ((_,_,_,geq) as node) (_,_,leq',_) =
 301   let rec remove_arcs_to_ascendents =
 302    function
 303       [] -> ()
 304     | (_,_,leq,_) as node'::tl ->
 305        remove_leq_arc node node';
 306        remove_arcs_to_ascendents (!leq@tl)
 307   in
 308    remove_arcs_to_ascendents !leq';
 309    List.iter (function son -> remove_transitive_arcs son node) !geq
 310  in
 311   remove_transitive_arcs node node'
 312 ;;
 313
 314 let geq_transitive_closure node node' =
 315  add_geq_arc node node';
 316  let rec remove_transitive_arcs ((_,_,leq,_) as node) (_,_,_,geq') =
 317   let rec remove_arcs_to_descendents =
 318    function
 319       [] -> ()
 320     | (_,_,_,geq) as node'::tl ->
 321        remove_geq_arc node node';
 322        remove_arcs_to_descendents (!geq@tl)
 323   in
 324    remove_arcs_to_descendents !geq';
 325    List.iter (function father -> remove_transitive_arcs father node) !leq
 326  in
 327   remove_transitive_arcs node node'
 328 ;;
 329
 330 let (@@) l1 n = if List.exists (function n' -> n===n') l1 then l1 else l1@[n]
 331
 332 let rec leq_reachable node =
 333  function
 334     [] -> false
 335   | node'::_ when node === node' -> true
 336   | (_,_,leq,_)::tl -> leq_reachable node (!leq@tl)
 337 ;;
 338
 339 let rec geq_reachable node =
 340  function
 341     [] -> false
 342   | node'::_ when node === node' -> true
 343   | (_,_,_,geq)::tl -> geq_reachable node (!geq@tl)
 344 ;;
 345
 346 exception SameEquivalenceClass of set * equivalence_class * equivalence_class;;
 347
 348 let locate_using_leq to_be_considered_and_now ((repr,_,leq,geq) as node)
 349  set start
 350 =
 351  let rec aux ((nodes,inf,sup) as set) already_visited =
 352   function
 353      [] -> set
 354    | (repr',_,_,geq') as node' :: tl ->
 355        if List.exists (function n -> n===node') already_visited then
 356         aux set already_visited tl
 357        else if repr=repr' then aux set (node'::already_visited) (!geq'@tl)
 358        else if leq_reachable node' !leq then
 359         aux set (node'::already_visited) (!geq'@tl)
 360        else if (List.exists (function n -> not (geq_reachable n [node'])) !geq)
 361         then
 362          aux set (node'::already_visited) tl
 363        else if test to_be_considered_and_now set SubsetEqual repr repr' then
 364         begin
 365          if List.exists (function n -> n===node') !geq then
 366           (* We have found two equal nodes! *)
 367           raise (SameEquivalenceClass (set,node,node'))
 368          else
 369           begin
 370            let sup = remove node sup in
 371            let inf =
 372             if !geq' = [] then
 373              let inf = remove node' inf in
 374               if !geq = [] then
 375                inf@@node
 376               else
 377                inf
 378             else
 379              inf
 380             in
 381              leq_transitive_closure node node';
 382              aux (nodes,inf,sup) (node'::already_visited) (!geq'@tl)
 383           end
 384         end
 385        else
 386         aux set (node'::already_visited) tl
 387  in
 388   aux set [] start
 389 ;;
 390
 391 let locate_using_geq to_be_considered_and_now ((repr,_,leq,geq) as node)
 392  set start
 393 =
 394  let rec aux ((nodes,inf,sup) as set) already_visited =
 395   function
 396      [] -> set
 397    | (repr',_,leq',_) as node' :: tl ->
 398        if List.exists (function n -> n===node') already_visited then
 399         aux set already_visited tl
 400        else if repr=repr' then aux set (node'::already_visited) (!leq'@tl)
 401        else if geq_reachable node' !geq then
 402         aux set (node'::already_visited) (!leq'@tl)
 403        else if (List.exists (function n -> not (leq_reachable n [node'])) !leq)
 404         then
 405          aux set (node'::already_visited) tl
 406        else if test to_be_considered_and_now set SupersetEqual repr repr' then
 407         begin
 408          if List.exists (function n -> n===node') !leq then
 409           (* We have found two equal nodes! *)
 410           raise (SameEquivalenceClass (set,node,node'))
 411          else
 412           begin
 413            let inf = remove node inf in
 414            let sup =
 415             if !leq' = [] then
 416              let sup = remove node' sup in
 417              if !leq = [] then
 418               sup@@node
 419              else
 420               sup
 421             else
 422              sup
 423            in
 424             geq_transitive_closure node node';
 425             aux (nodes,inf,sup) (node'::already_visited) (!leq'@tl)
 426           end
 427         end
 428        else
 429         aux set (node'::already_visited) tl
 430  in
 431   aux set [] start
 432 ;;
 433
 434 let analyze_one to_be_considered repr hecandidate (news,((nodes,inf,sup) as set)) =
 435 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then ((*ps_of_set ([],None,[]) set;*) assert false);
 436 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then (ps_of_set ([],None,[]) set; assert false);
 437  let candidate = hecandidate::repr in
 438   if List.length (List.filter ((=) M) candidate) > 1 then
 439    news,set
 440   else
 441    try
 442     let leq = ref [] in
 443     let geq = ref [] in
 444     let node = candidate,[],leq,geq in
 445     let nodes = nodes@[node] in
 446     let set = nodes,inf@[node],sup@[node] in
 447     let set,start_inf,start_sup =
 448      let repr_node =
 449       match List.filter (fun (repr',_,_,_) -> repr=repr') nodes with
 450          [node] -> node
 451        | _ -> assert false
 452      in
 453       match hecandidate,repr with
 454          I, I::_ -> raise (SameEquivalenceClass (set,node,repr_node))
 455        | I, _ ->
 456           add_leq_arc node repr_node;
 457           (nodes,remove repr_node inf@[node],sup),inf,sup
 458        | C, C::_ -> raise (SameEquivalenceClass (set,node,repr_node))
 459        | C, _ ->
 460           add_geq_arc node repr_node;
 461           (nodes,inf,remove repr_node sup@[node]),inf,sup
 462        | M, M::M::_ -> raise (SameEquivalenceClass (set,node,repr_node))
 463        | M, _ -> set,inf,sup
 464     in
 465     let set =
 466      locate_using_leq (to_be_considered,Some repr,news) node set start_sup in
 467 (
 468 let _,inf,sup = set in
 469 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
 470 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then (ps_of_set ([],None,[]) set; assert false);
 471 );
 472     let set =
 473      locate_using_geq (to_be_considered,Some repr,news) node set start_inf
 474     in
 475 (
 476 let _,inf,sup = set in
 477 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
 478 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then ((*ps_of_set ([],None,[]) set;*) assert false);
 479 );
 480      news@[candidate],set
 481    with
 482     SameEquivalenceClass ((nodes,inf,sup) as set,((r,_,leq_d,geq_d) as node_to_be_deleted),node')->
 483 (
 484 let _,inf,sup = set in
 485 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
 486 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then ((*ps_of_set ([],None,[]) set;*) assert false);
 487 );
 488      let rec clean inf sup res =
 489       function
 490          [] -> inf,sup,res
 491        | node::tl when node===node_to_be_deleted ->
 492           clean inf sup res tl
 493        | (repr',others,leq,geq) as node::tl ->
 494           leq :=
 495            (let rec aux res =
 496              function
 497                 [] -> res
 498               | (_,_,leq,_) as node::tl ->
 499                  if node_to_be_deleted <=> node then
 500                   aux (res@[node]) tl
 501                  else
 502                   (List.filter (fun n ->not (leq_reachable n (res@tl))) !leq)@tl
 503             in
 504              aux [] !leq);
 505           let sup = if !leq = [] then sup@@node else sup in
 506           geq :=
 507            (let rec aux res =
 508              function
 509                 [] -> res
 510               | (_,_,_,geq) as node::tl ->
 511                  if node_to_be_deleted <=> node then
 512                   aux (res@[node]) tl
 513                  else
 514                   (List.filter (fun n ->not (geq_reachable n (res@tl))) !geq)@tl
 515             in
 516              aux [] !geq);
 517           let inf = if !geq = [] then inf@@node else inf in
 518           if node===node' then
 519            clean inf sup ((repr',others@[candidate],leq,geq)::res) tl
 520           else
 521            clean inf sup (node::res) tl
 522      in
 523      let inf,sup,nodes = clean inf sup [] nodes in
 524      let inf = remove node_to_be_deleted inf in
 525      let sup = remove node_to_be_deleted sup in
 526 let set = nodes,inf,sup in
 527 (
 528 let _,inf,sup = set in
 529 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
 530 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then (ps_of_set ([],None,[]) set; assert false);
 531 );
 532       news,(nodes,inf,sup)
 533 ;;
 534
 535 let rec explore i (set:set) news =
 536  let rec aux news set =
 537   function
 538      [] -> news,set
 539    | repr::tl ->
 540       let news,set =
 541        List.fold_right (analyze_one tl repr) [I;C;M] (news,set)
 542       in
 543        aux news set tl
 544  in
 545   let news,set = aux [] set news in
 546    if news = [] then
 547     begin
 548      print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
 549      print_endline (string_of_set set ^ "\n----------------");
 550      ps_of_set ([],None,[]) set
 551     end
 552    else
 553     begin
 554      print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
 555      print_endline (string_of_set set ^ "\n----------------");
 556      explore (i+1) set news
 557     end
 558 in
 559  let id = [] in
 560  let id_node = id,[],ref [], ref [] in
 561  let set = [id_node],[id_node],[id_node] in
 562   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
 563   print_endline (string_of_set set ^ "\n----------------");
 564   (*ignore (Unix.system "rm -f log");*)
 565   assert (Unix.system "cp formal_topology.ma log.ma" = Unix.WEXITED 0);
 566   ps_of_set ([id],None,[]) set;
 567   explore 1 set [id]
 568 ;;