X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Ftheory_explorer.ml;h=d857ab93e1f1f22d77c46786aa1f258cf57ec611;hb=855c09b06dd6c952063e61cf00df52685f400665;hp=be1e107fb21081f8d62ea0bcc0bec192692f656f;hpb=99ca90bf28a25fcd1cd84596c37be43c97f74e6e;p=helm.git 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 be1e107fb..d857ab93e 100644 --- a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml +++ b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml @@ -1,3 +1,11 @@ +type rel = Equal | SubsetEqual | SupersetEqual + +let string_of_rel = + function + Equal -> "=" + | SubsetEqual -> "⊆" + | SupersetEqual -> "⊇" + (* operator *) type op = I | C | M @@ -13,6 +21,8 @@ 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 @@ -40,12 +50,16 @@ let string_of_equivalence_class (repr,others,leq,_) = let dot_of_equivalence_class (repr,others,leq,_) = (if others <> [] then let eq = String.concat " = " (List.map string_of_cop (repr::others)) in - string_of_cop repr ^ "[label=\"" ^ eq ^ "\"];\n" - else "") ^ + 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',_,_,_) -> - string_of_cop repr' ^ " -> " ^ string_of_cop repr ^ ";") !leq) + dot_of_cop repr' ^ " -> " ^ dot_of_cop repr ^ ";") !leq) (* set of equivalence classes *) type set = equivalence_class list @@ -53,26 +67,44 @@ type set = equivalence_class list let string_of_set s = String.concat "\n" (List.map string_of_equivalence_class s) -let ps_of_set ?processing 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 - (string_of_cop repr' ^ " -> " ^ string_of_cop repr ^ - " [" ^ - (if rel="=" then "arrowhead=none " else "") ^ - "style=dashed];\n")); + 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 "dot -Tps xxx.dot > xxx.ps") -let test set rel candidate repr = - ps_of_set ~processing:(candidate,rel,repr) set; +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 ^ " " ^ rel ^ " " ^ string_of_cop repr ^ "? "); + (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 @@ -96,22 +128,30 @@ let test set rel candidate repr = 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 ^ " " ^ rel ^ " " ^ - matita_of_cop "A" repr ^ ". intros; auto size=6 depth=4. qed.\n"); + ("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 >> 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 candidate set = +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 set "=" candidate repr then + if test to_be_considered_and_now set Equal candidate repr then (repr,others@[candidate],leq,geq)::tl else eqclass::(aux tl) @@ -119,18 +159,18 @@ let normalize candidate set = aux set ;; -let locate ((repr,_,leq,geq) as node) 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 set "⊆" 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 set "⊆" repr' repr then + else if test to_be_considered_and_now set SupersetEqual repr repr' then begin geq := node' :: !geq; leq' := node :: !leq' @@ -140,13 +180,13 @@ let locate ((repr,_,leq,geq) as node) set = aux set ;; -let analyze_one i repr hecandidate (news,set) = +let analyze_one to_be_considered repr hecandidate (news,set) = let candidate = hecandidate::repr in - if List.length (List.filter ((=) M) candidate) > i then + if List.length (List.filter ((=) M) candidate) > 1 then news,set else try - let set = normalize candidate set in + let set = normalize (to_be_considered,Some repr,news) candidate set in news,set with Not_found -> @@ -154,42 +194,39 @@ let analyze_one i repr hecandidate (news,set) = let geq = ref [] in let node = candidate,[],leq,geq in let set = node::set in - locate node set; + locate (to_be_considered,Some repr,news) node set; candidate::news,set ;; -let rec explore i j set news = +let rec explore i set news = let rec aux news set = function [] -> news,set | repr::tl -> let news,set = - List.fold_right (analyze_one i repr) [I;C;M] (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 ^ " j=" ^ string_of_int j); + print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i); print_endline (string_of_set set ^ "\n----------------"); - if i < 2 then - explore (i+1) 1 set (List.map (function (repr,_,_,_) -> repr) set) - else - ps_of_set set + ps_of_set ([],None,[]) set end else begin - print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i ^ " j=" ^ string_of_int j); + print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i); print_endline (string_of_set set ^ "\n----------------"); - explore i (j+1) set news + 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 set; - explore 0 1 set [id] + (*ignore (Unix.system "rm -f log");*) + ps_of_set ([id],None,[]) set; + explore 1 set [id] ;;