10 (* compound operator *)
11 type compound_operator = op list
13 let string_of_cop op =
14 if op = [] then "id" else String.concat "" (List.map string_of_op op)
16 let rec matita_of_cop v =
19 | I::tl -> "i (" ^ matita_of_cop v tl ^ ")"
20 | C::tl -> "c (" ^ matita_of_cop v tl ^ ")"
21 | M::tl -> "m (" ^ matita_of_cop v tl ^ ")"
23 (* representative, other elements in the equivalence class,
24 leq classes, geq classes *)
25 type equivalence_class =
26 compound_operator * compound_operator list *
27 equivalence_class list ref * equivalence_class list ref
29 let string_of_equivalence_class (repr,others,leq,_) =
30 String.concat " = " (List.map string_of_cop (repr::others)) ^
35 (function (repr',_,_,_) ->
36 string_of_cop repr ^ " <= " ^ string_of_cop repr') !leq)
40 let dot_of_equivalence_class (repr,others,leq,_) =
42 let eq = String.concat " = " (List.map string_of_cop (repr::others)) in
43 string_of_cop repr ^ "[label=\"" ^ eq ^ "\"];\n"
47 (function (repr',_,_,_) ->
48 string_of_cop repr' ^ " -> " ^ string_of_cop repr ^ ";") !leq)
50 (* set of equivalence classes *)
51 type set = equivalence_class list
54 String.concat "\n" (List.map string_of_equivalence_class s)
56 let ps_of_set ?processing s =
57 let ch = open_out "xxx.dot" in
58 output_string ch "digraph G {\n";
59 output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s));
60 (match processing with
62 | Some (repr,rel,repr') ->
64 (string_of_cop repr' ^ " -> " ^ string_of_cop repr ^
66 (if rel="=" then "arrowhead=none " else "") ^
68 output_string ch "}\n";
70 ignore (Unix.system "dot -Tps xxx.dot > xxx.ps")
72 let test set rel candidate repr =
73 ps_of_set ~processing:(candidate,rel,repr) set;
75 (string_of_cop candidate ^ " " ^ rel ^ " " ^ string_of_cop repr ^ "? ");
77 assert (Unix.system "cp formal_topology.ma xxx.ma" = Unix.WEXITED 0);
78 let ch = open_out_gen [Open_append] 0 "xxx.ma" in
81 (function (repr,others,leq,_) ->
86 ("axiom ax" ^ string_of_int !i ^
88 matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n");
91 (function (repr',_,_,_) ->
94 ("axiom ax" ^ string_of_int !i ^
96 matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n");
100 ("theorem foo: \\forall A." ^ matita_of_cop "A" candidate ^ " " ^ rel ^ " " ^
101 matita_of_cop "A" repr ^ ". intros; auto size=6 depth=4. qed.\n");
104 Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0
106 print_endline (if res then "y" else "n");
109 let normalize candidate set =
112 [] -> raise Not_found
113 | (repr,others,leq,geq) as eqclass :: tl ->
114 if test set "=" candidate repr then
115 (repr,others@[candidate],leq,geq)::tl
122 let locate ((repr,_,leq,geq) as node) set =
126 | (repr',_,leq',geq') as node' :: tl ->
127 if repr = repr' then ()
128 else if test set "⊆" repr repr' then
130 leq := node' :: !leq;
131 geq' := node :: !geq'
133 else if test set "⊆" repr' repr then
135 geq := node' :: !geq;
136 leq' := node :: !leq'
143 let analyze_one i repr hecandidate (news,set) =
144 let candidate = hecandidate::repr in
145 if List.length (List.filter ((=) M) candidate) > i then
149 let set = normalize candidate set in
155 let node = candidate,[],leq,geq in
156 let set = node::set in
161 let rec explore i j set news =
162 let rec aux news set =
167 List.fold_right (analyze_one i repr) [I;C;M] (news,set)
171 let news,set = aux [] set news in
174 print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i ^ " j=" ^ string_of_int j);
175 print_endline (string_of_set set ^ "\n----------------");
177 explore (i+1) 1 set (List.map (function (repr,_,_,_) -> repr) set)
183 print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i ^ " j=" ^ string_of_int j);
184 print_endline (string_of_set set ^ "\n----------------");
185 explore i (j+1) set news
189 let set = [id,[],ref [], ref []] in
190 print_endline ("PRIMA ITERAZIONE, i=0, j=0");
191 print_endline (string_of_set set ^ "\n----------------");
192 ignore (Unix.system "rm -f log");