]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/formal_topology/bin/comb.ml
mod change (-x)
[helm.git] / matitaB / matita / contribs / formal_topology / bin / comb.ml
1 (* 0: 7       4    0.312    3 5 7
2    1: 29      6    0.549    3 8 16 24 29
3    2: 120    10   25.525    3 8 19 39 66  95 113 119 120
4    3: > 327  >9             3 8 19 39 75 134 208 274
5    4: > 657  >9             3 8 19 39 75 139 245
6    5: > 526  >8             3 8 19 39 75 139 245
7    6: > 529  >8
8    7: > 529  >8
9    8: > 529  >8
10
11 (CMM?)+ | (MM?C)+
12
13 cCw = Cw
14 -Cw = MCw
15 cMw = CMw
16 -MMw = -w
17 -MCw = MMCw
18 iw = w
19
20
21   s <= s'            s <= s'         s <= s'           s <= s'
22 ===========        ===========     ============      ==========
23  ws <= Cws'         Cs <= Cs'       CMs' <= Ms       Ms' <= MCs
24
25   s <= s'          s <= s'
26 ===========     ============
27  s <= MMs'        Ms' <= Ms
28
29 *)
30
31 type t = M | I | C
32 type w = t list
33 type eqclass = w list
34
35 type dir = Le | Ge
36
37 let rules =
38  [ [I],     Le, [];
39    [C],     Ge, [];
40    [I;I],   Ge, [I];
41    [C;C],   Le, [C];
42    [I],     Le, [I];
43    [I],     Ge, [I];
44    [C],     Le, [C];
45    [C],     Ge, [C];
46    [C;M],   Le, [M;I];
47    [C;M;I], Le, [M;I];  (* ??? *)
48    [I;M],   Le, [M;C];
49    [I;M;C], Ge, [I;M];  (* ??? *)
50    [M;M;M], Ge, [M];
51    [M;M],   Ge, [];
52    [M],     Le, [M];
53    [M],     Ge, [M];
54    (* classical
55    [M;M],   Le, [];
56    [C;M],   Ge, [M;I];
57    *)
58  ]
59 ;;
60
61 let inject =
62  let cache = Hashtbl.create 5393 in
63  function w ->
64   try
65    Hashtbl.find cache w
66   with
67    Not_found ->
68     let rec aux acc =
69      function
70         [] -> acc
71       | he::tl -> aux (4 * acc + (match he with I -> 1 | C -> 2 | M -> 3)) tl
72     in
73      let res = 0, aux 0 w, w in
74       Hashtbl.add cache w res;
75       res
76 ;;
77
78 module VL =
79  struct
80   type t = eqclass
81   let compare = compare
82   let hash = Hashtbl.hash
83   let equal = (=)
84  end
85
86 module GL = Graph.Imperative.Digraph.Concrete(VL);;
87
88 let swap = function Le -> Ge | Ge -> Le;;
89
90 let rec new_dir dir =
91  function
92     [] -> dir
93   | M::tl -> new_dir (swap dir) tl
94   | (C|I)::tl -> new_dir dir tl
95 ;;
96
97 let string_of_w w =
98  let s =
99   String.concat ""
100    (List.map (function I -> "i" | C -> "c" | M -> "-") w)
101  in
102   if s = "" then "." else s
103 ;;
104
105 let string_of_w' w =
106  let s =
107   String.concat ""
108    (List.map (function I -> "i" | C -> "c" | M -> "m") w)
109  in
110   if s = "" then "E" else s
111 ;;
112
113 let string_of_eqclass l = String.concat "=" (List.map string_of_w l);;
114
115 let name_of_eqclass l = String.concat "_" (List.map string_of_w' l);;
116
117 exception NoMatch;;
118
119 let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2;;
120
121 let uniq l =
122  let rec aux acc = function
123   | [] -> acc
124   | h::[] -> h::acc
125   | h1::h2::tl when h1=h2 -> aux (h2::acc) tl
126   | h1::tl (* when h1 <> h2 *) -> aux (h1::acc) tl
127  in
128   List.rev (aux [] (List.sort compare l))
129 ;;
130
131 let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) =
132  if dir <> dir' then
133   raise NoMatch
134  else
135   let rec aux =
136    function
137       [],w -> w
138     | x::lhs,x'::w when x = x' -> aux (lhs,w)
139     | _,_ -> raise NoMatch in
140   let w' = aux (lhs,w) in
141    if List.length rhs < List.length lhs then rhs @@ [w']
142    else rhs @@ apply_rules (aux (lhs,w),new_dir dir lhs)
143 and apply_rules (w,_ as w_and_dir) =
144  if w = [] then [[]]
145  else
146   let rec aux =
147    function
148       [] -> []
149     | rule::tl ->
150        (try apply_rule_at_beginning rule w_and_dir
151         with NoMatch -> [])
152        @
153        aux tl
154   in
155    aux rules
156 ;;
157
158 let apply_rules (w,dir as w_and_dir) =
159  List.map (fun w' -> w,dir,w')
160   (uniq (apply_rules w_and_dir))
161 ;;
162
163 let step (l : w list) =
164  uniq
165   (List.flatten
166     (List.map
167      (function w ->
168        List.map (fun x -> x@w)
169        (if List.length (List.filter (fun w -> w = M) w) >= 5 then
170          [[I];[C]]
171         else
172          [[I];[C];[M]])
173      ) l))
174 ;;
175
176 let mapi f l =
177  let rec aux acc i =
178   function
179      [] -> acc
180    | he::tl ->
181       if i mod 1000 = 0 then
182        begin
183         print_string ("@" ^ string_of_int i ^ " ");
184         flush stdout;
185        end;
186       aux (f he :: acc) (i+1) tl
187  in
188   let res = List.rev (aux [] 1 l) in
189    print_newline ();
190    res
191 ;;
192
193 let iteri f l =
194  let rec aux i =
195   function
196      [] -> ()
197    | he::tl ->
198       if i mod 1000 = 0 then
199        begin
200         print_string ("@" ^ string_of_int i ^ " ");
201         flush stdout;
202        end;
203       f he; aux (i+1) tl
204  in
205   aux 1 l;
206   print_newline ();
207 ;;
208
209 let normalize canonical (l : w list) =
210  print_endline (string_of_int (List.length l) ^ " nodes to be normalized");
211  let rec aux all l =
212   let rels =
213    List.flatten
214     (mapi (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) in
215   let arcs =
216    mapi
217     (function (x,rel,y) ->
218       let x = canonical x(*(inject x)*) in
219       let y = canonical y(*(inject y)*) in
220        match rel with Le -> x,y | Ge -> y,x) rels in
221   let res = uniq arcs in
222   let nodes = uniq (l @ List.map (fun (_,_,n) -> n) rels) in
223   let new_nodes = List.filter (fun n -> not (List.mem n all)) nodes in
224   let new_nodes = List.filter (function n -> [n] = canonical n) new_nodes in
225    if new_nodes = [] then
226     res
227    else
228     uniq (res @ aux nodes new_nodes)
229  in
230   aux l l
231 ;;
232
233 let visualize graph =
234  let module GL =
235   struct
236    include GL;;
237    let edge_attributes _ = []
238    let default_edge_attributes _ = []
239    let get_subgraph _ = None
240    let vertex_attributes v = [`Label (string_of_eqclass (GL.V.label v))]
241    let vertex_name v = name_of_eqclass (GL.V.label v)
242    let default_vertex_attributes _ = []
243    let graph_attributes _ = []
244   end in
245  let module D = Graph.Graphviz.Dot(GL) in
246   let ch = open_out "/tmp/comb.dot" in
247    D.output_graph ch graph;
248    close_out ch;
249    ignore (Unix.system ("tred /tmp/comb.dot > /tmp/red.dot"));
250    ignore (Unix.system ("dot -Tps /tmp/red.dot > /tmp/red.ps"));
251    (*Unix.system ("ggv /tmp/red.ps");*)
252 ;;
253
254 let w_compare s1 s2 =
255  let c = compare (List.length s1) (List.length s2) in
256   if c = 0 then compare s1 s2 else c
257 ;;
258
259 exception Found of GL.V.t;;
260
261 let rec iter n cgraph (canonical: w -> GL.V.t) =
262  print_endline ("STEP " ^ string_of_int n);
263  let nodes = GL.fold_vertex (fun n l -> n::l) cgraph [] in
264  let nodes = step (List.map List.hd nodes) in
265 (*let nodes = [[C;M];[C;M;C;M];[C;M;C;M;C;M];[C;M;C;M;C;M;C;M];[C;M;C;M;C;M;C;M;C;M]] in*)
266 (*let nodes = [[C;I;C;I;C;I]] in*)
267  (*let nodes = step (List.concat nodes) in*)
268 (*List.iter (fun x -> prerr_endline ("#@ " ^ string_of_w x)) nodes;*)
269  let arcs = normalize canonical nodes in
270   iteri (fun (x,y) -> if x <> y then GL.add_edge cgraph x y) arcs;
271 (*List.iter (fun (x,y) -> prerr_endline (string_of_eqclass x ^ " -> " ^ string_of_eqclass y)) arcs;*)
272
273   print_endline ("<scc>");
274   let classes,norm =
275    let module SCC = Graph.Components.Make(GL) in SCC.scc cgraph in
276   let xxx =
277    let module SCC = Graph.Components.Make(GL) in SCC.scc_array cgraph in
278   print_endline ("</scc>");
279   let get_canonical n =
280    try List.sort w_compare (List.concat (xxx.(norm n)))
281    with Not_found -> n
282   in
283   let nodes = GL.fold_vertex (fun n l -> n::l) cgraph [] in
284   print_endline "get_canonical";
285   let nodes = mapi (fun n -> n,get_canonical n) nodes in
286   print_endline "/get_canonical";
287   print_endline ("collapse " ^ string_of_int (List.length nodes));
288   iteri
289    (function (n,n') ->
290      let succ = GL.succ cgraph n in
291      let pred = GL.pred cgraph n in
292       GL.remove_vertex cgraph n;
293       let add_edge s t = if s <> t then GL.add_edge cgraph s t in
294       List.iter (fun s -> add_edge n' (get_canonical s)) succ;
295       List.iter (fun p -> add_edge (get_canonical p) n') pred)
296    nodes;
297   print_endline (string_of_int classes ^ " classes");
298   print_endline ("-----");
299   print_endline "visualize";
300   visualize cgraph;
301   print_endline ("/////");
302   GL.iter_vertex (fun l -> print_endline ("?" ^ string_of_eqclass l)) cgraph;
303   let canonical =
304    function (*_,_,*)w ->
305     try
306      GL.iter_vertex (fun l -> if List.mem w l then raise (Found l)) cgraph;
307      [w]
308     with
309      Found l -> l in
310   if n > 0 then
311    iter (n - 1) cgraph canonical
312   else
313    ()
314 in
315  let cgraph = GL.create () in
316   GL.add_vertex cgraph [[]];
317   iter 9 cgraph (fun w(*(_,_,w)*) -> [w])
318 ;;