helm/software/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 ;;