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 -> List.map (fun x -> x@w) [[I];[C];[M];[]])
  99      l))
 100 ;;
 101
 102 let classify (l : w list) =
 103  List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
 104 ;;
 105
 106 let print_graph =
 107  List.iter
 108   (function (w,dir,w') ->
 109     prerr_endline (string_of_w w ^ string_of_dir dir ^ string_of_w w'))
 110 ;;
 111
 112 print_graph (classify (step (step (step [[]]))));;
 113
 114 (*
 115  let ns = ref [] in
 116   List.iter (function eqc -> ns := eqc::!ns) s;
 117   List.iter
 118    (function eqc ->
 119      List.iter
 120       (function x ->
 121         let eqc = simplify ([x] @@ eqc) in
 122          if not (List.exists (fun eqc' -> eqc === eqc') !ns) then
 123           ns := eqc::!ns
 124       ) [I;C;M]
 125    ) s;
 126   combine_classes !ns
 127 ;;
 128
 129
 130
 131 let subseteq l1 l2 =
 132  List.for_all (fun x -> List.mem x l2) l1
 133 ;;
 134
 135 let (===) l1 l2 = subseteq l1 l2 && subseteq l2 l1;;
 136
 137 let simplify eqc =
 138  let rec aux l =
 139   let l' = uniq (List.flatten (List.map apply_rules l)) in
 140   if l === l' then l else aux l'
 141  in
 142   aux eqc
 143 ;;
 144
 145 let combine_class_with_classes l1 =
 146  let rec aux =
 147   function
 148      [] -> [l1]
 149    | l2::tl ->
 150       if List.exists (fun x -> List.mem x l2) l1 then
 151        uniq (l1 @ l2) :: tl
 152       else
 153        l2:: aux tl
 154  in
 155   aux
 156 ;;
 157
 158 let combine_classes l =
 159  let rec aux acc =
 160   function
 161      [] -> acc
 162    | he::tl -> aux (combine_class_with_classes he acc) tl
 163  in
 164   aux [] l
 165 ;;
 166
 167 let step (s : eqclass list) =
 168  let ns = ref [] in
 169   List.iter (function eqc -> ns := eqc::!ns) s;
 170   List.iter
 171    (function eqc ->
 172      List.iter
 173       (function x ->
 174         let eqc = simplify ([x] @@ eqc) in
 175          if not (List.exists (fun eqc' -> eqc === eqc') !ns) then
 176           ns := eqc::!ns
 177       ) [I;C;M]
 178    ) s;
 179   combine_classes !ns
 180 ;;
 181
 182 let classes = step (step (step (step [[[]]]))) in
 183  prerr_endline ("Numero di classi trovate: " ^ string_of_int (List.length classes));
 184  print classes
 185 ;;
 186 *)