matita/contribs/formal_topology/bin/theory_explorer_do_not_trust_auto.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 *)
  65 type set = equivalence_class list
  66
  67 let string_of_set s =
  68  String.concat "\n" (List.map string_of_equivalence_class s)
  69
  70 let ps_of_set (to_be_considered,under_consideration,news) ?processing s =
  71  let ch = open_out "xxx.dot" in
  72   output_string ch "digraph G {\n";
  73   (match under_consideration with
  74       None -> ()
  75     | Some repr ->
  76        output_string ch (dot_of_cop repr ^ " [color=yellow];"));
  77   List.iter
  78    (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];")
  79    ) to_be_considered ;
  80   List.iter
  81    (function repr -> output_string ch (dot_of_cop repr ^ " [color=navy];")
  82    ) news ;
  83   output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s));
  84   output_string ch "\n";
  85   (match processing with
  86       None -> ()
  87     | Some (repr,rel,repr') ->
  88        output_string ch (dot_of_cop repr ^ " [color=red];");
  89        let repr,repr' =
  90         match rel with
  91            SupersetEqual -> repr',repr
  92          | Equal
  93          | SubsetEqual -> repr,repr'
  94        in
  95         output_string ch
  96          (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^
  97           " [" ^
  98           (match rel with Equal -> "arrowhead=none " | _ -> "") ^
  99           "style=dashed];\n"));
 100   output_string ch "}\n";
 101   close_out ch;
 102   ignore (Unix.system "tred xxx.dot > yyy.dot && dot -Tps yyy.dot > xxx.ps")
 103
 104 let test to_be_considered_and_now set rel candidate repr =
 105  ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;
 106  print_string
 107   (string_of_cop candidate ^ " " ^ string_of_rel rel ^ " " ^ string_of_cop repr ^ "? ");
 108  flush stdout;
 109  assert (Unix.system "cp formal_topology.ma xxx.ma" = Unix.WEXITED 0);
 110  let ch = open_out_gen [Open_append] 0 "xxx.ma" in
 111  let i = ref 0 in
 112   List.iter
 113    (function (repr,others,leq,_) ->
 114      List.iter
 115       (function repr' ->
 116         incr i;
 117         output_string ch
 118          ("axiom ax" ^ string_of_int !i ^
 119           ": \\forall A." ^
 120            matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n");
 121       ) others;
 122      List.iter
 123       (function (repr',_,_,_) ->
 124         incr i;
 125         output_string ch
 126          ("axiom ax" ^ string_of_int !i ^
 127           ": \\forall A." ^
 128            matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n");
 129       ) !leq;
 130    ) set;
 131   let candidate',rel',repr' =
 132    match rel with
 133       SupersetEqual -> repr,SubsetEqual,candidate
 134     | Equal
 135     | SubsetEqual -> candidate,rel,repr
 136   in
 137   output_string ch
 138    ("theorem foo: \\forall A." ^ matita_of_cop "A" candidate' ^
 139       " " ^ string_of_rel rel' ^ " " ^
 140       matita_of_cop "A" repr' ^ ". intros; auto size=6 depth=4. qed.\n");
 141   close_out ch;
 142   let res =
 143    (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*)
 144    Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0
 145   in
 146    print_endline (if res then "y" else "n");
 147    res
 148
 149 let normalize to_be_considered_and_now candidate set =
 150  let rec aux =
 151   function
 152      [] -> raise Not_found
 153    | (repr,others,leq,geq) as eqclass :: tl ->
 154        if test to_be_considered_and_now set Equal candidate repr then
 155         (repr,others@[candidate],leq,geq)::tl
 156        else
 157         eqclass::(aux tl)
 158  in
 159   aux set
 160 ;;
 161
 162 let locate to_be_considered_and_now ((repr,_,leq,geq) as node) set =
 163  let rec aux =
 164   function
 165      [] -> ()
 166    | (repr',_,leq',geq') as node' :: tl ->
 167        if repr = repr' then ()
 168        else if test to_be_considered_and_now set SubsetEqual repr repr' then
 169         begin
 170          leq  := node' :: !leq;
 171          geq' := node  :: !geq'
 172         end
 173        else if test to_be_considered_and_now set SupersetEqual repr repr' then
 174         begin
 175          geq  := node' :: !geq;
 176          leq' := node  :: !leq'
 177         end ;
 178        aux tl
 179  in
 180   aux set
 181 ;;
 182
 183 let analyze_one to_be_considered repr hecandidate (news,set) =
 184  let candidate = hecandidate::repr in
 185   if List.length (List.filter ((=) M) candidate) > 1 then
 186    news,set
 187   else
 188    try
 189     let set = normalize (to_be_considered,Some repr,news) candidate set in
 190      news,set
 191    with
 192     Not_found ->
 193      let leq = ref [] in
 194      let geq = ref [] in
 195      let node = candidate,[],leq,geq in
 196      let set = node::set in
 197       locate (to_be_considered,Some repr,news) node set;
 198       candidate::news,set
 199 ;;
 200
 201 let rec explore i set news =
 202  let rec aux news set =
 203   function
 204      [] -> news,set
 205    | repr::tl ->
 206       let news,set =
 207        List.fold_right (analyze_one tl repr) [I;C;M] (news,set)
 208       in
 209        aux news set tl
 210  in
 211   let news,set = aux [] set news in
 212    if news = [] then
 213     begin
 214      print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
 215      print_endline (string_of_set set ^ "\n----------------");
 216      ps_of_set ([],None,[]) set
 217     end
 218    else
 219     begin
 220      print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
 221      print_endline (string_of_set set ^ "\n----------------");
 222      explore (i+1) set news
 223     end
 224 in
 225  let id = [] in
 226  let set = [id,[],ref [], ref []] in
 227   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
 228   print_endline (string_of_set set ^ "\n----------------");
 229   (*ignore (Unix.system "rm -f log");*)
 230   ps_of_set ([id],None,[]) set;
 231   explore 1 set [id]
 232 ;;