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      output_string ch (dot_of_cop repr ^ " [shape=diamond];")
  81    ) inf ;
  82   List.iter
  83    (function (repr,_,_,_) ->
  84      output_string ch (dot_of_cop repr ^ " [shape=polygon];")
  85    ) sup ;
  86   List.iter
  87    (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];")
  88    ) to_be_considered ;
  89   List.iter
  90    (function repr -> output_string ch (dot_of_cop repr ^ " [color=navy];")
  91    ) news ;
  92   output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s));
  93   output_string ch "\n";
  94   (match processing with
  95       None -> ()
  96     | Some (repr,rel,repr') ->
  97        output_string ch (dot_of_cop repr ^ " [color=red];");
  98        let repr,repr' =
  99         match rel with
 100            SupersetEqual -> repr',repr
 101          | Equal
 102          | SubsetEqual -> repr,repr'
 103        in
 104         output_string ch
 105          (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^
 106           " [" ^
 107           (match rel with Equal -> "arrowhead=none " | _ -> "") ^
 108           "style=dashed];\n"));
 109   output_string ch "}\n";
 110   close_out ch;
 111   ignore (Unix.system "tred xxx.dot > yyy.dot && dot -Tps yyy.dot > xxx.ps")
 112
 113 let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr =
 114  ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;
 115  print_string
 116   (string_of_cop candidate ^ " " ^ string_of_rel rel ^ " " ^ string_of_cop repr ^ "? ");
 117  flush stdout;
 118  assert (Unix.system "cp formal_topology.ma xxx.ma" = Unix.WEXITED 0);
 119  let ch = open_out_gen [Open_append] 0 "xxx.ma" in
 120  let i = ref 0 in
 121   List.iter
 122    (function (repr,others,leq,_) ->
 123      List.iter
 124       (function repr' ->
 125         incr i;
 126         output_string ch
 127          ("axiom ax" ^ string_of_int !i ^
 128           ": \\forall A." ^
 129            matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n");
 130       ) others;
 131      List.iter
 132       (function (repr',_,_,_) ->
 133         incr i;
 134         output_string ch
 135          ("axiom ax" ^ string_of_int !i ^
 136           ": \\forall A." ^
 137            matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n");
 138       ) !leq;
 139    ) s;
 140   let candidate',rel',repr' =
 141    match rel with
 142       SupersetEqual -> repr,SubsetEqual,candidate
 143     | Equal
 144     | SubsetEqual -> candidate,rel,repr
 145   in
 146   output_string ch
 147    ("theorem foo: \\forall A." ^ matita_of_cop "A" candidate' ^
 148       " " ^ string_of_rel rel' ^ " " ^
 149       matita_of_cop "A" repr' ^ ". intros; auto size=6 depth=4. qed.\n");
 150   close_out ch;
 151   let res =
 152    (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*)
 153    Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0
 154   in
 155    print_endline (if res then "y" else "n");
 156    res
 157
 158 let rec leq_transitive_closure leq node ((repr,_,leq',geq') as node') =
 159  if not (List.mem node' !leq) then leq := node' :: !leq;
 160  if not (List.mem node !geq') then geq' := node :: !geq';
 161  List.iter (leq_transitive_closure leq node) !leq'
 162 ;;
 163
 164 let rec geq_transitive_closure geq node ((_,_,leq',geq') as node') =
 165  if not (List.mem node' !geq) then geq  := node' :: !geq;
 166  if not (List.mem node !leq') then leq' := node  :: !leq';
 167  List.iter (geq_transitive_closure geq node) !geq'
 168 ;;
 169
 170 let remove node l =
 171  let l' = List.filter (fun node' -> node != node') l in
 172  if List.length l = List.length l' then
 173   assert false
 174  else
 175   l'
 176 ;;
 177
 178 let locate_using_leq to_be_considered_and_now ((repr,_,leq,_) as node)
 179  ((nodes,inf,sup) as set)
 180 =
 181  let rec aux is_sup inf =
 182   function
 183      [] -> is_sup,inf
 184    | (repr',_,_,geq') as node' :: sup ->
 185        if repr=repr' then aux is_sup inf (!geq'@sup)
 186        else if List.mem node' !leq
 187             || test to_be_considered_and_now set SubsetEqual repr repr'
 188        then
 189         begin
 190          let inf = if !geq' = [] then remove node' inf else inf in
 191           leq_transitive_closure leq node node';
 192           aux false inf (!geq'@sup)
 193         end
 194        else
 195         aux is_sup inf sup
 196  in
 197   let is_sup,inf = aux true inf sup in
 198    if is_sup then
 199     nodes,inf,sup@[node]
 200    else
 201     nodes,inf,sup
 202 ;;
 203
 204 exception SameEquivalenceClass of equivalence_class * equivalence_class;;
 205
 206 let locate_using_geq to_be_considered_and_now ((repr,_,leq,geq) as node)
 207  ((nodes,inf,sup) as set)
 208 =
 209  let rec aux is_inf sup =
 210   function
 211      [] -> sup,is_inf
 212    | (repr',_,leq',_) as node' :: inf ->
 213        if repr=repr' then aux is_inf sup (!leq'@inf)
 214        else if List.mem node' !geq
 215             || test to_be_considered_and_now set SupersetEqual repr repr'
 216        then
 217         begin
 218          if List.mem node' !leq then
 219           (* We have found two equal nodes! *)
 220           raise (SameEquivalenceClass (node,node'))
 221          else
 222           begin
 223            let sup = if !leq' = [] then remove node' sup else sup in
 224             geq_transitive_closure geq node node';
 225             aux false sup (!leq'@inf)
 226           end
 227         end
 228        else
 229         aux is_inf sup inf
 230  in
 231   let sup,is_inf = aux true sup inf in
 232    if is_inf then
 233     nodes,inf@[node],sup
 234    else
 235     nodes,inf,sup
 236 ;;
 237
 238 let analyze_one to_be_considered repr hecandidate (news,((nodes,inf,sup) as set)) =
 239  let candidate = hecandidate::repr in
 240   if List.length (List.filter ((=) M) candidate) > 1 then
 241    news,set
 242   else
 243    try
 244     let leq = ref [] in
 245     let geq = ref [] in
 246     let node = candidate,[],leq,geq in
 247     let nodes = nodes@[node] in
 248     let set = nodes,inf,sup in
 249     let set = locate_using_leq (to_be_considered,Some repr,news) node set in
 250     let set = locate_using_geq (to_be_considered,Some repr,news) node set in
 251      news@[candidate],set
 252    with
 253     SameEquivalenceClass (node_to_be_deleted,node') ->
 254      let rec clean =
 255       function
 256          [] -> []
 257        | (repr',others,leq,geq) as node::tl ->
 258           leq := List.filter (function node -> node_to_be_deleted != node) !leq;
 259           geq := List.filter (function node -> node_to_be_deleted != node) !geq;
 260           if node==node' then
 261            (repr',others@[candidate],leq,geq)::clean tl
 262           else
 263            (repr',others,leq,geq)::clean tl
 264      in
 265      let nodes = clean nodes in
 266       news,(nodes,inf,sup)
 267 ;;
 268
 269 let rec explore i (set:set) news =
 270  let rec aux news set =
 271   function
 272      [] -> news,set
 273    | repr::tl ->
 274       let news,set =
 275        List.fold_right (analyze_one tl repr) [I;C;M] (news,set)
 276       in
 277        aux news set tl
 278  in
 279   let news,set = aux [] set news in
 280    if news = [] then
 281     begin
 282      print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
 283      print_endline (string_of_set set ^ "\n----------------");
 284      ps_of_set ([],None,[]) set
 285     end
 286    else
 287     begin
 288      print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
 289      print_endline (string_of_set set ^ "\n----------------");
 290      explore (i+1) set news
 291     end
 292 in
 293  let id = [] in
 294  let id_node = id,[],ref [], ref [] in
 295  let set = [id_node],[id_node],[id_node] in
 296   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
 297   print_endline (string_of_set set ^ "\n----------------");
 298   (*ignore (Unix.system "rm -f log");*)
 299   ps_of_set ([id],None,[]) set;
 300   explore 1 set [id]
 301 ;;