From: Claudio Sacerdoti Coen Date: Thu, 24 May 2007 10:56:33 +0000 (+0000) Subject: theory_explorer_do_not_trust_auto.ml is the version that does not trust X-Git-Tag: make_still_working~6306 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=49d22bdd0550130cad3070f991fc2b3f66a333e6;p=helm.git theory_explorer_do_not_trust_auto.ml is the version that does not trust auto. The algorithm is exponential. theory_explorer.ml trusts auto and requires only quadratic time. Not working properly yet. --- diff --git a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml index 3a9dcde30..ca5c1c271 100644 --- a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml +++ b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml @@ -43,7 +43,7 @@ let string_of_equivalence_class (repr,others,leq,_) = String.concat "\n" (List.map (function (repr',_,_,_) -> - string_of_cop repr ^ " <= " ^ string_of_cop repr') !leq) + string_of_cop repr ^ " ⊆ " ^ string_of_cop repr') !leq) else "") @@ -61,19 +61,28 @@ let dot_of_equivalence_class (repr,others,leq,_) = (function (repr',_,_,_) -> dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ ";") !leq) -(* set of equivalence classes *) -type set = equivalence_class list +(* set of equivalence classes, infima, suprema *) +type set = + equivalence_class list * equivalence_class list * equivalence_class list -let string_of_set s = +let string_of_set (s,_,_) = String.concat "\n" (List.map string_of_equivalence_class s) -let ps_of_set (to_be_considered,under_consideration,news) ?processing s = +let ps_of_set (to_be_considered,under_consideration,news) ?processing (s,inf,sup) = let ch = open_out "xxx.dot" in output_string ch "digraph G {\n"; (match under_consideration with None -> () | Some repr -> output_string ch (dot_of_cop repr ^ " [color=yellow];")); + List.iter + (function (repr,_,_,_) -> + output_string ch (dot_of_cop repr ^ " [shape=diamond];") + ) inf ; + List.iter + (function (repr,_,_,_) -> + output_string ch (dot_of_cop repr ^ " [shape=polygon];") + ) sup ; List.iter (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];") ) to_be_considered ; @@ -101,7 +110,7 @@ let ps_of_set (to_be_considered,under_consideration,news) ?processing s = close_out ch; ignore (Unix.system "tred xxx.dot > yyy.dot && dot -Tps yyy.dot > xxx.ps") -let test to_be_considered_and_now set rel candidate repr = +let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr = ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set; print_string (string_of_cop candidate ^ " " ^ string_of_rel rel ^ " " ^ string_of_cop repr ^ "? "); @@ -127,7 +136,7 @@ let test to_be_considered_and_now set rel candidate repr = ": \\forall A." ^ matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n"); ) !leq; - ) set; + ) s; let candidate',rel',repr' = match rel with SupersetEqual -> repr,SubsetEqual,candidate @@ -146,59 +155,118 @@ let test to_be_considered_and_now set rel candidate repr = print_endline (if res then "y" else "n"); res -let normalize to_be_considered_and_now candidate set = - let rec aux = +let rec leq_transitive_closure leq node ((repr,_,leq',geq') as node') = + if not (List.mem node' !leq) then leq := node' :: !leq; + if not (List.mem node !geq') then geq' := node :: !geq'; + List.iter (leq_transitive_closure leq node) !leq' +;; + +let rec geq_transitive_closure geq node ((_,_,leq',geq') as node') = + if not (List.mem node' !geq) then geq := node' :: !geq; + if not (List.mem node !leq') then leq' := node :: !leq'; + List.iter (geq_transitive_closure geq node) !geq' +;; + +let remove node l = + let l' = List.filter (fun node' -> node != node') l in + if List.length l = List.length l' then + assert false + else + l' +;; + +let locate_using_leq to_be_considered_and_now ((repr,_,leq,_) as node) + ((nodes,inf,sup) as set) += + let rec aux is_sup inf = function - [] -> raise Not_found - | (repr,others,leq,geq) as eqclass :: tl -> - if test to_be_considered_and_now set Equal candidate repr then - (repr,others@[candidate],leq,geq)::tl + [] -> is_sup,inf + | (repr',_,_,geq') as node' :: sup -> + if repr=repr' then aux is_sup inf (!geq'@sup) + else if List.mem node' !leq + || test to_be_considered_and_now set SubsetEqual repr repr' + then + begin + let inf = if !geq' = [] then remove node' inf else inf in + leq_transitive_closure leq node node'; + aux false inf (!geq'@sup) + end else - eqclass::(aux tl) + aux is_sup inf sup in - aux set + let is_sup,inf = aux true inf sup in + if is_sup then + nodes,inf,sup@[node] + else + nodes,inf,sup ;; -let locate to_be_considered_and_now ((repr,_,leq,geq) as node) set = - let rec aux = +exception SameEquivalenceClass of equivalence_class * equivalence_class;; + +let locate_using_geq to_be_considered_and_now ((repr,_,leq,geq) as node) + ((nodes,inf,sup) as set) += + let rec aux is_inf sup = function - [] -> () - | (repr',_,leq',geq') as node' :: tl -> - if repr = repr' then () - else if test to_be_considered_and_now set SubsetEqual repr repr' then + [] -> sup,is_inf + | (repr',_,leq',_) as node' :: inf -> + if repr=repr' then aux is_inf sup (!leq'@inf) + else if List.mem node' !geq + || test to_be_considered_and_now set SupersetEqual repr repr' + then begin - leq := node' :: !leq; - geq' := node :: !geq' + if List.mem node' !leq then + (* We have found two equal nodes! *) + raise (SameEquivalenceClass (node,node')) + else + begin + let sup = if !leq' = [] then remove node' sup else sup in + geq_transitive_closure geq node node'; + aux false sup (!leq'@inf) + end end - else if test to_be_considered_and_now set SupersetEqual repr repr' then - begin - geq := node' :: !geq; - leq' := node :: !leq' - end ; - aux tl + else + aux is_inf sup inf in - aux set + let sup,is_inf = aux true sup inf in + if is_inf then + nodes,inf@[node],sup + else + nodes,inf,sup ;; -let analyze_one to_be_considered repr hecandidate (news,set) = +let analyze_one to_be_considered repr hecandidate (news,((nodes,inf,sup) as set)) = let candidate = hecandidate::repr in if List.length (List.filter ((=) M) candidate) > 1 then news,set else try - let set = normalize (to_be_considered,Some repr,news) candidate set in - news,set + let leq = ref [] in + let geq = ref [] in + let node = candidate,[],leq,geq in + let nodes = nodes@[node] in + let set = nodes,inf,sup in + let set = locate_using_leq (to_be_considered,Some repr,news) node set in + let set = locate_using_geq (to_be_considered,Some repr,news) node set in + news@[candidate],set with - Not_found -> - let leq = ref [] in - let geq = ref [] in - let node = candidate,[],leq,geq in - let set = node::set in - locate (to_be_considered,Some repr,news) node set; - candidate::news,set + SameEquivalenceClass (node_to_be_deleted,node') -> + let rec clean = + function + [] -> [] + | (repr',others,leq,geq) as node::tl -> + leq := List.filter (function node -> node_to_be_deleted != node) !leq; + geq := List.filter (function node -> node_to_be_deleted != node) !geq; + if node==node' then + (repr',others@[candidate],leq,geq)::clean tl + else + (repr',others,leq,geq)::clean tl + in + let nodes = clean nodes in + news,(nodes,inf,sup) ;; -let rec explore i set news = +let rec explore i (set:set) news = let rec aux news set = function [] -> news,set @@ -223,7 +291,8 @@ let rec explore i set news = end in let id = [] in - let set = [id,[],ref [], ref []] in + let id_node = id,[],ref [], ref [] in + let set = [id_node],[id_node],[id_node] in print_endline ("PRIMA ITERAZIONE, i=0, j=0"); print_endline (string_of_set set ^ "\n----------------"); (*ignore (Unix.system "rm -f log");*) diff --git a/helm/software/matita/contribs/formal_topology/bin/theory_explorer_do_not_trust_auto.ml b/helm/software/matita/contribs/formal_topology/bin/theory_explorer_do_not_trust_auto.ml new file mode 100644 index 000000000..3a9dcde30 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/bin/theory_explorer_do_not_trust_auto.ml @@ -0,0 +1,232 @@ +type rel = Equal | SubsetEqual | SupersetEqual + +let string_of_rel = + function + Equal -> "=" + | SubsetEqual -> "⊆" + | SupersetEqual -> "⊇" + +(* operator *) +type op = I | C | M + +let string_of_op = + function + I -> "i" + | C -> "c" + | M -> "-" + +(* compound operator *) +type compound_operator = op list + +let string_of_cop op = + if op = [] then "id" else String.concat "" (List.map string_of_op op) + +let dot_of_cop op = "\"" ^ string_of_cop op ^ "\"" + +let rec matita_of_cop v = + function + | [] -> v + | I::tl -> "i (" ^ matita_of_cop v tl ^ ")" + | C::tl -> "c (" ^ matita_of_cop v tl ^ ")" + | M::tl -> "m (" ^ matita_of_cop v tl ^ ")" + +(* representative, other elements in the equivalence class, + leq classes, geq classes *) +type equivalence_class = + compound_operator * compound_operator list * + equivalence_class list ref * equivalence_class list ref + +let string_of_equivalence_class (repr,others,leq,_) = + String.concat " = " (List.map string_of_cop (repr::others)) ^ + (if !leq <> [] then + "\n" ^ + String.concat "\n" + (List.map + (function (repr',_,_,_) -> + string_of_cop repr ^ " <= " ^ string_of_cop repr') !leq) + else + "") + +let dot_of_equivalence_class (repr,others,leq,_) = + (if others <> [] then + let eq = String.concat " = " (List.map string_of_cop (repr::others)) in + dot_of_cop repr ^ "[label=\"" ^ eq ^ "\"];" ^ + if !leq = [] then "" else "\n" + else if !leq = [] then + dot_of_cop repr ^ ";" + else + "") ^ + String.concat "\n" + (List.map + (function (repr',_,_,_) -> + dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ ";") !leq) + +(* set of equivalence classes *) +type set = equivalence_class list + +let string_of_set s = + String.concat "\n" (List.map string_of_equivalence_class s) + +let ps_of_set (to_be_considered,under_consideration,news) ?processing s = + let ch = open_out "xxx.dot" in + output_string ch "digraph G {\n"; + (match under_consideration with + None -> () + | Some repr -> + output_string ch (dot_of_cop repr ^ " [color=yellow];")); + List.iter + (function repr -> output_string ch (dot_of_cop repr ^ " [color=green];") + ) to_be_considered ; + List.iter + (function repr -> output_string ch (dot_of_cop repr ^ " [color=navy];") + ) news ; + output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s)); + output_string ch "\n"; + (match processing with + None -> () + | Some (repr,rel,repr') -> + output_string ch (dot_of_cop repr ^ " [color=red];"); + let repr,repr' = + match rel with + SupersetEqual -> repr',repr + | Equal + | SubsetEqual -> repr,repr' + in + output_string ch + (dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ + " [" ^ + (match rel with Equal -> "arrowhead=none " | _ -> "") ^ + "style=dashed];\n")); + output_string ch "}\n"; + close_out ch; + ignore (Unix.system "tred xxx.dot > yyy.dot && dot -Tps yyy.dot > xxx.ps") + +let test to_be_considered_and_now set rel candidate repr = + ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set; + print_string + (string_of_cop candidate ^ " " ^ string_of_rel rel ^ " " ^ string_of_cop repr ^ "? "); + flush stdout; + assert (Unix.system "cp formal_topology.ma xxx.ma" = Unix.WEXITED 0); + let ch = open_out_gen [Open_append] 0 "xxx.ma" in + let i = ref 0 in + List.iter + (function (repr,others,leq,_) -> + List.iter + (function repr' -> + incr i; + output_string ch + ("axiom ax" ^ string_of_int !i ^ + ": \\forall A." ^ + matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n"); + ) others; + List.iter + (function (repr',_,_,_) -> + incr i; + output_string ch + ("axiom ax" ^ string_of_int !i ^ + ": \\forall A." ^ + matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n"); + ) !leq; + ) set; + let candidate',rel',repr' = + match rel with + SupersetEqual -> repr,SubsetEqual,candidate + | Equal + | SubsetEqual -> candidate,rel,repr + in + output_string ch + ("theorem foo: \\forall A." ^ matita_of_cop "A" candidate' ^ + " " ^ string_of_rel rel' ^ " " ^ + matita_of_cop "A" repr' ^ ". intros; auto size=6 depth=4. qed.\n"); + close_out ch; + let res = + (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*) + Unix.system "../../../matitac.opt xxx.ma > /dev/null 2>&1" = Unix.WEXITED 0 + in + print_endline (if res then "y" else "n"); + res + +let normalize to_be_considered_and_now candidate set = + let rec aux = + function + [] -> raise Not_found + | (repr,others,leq,geq) as eqclass :: tl -> + if test to_be_considered_and_now set Equal candidate repr then + (repr,others@[candidate],leq,geq)::tl + else + eqclass::(aux tl) + in + aux set +;; + +let locate to_be_considered_and_now ((repr,_,leq,geq) as node) set = + let rec aux = + function + [] -> () + | (repr',_,leq',geq') as node' :: tl -> + if repr = repr' then () + else if test to_be_considered_and_now set SubsetEqual repr repr' then + begin + leq := node' :: !leq; + geq' := node :: !geq' + end + else if test to_be_considered_and_now set SupersetEqual repr repr' then + begin + geq := node' :: !geq; + leq' := node :: !leq' + end ; + aux tl + in + aux set +;; + +let analyze_one to_be_considered repr hecandidate (news,set) = + let candidate = hecandidate::repr in + if List.length (List.filter ((=) M) candidate) > 1 then + news,set + else + try + let set = normalize (to_be_considered,Some repr,news) candidate set in + news,set + with + Not_found -> + let leq = ref [] in + let geq = ref [] in + let node = candidate,[],leq,geq in + let set = node::set in + locate (to_be_considered,Some repr,news) node set; + candidate::news,set +;; + +let rec explore i set news = + let rec aux news set = + function + [] -> news,set + | repr::tl -> + let news,set = + List.fold_right (analyze_one tl repr) [I;C;M] (news,set) + in + aux news set tl + in + let news,set = aux [] set news in + if news = [] then + begin + print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i); + print_endline (string_of_set set ^ "\n----------------"); + ps_of_set ([],None,[]) set + end + else + begin + print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i); + print_endline (string_of_set set ^ "\n----------------"); + explore (i+1) set news + end +in + let id = [] in + let set = [id,[],ref [], ref []] in + print_endline ("PRIMA ITERAZIONE, i=0, j=0"); + print_endline (string_of_set set ^ "\n----------------"); + (*ignore (Unix.system "rm -f log");*) + ps_of_set ([id],None,[]) set; + explore 1 set [id] +;;