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