X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=413c7b15ea7bd760ed301b64f46d025336c3a646;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=94f26a7e68c5c58c59d9fdf5ecbc906edf2ca5eb;hpb=b24260fd5c00791ad04042405e3942f288f54ab2;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 94f26a7e6..413c7b15e 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -2,6 +2,10 @@ open Inference;; open Utils;; +(* set to false to disable paramodulation inside auto_tac *) +let connect_to_auto = true;; + + (* profiling statistics... *) let infer_time = ref 0.;; let forward_simpl_time = ref 0.;; @@ -33,8 +37,8 @@ let maxmeta = ref 0;; type result = - | Failure - | Success of Inference.equality option * environment + | ParamodulationFailure + | ParamodulationSuccess of Inference.equality option * environment ;; @@ -83,7 +87,7 @@ module OrderedEquality = struct try let res = Pervasives.compare (List.hd a) (List.hd a') in if res <> 0 then res else Pervasives.compare eq1 eq2 - with _ -> Pervasives.compare eq1 eq2 + with Failure "hd" -> Pervasives.compare eq1 eq2 (* match a, a' with *) (* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *) (* let res = Pervasives.compare i j in *) @@ -277,7 +281,7 @@ let prune_passive howmany (active, _) passive = and ratio = float_of_int !weight_age_ratio in let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.)) and in_age = int_of_float (howmany /. (ratio +. 1.)) in - Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age; + debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age); let symbols, card = match active with | (Negative, e)::_ -> @@ -732,12 +736,13 @@ let rec given_clause env passive active = if !time_limit = 0. || !processed_clauses = 0 then passive else if !elapsed_time > !time_limit then ( - Printf.printf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time; + debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" + !time_limit !elapsed_time); make_passive [] [] ) else if kept > selection_estimate then ( - Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^ - "selection_estimate: %d)\n") kept selection_estimate; + debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^ + "(kept: %d, selection_estimate: %d)\n") + kept selection_estimate); prune_passive selection_estimate active passive ) else passive @@ -749,7 +754,7 @@ let rec given_clause env passive active = kept_clauses := (size_of_passive passive) + (size_of_active active); match passive_is_empty passive with - | true -> Failure + | true -> ParamodulationFailure | false -> let (sign, current), passive = select env passive active in let time1 = Unix.gettimeofday () in @@ -761,15 +766,14 @@ let rec given_clause env passive active = given_clause env passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( - Printf.printf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); - Success (Some current, env) + debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current)); + ParamodulationSuccess (Some current, env) ) else ( - print_endline "\n================================================"; - Printf.printf "selected: %s %s" - (string_of_sign sign) (string_of_equality ~env current); - print_newline (); + debug_print "\n================================================"; + debug_print (Printf.sprintf "selected: %s %s" + (string_of_sign sign) + (string_of_equality ~env current)); let t1 = Unix.gettimeofday () in let new' = infer env sign current active in @@ -778,7 +782,7 @@ let rec given_clause env passive active = let res, goal = contains_empty env new' in if res then - Success (goal, env) + ParamodulationSuccess (goal, env) else let t1 = Unix.gettimeofday () in let new' = forward_simplify_new env new' (* ~passive *) active in @@ -853,7 +857,7 @@ let rec given_clause env passive active = (* print_newline (); *) given_clause env passive active | true, goal -> - Success (goal, env) + ParamodulationSuccess (goal, env) ) ;; @@ -867,12 +871,13 @@ let rec given_clause_fullred env passive active = if !time_limit = 0. || !processed_clauses = 0 then passive else if !elapsed_time > !time_limit then ( - Printf.printf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time; + debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" + !time_limit !elapsed_time); make_passive [] [] ) else if kept > selection_estimate then ( - Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^ - "selection_estimate: %d)\n") kept selection_estimate; + debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^ + "(kept: %d, selection_estimate: %d)\n") + kept selection_estimate); prune_passive selection_estimate active passive ) else passive @@ -884,7 +889,7 @@ let rec given_clause_fullred env passive active = kept_clauses := (size_of_passive passive) + (size_of_active active); match passive_is_empty passive with - | true -> Failure + | true -> ParamodulationFailure | false -> let (sign, current), passive = select env passive active in let time1 = Unix.gettimeofday () in @@ -896,15 +901,14 @@ let rec given_clause_fullred env passive active = given_clause_fullred env passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( - Printf.printf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); - Success (Some current, env) + debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current)); + ParamodulationSuccess (Some current, env) ) else ( - print_endline "\n================================================"; - Printf.printf "selected: %s %s" - (string_of_sign sign) (string_of_equality ~env current); - print_newline (); + debug_print "\n================================================"; + debug_print (Printf.sprintf "selected: %s %s" + (string_of_sign sign) + (string_of_equality ~env current)); let t1 = Unix.gettimeofday () in let new' = infer env sign current active in @@ -945,31 +949,31 @@ let rec given_clause_fullred env passive active = if k < (kept - 1) then processed_clauses := !processed_clauses + (kept - 1 - k); -(* let _ = *) -(* Printf.printf "active:\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map *) -(* (fun (s, e) -> (string_of_sign s) ^ " " ^ *) -(* (string_of_equality ~env e)) (fst active)))); *) -(* print_newline (); *) -(* in *) -(* let _ = *) -(* match new' with *) -(* | neg, pos -> *) -(* Printf.printf "new':\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map *) -(* (fun e -> "Negative " ^ *) -(* (string_of_equality ~env e)) neg) @ *) -(* (List.map *) -(* (fun e -> "Positive " ^ *) -(* (string_of_equality ~env e)) pos))); *) -(* print_newline (); *) -(* in *) + let _ = + debug_print ( + Printf.sprintf "active:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) (fst active))))) + in + let _ = + match new' with + | neg, pos -> + debug_print ( + Printf.sprintf "new':\n%s\n" + (String.concat "\n" + ((List.map + (fun e -> "Negative " ^ + (string_of_equality ~env e)) neg) @ + (List.map + (fun e -> "Positive " ^ + (string_of_equality ~env e)) pos)))) + in match contains_empty env new' with | false, _ -> let passive = add_to_passive passive new' in - let (_, ns), (_, ps), _ = passive in +(* let (_, ns), (_, ps), _ = passive in *) (* Printf.printf "passive:\n%s\n" *) (* (String.concat "\n" *) (* ((List.map (fun e -> "Negative " ^ *) @@ -981,36 +985,19 @@ let rec given_clause_fullred env passive active = (* print_newline (); *) given_clause_fullred env passive active | true, goal -> - Success (goal, env) + ParamodulationSuccess (goal, env) ) ;; -let get_from_user ~(dbd:Mysql.dbd) = - let rec get () = - match read_line () with - | "" -> [] - | t -> t::(get ()) - in - let term_string = String.concat "\n" (get ()) in - let env, metasenv, term, ugraph = - List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0 - in - term, metasenv, ugraph -;; - - let given_clause_ref = ref given_clause;; -let main () = +let main dbd term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in let module PET = ProofEngineTypes in let module PP = CicPp in - let dbd = Mysql.quick_connect - ~host:"localhost" ~user:"helm" ~database:"mowgli" () in - let term, metasenv, ugraph = get_from_user ~dbd in let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in let proof, goals = status in @@ -1018,8 +1005,9 @@ let main () = let _, metasenv, meta_proof, _ = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in let equalities, maxm = find_equalities context proof in - let library_equalities, maxm = - find_library_equalities ~dbd (proof, goal') (maxm+1) in +(* let library_equalities, maxm = *) +(* find_library_equalities ~dbd context (proof, goal') (maxm+1) *) +(* in *) maxmeta := maxm+2; (* TODO ugly!! *) let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let new_meta_goal, metasenv, type_of_goal = @@ -1036,7 +1024,9 @@ let main () = let term_equality = equality_of_term new_meta_goal goal in let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in let active = make_active () in - let passive = make_passive [term_equality] equalities in + let passive = + make_passive [term_equality] (equalities (* @ library_equalities *)) + in Printf.printf "\ncurrent goal: %s\n" (string_of_equality ~env term_equality); Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); @@ -1057,19 +1047,10 @@ let main () = let finish = Unix.gettimeofday () in let _ = match res with - | Failure -> + | ParamodulationFailure -> Printf.printf "NO proof found! :-(\n\n" - | Success (Some goal, env) -> - Printf.printf "OK, found a proof!\n"; + | ParamodulationSuccess (Some goal, env) -> let proof = Inference.build_proof_term goal in - (* REMEMBER: we have to instantiate meta_proof, we should use - apply the "apply" tactic to proof and status - *) - let names = names_of_context context in - print_endline (PP.pp proof names); -(* print_endline (PP.ppterm proof); *) - - print_endline (string_of_float (finish -. start)); let newmetasenv = List.fold_left (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities @@ -1079,17 +1060,28 @@ let main () = let ty, ug = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in + Printf.printf "OK, found a proof!\n"; + (* REMEMBER: we have to instantiate meta_proof, we should use + apply the "apply" tactic to proof and status + *) + let names = names_of_context context in + print_endline (PP.pp proof names); + (* print_endline (PP.ppterm proof); *) + + print_endline (string_of_float (finish -. start)); Printf.printf "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" (CicPp.pp type_of_goal names) (CicPp.pp ty names) (string_of_bool - (fst (CicReduction.are_convertible context type_of_goal ty ug))); + (fst (CicReduction.are_convertible + context type_of_goal ty ug))); with e -> + Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e); Printf.printf "MAXMETA USED: %d\n" !maxmeta; in () - | Success (None, env) -> + | ParamodulationSuccess (None, env) -> Printf.printf "Success, but no proof?!?\n\n" in Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ @@ -1115,109 +1107,108 @@ let main () = ;; -let saturation_tactic status = +let saturate dbd (proof, goal) = let module C = Cic in - let saturation_tac (proof, goal) = - maxmeta := 0; -(* if List.length goals <> 1 then *) -(* raise (ProofEngineTypes.Fail "There should be only one open goal"); *) - -(* let goal' = List.hd goals in *) - let goal' = goal in - let uri, metasenv, meta_proof, term_to_prove = proof in - let _, context, goal = CicUtil.lookup_meta goal' metasenv in - let equalities, maxm = find_equalities context proof in - maxmeta := maxm+2; - let new_meta_goal, metasenv, type_of_goal = - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in - let _, context, ty = CicUtil.lookup_meta goal' metasenv in - Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty); - print_newline (); - Cic.Meta (maxm+1, irl), - (maxm+1, context, ty)::metasenv, - ty + maxmeta := 0; + let goal' = goal in + let uri, metasenv, meta_proof, term_to_prove = proof in + let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let equalities, maxm = find_equalities context proof in + let library_equalities, maxm = + find_library_equalities ~dbd context (proof, goal') (maxm+2) + in + maxmeta := maxm+2; + let new_meta_goal, metasenv, type_of_goal = + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let _, context, ty = CicUtil.lookup_meta goal' metasenv in + debug_print (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)); + Cic.Meta (maxm+1, irl), + (maxm+1, context, ty)::metasenv, + ty + in + let ugraph = CicUniv.empty_ugraph in + let env = (metasenv, context, ugraph) in +(* try *) + let term_equality = equality_of_term new_meta_goal goal in + let active = make_active () in + let passive = + make_passive [term_equality] (equalities @ library_equalities) in - let ugraph = CicUniv.empty_ugraph in - let env = (metasenv, context, ugraph) in - try - let term_equality = equality_of_term new_meta_goal goal in -(* let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *) - let active = make_active () in - let passive = make_passive [term_equality] equalities in - let res = given_clause_fullred env passive active in - match res with - | Success (Some goal, env) -> - Printf.printf "OK, found a proof!\n"; - let proof = Inference.build_proof_term goal in - let names = names_of_context context in - print_endline (CicPp.pp proof names); - let newmetasenv = - let i1 = - match new_meta_goal with - | C.Meta (i, _) -> i | _ -> assert false + let res = given_clause_fullred env passive active in + match res with + | ParamodulationSuccess (Some goal, env) -> + debug_print "OK, found a proof!"; + let proof = Inference.build_proof_term goal in + let names = names_of_context context in + let newmetasenv = + let i1 = + match new_meta_goal with + | C.Meta (i, _) -> i | _ -> assert false + in +(* let i2 = *) +(* match meta_proof with *) +(* | C.Meta (i, _) -> i *) +(* | t -> *) +(* Printf.printf "\nHMMM!!! meta_proof: %s\ngoal': %s" *) +(* (CicPp.pp meta_proof names) (string_of_int goal'); *) +(* print_newline (); *) +(* assert false *) +(* in *) + List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv + in + let newstatus = + try + let ty, ug = + CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in - let i2 = - match meta_proof with - | C.Meta (i, _) -> i | _ -> assert false + debug_print (CicPp.pp proof [](* names *)); + debug_print + (Printf.sprintf + "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n" + (CicPp.pp type_of_goal names) (CicPp.pp ty names) + (string_of_bool + (fst (CicReduction.are_convertible + context type_of_goal ty ug)))); + let equality_for_replace i t1 = + match t1 with + | C.Meta (n, _) -> n = i + | _ -> false in - List.filter (fun (i, _, _) -> i <> i1 && i <> i2) metasenv - in - let newstatus = - try - let ty, ug = - CicTypeChecker.type_of_aux' newmetasenv context proof ugraph - in - Printf.printf - "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" - (CicPp.pp type_of_goal names) (CicPp.pp ty names) - (string_of_bool - (fst (CicReduction.are_convertible - context type_of_goal ty ug))); - ((uri, newmetasenv, proof, term_to_prove), []) - with e -> - raise (ProofEngineTypes.Fail - "Found a proof, but it doesn't typecheck") - in - newstatus - | _ -> - raise (ProofEngineTypes.Fail "NO proof found") - with e -> - raise (ProofEngineTypes.Fail "saturation failed") - in - ProofEngineTypes.mk_tactic saturation_tac + let real_proof = + ProofEngineReduction.replace + ~equality:equality_for_replace + ~what:[goal'] ~with_what:[proof] + ~where:meta_proof + in + debug_print ( + Printf.sprintf "status:\n%s\n%s\n%s\n%s\n" + (match uri with Some uri -> UriManager.string_of_uri uri + | None -> "") + (print_metasenv newmetasenv) + (CicPp.pp real_proof [](* names *)) + (CicPp.pp term_to_prove names)); + ((uri, newmetasenv, real_proof, term_to_prove), []) + with CicTypeChecker.TypeCheckerFailure _ -> + debug_print "THE PROOF DOESN'T TYPECHECK!!!"; + debug_print (CicPp.pp proof names); + raise + (ProofEngineTypes.Fail "Found a proof, but it doesn't typecheck") + in + newstatus + | _ -> + raise (ProofEngineTypes.Fail "NO proof found") +(* with e -> *) +(* raise (Failure "saturation failed") *) ;; +(* dummy function called within matita to trigger linkage *) +let init () = ();; -let configuration_file = ref "../../matita/matita.conf.xml";; - -let _ = - let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1) - and set_sel v = symbols_ratio := v; symbols_counter := v; - and set_conf f = configuration_file := f - and set_lpo () = Utils.compare_terms := lpo - and set_kbo () = Utils.compare_terms := nonrec_kbo - and set_fullred b = use_fullred := b - and set_time_limit v = time_limit := float_of_int v - in - Arg.parse [ - "-f", Arg.Bool set_fullred, - "Enable/disable full-reduction strategy (default: enabled)"; - - "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 3)"; - - "-s", Arg.Int set_sel, - "symbols-based selection ratio (relative to the weight ratio, default: 2)"; - - "-c", Arg.String set_conf, "Configuration file (for the db connection)"; - - "-lpo", Arg.Unit set_lpo, "Use lpo term ordering"; - - "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)"; - "-l", Arg.Int set_time_limit, "Time limit (in seconds)"; - ] (fun a -> ()) "Usage:" -in -Helm_registry.load_from !configuration_file; -main () +(* UGLY SIDE EFFECT... *) +if connect_to_auto then ( + AutoTactic.paramodulation_tactic := saturate; + AutoTactic.term_is_equality := Inference.term_is_equality; +);;