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