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