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

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