From 18711733cdd65051fa094d5a5013ac306ea1bb60 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 2 Mar 2009 23:34:46 +0000 Subject: [PATCH] New version. --- .../contribs/formal_topology/bin/comb.ml | 158 +++++++++++------- 1 file changed, 101 insertions(+), 57 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml index d388acd89..af5633ff3 100755 --- 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 ;; +*) -- 2.39.2