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_dir = function Le -> "<=" | Ge -> ">=";;
  37
  38 let string_of_w w =
  39  String.concat ""
  40   (List.map (function I -> "i" | C -> "c" | M -> "-") w)
  41 ;;
  42
  43 let string_of_eqclass eqc =
  44  let eqc = List.sort compare eqc in
  45   String.concat "=" (List.map string_of_w eqc)
  46 ;;
  47
  48 let print = List.iter (fun eqc -> prerr_endline (string_of_eqclass eqc));;
  49
  50 exception NoMatch;;
  51
  52 let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2;;
  53
  54 let uniq l =
  55  let rec aux l =
  56   function
  57      [] -> l
  58    | he::tl -> aux (if List.mem he l then l else he::l) tl
  59  in
  60   aux [] l
  61 ;;
  62
  63 let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) =
  64  if dir <> dir' then
  65   raise NoMatch
  66  else
  67   let rec aux =
  68    function
  69       [],w -> w
  70     | x::lhs,x'::w when x = x' -> aux (lhs,w)
  71     | _,_ -> raise NoMatch
  72   in
  73    rhs @@ apply_rules (aux (lhs,w),new_dir dir lhs)
  74 and apply_rules (w,_ as w_and_dir) =
  75  if w = [] then [[]]
  76  else
  77   let rec aux =
  78    function
  79       [] -> []
  80     | rule::tl ->
  81        (try apply_rule_at_beginning rule w_and_dir
  82         with NoMatch -> [])
  83        @
  84        aux tl
  85   in
  86    aux rules
  87 ;;
  88
  89 let apply_rules (w,dir as w_and_dir) =
  90  List.map (fun w' -> w,dir,w')
  91   (uniq (apply_rules w_and_dir))
  92 ;;
  93
  94 let step (l : w list) =
  95  uniq
  96   (List.flatten
  97     (List.map
  98      (function w ->
  99        List.map (fun x -> x@w)
 100        (if List.mem M w then
 101          [[I];[C];[]]
 102         else
 103          [[I];[C](*;[M]*);[]])
 104      ) l))
 105 ;;
 106
 107 let leq rels x y =
 108  let rec aux avoid x y =
 109   x = y ||
 110    List.exists
 111     (fun (x',z) -> x=x' && not (List.mem z avoid) && aux (z::avoid) z y) rels
 112  in
 113   aux [x] x y
 114 ;;
 115
 116 let in_class rels eqc he =
 117  match eqc with
 118     [] -> assert false
 119   | k::_ -> leq rels k he && leq rels he k
 120 ;;
 121
 122 let add_class rels classes he =
 123 prerr_endline "Add";
 124  let rec aux visited =
 125   function
 126      [] -> [he]::visited
 127    | eqc::tl ->
 128       if in_class rels eqc he then
 129        (he::eqc)::tl@visited
 130       else
 131        aux (eqc::visited) tl
 132  in
 133   aux [] classes
 134 ;;
 135
 136 let classify (l : w list) =
 137 prerr_endline ("Classify: " ^ string_of_int (List.length l));
 138  let rels =
 139   List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
 140  in
 141   uniq
 142    (List.map
 143     (function (x,rel,y) -> match rel with Le -> x,y | Ge -> y,x) rels)
 144 ;;
 145
 146 let visualize graph =
 147   let dot = "" in
 148   (*Graph.Pack.Digraph.dot_output graph dot;*)
 149   Graph.Pack.Digraph.display_with_gv graph;
 150 exit 1;
 151 (*
 152   let ch = open_out "/tmp/comb.dot" in
 153    output_string ch dot;
 154    close_out ch;
 155    Unix.system ("tred /tmp/comb.dot > /tmp/red.dot");
 156    Unix.system ("dot -Tps /tmp/red.dot > /tmp/red.ps");
 157    Unix.system ("ggv /tmp/red.ps");
 158 *) ()
 159 ;;
 160
 161 let analyze arcs =
 162  let mk_vertex =
 163   let cache = ref [] in
 164   function w ->
 165    try
 166     List.assoc w !cache
 167    with
 168     Not_found ->
 169      let n =
 170       let rec aux acc =
 171        function
 172           [] -> acc
 173         | he::tl -> aux (acc * 4 + (match he with I -> 1 | C -> 2 | M -> 3)) tl
 174       in
 175        aux 0 w
 176      in
 177 prerr_endline (string_of_w w ^ " => " ^ string_of_int n);
 178       let v = Graph.Pack.Digraph.V.create n in
 179        cache := (w,v)::!cache;
 180        v in
 181  let graph = Graph.Pack.Digraph.create () in
 182  List.iter
 183   (function (x,y) ->
 184     Graph.Pack.Digraph.add_edge graph (mk_vertex x) (mk_vertex y)) arcs;
 185 prerr_endline ("<CLASSI>");
 186  let classes =  Graph.Pack.Digraph.Components.scc_list graph in
 187 List.iter (function l -> prerr_endline (String.concat "=" (List.map string_of_int (List.map Graph.Pack.Digraph.V.label l)))) classes;
 188 prerr_endline ("</CLASSI>");
 189  let classes,normalize =  Graph.Pack.Digraph.Components.scc graph in
 190 prerr_endline (string_of_int classes ^ " CLASSI");
 191  let arcs = uniq (List.map (fun (x,y) -> normalize (mk_vertex x),normalize (mk_vertex y)) arcs) in
 192  let cgraph = Graph.Pack.Digraph.create () in
 193  List.iter
 194   (function (x,y) ->
 195     Graph.Pack.Digraph.add_edge cgraph (Graph.Pack.Digraph.V.create x) (Graph.Pack.Digraph.V.create y)) arcs;
 196  visualize cgraph
 197 ;;
 198
 199 let rec iter n l =
 200  let arcs = analyze (classify l) in
 201  (*print_graph' (analyze arcs);*)
 202  if n > 0 then
 203   iter (n - 1) (step l)
 204 in
 205  iter 4 [[]]
 206 ;;