]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/formal_topology/bin/theory_explorer.ml
69911cfb356b4bae102ac55c66a7f46dac744b24
[helm.git] / matita / contribs / formal_topology / bin / theory_explorer.ml
1 (**** PROFILING ****)
2 let ok_time = ref 0.0;;
3 let ko_time = ref 0.0;;
4
5 let profile f x =
6  let before = Unix.gettimeofday () in
7  let res = f x in
8  let after = Unix.gettimeofday () in
9  let delta = after -. before in
10   if res = Unix.WEXITED 0 then
11    ok_time := !ok_time +. delta
12   else
13    ko_time := !ko_time +. delta;
14   res
15 ;;
16
17 let _ =
18  Sys.catch_break true;
19  at_exit
20   (function () ->
21     prerr_endline
22      ("\nTIME SPENT IN CHECKING GOOD CONJECTURES: " ^ string_of_float !ok_time);
23     prerr_endline
24      ("TIME SPENT IN CHECKING BAD CONJECTURES: " ^ string_of_float !ko_time);)
25 ;;
26
27 (**** END PROFILING ****)
28
29 type rel = Equal | SubsetEqual | SupersetEqual
30
31 let string_of_rel =
32  function
33     Equal -> "="
34   | SubsetEqual -> "⊆"
35   | SupersetEqual -> "⊇"
36
37 (* operator *)
38 type op = I | C | M
39
40 let string_of_op = function I -> "i" | C -> "c" | M -> "-"
41 let matita_of_op = function I -> "i" | C -> "c" | M -> "m"
42
43 (* compound operator *)
44 type compound_operator = op list
45
46 let string_of_cop op =
47  if op = [] then "id" else String.concat "" (List.map string_of_op op)
48
49 let dot_of_cop op = "\"" ^ string_of_cop op ^ "\""
50
51 let matita_of_cop v =
52  let rec aux =
53   function
54    | [] -> v
55    | [op] -> matita_of_op op ^ " " ^ v
56    | op::tl -> matita_of_op op ^ " (" ^ aux tl ^ ")"
57  in
58   aux
59
60 let name_of_theorem cop rel cop' =
61  let cop,rel,cop' =
62   match rel with
63      Equal -> cop,"eq",cop'
64    | SubsetEqual -> cop,"leq",cop'
65    | SupersetEqual -> cop',"leq",cop
66  in
67   rel ^ "_" ^
68    String.concat "" (List.map matita_of_op cop) ^ "_" ^
69    String.concat "" (List.map matita_of_op cop')
70 ;;
71
72 (* representative, other elements in the equivalence class,
73    leq classes, geq classes *)
74 type equivalence_class =
75  compound_operator * compound_operator list *
76   equivalence_class list ref * equivalence_class list ref
77
78 let (===) (repr,_,_,_) (repr',_,_,_) = repr = repr';;
79 let (<=>) (repr,_,_,_) (repr',_,_,_) = repr <> repr';;
80
81 let string_of_equivalence_class (repr,others,leq,_) =
82  String.concat " = " (List.map string_of_cop (repr::others)) ^
83   (if !leq <> [] then
84     "\n" ^
85      String.concat "\n" 
86       (List.map
87         (function (repr',_,_,_) ->
88            string_of_cop repr ^ " ⊆ " ^ string_of_cop repr') !leq)
89    else
90     "")
91
92 let dot_of_equivalence_class (repr,others,leq,_) =
93  (if others <> [] then
94    let eq = String.concat " = " (List.map string_of_cop (repr::others)) in
95     dot_of_cop repr ^ "[label=\"" ^ eq ^ "\"];" ^
96      if !leq = [] then "" else "\n"
97   else if !leq = [] then
98    dot_of_cop repr ^ ";"
99   else
100    "") ^
101    String.concat "\n" 
102     (List.map
103       (function (repr',_,_,_) ->
104          dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ ";") !leq)
105
106 (* set of equivalence classes, infima, suprema *)
107 type set =
108  equivalence_class list * equivalence_class list * equivalence_class list
109
110 let string_of_set (s,_,_) =
111  String.concat "\n" (List.map string_of_equivalence_class s)
112
113 let ps_of_set (to_be_considered,under_consideration,news) ?processing (s,inf,sup) =
114  let ch = open_out "xxx.dot" in
115   output_string ch "digraph G {\n";
116   (match under_consideration with
117       None -> ()
118     | Some repr ->
119        output_string ch (dot_of_cop repr ^ " [color=yellow];"));
120   List.iter
121    (function (repr,_,_,_) ->
122      if List.exists (function (repr',_,_,_) -> repr=repr') sup then
123       output_string ch (dot_of_cop repr ^ " [shape=Mdiamond];")
124      else
125       output_string ch (dot_of_cop repr ^ " [shape=diamond];")
126    ) inf ;
127   List.iter
128    (function (repr,_,_,_) ->
129      if not (List.exists (function (repr',_,_,_) -> repr=repr') inf) then
130       output_string ch (dot_of_cop repr ^ " [shape=polygon];")
131    ) sup ;
132   List.iter
133    (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];")
134    ) to_be_considered ;
135   List.iter
136    (function repr -> output_string ch (dot_of_cop repr ^ " [color=navy];")
137    ) news ;
138   output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s));
139   output_string ch "\n";
140   (match processing with
141       None -> ()
142     | Some (repr,rel,repr') ->
143        output_string ch (dot_of_cop repr ^ " [color=red];");
144        let repr,repr' =
145         match rel with
146            SupersetEqual -> repr',repr
147          | Equal
148          | SubsetEqual -> repr,repr'
149        in
150         output_string ch
151          (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^
152           " [" ^
153           (match rel with Equal -> "arrowhead=none " | _ -> "") ^
154           "style=dashed];\n"));
155   output_string ch "}\n";
156   close_out ch;
157   (*ignore (Unix.system "tred xxx.dot > yyy.dot && dot -Tps yyy.dot > xxx.ps")*)
158   ignore (Unix.system "cp xxx.ps xxx_old.ps && dot -Tps xxx.dot > xxx.ps");
159   (*ignore (read_line ())*)
160 ;;
161
162 (******** communication with matitawiki ************)
163 let min_ch,mout_ch = Unix.open_process "../../../matitawiki.opt 2> /dev/null";;
164
165 let exec_cmd ?(undo=false) s =
166  let un = if undo then "un" else "" in
167 (*prerr_endline ("<pgip><" ^ un ^ "doitem>" ^ s ^ "</" ^ un ^ "doitem></pgip>\n");*)
168  output_string mout_ch ("<pgip><" ^ un ^ "doitem>" ^ s ^ "</" ^ un ^ "doitem></pgip>\n");
169  flush mout_ch;
170  let rec aux v =
171   let l = input_line min_ch in
172   let last = String.length l - 1 in
173    assert (last > 0);
174    if l.[last] = Char.chr 249 then
175     int_of_string (String.sub l 0 last)
176    else
177     aux l
178  in
179   aux "x"
180 ;;
181
182 let exec_cmds =
183  let rec aux undopos =
184   function
185      [] -> true
186    | he::tl ->
187       let pos = exec_cmd he in
188        if pos = -1 then
189         begin
190          match undopos with
191             None -> assert false
192           | Some undopos ->
193              assert (exec_cmd ~undo:true (string_of_int (undopos - 1)) <> -1);
194              false
195         end
196        else
197         match undopos with
198            None -> aux (Some pos) tl
199          | _ -> aux undopos tl
200  in
201   aux None
202
203 let _ =
204  assert (exec_cmd "set \"baseuri\" \"cic:/matita/theory_former\"." <> -1);
205  assert (exec_cmd "include \"formal_topology.ma\"." <> -1);
206 ;;
207
208 (********* testing a conjecture *******************)
209
210 let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr =
211  ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;
212  print_string
213   (string_of_cop candidate ^ " " ^ string_of_rel rel ^ " " ^ string_of_cop repr ^ "? ");
214  flush stdout;
215 (*
216  assert (Unix.system "cat log.ma | sed s/^theorem/axiom/g | sed 's/\\. intros.*qed\\././g' > xxx.ma" = Unix.WEXITED 0);
217  let ch = open_out_gen [Open_append] 0 "xxx.ma" in
218 *)
219 (*
220  let i = ref 0 in
221   List.iter
222    (function (repr,others,leq,_) ->
223      List.iter
224       (function repr' ->
225         incr i;
226         output_string ch
227          ("axiom ax" ^ string_of_int !i ^
228           ": \\forall A." ^
229            matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n");
230       ) others;
231      List.iter
232       (function (repr',_,_,_) ->
233         incr i;
234         output_string ch
235          ("axiom ax" ^ string_of_int !i ^
236           ": \\forall A." ^
237            matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n");
238       ) !leq;
239    ) s;
240 *)
241   let candidate',rel',repr' =
242    match rel with
243       SupersetEqual -> repr,SubsetEqual,candidate
244     | Equal
245     | SubsetEqual -> candidate,rel,repr in
246   let query1 =
247    let name = name_of_theorem candidate' rel' repr' in
248    ("theorem " ^ name ^ ": \\forall A." ^ matita_of_cop "A" candidate' ^
249       " " ^ string_of_rel rel' ^ " " ^
250       matita_of_cop "A" repr' ^ ".") in
251   let query2 = "intros;" in
252   let query3 = "autobatch size=8 depth=3 width=2." in
253   let query4 = "qed." in
254   let query = query1 ^ query2 ^ query3 ^ query4 in
255 (*
256   output_string ch (query ^ "\n");
257   close_out ch;
258 *)
259   let res = exec_cmds [query1; query2; query3; query4] in
260 (*
261   let res =
262    (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*)
263    profile Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0
264   in
265 *)
266    ignore (Unix.system "echo '(*' >> log.ma && cat xxx.dot >> log.ma && echo '*)' >> log.ma");
267    let ch = open_out_gen [Open_append] 0o0600 "log.ma" in
268    if res then
269     output_string ch (query ^ "\n")
270    else
271     output_string ch ("(* " ^ query ^ "*)\n");
272    close_out ch;
273    print_endline (if res then "y" else "n");
274    res
275
276 let remove node = List.filter (fun node' -> node <=> node');;
277
278 let add_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
279  leq := node' :: !leq;
280  geq' := node :: !geq'
281 ;;
282
283 let add_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
284  geq := node' :: !geq;
285  leq' := node :: !leq'
286 ;;
287
288 let remove_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
289  leq := remove node' !leq;
290  geq' := remove node !geq'
291 ;;
292
293 let remove_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
294  geq := remove node' !geq;
295  leq' := remove node !leq'
296 ;;
297
298 let leq_transitive_closure node node' =
299  add_leq_arc node node';
300  let rec remove_transitive_arcs ((_,_,_,geq) as node) (_,_,leq',_) =
301   let rec remove_arcs_to_ascendents =
302    function
303       [] -> ()
304     | (_,_,leq,_) as node'::tl ->
305        remove_leq_arc node node';
306        remove_arcs_to_ascendents (!leq@tl)
307   in
308    remove_arcs_to_ascendents !leq';
309    List.iter (function son -> remove_transitive_arcs son node) !geq
310  in
311   remove_transitive_arcs node node'
312 ;;
313
314 let geq_transitive_closure node node' =
315  add_geq_arc node node';
316  let rec remove_transitive_arcs ((_,_,leq,_) as node) (_,_,_,geq') =
317   let rec remove_arcs_to_descendents =
318    function
319       [] -> ()
320     | (_,_,_,geq) as node'::tl ->
321        remove_geq_arc node node';
322        remove_arcs_to_descendents (!geq@tl)
323   in
324    remove_arcs_to_descendents !geq';
325    List.iter (function father -> remove_transitive_arcs father node) !leq
326  in
327   remove_transitive_arcs node node'
328 ;;
329
330 let (@@) l1 n = if List.exists (function n' -> n===n') l1 then l1 else l1@[n]
331
332 let rec leq_reachable node =
333  function
334     [] -> false
335   | node'::_ when node === node' -> true
336   | (_,_,leq,_)::tl -> leq_reachable node (!leq@tl)
337 ;;
338
339 let rec geq_reachable node =
340  function
341     [] -> false
342   | node'::_ when node === node' -> true
343   | (_,_,_,geq)::tl -> geq_reachable node (!geq@tl)
344 ;;
345
346 let locate_using_leq to_be_considered_and_now ((repr,_,leq,geq) as node)
347  set start
348 =
349  let rec aux ((nodes,inf,sup) as set) already_visited =
350   function
351      [] -> set
352    | (repr',_,_,geq') as node' :: tl ->
353        if List.exists (function n -> n===node') already_visited then
354         aux set already_visited tl
355        else if repr=repr' then aux set (node'::already_visited) (!geq'@tl)
356        else if leq_reachable node' !leq then
357         aux set (node'::already_visited) (!geq'@tl)
358        else if test to_be_considered_and_now set SubsetEqual repr repr' then
359         begin
360          let sup = remove node sup in
361          let inf =
362           if !geq' = [] then
363            let inf = remove node' inf in
364             if !geq = [] then
365              inf@@node
366             else
367              inf
368           else
369            inf
370           in
371            leq_transitive_closure node node';
372            aux (nodes,inf,sup) (node'::already_visited) (!geq'@tl)
373         end
374        else
375         aux set (node'::already_visited) tl
376  in
377   aux set [] start
378 ;;
379
380 exception SameEquivalenceClass of set * equivalence_class * equivalence_class;;
381
382 let locate_using_geq to_be_considered_and_now ((repr,_,leq,geq) as node)
383  set start
384 =
385  let rec aux ((nodes,inf,sup) as set) already_visited =
386   function
387      [] -> set
388    | (repr',_,leq',_) as node' :: tl ->
389        if List.exists (function n -> n===node') already_visited then
390         aux set already_visited tl
391        else if repr=repr' then aux set (node'::already_visited) (!leq'@tl)
392        else if geq_reachable node' !geq then
393         aux set (node'::already_visited) (!leq'@tl)
394        else if test to_be_considered_and_now set SupersetEqual repr repr' then
395         begin
396          if List.exists (function n -> n===node') !leq then
397           (* We have found two equal nodes! *)
398           raise (SameEquivalenceClass (set,node,node'))
399          else
400           begin
401            let inf = remove node inf in
402            let sup =
403             if !leq' = [] then
404              let sup = remove node' sup in
405              if !leq = [] then
406               sup@@node
407              else
408               sup
409             else
410              sup
411            in
412             geq_transitive_closure node node';
413             aux (nodes,inf,sup) (node'::already_visited) (!leq'@tl)
414           end
415         end
416        else
417         aux set (node'::already_visited) tl
418  in
419   aux set [] start
420 ;;
421
422 let analyze_one to_be_considered repr hecandidate (news,((nodes,inf,sup) as set)) =
423 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then ((*ps_of_set ([],None,[]) set;*) assert false);
424 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then (ps_of_set ([],None,[]) set; assert false);
425  let candidate = hecandidate::repr in
426   if List.length (List.filter ((=) M) candidate) > 1 then
427    news,set
428   else
429    try
430     let leq = ref [] in
431     let geq = ref [] in
432     let node = candidate,[],leq,geq in
433     let nodes = nodes@[node] in
434     let set = nodes,inf@[node],sup@[node] in
435     let start_inf,start_sup =
436      let repr_node =
437       match List.filter (fun (repr',_,_,_) -> repr=repr') nodes with
438          [node] -> node
439        | _ -> assert false
440      in
441 inf,sup(*
442      match hecandidate with
443         I -> inf,[repr_node]
444       | C -> [repr_node],sup
445       | M -> inf,sup
446 *)
447     in
448     let set =
449      locate_using_leq (to_be_considered,Some repr,news) node set start_sup in
450 (
451 let _,inf,sup = set in
452 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
453 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then (ps_of_set ([],None,[]) set; assert false);
454 );
455     let set =
456      locate_using_geq (to_be_considered,Some repr,news) node set start_inf
457     in
458 (
459 let _,inf,sup = set in
460 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
461 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then ((*ps_of_set ([],None,[]) set;*) assert false);
462 );
463      news@[candidate],set
464    with
465     SameEquivalenceClass ((nodes,inf,sup) as set,((r,_,leq_d,geq_d) as node_to_be_deleted),node')->
466 (
467 let _,inf,sup = set in
468 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
469 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then ((*ps_of_set ([],None,[]) set;*) assert false);
470 );
471      let rec clean inf sup res =
472       function
473          [] -> inf,sup,res
474        | node::tl when node===node_to_be_deleted ->
475           clean inf sup res tl
476        | (repr',others,leq,geq) as node::tl ->
477           leq :=
478            (let rec aux res =
479              function
480                 [] -> res
481               | (_,_,leq,_) as node::tl ->
482                  if node_to_be_deleted <=> node then
483                   aux (res@[node]) tl
484                  else
485                   (List.filter (fun n ->not (leq_reachable n (res@tl))) !leq)@tl
486             in
487              aux [] !leq);
488           let sup = if !leq = [] then sup@@node else sup in
489           geq :=
490            (let rec aux res =
491              function
492                 [] -> res
493               | (_,_,_,geq) as node::tl ->
494                  if node_to_be_deleted <=> node then
495                   aux (res@[node]) tl
496                  else
497                   (List.filter (fun n ->not (geq_reachable n (res@tl))) !geq)@tl
498             in
499              aux [] !geq);
500           let inf = if !geq = [] then inf@@node else inf in
501           if node===node' then
502            clean inf sup ((repr',others@[candidate],leq,geq)::res) tl
503           else
504            clean inf sup (node::res) tl
505      in
506      let inf,sup,nodes = clean inf sup [] nodes in
507      let inf = remove node_to_be_deleted inf in
508      let sup = remove node_to_be_deleted sup in
509 let set = nodes,inf,sup in
510 (
511 let _,inf,sup = set in
512 if not (List.for_all (fun ((_,_,_,geq) as node) -> !geq = [] && let rec check_sups = function [] -> true | (_,_,leq,_) as node::tl -> if !leq = [] then List.exists (fun n -> n===node) sup && check_sups tl else check_sups (!leq@tl) in check_sups [node]) inf) then (ps_of_set ([],None,[]) set; assert false);
513 if not (List.for_all (fun ((_,_,leq,_) as node) -> !leq = [] && let rec check_infs = function [] -> true | (_,_,_,geq) as node::tl -> if !geq = [] then List.exists (fun n -> n===node) inf && check_infs tl else check_infs (!geq@tl) in check_infs [node]) sup) then (ps_of_set ([],None,[]) set; assert false);
514 );
515       news,(nodes,inf,sup)
516 ;;
517
518 let rec explore i (set:set) news =
519  let rec aux news set =
520   function
521      [] -> news,set
522    | repr::tl ->
523       let news,set =
524        List.fold_right (analyze_one tl repr) [I;C;M] (news,set)
525       in
526        aux news set tl
527  in
528   let news,set = aux [] set news in
529    if news = [] then
530     begin
531      print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
532      print_endline (string_of_set set ^ "\n----------------");
533      ps_of_set ([],None,[]) set
534     end
535    else
536     begin
537      print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
538      print_endline (string_of_set set ^ "\n----------------");
539      explore (i+1) set news
540     end
541 in
542  let id = [] in
543  let id_node = id,[],ref [], ref [] in
544  let set = [id_node],[id_node],[id_node] in
545   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
546   print_endline (string_of_set set ^ "\n----------------");
547   (*ignore (Unix.system "rm -f log");*)
548   assert (Unix.system "cp formal_topology.ma log.ma" = Unix.WEXITED 0);
549   ps_of_set ([id],None,[]) set;
550   explore 1 set [id]
551 ;;