6 | Success of Cic.term option * environment
10 type equality_sign = Negative | Positive;;
12 let string_of_sign = function
13 | Negative -> "Negative"
14 | Positive -> "Positive"
18 module OrderedEquality =
20 type t = Inference.equality
23 match meta_convertibility_eq eq1 eq2 with
25 | false -> Pervasives.compare eq1 eq2
28 module EqualitySet = Set.Make(OrderedEquality);;
32 let select env passive =
34 | hd::tl, pos -> (Negative, hd), (tl, pos)
35 | [], hd::tl -> (Positive, hd), ([], tl)
36 | _, _ -> assert false
41 let select env passive =
43 | neg, pos when EqualitySet.is_empty neg ->
44 let elem = EqualitySet.min_elt pos in
45 (Positive, elem), (neg, EqualitySet.remove elem pos)
47 let elem = EqualitySet.min_elt neg in
48 (Negative, elem), (EqualitySet.remove elem neg, pos)
53 (* TODO: find a better way! *)
56 let infer env sign current active =
57 let rec infer_negative current = function
59 | (Negative, _)::tl -> infer_negative current tl
60 | (Positive, equality)::tl ->
61 let res = superposition_left env current equality in
62 let neg, pos = infer_negative current tl in
65 and infer_positive current = function
67 | (Negative, equality)::tl ->
68 let res = superposition_left env equality current in
69 let neg, pos = infer_positive current tl in
71 | (Positive, equality)::tl ->
72 let maxm, res = superposition_right !maxmeta env current equality in
73 let maxm, res' = superposition_right maxm env equality current in
75 let neg, pos = infer_positive current tl in
77 (* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
78 (* (string_of_equality ~env current) (string_of_equality ~env equality) *)
79 (* (String.concat "\n" (List.map (string_of_equality ~env) res)); *)
80 (* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
81 (* (string_of_equality ~env equality) (string_of_equality ~env current) *)
82 (* (String.concat "\n" (List.map (string_of_equality ~env) res')); *)
87 | Negative -> infer_negative current active
88 | Positive -> infer_positive current active
92 let contains_empty env (negative, positive) =
93 let metasenv, context, ugraph = env in
95 let (proof, _, _, _) =
97 (fun (proof, (ty, left, right), m, a) ->
98 fst (CicReduction.are_convertible context left right ugraph))
107 let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) =
108 let find sign eq1 eq2 =
109 if meta_convertibility_eq eq1 eq2 then (
110 (* Printf.printf "Trovato equazione duplicata di segno %s\n%s\n\n" *)
111 (* (string_of_sign sign) (string_of_equality eq1); *)
116 let ok sign equalities equality =
117 not (List.exists (find sign equality) equalities)
119 let neg = List.filter (ok Negative passive_neg) new_neg in
120 let pos = List.filter (ok Positive passive_pos) new_pos in
121 (* let neg, pos = new_neg, new_pos in *)
122 (neg @ passive_neg, passive_pos @ pos)
126 let is_identity ((_, context, ugraph) as env) = function
127 | ((_, (ty, left, right), _, _) as equality) ->
130 (fst (CicReduction.are_convertible context left right ugraph)))
133 (* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
134 (* print_newline (); *)
140 let forward_simplify env (sign, current) active =
141 (* if sign = Negative then *)
142 (* Some (sign, current) *)
144 let rec aux env (sign, current) =
146 | [] -> Some (sign, current)
147 | (Negative, _)::tl -> aux env (sign, current) tl
148 | (Positive, equality)::tl ->
149 let newmeta, current = demodulation !maxmeta env current equality in
151 if is_identity env current then
154 aux env (sign, current) tl
156 aux env (sign, current) active
160 let forward_simplify_new env (new_neg, new_pos) active =
161 let remove_identities equalities =
162 let ok eq = not (is_identity env eq) in
163 List.filter ok equalities
165 let rec simpl active target =
168 | (Negative, _)::tl -> simpl tl target
169 | (Positive, source)::tl ->
170 let newmeta, target = demodulation !maxmeta env target source in
172 if is_identity env target then target
175 let new_neg = List.map (simpl active) new_neg
176 and new_pos = List.map (simpl active) new_pos in
177 new_neg, remove_identities new_pos
181 let backward_simplify env (sign, current) active =
187 (fun (s, equality) ->
189 (* | Negative -> s, equality *)
191 let newmeta, equality =
192 demodulation !maxmeta env equality current in
198 List.filter (fun (s, eq) -> not (is_identity env eq)) active
201 List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
204 (fun (s, eq) res -> if find eq res then res else (s, eq)::res)
210 let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) =
211 let add_all = List.fold_left (fun res eq -> EqualitySet.add eq res) in
212 add_all passive_neg new_neg, add_all passive_pos new_pos
217 let rec given_clause env passive active =
219 (* | s1, s2 when (EqualitySet.is_empty s1) && (EqualitySet.is_empty s2) -> *)
223 (* Printf.printf "before select\n"; *)
224 let (sign, current), passive = select env passive in
225 (* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
226 (* (string_of_sign sign) (string_of_equality ~env current); *)
227 match forward_simplify env (sign, current) active with
228 | None when sign = Negative ->
229 Printf.printf "OK!!! %s %s" (string_of_sign sign)
230 (string_of_equality ~env current);
232 let proof, _, _, _ = current in
233 Success (Some proof, env)
235 Printf.printf "avanti... %s %s" (string_of_sign sign)
236 (string_of_equality ~env current);
238 given_clause env passive active
239 | Some (sign, current) ->
240 (* Printf.printf "sign: %s\ncurrent: %s\n" *)
241 (* (string_of_sign sign) (string_of_equality ~env current); *)
242 (* print_newline (); *)
244 let new' = infer env sign current active in
247 backward_simplify env (sign, current) active
248 (* match new' with *)
249 (* | [], [] -> backward_simplify env (sign, current) active *)
253 let new' = forward_simplify_new env new' active in
255 print_endline "\n================================================";
257 Printf.printf "active:\n%s\n"
260 (fun (s, e) -> (string_of_sign s) ^ " " ^
261 (string_of_equality ~env e)) active)));
265 (* match new' with *)
267 (* Printf.printf "new':\n%s\n" *)
268 (* (String.concat "\n" *)
270 (* (fun e -> "Negative " ^ *)
271 (* (string_of_equality ~env e)) neg) @ *)
273 (* (fun e -> "Positive " ^ *)
274 (* (string_of_equality ~env e)) pos))); *)
275 (* print_newline (); *)
277 match contains_empty env new' with
281 | Negative -> (sign, current)::active
282 | Positive -> active @ [(sign, current)]
284 let passive = add_to_passive passive new' in
285 given_clause env passive active
291 let get_from_user () =
292 let dbd = Mysql.quick_connect
293 ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
295 match read_line () with
299 let term_string = String.concat "\n" (get ()) in
300 let env, metasenv, term, ugraph =
301 List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
303 term, metasenv, ugraph
308 let module C = Cic in
309 let module T = CicTypeChecker in
310 let module PET = ProofEngineTypes in
311 let module PP = CicPp in
312 let term, metasenv, ugraph = get_from_user () in
313 let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
315 PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
316 let goal = List.nth goals 0 in
317 let _, metasenv, meta_proof, _ = proof in
318 let _, context, goal = CicUtil.lookup_meta goal metasenv in
319 let equalities, maxm = find_equalities context proof in
320 maxmeta := maxm; (* TODO ugly!! *)
321 let env = (metasenv, context, ugraph) in
323 let term_equality = equality_of_term meta_proof goal in
324 let meta_proof, (eq_ty, left, right), _, _ = term_equality in
327 (* (EqualitySet.singleton term_equality, *)
329 (* (fun res eq -> EqualitySet.add eq res) EqualitySet.empty equalities) *)
331 let passive = [term_equality], equalities in
332 Printf.printf "\ncurrent goal: %s ={%s} %s\n"
333 (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
334 Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
335 Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
336 Printf.printf "\nequalities:\n";
338 (function (_, (ty, t1, t2), _, _) ->
339 let w1 = weight_of_term t1 in
340 let w2 = weight_of_term t2 in
341 let res = nonrec_kbo t1 t2 in
342 Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
343 (PP.ppterm t1) (string_of_weight w1)
344 (string_of_comparison res)
345 (PP.ppterm t2) (string_of_weight w2))
347 print_endline "--------------------------------------------------";
348 let start = Sys.time () in
350 let res = given_clause env passive active in
351 let finish = Sys.time () in
354 Printf.printf "NO proof found! :-(\n\n"
355 | Success (Some proof, env) ->
356 Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof)
358 | Success (None, env) ->
359 Printf.printf "Success, but no proof?!?\n\n"
361 print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
366 let configuration_file = "../../gTopLevel/gTopLevel.conf.xml" in
367 Helm_registry.load_from configuration_file