]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/formal_topology/bin/theory_explorer.ml
Still bugged.
[helm.git] / matita / contribs / formal_topology / bin / theory_explorer.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, infima, suprema *)
65 type set =
66  equivalence_class list * equivalence_class list * equivalence_class list
67
68 let string_of_set (s,_,_) =
69  String.concat "\n" (List.map string_of_equivalence_class s)
70
71 let ps_of_set (to_be_considered,under_consideration,news) ?processing (s,inf,sup) =
72  let ch = open_out "xxx.dot" in
73   output_string ch "digraph G {\n";
74   (match under_consideration with
75       None -> ()
76     | Some repr ->
77        output_string ch (dot_of_cop repr ^ " [color=yellow];"));
78   List.iter
79    (function (repr,_,_,_) ->
80      if List.exists (function (repr',_,_,_) -> repr=repr') sup then
81       output_string ch (dot_of_cop repr ^ " [shape=Mdiamond];")
82      else
83       output_string ch (dot_of_cop repr ^ " [shape=diamond];")
84    ) inf ;
85   List.iter
86    (function (repr,_,_,_) ->
87      if not (List.exists (function (repr',_,_,_) -> repr=repr') inf) then
88       output_string ch (dot_of_cop repr ^ " [shape=polygon];")
89    ) sup ;
90   List.iter
91    (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];")
92    ) to_be_considered ;
93   List.iter
94    (function repr -> output_string ch (dot_of_cop repr ^ " [color=navy];")
95    ) news ;
96   output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s));
97   output_string ch "\n";
98   (match processing with
99       None -> ()
100     | Some (repr,rel,repr') ->
101        output_string ch (dot_of_cop repr ^ " [color=red];");
102        let repr,repr' =
103         match rel with
104            SupersetEqual -> repr',repr
105          | Equal
106          | SubsetEqual -> repr,repr'
107        in
108         output_string ch
109          (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^
110           " [" ^
111           (match rel with Equal -> "arrowhead=none " | _ -> "") ^
112           "style=dashed];\n"));
113   output_string ch "}\n";
114   close_out ch;
115   (*ignore (Unix.system "tred xxx.dot > yyy.dot && dot -Tps yyy.dot > xxx.ps")*)
116   ignore (Unix.system "dot -Tps xxx.dot > xxx.ps");
117   ignore (read_line ())
118
119 let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr =
120  ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;
121  print_string
122   (string_of_cop candidate ^ " " ^ string_of_rel rel ^ " " ^ string_of_cop repr ^ "? ");
123  flush stdout;
124  assert (Unix.system "cp formal_topology.ma xxx.ma" = Unix.WEXITED 0);
125  let ch = open_out_gen [Open_append] 0 "xxx.ma" in
126  let i = ref 0 in
127   List.iter
128    (function (repr,others,leq,_) ->
129      List.iter
130       (function repr' ->
131         incr i;
132         output_string ch
133          ("axiom ax" ^ string_of_int !i ^
134           ": \\forall A." ^
135            matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n");
136       ) others;
137      List.iter
138       (function (repr',_,_,_) ->
139         incr i;
140         output_string ch
141          ("axiom ax" ^ string_of_int !i ^
142           ": \\forall A." ^
143            matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n");
144       ) !leq;
145    ) s;
146   let candidate',rel',repr' =
147    match rel with
148       SupersetEqual -> repr,SubsetEqual,candidate
149     | Equal
150     | SubsetEqual -> candidate,rel,repr
151   in
152   output_string ch
153    ("theorem foo: \\forall A." ^ matita_of_cop "A" candidate' ^
154       " " ^ string_of_rel rel' ^ " " ^
155       matita_of_cop "A" repr' ^ ". intros; auto size=6 depth=4. qed.\n");
156   close_out ch;
157   let res =
158    (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*)
159    Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0
160   in
161    print_endline (if res then "y" else "n");
162    res
163
164 let remove node = List.filter (fun node' -> node != node');;
165
166 let add_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
167  leq := node' :: !leq;
168  geq' := node :: !geq'
169 ;;
170
171 let add_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
172  geq := node' :: !geq;
173  leq' := node :: !leq'
174 ;;
175
176 let remove_leq_arc ((_,_,leq,_) as node) ((_,_,_,geq') as node') =
177  leq := remove node' !leq;
178  geq' := remove node !geq'
179 ;;
180
181 let remove_geq_arc ((_,_,_,geq) as node) ((_,_,leq',_) as node') =
182  geq := remove node' !geq;
183  leq' := remove node !leq'
184 ;;
185
186 let leq_transitive_closure node node' =
187  add_leq_arc node node';
188  let rec remove_transitive_arcs ((_,_,_,geq) as node) (_,_,leq',_) =
189   let rec remove_arcs_to_ascendents =
190    function
191       [] -> ()
192     | (_,_,leq,_) as node'::tl ->
193        remove_leq_arc node node';
194        remove_arcs_to_ascendents (!leq@tl)
195   in
196    remove_arcs_to_ascendents !leq';
197    List.iter (function son -> remove_transitive_arcs son node) !geq
198  in
199   remove_transitive_arcs node node'
200 ;;
201
202 let geq_transitive_closure node node' =
203  add_geq_arc node node';
204  let rec remove_transitive_arcs ((_,_,leq,_) as node) (_,_,_,geq') =
205   let rec remove_arcs_to_descendents =
206    function
207       [] -> ()
208     | (_,_,_,geq) as node'::tl ->
209        remove_geq_arc node node';
210        remove_arcs_to_descendents (!geq@tl)
211   in
212    remove_arcs_to_descendents !geq';
213    List.iter (function father -> remove_transitive_arcs father node) !leq
214  in
215   remove_transitive_arcs node node'
216 ;;
217
218 let (@@) l1 e = if List.memq e l1 then l1 else l1@[e]
219
220 let locate_using_leq to_be_considered_and_now ((repr,_,leq,_) as node)
221  ((_,_,sup) as set)
222 =
223  let rec aux is_sup ((nodes,inf,sup) as set) =
224   function
225      [] ->
226       if is_sup then
227        nodes,inf,sup@@node
228       else
229        set
230    | (repr',_,_,geq') as node' :: tl ->
231        if repr=repr' then aux is_sup set (!geq'@tl)
232        else if List.mem node' !leq
233             || test to_be_considered_and_now set SubsetEqual repr repr'
234        then
235         begin
236          let inf = if !geq' = [] then (remove node' inf)@@node else inf in
237           leq_transitive_closure node node';
238           aux false (nodes,inf,sup) (!geq'@tl)
239         end
240        else
241         aux is_sup set tl
242  in
243 prerr_endline ("SUP: " ^ String.concat "," (List.map (fun (x,_,_,_) -> string_of_cop x) sup));
244   aux true set sup
245 ;;
246
247 exception SameEquivalenceClass of equivalence_class * equivalence_class;;
248
249 let locate_using_geq to_be_considered_and_now ((repr,_,leq,geq) as node)
250  ((_,inf,_) as set)
251 =
252  let rec aux is_inf ((nodes,inf,sup) as set) =
253   function
254      [] ->
255       if is_inf then
256        nodes,inf@@node,sup
257       else
258        set
259    | (repr',_,leq',_) as node' :: tl ->
260        if repr=repr' then aux is_inf set (!leq'@tl)
261        else if List.mem node' !geq
262             || test to_be_considered_and_now set SupersetEqual repr repr'
263        then
264         begin
265          if List.mem node' !leq then
266           (* We have found two equal nodes! *)
267           raise (SameEquivalenceClass (node,node'))
268          else
269           begin
270            let sup = if !leq' = [] then (remove node' sup)@@node else sup in
271             geq_transitive_closure node node';
272             aux false (nodes,inf,sup) (!leq'@tl)
273           end
274         end
275        else
276         aux is_inf set tl
277  in
278 prerr_endline ("INF: " ^ String.concat "," (List.map (fun (x,_,_,_) -> string_of_cop x) inf));
279   aux true set inf
280 ;;
281
282 let analyze_one to_be_considered repr hecandidate (news,((nodes,inf,sup) as set)) =
283  let candidate = hecandidate::repr in
284   if List.length (List.filter ((=) M) candidate) > 1 then
285    news,set
286   else
287    try
288     let leq = ref [] in
289     let geq = ref [] in
290     let node = candidate,[],leq,geq in
291     let nodes = nodes@[node] in
292     let set = nodes,inf,sup in
293     let set = locate_using_leq (to_be_considered,Some repr,news) node set in
294     let set = locate_using_geq (to_be_considered,Some repr,news) node set in
295      news@[candidate],set
296    with
297     SameEquivalenceClass (node_to_be_deleted,node') ->
298      let rec clean =
299       function
300          [] -> []
301        | (repr',others,leq,geq) as node::tl ->
302           leq := List.filter (function node -> node_to_be_deleted != node) !leq;
303           geq := List.filter (function node -> node_to_be_deleted != node) !geq;
304           if node==node' then
305            (repr',others@[candidate],leq,geq)::clean tl
306           else
307            (repr',others,leq,geq)::clean tl
308      in
309      let nodes = clean nodes in
310       news,(nodes,inf,sup)
311 ;;
312
313 let rec explore i (set:set) news =
314  let rec aux news set =
315   function
316      [] -> news,set
317    | repr::tl ->
318       let news,set =
319        List.fold_right (analyze_one tl repr) [I;C;M] (news,set)
320       in
321        aux news set tl
322  in
323   let news,set = aux [] set news in
324    if news = [] then
325     begin
326      print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i);
327      print_endline (string_of_set set ^ "\n----------------");
328      ps_of_set ([],None,[]) set
329     end
330    else
331     begin
332      print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i);
333      print_endline (string_of_set set ^ "\n----------------");
334      explore (i+1) set news
335     end
336 in
337  let id = [] in
338  let id_node = id,[],ref [], ref [] in
339  let set = [id_node],[id_node],[id_node] in
340   print_endline ("PRIMA ITERAZIONE, i=0, j=0");
341   print_endline (string_of_set set ^ "\n----------------");
342   (*ignore (Unix.system "rm -f log");*)
343   ps_of_set ([id],None,[]) set;
344   explore 1 set [id]
345 ;;