From 758dbd74dccfb2491b59e4267600caf1d485e77a Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Fri, 5 Aug 2005 07:38:06 +0000 Subject: [PATCH] some bugs fixed --- helm/ocaml/paramodulation/inference.ml | 3 + helm/ocaml/paramodulation/saturate_main.ml | 3 +- helm/ocaml/paramodulation/saturation.ml | 314 +++++++++++---------- 3 files changed, 176 insertions(+), 144 deletions(-) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 746a2faea..09a023457 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1141,6 +1141,9 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = let rec aux newmeta = function | [] -> [], newmeta | (term, termty)::tl -> + debug_print ( + Printf.sprintf "Examining: %s (%s)" + (CicPp.ppterm term) (CicPp.ppterm termty)); let res, newmeta = match termty with | C.Prod (name, s, t) -> diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index 05d2cd047..6d3c9966c 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -1,6 +1,6 @@ let configuration_file = ref "../../matita/matita.conf.xml";; -let core_notation_script = "../../matita/core_notation.ma";; +let core_notation_script = "../../matita/core_notation.moo";; let get_from_user ~(dbd:Mysql.dbd) = let rec get () = @@ -45,6 +45,7 @@ let _ = in Helm_registry.load_from !configuration_file; CicNotation.load_notation core_notation_script; +CicNotation.load_notation "../../matita/coq.moo"; let dbd = Mysql.quick_connect ~host:(Helm_registry.get "db.host") ~user:(Helm_registry.get "db.user") diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 413c7b15e..5d5273d51 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -1005,9 +1005,9 @@ let main dbd term metasenv ugraph = 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 context (proof, goal') (maxm+1) *) -(* in *) + let library_equalities, maxm = + find_library_equalities ~dbd context (proof, goal') (maxm+2) + in maxmeta := maxm+2; (* TODO ugly!! *) let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let new_meta_goal, metasenv, type_of_goal = @@ -1023,84 +1023,97 @@ let main dbd term metasenv ugraph = 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 (* @ library_equalities *)) - in - Printf.printf "\ncurrent goal: %s\n" - (string_of_equality ~env term_equality); - Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); - Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); - Printf.printf "\nequalities:\n%s\n" - (String.concat "\n" - (List.map - (string_of_equality ~env) - equalities)); - print_endline "--------------------------------------------------"; - let start = Unix.gettimeofday () in - print_endline "GO!"; - start_time := Unix.gettimeofday (); - let res = - (if !use_fullred then given_clause_fullred else given_clause) - env passive active - in - let finish = Unix.gettimeofday () in - let _ = - match res with - | ParamodulationFailure -> - Printf.printf "NO proof found! :-(\n\n" - | ParamodulationSuccess (Some goal, env) -> - let proof = Inference.build_proof_term goal in - let newmetasenv = - List.fold_left - (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities - in - let _ = - try - let ty, ug = - CicTypeChecker.type_of_aux' newmetasenv context proof ugraph + if is_identity env term_equality then + let proof = + Cic.Appl [Cic.MutConstruct (* reflexivity *) + (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); + eq_ty; left] + in + let _ = + Printf.printf "OK, found a proof!\n"; + let names = names_of_context context in + print_endline (PP.pp proof names) + in + () + else + let active = make_active () 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); + Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); + Printf.printf "\nequalities:\n%s\n" + (String.concat "\n" + (List.map + (string_of_equality ~env) + equalities)); + print_endline "--------------------------------------------------"; + let start = Unix.gettimeofday () in + print_endline "GO!"; + start_time := Unix.gettimeofday (); + let res = + (if !use_fullred then given_clause_fullred else given_clause) + env passive active + in + let finish = Unix.gettimeofday () in + let _ = + match res with + | ParamodulationFailure -> + Printf.printf "NO proof found! :-(\n\n" + | ParamodulationSuccess (Some goal, env) -> + let proof = Inference.build_proof_term goal in + let newmetasenv = + List.fold_left + (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities 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))); - with e -> - Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e); - Printf.printf "MAXMETA USED: %d\n" !maxmeta; - in - () - - | ParamodulationSuccess (None, env) -> - Printf.printf "Success, but no proof?!?\n\n" - in - Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ - "forward_simpl_new_time: %.9f\n" ^^ - "backward_simpl_time: %.9f\n") - !infer_time !forward_simpl_time !forward_simpl_new_time - !backward_simpl_time; - Printf.printf "passive_maintainance_time: %.9f\n" - !passive_maintainance_time; - Printf.printf " successful unification/matching time: %.9f\n" - !Indexing.match_unif_time_ok; - Printf.printf " failed unification/matching time: %.9f\n" - !Indexing.match_unif_time_no; - Printf.printf " indexing retrieval time: %.9f\n" - !Indexing.indexing_retrieval_time; - Printf.printf " demodulate_term.build_newtarget_time: %.9f\n" - !Indexing.build_newtarget_time; - Printf.printf "derived %d clauses, kept %d clauses.\n" - !derived_clauses !kept_clauses; + let _ = + try + 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))); + with e -> + Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e); + Printf.printf "MAXMETA USED: %d\n" !maxmeta; + in + () + + | ParamodulationSuccess (None, env) -> + Printf.printf "Success, but no proof?!?\n\n" + in + Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ + "forward_simpl_new_time: %.9f\n" ^^ + "backward_simpl_time: %.9f\n") + !infer_time !forward_simpl_time !forward_simpl_new_time + !backward_simpl_time; + Printf.printf "passive_maintainance_time: %.9f\n" + !passive_maintainance_time; + Printf.printf " successful unification/matching time: %.9f\n" + !Indexing.match_unif_time_ok; + Printf.printf " failed unification/matching time: %.9f\n" + !Indexing.match_unif_time_no; + Printf.printf " indexing retrieval time: %.9f\n" + !Indexing.indexing_retrieval_time; + Printf.printf " demodulate_term.build_newtarget_time: %.9f\n" + !Indexing.build_newtarget_time; + Printf.printf "derived %d clauses, kept %d clauses.\n" + !derived_clauses !kept_clauses; with exc -> print_endline ("EXCEPTION: " ^ (Printexc.to_string exc)); raise exc @@ -1114,10 +1127,6 @@ let saturate dbd (proof, goal) = 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 @@ -1130,22 +1139,41 @@ let saturate dbd (proof, goal) = 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 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 term_equality = equality_of_term new_meta_goal goal in + let res = + if is_identity env term_equality then + let w, _, (eq_ty, left, right, o), m, a = term_equality in + let proof = + Cic.Appl [Cic.MutConstruct (* reflexivity *) + (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); + eq_ty; left] + in + ParamodulationSuccess + (Some (0, Inference.BasicProof proof, + (eq_ty, left, right, o), m, a), env) + else + let library_equalities, maxm = + find_library_equalities ~dbd context (proof, goal') (maxm+2) + in + maxmeta := maxm+2; + + let active = make_active () in + let passive = + make_passive [term_equality] (equalities @ library_equalities) + in + let res = given_clause_fullred env passive active in + res + 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 *) @@ -1155,49 +1183,49 @@ let saturate dbd (proof, 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 - 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 - 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") + 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 + 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 + 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") *) ;; -- 2.39.2