From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 5 Mar 2009 11:47:13 +0000 (+0000)
Subject: New version: only new nodes are normalized; moreover, reduction stops as soon
X-Git-Tag: make_still_working~4171
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dd70926289053cdc003776a5074d2262a2ec8243;p=helm.git

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 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 [[]] []
 ;;