New version.

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index d388acd89f9a209568fb2398f8a75b43c31e467c..af5633ff35a79c19a15e9650d2abdfcfac8a025e 100755 (executable)
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -2,89 +2,132 @@ type t = M | I | C
 type w = t list
 type eqclass = w list
 
+type dir = Le | Ge
+
 let rules =
- [ [I;I],   [I];
-   [C;C],   [C];
-   [M;M],   [];
-   [M;C],   [I;M];
-   [C;M],   [M;I];
-(*
-axiom leq_refl: ∀A. A ⊆ A.
-axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
-axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C.
-
-axiom i_contrattivita: ∀A. i A ⊆ A.
-axiom i_idempotenza: ∀A. i (i A) = i A.
-axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B.
-axiom c_espansivita: ∀A. A ⊆ c A.
-axiom c_idempotenza: ∀A. c (c A) = c A.
-axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B.
-axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A.
-axiom m_saturazione: ∀A. A ⊆ m (m A).
-axiom m_puntofisso: ∀A. m A = m (m (m A)).
-axiom th1: ∀A. c (m A) ⊆ m (i A).
-axiom th2: ∀A. i (m A) ⊆ m (c A).
-lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B.
-lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B.
-*)
+ [ [I],     Le, [];
+   [C],     Ge, [];
+   [I;I],   Ge, [I];
+   [C;C],   Le, [C];
+   [I],     Le, [I];
+   [I],     Ge, [I];
+   [C],     Le, [C];
+   [C],     Ge, [C];
+   [C;M],   Le, [M;I];
+   [C;M;I], Le, [M;I];  (* ??? *)
+   [I;M],   Le, [M;C];
+   [I;M;C], Ge, [I;M];  (* ??? *)
+   [M;M;M], Ge, [M];
+   [M;M],   Ge, [];
+   [M],     Le, [M];
+   [M],     Ge, [M];
  ]
 ;;
 
-let print_w w =
+let swap = function Le -> Ge | Ge -> Le;;
+
+let rec new_dir dir =
+ function
+    [] -> dir
+  | M::tl -> new_dir (swap dir) tl
+  | (C|I)::tl -> new_dir dir tl
+;;
+
+let string_of_dir = function Le -> "<=" | Ge -> ">=";;
+
+let string_of_w w =
  String.concat ""
   (List.map (function I -> "i" | C -> "c" | M -> "-") w)
 ;;
 
-let print_eqclass eqc =
+let string_of_eqclass eqc =
  let eqc = List.sort compare eqc in
-  prerr_endline (String.concat "=" (List.map print_w eqc))
+  String.concat "=" (List.map string_of_w eqc)
 ;;
 
-let print = List.iter print_eqclass;;
+let print = List.iter (fun eqc -> prerr_endline (string_of_eqclass eqc));;
 
 exception NoMatch;;
 
-let apply_rule_at_beginning (lhs,rhs) l =
- let rec aux =
+let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2;;
+
+let uniq l =
+ let rec aux l =
   function
-     [],l -> l
-   | x::lhs,x'::l when x = x' -> aux (lhs,l)
-   | _,_ -> raise NoMatch
+     [] -> l
+   | he::tl -> aux (if List.mem he l then l else he::l) tl
  in
-  rhs @ aux (lhs,l)
+  aux [] l
 ;;
 
-let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2
+let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) =
+ if dir <> dir' then
+  raise NoMatch
+ else
+  let rec aux =
+   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)
+and apply_rules (w,_ as w_and_dir) =
+ if w = [] then [[]]
+ else
+  let rec aux =
+   function
+      [] -> []
+    | rule::tl ->
+       (try apply_rule_at_beginning rule w_and_dir
+        with NoMatch -> [])
+       @
+       aux tl
+  in
+   aux rules
 ;;
 
-let rec apply_rule rule w =
- (try
-   [apply_rule_at_beginning rule w]
-  with
-   NoMatch -> []) @
- match w with
-    [] -> []
-  | he::tl -> [he] @@ apply_rule rule tl
+let apply_rules (w,dir as w_and_dir) =
+ List.map (fun w' -> w,dir,w')
+  (uniq (apply_rules w_and_dir))
 ;;
 
-let uniq =
- let rec aux l =
-  function
-     [] -> l
-   | he::tl -> aux (if List.mem he l then l else he::l) tl
- in
-  aux []
+let step (l : w list) =
+ uniq
+  (List.flatten
+    (List.map
+     (function w -> List.map (fun x -> x@w) [[I];[C];[M];[]])
+     l))
 ;;
 
-let apply_rules w =
- let rec aux =
-  function
-     [] -> [w]
-   | rule::rules -> apply_rule rule w @ aux rules
- in
-  uniq (aux rules)
+let classify (l : w list) =
+ List.flatten (List.map (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l)
 ;;
 
+let print_graph =
+ List.iter
+  (function (w,dir,w') ->
+    prerr_endline (string_of_w w ^ string_of_dir dir ^ string_of_w w'))
+;;
+
+print_graph (classify (step (step (step [[]]))));;
+
+(*
+ let ns = ref [] in
+  List.iter (function eqc -> ns := eqc::!ns) s;
+  List.iter
+   (function eqc ->
+     List.iter
+      (function x ->
+        let eqc = simplify ([x] @@ eqc) in
+         if not (List.exists (fun eqc' -> eqc === eqc') !ns) then
+          ns := eqc::!ns
+      ) [I;C;M]
+   ) s;
+  combine_classes !ns
+;;
+
+
+
 let subseteq l1 l2 =
  List.for_all (fun x -> List.mem x l2) l1
 ;;
@@ -140,3 +183,4 @@ let classes = step (step (step (step [[[]]]))) in
  prerr_endline ("Numero di classi trovate: " ^ string_of_int (List.length classes));
  print classes
 ;;
+*)