From dd70926289053cdc003776a5074d2262a2ec8243 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 5 Mar 2009 11:47:13 +0000
Subject: [PATCH] New version: only new nodes are normalized; moreover,
 reduction stops as soon as the term becomes shorter.

---
 .../contribs/formal_topology/bin/Makefile     |  2 +-
 .../contribs/formal_topology/bin/comb.ml      | 29 +++++++++++--------
 2 files changed, 18 insertions(+), 13 deletions(-)

diff --git a/helm/software/matita/contribs/formal_topology/bin/Makefile b/helm/software/matita/contribs/formal_topology/bin/Makefile
index 1f2421a9d..a9298a921 100644
--- 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 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 [[]] []
 ;;
-- 
2.39.2