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

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