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 (sign, current) ?passive active =
251 | Some ((pn, _), (pp, _)) ->
252 (List.map (fun e -> Negative, e) pn),
253 (List.map (fun e -> Positive, e) pp)
255 let all = active @ pn @ pp in
256 let rec find_duplicate sign current = function
258 | (s, eq)::tl when s = sign ->
259 if meta_convertibility_eq current eq then true
260 else find_duplicate sign current tl
261 | _::tl -> find_duplicate sign current tl
263 (* let duplicate = find_duplicate sign current all in *)
264 (* if duplicate then *)
267 let rec aux env (sign, current) = function
268 | [] -> Some (sign, current)
269 | (Negative, _)::tl -> aux env (sign, current) tl
270 | (Positive, equality)::tl ->
271 let newmeta, newcurrent =
272 demodulation !maxmeta env current equality in
274 if is_identity env newcurrent then
275 if sign = Negative then
279 else if newcurrent <> current then
280 aux env (sign, newcurrent) active
282 aux env (sign, newcurrent) tl
284 let res = aux env (sign, current) all in
288 if find_duplicate s c all then
291 let pred (sign, eq) =
292 if sign <> s then false
293 else subsumption env c eq
295 if List.exists pred all then None
300 let forward_simplify_new env (new_neg, new_pos) ?passive active =
304 | Some ((pn, _), (pp, _)) ->
305 (List.map (fun e -> Negative, e) pn),
306 (List.map (fun e -> Positive, e) pp)
308 let all = active @ pn @ pp in
309 let remove_identities equalities =
310 let ok eq = not (is_identity env eq) in
311 List.filter ok equalities
313 let rec simpl all' target =
316 | (Negative, _)::tl -> simpl tl target
317 | (Positive, source)::tl ->
318 let newmeta, newtarget = demodulation !maxmeta env target source in
320 if is_identity env newtarget then newtarget
321 else if newtarget <> target then (
322 (* Printf.printf "OK:\n%s\n%s\n" *)
323 (* (string_of_equality ~env target) *)
324 (* (string_of_equality ~env newtarget); *)
325 (* print_newline (); *)
328 else simpl tl newtarget
330 let new_neg = List.map (simpl all) new_neg
331 and new_pos = remove_identities (List.map (simpl all) new_pos) in
333 List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos
335 let new_pos = EqualitySet.elements new_pos_set in
336 let f sign' target (sign, eq) =
337 (* Printf.printf "f %s <%s> (%s, <%s>)\n" *)
338 (* (string_of_sign sign') (string_of_equality ~env target) *)
339 (* (string_of_sign sign) (string_of_equality ~env eq); *)
340 if sign <> sign' then false
341 else subsumption env target eq
343 (* new_neg, new_pos *)
344 (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
345 List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
349 let backward_simplify_active env (new_neg, new_pos) active =
350 let new_pos = List.map (fun e -> Positive, e) new_pos in
353 (fun (s, equality) (res, newn) ->
354 match forward_simplify env (s, equality) new_pos with
355 | None when s = Negative ->
356 Printf.printf "\nECCO QUI: %s\n"
357 (string_of_equality ~env equality);
369 List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
373 if (is_identity env eq) || (find eq res) then res else (s, eq)::res
377 if (is_identity env eq) || (find eq res) then res else (s, eq)::res)
380 (fun (s, eq) (n, p) ->
381 if (s <> Negative) && (is_identity env eq) then
384 if s = Negative then eq::n, p
389 | [], [] -> active, None
390 | _ -> active, Some newa
394 let backward_simplify_passive env (new_neg, new_pos) passive =
395 let new_pos = List.map (fun e -> Positive, e) new_pos in
396 let (nl, ns), (pl, ps) = passive in
397 let f sign equality (resl, ress, newn) =
398 match forward_simplify env (sign, equality) new_pos with
399 | None -> resl, EqualitySet.remove equality ress, newn
402 equality::resl, ress, newn
404 let ress = EqualitySet.remove equality ress in
407 let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
408 and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
409 match newn, newp with
410 | [], [] -> ((nl, ns), (pl, ps)), None
411 | _, _ -> ((nl, ns), (pl, ps)), Some (newn, newp)
415 let backward_simplify env new' ?passive active =
416 let active, newa = backward_simplify_active env new' active in
419 active, (([], EqualitySet.empty), ([], EqualitySet.empty)), newa, None
422 backward_simplify_passive env new' passive in
423 active, passive, newa, newp
428 let rec given_clause env passive active =
429 match passive_is_empty passive with
432 (* Printf.printf "before select\n"; *)
433 let (sign, current), passive = select env passive active in
434 (* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
435 (* (string_of_sign sign) (string_of_equality ~env current); *)
436 match forward_simplify env (sign, current) ~passive active with
437 (* | None when sign = Negative -> *)
438 (* Printf.printf "OK!!! %s %s" (string_of_sign sign) *)
439 (* (string_of_equality ~env current); *)
440 (* print_newline (); *)
441 (* let proof, _, _, _ = current in *)
442 (* Success (Some proof, env) *)
444 (* Printf.printf "avanti... %s %s" (string_of_sign sign) *)
445 (* (string_of_equality ~env current); *)
446 (* print_newline (); *)
447 given_clause env passive active
448 | Some (sign, current) ->
449 if (sign = Negative) && (is_identity env current) then (
450 Printf.printf "OK!!! %s %s" (string_of_sign sign)
451 (string_of_equality ~env current);
453 let proof, _, _, _ = current in
454 Success (Some proof, env)
456 print_endline "\n================================================";
457 Printf.printf "selected: %s %s"
458 (string_of_sign sign) (string_of_equality ~env current);
461 let new' = infer env sign current active in
462 let res, proof = contains_empty env new' in
466 let new' = forward_simplify_new env new' active in
471 let active, _, newa, _ =
472 backward_simplify env ([], [current]) active
477 let nn = List.map (fun e -> Negative, e) n
478 and pp = List.map (fun e -> Positive, e) p in
482 Printf.printf "active:\n%s\n"
485 (fun (s, e) -> (string_of_sign s) ^ " " ^
486 (string_of_equality ~env e)) active)));
492 Printf.printf "new':\n%s\n"
495 (fun e -> "Negative " ^
496 (string_of_equality ~env e)) neg) @
498 (fun e -> "Positive " ^
499 (string_of_equality ~env e)) pos)));
502 match contains_empty env new' with
506 | Negative -> (sign, current)::active
507 | Positive -> active @ [(sign, current)]
509 let passive = add_to_passive passive new' in
510 let (_, ns), (_, ps) = passive in
511 Printf.printf "passive:\n%s\n"
513 ((List.map (fun e -> "Negative " ^
514 (string_of_equality ~env e))
515 (EqualitySet.elements ns)) @
516 (List.map (fun e -> "Positive " ^
517 (string_of_equality ~env e))
518 (EqualitySet.elements ps))));
520 given_clause env passive active
527 let rec given_clause_fullred env passive active =
528 match passive_is_empty passive with
531 (* Printf.printf "before select\n"; *)
532 let (sign, current), passive = select env passive active in
533 (* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
534 (* (string_of_sign sign) (string_of_equality ~env current); *)
535 match forward_simplify env (sign, current) ~passive active with
537 given_clause_fullred env passive active
538 | Some (sign, current) ->
539 if (sign = Negative) && (is_identity env current) then (
540 Printf.printf "OK!!! %s %s" (string_of_sign sign)
541 (string_of_equality ~env current);
543 let proof, _, _, _ = current in
544 Success (Some proof, env)
546 print_endline "\n================================================";
547 Printf.printf "selected: %s %s"
548 (string_of_sign sign) (string_of_equality ~env current);
551 let new' = infer env sign current active in
554 if is_identity env current then active
557 | Negative -> (sign, current)::active
558 | Positive -> active @ [(sign, current)]
561 (* match new' with *)
563 (* Printf.printf "new' before simpl:\n%s\n" *)
564 (* (String.concat "\n" *)
566 (* (fun e -> "Negative " ^ *)
567 (* (string_of_equality ~env e)) neg) @ *)
569 (* (fun e -> "Positive " ^ *)
570 (* (string_of_equality ~env e)) pos))); *)
571 (* print_newline (); *)
573 let rec simplify new' active passive =
574 let new' = forward_simplify_new env new' ~passive active in
575 let active, passive, newa, retained =
576 backward_simplify env new' ~passive active
578 match newa, retained with
579 | None, None -> active, passive, new'
581 | None, Some (n, p) ->
583 simplify (nn @ n, np @ p) active passive
584 | Some (n, p), Some (rn, rp) ->
586 simplify (nn @ n @ rn, np @ p @ rp) active passive
588 let active, passive, new' = simplify new' active passive in
590 Printf.printf "active:\n%s\n"
593 (fun (s, e) -> (string_of_sign s) ^ " " ^
594 (string_of_equality ~env e)) active)));
600 Printf.printf "new':\n%s\n"
603 (fun e -> "Negative " ^
604 (string_of_equality ~env e)) neg) @
606 (fun e -> "Positive " ^
607 (string_of_equality ~env e)) pos)));
610 match contains_empty env new' with
612 let passive = add_to_passive passive new' in
613 (* let (_, ns), (_, ps) = passive in *)
614 (* Printf.printf "passive:\n%s\n" *)
615 (* (String.concat "\n" *)
616 (* ((List.map (fun e -> "Negative " ^ *)
617 (* (string_of_equality ~env e)) *)
618 (* (EqualitySet.elements ns)) @ *)
619 (* (List.map (fun e -> "Positive " ^ *)
620 (* (string_of_equality ~env e)) *)
621 (* (EqualitySet.elements ps)))); *)
622 (* print_newline (); *)
623 given_clause_fullred env passive active
630 let get_from_user () =
631 let dbd = Mysql.quick_connect
632 ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
634 match read_line () with
638 let term_string = String.concat "\n" (get ()) in
639 let env, metasenv, term, ugraph =
640 List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
642 term, metasenv, ugraph
646 let given_clause_ref = ref given_clause;;
650 let module C = Cic in
651 let module T = CicTypeChecker in
652 let module PET = ProofEngineTypes in
653 let module PP = CicPp in
654 let term, metasenv, ugraph = get_from_user () in
655 let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
657 PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
658 let goal = List.nth goals 0 in
659 let _, metasenv, meta_proof, _ = proof in
660 let _, context, goal = CicUtil.lookup_meta goal metasenv in
661 let equalities, maxm = find_equalities context proof in
662 maxmeta := maxm; (* TODO ugly!! *)
663 let env = (metasenv, context, ugraph) in
665 let term_equality = equality_of_term meta_proof goal in
666 let meta_proof, (eq_ty, left, right), _, _ = term_equality in
668 let passive = make_passive [term_equality] equalities in
669 Printf.printf "\ncurrent goal: %s ={%s} %s\n"
670 (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
671 Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
672 Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
673 Printf.printf "\nequalities:\n";
675 (function (_, (ty, t1, t2), _, _) ->
676 let w1 = weight_of_term t1 in
677 let w2 = weight_of_term t2 in
678 let res = !compare_terms t1 t2 in
679 Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
680 (PP.ppterm t1) (string_of_weight w1)
681 (string_of_comparison res)
682 (PP.ppterm t2) (string_of_weight w2))
684 print_endline "--------------------------------------------------";
685 let start = Unix.gettimeofday () in
687 let res = !given_clause_ref env passive active in
688 let finish = Unix.gettimeofday () in
691 Printf.printf "NO proof found! :-(\n\n"
692 | Success (Some proof, env) ->
693 Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof)
695 | Success (None, env) ->
696 Printf.printf "Success, but no proof?!?\n\n"
698 print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
702 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
705 let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
706 and set_sel v = symbols_ratio := v; symbols_counter := v;
707 and set_conf f = configuration_file := f
708 and set_lpo () = Utils.compare_terms := lpo
709 and set_kbo () = Utils.compare_terms := nonrec_kbo
710 and set_fullred () = given_clause_ref := given_clause_fullred
713 "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
715 "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
717 "-s", Arg.Int set_sel,
718 "symbols-based selection ratio (relative to the weight ratio)";
720 "-c", Arg.String set_conf, "Configuration file (for the db connection)";
722 "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
724 "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
725 ] (fun a -> ()) "Usage:"
727 Helm_registry.load_from !configuration_file;