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