New version: only new nodes are normalized; moreover, reduction stops as soon

as the term becomes shorter.

diff --git a/helm/software/matita/contribs/formal_topology/bin/Makefile b/helm/software/matita/contribs/formal_topology/bin/Makefile
index 1f2421a9dd28e7be0e1ca6e60ae3ac426ddda82b..a9298a9212fc5e8c24befa438f0ad2f08052aedb 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/bin/Makefile
+++ b/helm/software/matita/contribs/formal_topology/bin/Makefile
@@ -1,2 +1,2 @@
 comb: comb.ml
-       ocamlfind ocamlc -linkpkg -package ocamlgraph,unix -o comb comb.ml
+       ocamlfind ocamlc -g -linkpkg -package ocamlgraph,unix -o comb comb.ml

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index 2f4d46fcac930ad2456db3c522c2d12f8bbeddee..7b48cb3c2bd0b2fc2e492a6a6c5256b2c70e07da 100755 (executable)
--- 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 [[]] []
 ;;