X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Fcomb.ml;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Fcomb.ml;h=7b48cb3c2bd0b2fc2e492a6a6c5256b2c70e07da;hb=dd70926289053cdc003776a5074d2262a2ec8243;hp=2f4d46fcac930ad2456db3c522c2d12f8bbeddee;hpb=7bc72d8afaebb1d2070a26b07f9bf4242b648e2c;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index 2f4d46fca..7b48cb3c2 100755
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -1,8 +1,11 @@
-(* 0: 7
+(* 0: 7       4
    1: 29      6
    2: 120    10
    3: > 327  >9
-   4: ???
+   4: > 657  >9
+   5: > 526  >8
+   6: > 529  >8
+   7:
 *)
 
 type t = M | I | C
@@ -116,9 +119,10 @@ let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) =
    function
       [],w -> w
     | x::lhs,x'::w when x = x' -> aux (lhs,w)
-    | _,_ -> raise NoMatch
-  in
-   rhs @@ apply_rules (aux (lhs,w),new_dir dir lhs)
+    | _,_ -> raise NoMatch in
+  let w' = aux (lhs,w) in
+   if List.length rhs < List.length lhs then rhs @@ [w']
+   else rhs @@ apply_rules (aux (lhs,w),new_dir dir lhs)
 and apply_rules (w,_ as w_and_dir) =
  if w = [] then [[]]
  else
@@ -145,10 +149,10 @@ let step (l : w list) =
     (List.map
      (function w ->
        List.map (fun x -> x@w)
-       (if List.length (List.filter (fun w -> w = M) w) >= 3 then
-         [[I];[C];[]]
+       (if List.length (List.filter (fun w -> w = M) w) >= 7 then
+         [[I];[C]]
         else
-         [[I];[C];[M];[]])
+         [[I];[C];[M]])
      ) l))
 ;;
 
@@ -282,13 +286,14 @@ let analyze (norm,arcs) =
  print_endline ("/////");
 ;;
 
-let rec iter n l =
+let rec iter n nodes old_arcs =
  print_endline ("STEP " ^ string_of_int n);
- let pkg = classify (normalize l) in
+ let arcs = old_arcs @ normalize nodes in
+ let pkg = classify arcs in
  if n > 0 then
-  iter (n - 1) (step l)
+  iter (n - 1) (step nodes) arcs
  else
   analyze pkg
 in
- iter 15 [[]]
+ iter 8 [[]] []
 ;;