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 (******** 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 = 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 let locate_using_leq to_be_considered_and_now ((repr,_,leq,geq) as node)
 347  set start
 348 =
 349  let rec aux ((nodes,inf,sup) as set) already_visited =
 350   function
 351      [] -> set
 352    | (repr',_,_,geq') as node' :: tl ->
 353        if List.exists (function n -> n===node') already_visited then
 354         aux set already_visited tl
 355        else if repr=repr' then aux set (node'::already_visited) (!geq'@tl)
 356        else if leq_reachable node' !leq then
 357         aux set (node'::already_visited) tl
 358        else if test to_be_considered_and_now set SubsetEqual repr repr' then
 359         begin
 360          let sup = remove node sup in
 361          let inf =
 362           if !geq' = [] then
 363            let inf = remove node' inf in
 364             if !geq = [] then
 365              inf@@node
 366             else
 367              inf
 368           else
 369            inf
 370           in
 371            leq_transitive_closure node node';
 372            aux (nodes,inf,sup) (node'::already_visited) (!geq'@tl)
 373         end
 374        else
 375         aux set (node'::already_visited) tl
 376  in
 377   aux set [] start
 378 ;;
 379
 380 exception SameEquivalenceClass of set * equivalence_class * equivalence_class;;
 381
 382 let locate_using_geq to_be_considered_and_now ((repr,_,leq,geq) as node)
 383  set start
 384 =
 385  let rec aux ((nodes,inf,sup) as set) already_visited =
 386   function
 387      [] -> set
 388    | (repr',_,leq',_) as node' :: tl ->
 389        if List.exists (function n -> n===node') already_visited then
 390         aux set already_visited tl
 391        else if repr=repr' then aux set (node'::already_visited) (!leq'@tl)
 392        else if geq_reachable node' !geq then
 393         aux set (node'::already_visited) tl
 394        else if test to_be_considered_and_now set SupersetEqual repr repr' then
 395         begin
 396          if List.exists (function n -> n===node') !leq then
 397           (* We have found two equal nodes! *)
 398           raise (SameEquivalenceClass (set,node,node'))
 399          else
 400           begin
 401            let inf = remove node inf in
 402            let sup =
 403             if !leq' = [] then
 404              let sup = remove node' sup in
 405              if !leq = [] then
 406               sup@@node
 407              else
 408               sup
 409             else
 410              sup
 411            in
 412             geq_transitive_closure node node';
 413             aux (nodes,inf,sup) (node'::already_visited) (!leq'@tl)
 414           end
 415         end
 416        else
 417         aux set (node'::already_visited) tl
 418  in
 419   aux set [] start
 420 ;;
 421
 422 let analyze_one to_be_considered repr hecandidate (news,((nodes,inf,sup) as set)) =
 423 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);
 424 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);
 425  let candidate = hecandidate::repr in
 426   if List.length (List.filter ((=) M) candidate) > 1 then
 427    news,set
 428   else
 429    try
 430     let leq = ref [] in
 431     let geq = ref [] in
 432     let node = candidate,[],leq,geq in
 433     let nodes = nodes@[node] in
 434     let set = nodes,inf@[node],sup@[node] in
 435     let start_inf,start_sup =
 436      let repr_node =
 437       match List.filter (fun (repr',_,_,_) -> repr=repr') nodes with
 438          [node] -> node
 439        | _ -> assert false
 440      in
 441 inf,sup(*
 442      match hecandidate with
 443         I -> inf,[repr_node]
 444       | C -> [repr_node],sup
 445       | M -> inf,sup
 446 *)
 447     in
 448     let set =
 449      locate_using_leq (to_be_considered,Some repr,news) node set start_sup in
 450 (
 451 let _,inf,sup = set in
 452 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);
 453 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);
 454 );
 455     let set =
 456      locate_using_geq (to_be_considered,Some repr,news) node set start_inf
 457     in
 458 (
 459 let _,inf,sup = set in
 460 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);
 461 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);
 462 );
 463      news@[candidate],set
 464    with
 465     SameEquivalenceClass ((nodes,inf,sup) as set,((r,_,leq_d,geq_d) as node_to_be_deleted),node')->
 466 (
 467 let _,inf,sup = set in
 468 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);
 469 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);
 470 );
 471      let rec clean inf sup res =
 472       function
 473          [] -> inf,sup,res
 474        | node::tl when node===node_to_be_deleted ->
 475           clean inf sup res tl
 476        | (repr',others,leq,geq) as node::tl ->
 477           leq :=
 478            (let rec aux res =
 479              function
 480                 [] -> res
 481               | (_,_,leq,_) as node::tl ->
 482                  if node_to_be_deleted <=> node then
 483                   aux (res@[node]) tl
 484                  else
 485                   (List.filter (fun n ->not (leq_reachable n (res@tl))) !leq)@tl
 486             in
 487              aux [] !leq);
 488           let sup = if !leq = [] then sup@@node else sup in
 489           geq :=
 490            (let rec aux res =
 491              function
 492                 [] -> res
 493               | (_,_,_,geq) as node::tl ->
 494                  if node_to_be_deleted <=> node then
 495                   aux (res@[node]) tl
 496                  else
 497                   (List.filter (fun n ->not (geq_reachable n (res@tl))) !geq)@tl
 498             in
 499              aux [] !geq);
 500           let inf = if !geq = [] then inf@@node else inf in
 501           if node===node' then
 502            clean inf sup ((repr',others@[candidate],leq,geq)::res) tl
 503           else
 504            clean inf sup (node::res) tl
 505      in
 506      let inf,sup,nodes = clean inf sup [] nodes in
 507      let inf = remove node_to_be_deleted inf in
 508      let sup = remove node_to_be_deleted sup in
 509 let set = nodes,inf,sup in
 510 (
 511 let _,inf,sup = set in
 512 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);
 513 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);
 514 );
 515       news,(nodes,inf,sup)
 516 ;;
 517
 518 let rec explore i (set:set) news =
 519  let rec aux news set =
 520   function
 521      [] -> news,set
 522    | repr::tl ->
 523       let news,set =
 524        List.fold_right (analyze_one tl repr) [I;C;M] (news,set)
 525       in
 526        aux news set tl
 527  in
 528   let news,set = aux [] set news in
 529    if news = [] then
 530     begin
 531      print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
 532      print_endline (string_of_set set ^ "\n----------------");
 533      ps_of_set ([],None,[]) set
 534     end
 535    else
 536     begin
 537      print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
 538      print_endline (string_of_set set ^ "\n----------------");
 539      explore (i+1) set news
 540     end
 541 in
 542  let id = [] in
 543  let id_node = id,[],ref [], ref [] in
 544  let set = [id_node],[id_node],[id_node] in
 545   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
 546   print_endline (string_of_set set ^ "\n----------------");
 547   (*ignore (Unix.system "rm -f log");*)
 548   assert (Unix.system "cp formal_topology.ma log.ma" = Unix.WEXITED 0);
 549   ps_of_set ([id],None,[]) set;
 550   explore 1 set [id]
 551 ;;