helm/software/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 = Unix.WEXITED 0 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 let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr =
 163  ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;
 164  print_string
 165   (string_of_cop candidate ^ " " ^ string_of_rel rel ^ " " ^ string_of_cop repr ^ "? ");
 166  flush stdout;
 167  assert (Unix.system "cat log.ma | sed s/^theorem/axiom/g | sed 's/\\. intros.*qed\\././g' > xxx.ma" = Unix.WEXITED 0);
 168  let ch = open_out_gen [Open_append] 0 "xxx.ma" in
 169 (*
 170  let i = ref 0 in
 171   List.iter
 172    (function (repr,others,leq,_) ->
 173      List.iter
 174       (function repr' ->
 175         incr i;
 176         output_string ch
 177          ("axiom ax" ^ string_of_int !i ^
 178           ": \\forall A." ^
 179            matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n");
 180       ) others;
 181      List.iter
 182       (function (repr',_,_,_) ->
 183         incr i;
 184         output_string ch
 185          ("axiom ax" ^ string_of_int !i ^
 186           ": \\forall A." ^
 187            matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n");
 188       ) !leq;
 189    ) s;
 190 *)
 191   let candidate',rel',repr' =
 192    match rel with
 193       SupersetEqual -> repr,SubsetEqual,candidate
 194     | Equal
 195     | SubsetEqual -> candidate,rel,repr in
 196   let query =
 197    let name = name_of_theorem candidate' rel' repr' in
 198    ("theorem " ^ name ^ ": \\forall A." ^ matita_of_cop "A" candidate' ^
 199       " " ^ string_of_rel rel' ^ " " ^
 200       matita_of_cop "A" repr' ^ ". intros; autobatch size=8 depth=3 width=2. qed.") in
 201   output_string ch (query ^ "\n");
 202   close_out ch;
 203   let res =
 204    (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*)
 205    profile Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0
 206   in
 207    ignore (Unix.system "echo '(*' >> log.ma && cat xxx.dot >> log.ma && echo '*)' >> log.ma");
 208    let ch = open_out_gen [Open_append] 0o0600 "log.ma" in
 209    if res then
 210     output_string ch (query ^ "\n")
 211    else
 212     output_string ch ("(* " ^ query ^ "*)\n");
 213    close_out ch;
 214    print_endline (if res then "y" else "n");
 215    res
 216
 217 let remove node = List.filter (fun node' -> node <=> node');;
 218
 219 let add_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
 220  leq := node' :: !leq;
 221  geq' := node :: !geq'
 222 ;;
 223
 224 let add_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
 225  geq := node' :: !geq;
 226  leq' := node :: !leq'
 227 ;;
 228
 229 let remove_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
 230  leq := remove node' !leq;
 231  geq' := remove node !geq'
 232 ;;
 233
 234 let remove_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
 235  geq := remove node' !geq;
 236  leq' := remove node !leq'
 237 ;;
 238
 239 let leq_transitive_closure node node' =
 240  add_leq_arc node node';
 241  let rec remove_transitive_arcs ((_,_,_,geq) as node) (_,_,leq',_) =
 242   let rec remove_arcs_to_ascendents =
 243    function
 244       [] -> ()
 245     | (_,_,leq,_) as node'::tl ->
 246        remove_leq_arc node node';
 247        remove_arcs_to_ascendents (!leq@tl)
 248   in
 249    remove_arcs_to_ascendents !leq';
 250    List.iter (function son -> remove_transitive_arcs son node) !geq
 251  in
 252   remove_transitive_arcs node node'
 253 ;;
 254
 255 let geq_transitive_closure node node' =
 256  add_geq_arc node node';
 257  let rec remove_transitive_arcs ((_,_,leq,_) as node) (_,_,_,geq') =
 258   let rec remove_arcs_to_descendents =
 259    function
 260       [] -> ()
 261     | (_,_,_,geq) as node'::tl ->
 262        remove_geq_arc node node';
 263        remove_arcs_to_descendents (!geq@tl)
 264   in
 265    remove_arcs_to_descendents !geq';
 266    List.iter (function father -> remove_transitive_arcs father node) !leq
 267  in
 268   remove_transitive_arcs node node'
 269 ;;
 270
 271 let (@@) l1 n = if List.exists (function n' -> n===n') l1 then l1 else l1@[n]
 272
 273 let rec leq_reachable node =
 274  function
 275     [] -> false
 276   | node'::_ when node === node' -> true
 277   | (_,_,leq,_)::tl -> leq_reachable node (!leq@tl)
 278 ;;
 279
 280 let rec geq_reachable node =
 281  function
 282     [] -> false
 283   | node'::_ when node === node' -> true
 284   | (_,_,_,geq)::tl -> geq_reachable node (!geq@tl)
 285 ;;
 286
 287 let locate_using_leq to_be_considered_and_now ((repr,_,leq,geq) as node)
 288  set start
 289 =
 290  let rec aux ((nodes,inf,sup) as set) already_visited =
 291   function
 292      [] -> set
 293    | (repr',_,_,geq') as node' :: tl ->
 294        if List.exists (function n -> n===node') already_visited then
 295         aux set already_visited tl
 296        else if repr=repr' then aux set (node'::already_visited) (!geq'@tl)
 297        else if leq_reachable node' !leq then
 298         aux set (node'::already_visited) tl
 299        else if test to_be_considered_and_now set SubsetEqual repr repr' then
 300         begin
 301          let sup = remove node sup in
 302          let inf =
 303           if !geq' = [] then
 304            let inf = remove node' inf in
 305             if !geq = [] then
 306              inf@@node
 307             else
 308              inf
 309           else
 310            inf
 311           in
 312            leq_transitive_closure node node';
 313            aux (nodes,inf,sup) (node'::already_visited) (!geq'@tl)
 314         end
 315        else
 316         aux set (node'::already_visited) tl
 317  in
 318   aux set [] start
 319 ;;
 320
 321 exception SameEquivalenceClass of set * equivalence_class * equivalence_class;;
 322
 323 let locate_using_geq to_be_considered_and_now ((repr,_,leq,geq) as node)
 324  set start
 325 =
 326  let rec aux ((nodes,inf,sup) as set) already_visited =
 327   function
 328      [] -> set
 329    | (repr',_,leq',_) as node' :: tl ->
 330        if List.exists (function n -> n===node') already_visited then
 331         aux set already_visited tl
 332        else if repr=repr' then aux set (node'::already_visited) (!leq'@tl)
 333        else if geq_reachable node' !geq then
 334         aux set (node'::already_visited) tl
 335        else if test to_be_considered_and_now set SupersetEqual repr repr' then
 336         begin
 337          if List.exists (function n -> n===node') !leq then
 338           (* We have found two equal nodes! *)
 339           raise (SameEquivalenceClass (set,node,node'))
 340          else
 341           begin
 342            let inf = remove node inf in
 343            let sup =
 344             if !leq' = [] then
 345              let sup = remove node' sup in
 346              if !leq = [] then
 347               sup@@node
 348              else
 349               sup
 350             else
 351              sup
 352            in
 353             geq_transitive_closure node node';
 354             aux (nodes,inf,sup) (node'::already_visited) (!leq'@tl)
 355           end
 356         end
 357        else
 358         aux set (node'::already_visited) tl
 359  in
 360   aux set [] start
 361 ;;
 362
 363 let analyze_one to_be_considered repr hecandidate (news,((nodes,inf,sup) as set)) =
 364 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);
 365 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);
 366  let candidate = hecandidate::repr in
 367   if List.length (List.filter ((=) M) candidate) > 1 then
 368    news,set
 369   else
 370    try
 371     let leq = ref [] in
 372     let geq = ref [] in
 373     let node = candidate,[],leq,geq in
 374     let nodes = nodes@[node] in
 375     let set = nodes,inf@[node],sup@[node] in
 376     let start_inf,start_sup =
 377      let repr_node =
 378       match List.filter (fun (repr',_,_,_) -> repr=repr') nodes with
 379          [node] -> node
 380        | _ -> assert false
 381      in
 382 inf,sup(*
 383      match hecandidate with
 384         I -> inf,[repr_node]
 385       | C -> [repr_node],sup
 386       | M -> inf,sup
 387 *)
 388     in
 389     let set =
 390      locate_using_leq (to_be_considered,Some repr,news) node set start_sup in
 391 (
 392 let _,inf,sup = set in
 393 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);
 394 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);
 395 );
 396     let set =
 397      locate_using_geq (to_be_considered,Some repr,news) node set start_inf
 398     in
 399 (
 400 let _,inf,sup = set in
 401 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);
 402 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);
 403 );
 404      news@[candidate],set
 405    with
 406     SameEquivalenceClass ((nodes,inf,sup) as set,((r,_,leq_d,geq_d) as node_to_be_deleted),node')->
 407 (
 408 let _,inf,sup = set in
 409 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);
 410 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);
 411 );
 412      let rec clean inf sup res =
 413       function
 414          [] -> inf,sup,res
 415        | node::tl when node===node_to_be_deleted ->
 416           clean inf sup res tl
 417        | (repr',others,leq,geq) as node::tl ->
 418           leq :=
 419            (let rec aux res =
 420              function
 421                 [] -> res
 422               | (_,_,leq,_) as node::tl ->
 423                  if node_to_be_deleted <=> node then
 424                   aux (res@[node]) tl
 425                  else
 426                   (List.filter (fun n ->not (leq_reachable n (res@tl))) !leq)@tl
 427             in
 428              aux [] !leq);
 429           let sup = if !leq = [] then sup@@node else sup in
 430           geq :=
 431            (let rec aux res =
 432              function
 433                 [] -> res
 434               | (_,_,_,geq) as node::tl ->
 435                  if node_to_be_deleted <=> node then
 436                   aux (res@[node]) tl
 437                  else
 438                   (List.filter (fun n ->not (geq_reachable n (res@tl))) !geq)@tl
 439             in
 440              aux [] !geq);
 441           let inf = if !geq = [] then inf@@node else inf in
 442           if node===node' then
 443            clean inf sup ((repr',others@[candidate],leq,geq)::res) tl
 444           else
 445            clean inf sup (node::res) tl
 446      in
 447      let inf,sup,nodes = clean inf sup [] nodes in
 448      let inf = remove node_to_be_deleted inf in
 449      let sup = remove node_to_be_deleted sup in
 450 let set = nodes,inf,sup in
 451 (
 452 let _,inf,sup = set in
 453 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);
 454 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);
 455 );
 456       news,(nodes,inf,sup)
 457 ;;
 458
 459 let rec explore i (set:set) news =
 460  let rec aux news set =
 461   function
 462      [] -> news,set
 463    | repr::tl ->
 464       let news,set =
 465        List.fold_right (analyze_one tl repr) [I;C;M] (news,set)
 466       in
 467        aux news set tl
 468  in
 469   let news,set = aux [] set news in
 470    if news = [] then
 471     begin
 472      print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
 473      print_endline (string_of_set set ^ "\n----------------");
 474      ps_of_set ([],None,[]) set
 475     end
 476    else
 477     begin
 478      print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
 479      print_endline (string_of_set set ^ "\n----------------");
 480      explore (i+1) set news
 481     end
 482 in
 483  let id = [] in
 484  let id_node = id,[],ref [], ref [] in
 485  let set = [id_node],[id_node],[id_node] in
 486   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
 487   print_endline (string_of_set set ^ "\n----------------");
 488   (*ignore (Unix.system "rm -f log");*)
 489   assert (Unix.system "cp formal_topology.ma log.ma" = Unix.WEXITED 0);
 490   ps_of_set ([id],None,[]) set;
 491   explore 1 set [id]
 492 ;;