helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml

   1 type rel = Equal | SubsetEqual | SupersetEqual
   2
   3 let string_of_rel =
   4  function
   5     Equal -> "="
   6   | SubsetEqual -> "⊆"
   7   | SupersetEqual -> "⊇"
   8
   9 (* operator *)
  10 type op = I | C | M
  11
  12 let string_of_op =
  13  function
  14     I -> "i"
  15   | C -> "c"
  16   | M -> "-"
  17
  18 (* compound operator *)
  19 type compound_operator = op list
  20
  21 let string_of_cop op =
  22  if op = [] then "id" else String.concat "" (List.map string_of_op op)
  23
  24 let dot_of_cop op = "\"" ^ string_of_cop op ^ "\""
  25
  26 let rec matita_of_cop v =
  27  function
  28   | [] -> v
  29   | I::tl -> "i (" ^ matita_of_cop v tl ^ ")"
  30   | C::tl -> "c (" ^ matita_of_cop v tl ^ ")"
  31   | M::tl -> "m (" ^ matita_of_cop v tl ^ ")"
  32
  33 (* representative, other elements in the equivalence class,
  34    leq classes, geq classes *)
  35 type equivalence_class =
  36  compound_operator * compound_operator list *
  37   equivalence_class list ref * equivalence_class list ref
  38
  39 let string_of_equivalence_class (repr,others,leq,_) =
  40  String.concat " = " (List.map string_of_cop (repr::others)) ^
  41   (if !leq <> [] then
  42     "\n" ^
  43      String.concat "\n"
  44       (List.map
  45         (function (repr',_,_,_) ->
  46            string_of_cop repr ^ " ⊆ " ^ string_of_cop repr') !leq)
  47    else
  48     "")
  49
  50 let dot_of_equivalence_class (repr,others,leq,_) =
  51  (if others <> [] then
  52    let eq = String.concat " = " (List.map string_of_cop (repr::others)) in
  53     dot_of_cop repr ^ "[label=\"" ^ eq ^ "\"];" ^
  54      if !leq = [] then "" else "\n"
  55   else if !leq = [] then
  56    dot_of_cop repr ^ ";"
  57   else
  58    "") ^
  59    String.concat "\n"
  60     (List.map
  61       (function (repr',_,_,_) ->
  62          dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ ";") !leq)
  63
  64 (* set of equivalence classes, infima, suprema *)
  65 type set =
  66  equivalence_class list * equivalence_class list * equivalence_class list
  67
  68 let string_of_set (s,_,_) =
  69  String.concat "\n" (List.map string_of_equivalence_class s)
  70
  71 let ps_of_set (to_be_considered,under_consideration,news) ?processing (s,inf,sup) =
  72  let ch = open_out "xxx.dot" in
  73   output_string ch "digraph G {\n";
  74   (match under_consideration with
  75       None -> ()
  76     | Some repr ->
  77        output_string ch (dot_of_cop repr ^ " [color=yellow];"));
  78   List.iter
  79    (function (repr,_,_,_) ->
  80      if List.exists (function (repr',_,_,_) -> repr=repr') sup then
  81       output_string ch (dot_of_cop repr ^ " [shape=Mdiamond];")
  82      else
  83       output_string ch (dot_of_cop repr ^ " [shape=diamond];")
  84    ) inf ;
  85   List.iter
  86    (function (repr,_,_,_) ->
  87      if not (List.exists (function (repr',_,_,_) -> repr=repr') inf) then
  88       output_string ch (dot_of_cop repr ^ " [shape=polygon];")
  89    ) sup ;
  90   List.iter
  91    (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];")
  92    ) to_be_considered ;
  93   List.iter
  94    (function repr -> output_string ch (dot_of_cop repr ^ " [color=navy];")
  95    ) news ;
  96   output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s));
  97   output_string ch "\n";
  98   (match processing with
  99       None -> ()
 100     | Some (repr,rel,repr') ->
 101        output_string ch (dot_of_cop repr ^ " [color=red];");
 102        let repr,repr' =
 103         match rel with
 104            SupersetEqual -> repr',repr
 105          | Equal
 106          | SubsetEqual -> repr,repr'
 107        in
 108         output_string ch
 109          (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^
 110           " [" ^
 111           (match rel with Equal -> "arrowhead=none " | _ -> "") ^
 112           "style=dashed];\n"));
 113   output_string ch "}\n";
 114   close_out ch;
 115   (*ignore (Unix.system "tred xxx.dot > yyy.dot && dot -Tps yyy.dot > xxx.ps")*)
 116   ignore (Unix.system "dot -Tps xxx.dot > xxx.ps");
 117   ignore (read_line ())
 118
 119 let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr =
 120  ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;
 121  print_string
 122   (string_of_cop candidate ^ " " ^ string_of_rel rel ^ " " ^ string_of_cop repr ^ "? ");
 123  flush stdout;
 124  assert (Unix.system "cp formal_topology.ma xxx.ma" = Unix.WEXITED 0);
 125  let ch = open_out_gen [Open_append] 0 "xxx.ma" in
 126  let i = ref 0 in
 127   List.iter
 128    (function (repr,others,leq,_) ->
 129      List.iter
 130       (function repr' ->
 131         incr i;
 132         output_string ch
 133          ("axiom ax" ^ string_of_int !i ^
 134           ": \\forall A." ^
 135            matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n");
 136       ) others;
 137      List.iter
 138       (function (repr',_,_,_) ->
 139         incr i;
 140         output_string ch
 141          ("axiom ax" ^ string_of_int !i ^
 142           ": \\forall A." ^
 143            matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n");
 144       ) !leq;
 145    ) s;
 146   let candidate',rel',repr' =
 147    match rel with
 148       SupersetEqual -> repr,SubsetEqual,candidate
 149     | Equal
 150     | SubsetEqual -> candidate,rel,repr
 151   in
 152   output_string ch
 153    ("theorem foo: \\forall A." ^ matita_of_cop "A" candidate' ^
 154       " " ^ string_of_rel rel' ^ " " ^
 155       matita_of_cop "A" repr' ^ ". intros; auto size=6 depth=4. qed.\n");
 156   close_out ch;
 157   let res =
 158    (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*)
 159    Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0
 160   in
 161    print_endline (if res then "y" else "n");
 162    res
 163
 164 let remove node = List.filter (fun node' -> node != node');;
 165
 166 let add_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
 167  leq := node' :: !leq;
 168  geq' := node :: !geq'
 169 ;;
 170
 171 let add_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
 172  geq := node' :: !geq;
 173  leq' := node :: !leq'
 174 ;;
 175
 176 let remove_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
 177  leq := remove node' !leq;
 178  geq' := remove node !geq'
 179 ;;
 180
 181 let remove_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
 182  geq := remove node' !geq;
 183  leq' := remove node !leq'
 184 ;;
 185
 186 let leq_transitive_closure node node' =
 187  add_leq_arc node node';
 188  let rec remove_transitive_arcs ((_,_,_,geq) as node) (_,_,leq',_) =
 189   let rec remove_arcs_to_ascendents =
 190    function
 191       [] -> ()
 192     | (_,_,leq,_) as node'::tl ->
 193        remove_leq_arc node node';
 194        remove_arcs_to_ascendents (!leq@tl)
 195   in
 196    remove_arcs_to_ascendents !leq';
 197    List.iter (function son -> remove_transitive_arcs son node) !geq
 198  in
 199   remove_transitive_arcs node node'
 200 ;;
 201
 202 let geq_transitive_closure node node' =
 203  add_geq_arc node node';
 204  let rec remove_transitive_arcs ((_,_,leq,_) as node) (_,_,_,geq') =
 205   let rec remove_arcs_to_descendents =
 206    function
 207       [] -> ()
 208     | (_,_,_,geq) as node'::tl ->
 209        remove_geq_arc node node';
 210        remove_arcs_to_descendents (!geq@tl)
 211   in
 212    remove_arcs_to_descendents !geq';
 213    List.iter (function father -> remove_transitive_arcs father node) !leq
 214  in
 215   remove_transitive_arcs node node'
 216 ;;
 217
 218 let (@@) l1 e = if List.memq e l1 then l1 else l1@[e]
 219
 220 let rec leq_reachable node =
 221  function
 222     [] -> false
 223   | node'::_ when node == node' -> true
 224   | (_,_,leq,_)::tl -> leq_reachable node (!leq@tl)
 225 ;;
 226
 227 let rec geq_reachable node =
 228  function
 229     [] -> false
 230   | node'::_ when node == node' -> true
 231   | (_,_,_,geq)::tl -> geq_reachable node (!geq@tl)
 232 ;;
 233
 234 let locate_using_leq to_be_considered_and_now ((repr,_,leq,_) as node)
 235  ((_,_,sup) as set)
 236 =
 237  let rec aux is_sup ((nodes,inf,sup) as set) =
 238   function
 239      [] ->
 240       if is_sup then
 241        nodes,inf,sup@@node
 242       else
 243        set
 244    | (repr',_,_,geq') as node' :: tl ->
 245        if repr=repr' then aux is_sup set (!geq'@tl)
 246        else if leq_reachable node' !leq then
 247         aux is_sup set tl
 248        else if test to_be_considered_and_now set SubsetEqual repr repr' then
 249         begin
 250          let inf = if !geq' = [] then (remove node' inf)@@node else inf in
 251           leq_transitive_closure node node';
 252           aux false (nodes,inf,sup) (!geq'@tl)
 253         end
 254        else
 255         aux is_sup set tl
 256  in
 257 prerr_endline ("SUP: " ^ String.concat "," (List.map (fun (x,_,_,_) -> string_of_cop x) sup));
 258   aux true set sup
 259 ;;
 260
 261 exception SameEquivalenceClass of equivalence_class * equivalence_class;;
 262
 263 let locate_using_geq to_be_considered_and_now ((repr,_,leq,geq) as node)
 264  ((_,inf,_) as set)
 265 =
 266  let rec aux is_inf ((nodes,inf,sup) as set) =
 267   function
 268      [] ->
 269       if is_inf then
 270        nodes,inf@@node,sup
 271       else
 272        set
 273    | (repr',_,leq',_) as node' :: tl ->
 274        if repr=repr' then aux is_inf set (!leq'@tl)
 275        else if geq_reachable node' !geq then
 276         aux is_inf set tl
 277        else if test to_be_considered_and_now set SupersetEqual repr repr' then
 278         begin
 279          if List.mem node' !leq then
 280           (* We have found two equal nodes! *)
 281           raise (SameEquivalenceClass (node,node'))
 282          else
 283           begin
 284            let sup = if !leq' = [] then (remove node' sup)@@node else sup in
 285             geq_transitive_closure node node';
 286             aux false (nodes,inf,sup) (!leq'@tl)
 287           end
 288         end
 289        else
 290         aux is_inf set tl
 291  in
 292 prerr_endline ("INF: " ^ String.concat "," (List.map (fun (x,_,_,_) -> string_of_cop x) inf));
 293   aux true set inf
 294 ;;
 295
 296 let analyze_one to_be_considered repr hecandidate (news,((nodes,inf,sup) as set)) =
 297  let candidate = hecandidate::repr in
 298   if List.length (List.filter ((=) M) candidate) > 1 then
 299    news,set
 300   else
 301    try
 302     let leq = ref [] in
 303     let geq = ref [] in
 304     let node = candidate,[],leq,geq in
 305     let nodes = nodes@[node] in
 306     let set = nodes,inf,sup in
 307     let set = locate_using_leq (to_be_considered,Some repr,news) node set in
 308     let set = locate_using_geq (to_be_considered,Some repr,news) node set in
 309      news@[candidate],set
 310    with
 311     SameEquivalenceClass (node_to_be_deleted,node') ->
 312      let rec clean =
 313       function
 314          [] -> []
 315        | (repr',others,leq,geq) as node::tl ->
 316           leq := List.filter (function node -> node_to_be_deleted != node) !leq;
 317           geq := List.filter (function node -> node_to_be_deleted != node) !geq;
 318           if node==node' then
 319            (repr',others@[candidate],leq,geq)::clean tl
 320           else
 321            (repr',others,leq,geq)::clean tl
 322      in
 323      let nodes = clean nodes in
 324       news,(nodes,inf,sup)
 325 ;;
 326
 327 let rec explore i (set:set) news =
 328  let rec aux news set =
 329   function
 330      [] -> news,set
 331    | repr::tl ->
 332       let news,set =
 333        List.fold_right (analyze_one tl repr) [I;C;M] (news,set)
 334       in
 335        aux news set tl
 336  in
 337   let news,set = aux [] set news in
 338    if news = [] then
 339     begin
 340      print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
 341      print_endline (string_of_set set ^ "\n----------------");
 342      ps_of_set ([],None,[]) set
 343     end
 344    else
 345     begin
 346      print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
 347      print_endline (string_of_set set ^ "\n----------------");
 348      explore (i+1) set news
 349     end
 350 in
 351  let id = [] in
 352  let id_node = id,[],ref [], ref [] in
 353  let set = [id_node],[id_node],[id_node] in
 354   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
 355   print_endline (string_of_set set ^ "\n----------------");
 356   (*ignore (Unix.system "rm -f log");*)
 357   ps_of_set ([id],None,[]) set;
 358   explore 1 set [id]
 359 ;;