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"
19 let symbols_of_equality (_, (_, left, right), _, _) =
20 TermSet.union (symbols_of_term left) (symbols_of_term right)
24 let symbols_of_equality ((_, (_, left, right), _, _) as equality) =
25 let m1 = symbols_of_term left in
30 let c = TermMap.find k res in
31 TermMap.add k (c+v) res
34 (symbols_of_term right) m1
36 (* Printf.printf "symbols_of_equality %s:\n" *)
37 (* (string_of_equality equality); *)
38 (* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
39 (* print_newline (); *)
44 module OrderedEquality =
46 type t = Inference.equality
49 match meta_convertibility_eq eq1 eq2 with
52 let _, (ty, left, right), _, _ = eq1
53 and _, (ty', left', right'), _, _ = eq2 in
54 let weight_of t = fst (weight_of_term ~consider_metas:false t) in
55 let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
56 and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
57 match Pervasives.compare w1 w2 with
58 | 0 -> Pervasives.compare eq1 eq2
62 module EqualitySet = Set.Make(OrderedEquality);;
65 let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
66 let weight_age_counter = ref !weight_age_ratio;;
68 let symbols_ratio = ref 0;;
69 let symbols_counter = ref 0;;
72 let select env passive active =
73 let (neg_list, neg_set), (pos_list, pos_set) = passive in
75 List.filter (fun e -> not (e = eq)) l
77 if !weight_age_ratio > 0 then
78 weight_age_counter := !weight_age_counter - 1;
79 match !weight_age_counter with
81 weight_age_counter := !weight_age_ratio;
82 match neg_list, pos_list with
84 (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set))
86 (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set))
87 | _, _ -> assert false
89 | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
90 symbols_counter := !symbols_counter - 1;
92 TermMap.fold (fun k v res -> res + v) map 0
96 let symbols = symbols_of_equality e in
97 let card = cardinality symbols in
98 let f equality (i, e) =
102 if TermMap.mem k symbols then
103 let c = TermMap.find k symbols in
104 let c1 = abs (c - v) in
109 (symbols_of_equality equality) (0, 0)
111 (* Printf.printf "equality: %s, common: %d, others: %d\n" *)
112 (* (string_of_equality ~env equality) common others; *)
113 let c = others + (abs (common - card)) in
114 if c < i then (c, equality)
117 let e1 = EqualitySet.min_elt pos_set in
122 if TermMap.mem k symbols then
123 let c = TermMap.find k symbols in
124 let c1 = abs (c - v) in
125 let c2 = v - (abs (c - v)) in
129 (symbols_of_equality e1) (0, 0)
131 (others + (abs (common - card))), e1
133 let _, current = EqualitySet.fold f pos_set initial in
134 Printf.printf "\nsymbols-based selection: %s\n\n"
135 (string_of_equality ~env current);
138 (remove current pos_list, EqualitySet.remove current pos_set))
140 let current = EqualitySet.min_elt pos_set in
143 (remove current pos_list, EqualitySet.remove current pos_set)
145 (Positive, current), passive
148 symbols_counter := !symbols_ratio;
149 let set_selection set = EqualitySet.min_elt set in
150 if EqualitySet.is_empty neg_set then
151 let current = set_selection pos_set in
154 (remove current pos_list, EqualitySet.remove current pos_set)
156 (Positive, current), passive
158 let current = set_selection neg_set in
160 (remove current neg_list, EqualitySet.remove current neg_set),
163 (Negative, current), passive
167 let make_passive neg pos =
168 let set_of equalities =
169 List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
171 (neg, set_of neg), (pos, set_of pos)
175 let add_to_passive passive (new_neg, new_pos) =
176 let (neg_list, neg_set), (pos_list, pos_set) = passive in
177 let ok set equality = not (EqualitySet.mem equality set) in
178 let neg = List.filter (ok neg_set) new_neg
179 and pos = List.filter (ok pos_set) new_pos in
180 let add set equalities =
181 List.fold_left (fun s e -> EqualitySet.add e s) set equalities
183 (neg @ neg_list, add neg_set neg), (pos_list @ pos, add pos_set pos)
187 let passive_is_empty = function
188 | ([], _), ([], _) -> true
193 (* TODO: find a better way! *)
194 let maxmeta = ref 0;;
196 let infer env sign current active =
197 let rec infer_negative current = function
199 | (Negative, _)::tl -> infer_negative current tl
200 | (Positive, equality)::tl ->
201 let res = superposition_left env current equality in
202 let neg, pos = infer_negative current tl in
205 and infer_positive current = function
207 | (Negative, equality)::tl ->
208 let res = superposition_left env equality current in
209 let neg, pos = infer_positive current tl in
211 | (Positive, equality)::tl ->
212 let maxm, res = superposition_right !maxmeta env current equality in
213 let maxm, res' = superposition_right maxm env equality current in
215 let neg, pos = infer_positive current tl in
217 (* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
218 (* (string_of_equality ~env current) (string_of_equality ~env equality) *)
219 (* (String.concat "\n" (List.map (string_of_equality ~env) res)); *)
220 (* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
221 (* (string_of_equality ~env equality) (string_of_equality ~env current) *)
222 (* (String.concat "\n" (List.map (string_of_equality ~env) res')); *)
224 neg, res @ res' @ pos
227 | Negative -> infer_negative current active
228 | Positive -> infer_positive current active
232 let contains_empty env (negative, positive) =
233 let metasenv, context, ugraph = env in
235 let (proof, _, _, _) =
237 (fun (proof, (ty, left, right), m, a) ->
238 fst (CicReduction.are_convertible context left right ugraph))
247 let forward_simplify env ?(active=[]) ?passive (sign, current) =
248 (* first step, remove already present equalities *)
252 | Some ((pn, _), (pp, _)) ->
253 (List.map (fun e -> Negative, e) pn),
254 (List.map (fun e -> Positive, e) pp)
256 let all = active @ pn @ pp in
258 let rec aux = function
260 | (s, eq)::tl when s = sign ->
261 if meta_convertibility_eq current eq then true
270 let rec aux env (sign, current) = function
271 | [] -> Some (sign, current)
272 | (Negative, _)::tl -> aux env (sign, current) tl
273 | (Positive, equality)::tl ->
274 let newmeta, newcurrent =
275 demodulation !maxmeta env current equality in
277 if is_identity env newcurrent then
279 else if newcurrent <> current then
280 aux env (sign, newcurrent) active
282 aux env (sign, newcurrent) tl
284 aux env (sign, current) all
288 let forward_simplify_new env ?(active=[]) ?passive (new_neg, new_pos) =
292 | Some ((pn, _), (pp, _)) ->
293 (List.map (fun e -> Negative, e) pn),
294 (List.map (fun e -> Positive, e) pp)
296 let all = active @ pn @ pp in
297 let remove_identities equalities =
298 let ok eq = not (is_identity env eq) in
299 List.filter ok equalities
301 let rec simpl all' target =
304 | (Negative, _)::tl -> simpl tl target
305 | (Positive, source)::tl ->
306 let newmeta, newtarget = demodulation !maxmeta env target source in
308 if is_identity env newtarget then newtarget
309 else if newtarget <> target then (
310 (* Printf.printf "OK:\n%s\n%s\n" *)
311 (* (string_of_equality ~env target) *)
312 (* (string_of_equality ~env newtarget); *)
313 (* print_newline (); *)
316 else simpl tl newtarget
318 let new_neg = List.map (simpl all) new_neg
319 and new_pos = remove_identities (List.map (simpl all) new_pos) in
321 List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos
323 new_neg, EqualitySet.elements new_pos_set
328 let backward_simplify_active env (sign, current) active =
334 (fun (s, equality) ->
336 (* | Negative -> s, equality *)
338 let newmeta, equality =
339 demodulation !maxmeta env equality current in
345 List.filter (fun (s, eq) -> not (is_identity env eq)) active
348 List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
351 (fun (s, eq) res -> if find eq res then res else (s, eq)::res)
357 let backward_simplify_active env (new_neg, new_pos) active =
358 let new_pos = List.map (fun e -> Positive, e) new_pos in
361 (fun (s, equality) res ->
362 match forward_simplify env ~active:new_pos (s, equality) with
368 List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
372 if (is_identity env eq) || (find eq res) then
380 let backward_simplify_passive env (new_neg, new_pos) passive =
381 let new_pos = List.map (fun e -> Positive, e) new_pos in
382 let (nl, ns), (pl, ps) = passive in
383 let f sign equality (resl, ress, newn) =
384 match forward_simplify env ~active:new_pos (sign, equality) with
385 | None -> resl, EqualitySet.remove equality ress, newn
388 equality::resl, ress, newn
390 let ress = EqualitySet.remove equality ress in
393 let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
394 and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
395 match newn, newp with
396 | [], [] -> ((nl, ns), (pl, ps)), None
397 | _, _ -> ((nl, ns), (pl, ps)), Some (newn, newp)
401 let backward_simplify env ?(active=[]) ?passive new' =
402 let active = backward_simplify_active env new' active in
405 active, (([], EqualitySet.empty), ([], EqualitySet.empty)), None
408 backward_simplify_passive env new' passive in
409 active, passive, new'
414 let rec given_clause env passive active =
415 match passive_is_empty passive with
418 (* Printf.printf "before select\n"; *)
419 let (sign, current), passive = select env passive active in
420 (* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
421 (* (string_of_sign sign) (string_of_equality ~env current); *)
422 match forward_simplify env (sign, current) ~active ~passive with
423 | None when sign = Negative ->
424 Printf.printf "OK!!! %s %s" (string_of_sign sign)
425 (string_of_equality ~env current);
427 let proof, _, _, _ = current in
428 Success (Some proof, env)
430 (* Printf.printf "avanti... %s %s" (string_of_sign sign) *)
431 (* (string_of_equality ~env current); *)
432 (* print_newline (); *)
433 given_clause env passive active
434 | Some (sign, current) ->
435 print_endline "\n================================================";
436 Printf.printf "selected: %s %s"
437 (string_of_sign sign) (string_of_equality ~env current);
440 let new' = infer env sign current active in
442 let res, proof = contains_empty env new' in
446 let new' = forward_simplify_new env new' ~active in
448 (* let active, passive, retained = *)
449 (* backward_simplify env [(sign, current)] ~active ~passive *)
456 backward_simplify env ([], [current]) ~active
461 Printf.printf "active:\n%s\n"
464 (fun (s, e) -> (string_of_sign s) ^ " " ^
465 (string_of_equality ~env e)) active)));
471 Printf.printf "new':\n%s\n"
474 (fun e -> "Negative " ^
475 (string_of_equality ~env e)) neg) @
477 (fun e -> "Positive " ^
478 (string_of_equality ~env e)) pos)));
481 match contains_empty env new' with
485 | Negative -> (sign, current)::active
486 | Positive -> active @ [(sign, current)]
488 let passive = add_to_passive passive new' in
489 let (_, ns), (_, ps) = passive in
490 Printf.printf "passive:\n%s\n"
492 ((List.map (fun e -> "Negative " ^
493 (string_of_equality ~env e))
494 (EqualitySet.elements ns)) @
495 (List.map (fun e -> "Positive " ^
496 (string_of_equality ~env e))
497 (EqualitySet.elements ps))));
499 given_clause env passive active
506 let rec given_clause env passive active =
507 match passive_is_empty passive with
510 (* Printf.printf "before select\n"; *)
511 let (sign, current), passive = select env passive active in
512 (* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
513 (* (string_of_sign sign) (string_of_equality ~env current); *)
514 print_endline "\n================================================";
515 Printf.printf "selected: %s %s"
516 (string_of_sign sign) (string_of_equality ~env current);
519 let new' = infer env sign current active in
521 let rec simplify new' active passive =
522 let new' = forward_simplify_new env new' ~active ~passive in
523 let active, passive, retained =
524 backward_simplify env new' ~active ~passive
527 | None -> active, passive, new'
530 simplify (nn @ rn, np @ rp) active passive
532 let active, passive, new' = simplify new' active passive in
534 Printf.printf "active:\n%s\n"
537 (fun (s, e) -> (string_of_sign s) ^ " " ^
538 (string_of_equality ~env e)) active)));
544 Printf.printf "new':\n%s\n"
547 (fun e -> "Negative " ^
548 (string_of_equality ~env e)) neg) @
550 (fun e -> "Positive " ^
551 (string_of_equality ~env e)) pos)));
554 match contains_empty env new' with
558 | Negative -> (sign, current)::active
559 | Positive -> active @ [(sign, current)]
561 let passive = add_to_passive passive new' in
562 let (_, ns), (_, ps) = passive in
563 Printf.printf "passive:\n%s\n"
565 ((List.map (fun e -> "Negative " ^
566 (string_of_equality ~env e))
567 (EqualitySet.elements ns)) @
568 (List.map (fun e -> "Positive " ^
569 (string_of_equality ~env e))
570 (EqualitySet.elements ps))));
572 given_clause env passive active
579 let get_from_user () =
580 let dbd = Mysql.quick_connect
581 ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
583 match read_line () with
587 let term_string = String.concat "\n" (get ()) in
588 let env, metasenv, term, ugraph =
589 List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
591 term, metasenv, ugraph
596 let module C = Cic in
597 let module T = CicTypeChecker in
598 let module PET = ProofEngineTypes in
599 let module PP = CicPp in
600 let term, metasenv, ugraph = get_from_user () in
601 let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
603 PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
604 let goal = List.nth goals 0 in
605 let _, metasenv, meta_proof, _ = proof in
606 let _, context, goal = CicUtil.lookup_meta goal metasenv in
607 let equalities, maxm = find_equalities context proof in
608 maxmeta := maxm; (* TODO ugly!! *)
609 let env = (metasenv, context, ugraph) in
611 let term_equality = equality_of_term meta_proof goal in
612 let meta_proof, (eq_ty, left, right), _, _ = term_equality in
614 let passive = make_passive [term_equality] equalities in
615 Printf.printf "\ncurrent goal: %s ={%s} %s\n"
616 (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
617 Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
618 Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
619 Printf.printf "\nequalities:\n";
621 (function (_, (ty, t1, t2), _, _) ->
622 let w1 = weight_of_term t1 in
623 let w2 = weight_of_term t2 in
624 let res = !compare_terms t1 t2 in
625 Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
626 (PP.ppterm t1) (string_of_weight w1)
627 (string_of_comparison res)
628 (PP.ppterm t2) (string_of_weight w2))
630 print_endline "--------------------------------------------------";
631 let start = Unix.gettimeofday () in
633 let res = given_clause env passive active in
634 let finish = Unix.gettimeofday () in
637 Printf.printf "NO proof found! :-(\n\n"
638 | Success (Some proof, env) ->
639 Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof)
641 | Success (None, env) ->
642 Printf.printf "Success, but no proof?!?\n\n"
644 print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
648 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
651 let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
652 and set_sel v = symbols_ratio := v; symbols_counter := v;
653 and set_conf f = configuration_file := f
654 and set_lpo () = Utils.compare_terms := lpo
655 and set_kbo () = Utils.compare_terms := nonrec_kbo
658 "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
660 "-s", Arg.Int set_sel,
661 "symbols-based selection ratio (relative to the weight ratio)";
663 "-c", Arg.String set_conf, "Configuration file (for the db connection)";
665 "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
667 "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
668 ] (fun a -> ()) "Usage:"
670 Helm_registry.load_from !configuration_file;