helm/software/matita/contribs/formal_topology/bin/comb.ml

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