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

   1 (* operator *)
   2 type op = I | C | M
   3
   4 let string_of_op =
   5  function
   6     I -> "i"
   7   | C -> "c"
   8   | M -> "-"
   9
  10 (* compound operator *)
  11 type compound_operator = op list
  12
  13 let string_of_cop op =
  14  if op = [] then "id" else String.concat "" (List.map string_of_op op)
  15
  16 let dot_of_cop op = "\"" ^ string_of_cop op ^ "\""
  17
  18 let rec matita_of_cop v =
  19  function
  20   | [] -> v
  21   | I::tl -> "i (" ^ matita_of_cop v tl ^ ")"
  22   | C::tl -> "c (" ^ matita_of_cop v tl ^ ")"
  23   | M::tl -> "m (" ^ matita_of_cop v tl ^ ")"
  24
  25 (* representative, other elements in the equivalence class,
  26    leq classes, geq classes *)
  27 type equivalence_class =
  28  compound_operator * compound_operator list *
  29   equivalence_class list ref * equivalence_class list ref
  30
  31 let string_of_equivalence_class (repr,others,leq,_) =
  32  String.concat " = " (List.map string_of_cop (repr::others)) ^
  33   (if !leq <> [] then
  34     "\n" ^
  35      String.concat "\n"
  36       (List.map
  37         (function (repr',_,_,_) ->
  38            string_of_cop repr ^ " <= " ^ string_of_cop repr') !leq)
  39    else
  40     "")
  41
  42 let dot_of_equivalence_class (repr,others,leq,_) =
  43  (if others <> [] then
  44    let eq = String.concat " = " (List.map string_of_cop (repr::others)) in
  45     dot_of_cop repr ^ "[label=\"" ^ eq ^ "\"];" ^
  46      if !leq = [] then "" else "\n"
  47   else if !leq = [] then
  48    dot_of_cop repr ^ ";"
  49   else
  50    "") ^
  51    String.concat "\n"
  52     (List.map
  53       (function (repr',_,_,_) ->
  54          dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ ";") !leq)
  55
  56 (* set of equivalence classes *)
  57 type set = equivalence_class list
  58
  59 let string_of_set s =
  60  String.concat "\n" (List.map string_of_equivalence_class s)
  61
  62 let ps_of_set (to_be_considered,under_consideration,news) ?processing s =
  63  let ch = open_out "xxx.dot" in
  64   output_string ch "digraph G {\n";
  65   (match under_consideration with
  66       None -> ()
  67     | Some repr ->
  68        output_string ch (dot_of_cop repr ^ " [color=yellow];"));
  69   List.iter
  70    (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];")
  71    ) to_be_considered ;
  72   List.iter
  73    (function repr -> output_string ch (dot_of_cop repr ^ " [color=navy];")
  74    ) news ;
  75   output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s));
  76   output_string ch "\n";
  77   (match processing with
  78       None -> ()
  79     | Some (repr,rel,repr') ->
  80        output_string ch (dot_of_cop repr ^ " [color=red];");
  81        output_string ch
  82         (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^
  83          " [" ^
  84          (if rel="=" then "arrowhead=none " else "") ^
  85          "style=dashed];\n"));
  86   output_string ch "}\n";
  87   close_out ch;
  88   ignore (Unix.system "dot -Tps xxx.dot > xxx.ps")
  89
  90 let test to_be_considered_and_now set rel candidate repr =
  91  ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;
  92  print_string
  93   (string_of_cop candidate ^ " " ^ rel ^ " " ^ string_of_cop repr ^ "? ");
  94  flush stdout;
  95  assert (Unix.system "cp formal_topology.ma xxx.ma" = Unix.WEXITED 0);
  96  let ch = open_out_gen [Open_append] 0 "xxx.ma" in
  97  let i = ref 0 in
  98   List.iter
  99    (function (repr,others,leq,_) ->
 100      List.iter
 101       (function repr' ->
 102         incr i;
 103         output_string ch
 104          ("axiom ax" ^ string_of_int !i ^
 105           ": \\forall A." ^
 106            matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n");
 107       ) others;
 108      List.iter
 109       (function (repr',_,_,_) ->
 110         incr i;
 111         output_string ch
 112          ("axiom ax" ^ string_of_int !i ^
 113           ": \\forall A." ^
 114            matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n");
 115       ) !leq;
 116    ) set;
 117   output_string ch
 118    ("theorem foo: \\forall A." ^ matita_of_cop "A" candidate ^ " " ^ rel ^ " " ^
 119      matita_of_cop "A" repr ^ ". intros; auto size=6 depth=4. qed.\n");
 120   close_out ch;
 121   let res =
 122    Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0
 123   in
 124    print_endline (if res then "y" else "n");
 125    res
 126
 127 let normalize to_be_considered_and_now candidate set =
 128  let rec aux =
 129   function
 130      [] -> raise Not_found
 131    | (repr,others,leq,geq) as eqclass :: tl ->
 132        if test to_be_considered_and_now set "=" candidate repr then
 133         (repr,others@[candidate],leq,geq)::tl
 134        else
 135         eqclass::(aux tl)
 136  in
 137   aux set
 138 ;;
 139
 140 let locate to_be_considered_and_now ((repr,_,leq,geq) as node) set =
 141  let rec aux =
 142   function
 143      [] -> ()
 144    | (repr',_,leq',geq') as node' :: tl ->
 145        if repr = repr' then ()
 146        else if test to_be_considered_and_now set "⊆" repr repr' then
 147         begin
 148          leq  := node' :: !leq;
 149          geq' := node  :: !geq'
 150         end
 151        else if test to_be_considered_and_now set "⊆" repr' repr then
 152         begin
 153          geq  := node' :: !geq;
 154          leq' := node  :: !leq'
 155         end ;
 156        aux tl
 157  in
 158   aux set
 159 ;;
 160
 161 let analyze_one to_be_considered repr hecandidate (news,set) =
 162  let candidate = hecandidate::repr in
 163   if List.length (List.filter ((=) M) candidate) > 1 then
 164    news,set
 165   else
 166    try
 167     let set = normalize (to_be_considered,Some repr,news) candidate set in
 168      news,set
 169    with
 170     Not_found ->
 171      let leq = ref [] in
 172      let geq = ref [] in
 173      let node = candidate,[],leq,geq in
 174      let set = node::set in
 175       locate (to_be_considered,Some repr,news) node set;
 176       candidate::news,set
 177 ;;
 178
 179 let rec explore i set news =
 180  let rec aux news set =
 181   function
 182      [] -> news,set
 183    | repr::tl ->
 184       let news,set =
 185        List.fold_right (analyze_one tl repr) [I;C;M] (news,set)
 186       in
 187        aux news set tl
 188  in
 189   let news,set = aux [] set news in
 190    if news = [] then
 191     begin
 192      print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
 193      print_endline (string_of_set set ^ "\n----------------");
 194      ps_of_set ([],None,[]) set
 195     end
 196    else
 197     begin
 198      print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
 199      print_endline (string_of_set set ^ "\n----------------");
 200      explore (i+1) set news
 201     end
 202 in
 203  let id = [] in
 204  let set = [id,[],ref [], ref []] in
 205   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
 206   print_endline (string_of_set set ^ "\n----------------");
 207   ignore (Unix.system "rm -f log");
 208   ps_of_set ([id],None,[]) set;
 209   explore 1 set [id]
 210 ;;