From c3af85c9492385a7a0de0f5aa57df241ee0bd553 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Mon, 26 Sep 2005 15:11:43 +0000 Subject: [PATCH] new paramodulation --- helm/ocaml/paramodulation/Makefile | 9 +- helm/ocaml/paramodulation/indexing.ml | 172 ++- helm/ocaml/paramodulation/inference.ml | 241 ++-- helm/ocaml/paramodulation/inference.mli | 19 +- helm/ocaml/paramodulation/saturate_main.ml | 14 +- helm/ocaml/paramodulation/saturation.ml | 1330 +++++++++++++++----- helm/ocaml/paramodulation/utils.ml | 7 +- 7 files changed, 1300 insertions(+), 492 deletions(-) diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index 88d313d3c..94c4c28df 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -1,6 +1,11 @@ PACKAGE = paramodulation -REQUIRES = helm-tactics helm-cic_disambiguation +REQUIRES = \ + helm-registry \ + helm-cic_transformations \ + helm-tactics \ + helm-cic_disambiguation \ + mysql INTERFACE_FILES = \ utils.mli \ @@ -17,7 +22,7 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \ # test_indexing.ml -include ../Makefile.common +include ../helm/ocaml/Makefile.common paramodulation.cmo: $(IMPLEMENTATION_FILES:%.ml=%.cmo) diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index ed22ef472..e30d44034 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -90,12 +90,10 @@ let indexing_retrieval_time = ref 0.;; let apply_subst = CicMetaSubst.apply_subst -(* Profiling code -let apply_subst = - let profile = CicUtil.profile "apply_subst" in - (fun s a -> profile.profile (apply_subst s) a) -;; -*) +(* let apply_subst = *) +(* let profile = CicUtil.profile "apply_subst" in *) +(* (fun s a -> profile (apply_subst s) a) *) +(* ;; *) (* @@ -249,6 +247,15 @@ let rec find_matches metasenv context ugraph lift_amount term termty = and other' = (* M. *)apply_subst s other in let order = cmp c' other' in let names = U.names_of_context context in +(* let _ = *) +(* debug_print *) +(* (Printf.sprintf "OK matching: %s and %s, order: %s" *) +(* (CicPp.ppterm c') *) +(* (CicPp.ppterm other') *) +(* (Utils.string_of_comparison order)); *) +(* debug_print *) +(* (Printf.sprintf "subst:\n%s\n" (Utils.print_subst s)) *) +(* in *) if order = U.Gt then res else @@ -373,29 +380,34 @@ let subsumption env table target = find_all_matches ~unif_fun:Inference.matching metasenv context ugraph 0 left ty leftc in - let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) = - try - let other = if pos = Utils.Left then r else l in - let subst', menv', ug' = - let t1 = Unix.gettimeofday () in + let rec ok what = function + | [] -> false, [] + | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _))::tl -> try - let r = - Inference.matching metasenv context what other ugraph in - let t2 = Unix.gettimeofday () in - match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); - r - with Inference.MatchingFailure as e -> - let t2 = Unix.gettimeofday () in - match_unif_time_no := !match_unif_time_no +. (t2 -. t1); - raise e - in - samesubst subst subst' - with Inference.MatchingFailure -> - false + let other = if pos = Utils.Left then r else l in + let subst', menv', ug' = + let t1 = Unix.gettimeofday () in + try + let r = + Inference.matching metasenv context what other ugraph in + let t2 = Unix.gettimeofday () in + match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); + r + with Inference.MatchingFailure as e -> + let t2 = Unix.gettimeofday () in + match_unif_time_no := !match_unif_time_no +. (t2 -. t1); + raise e + in + if samesubst subst subst' then + true, subst + else + ok what tl + with Inference.MatchingFailure -> + ok what tl in - let r = List.exists (ok right) leftr in + let r, subst = ok right leftr in if r then - true + true, subst else let rightr = match right with @@ -405,11 +417,11 @@ let subsumption env table target = find_all_matches ~unif_fun:Inference.matching metasenv context ugraph 0 right ty rightc in - List.exists (ok left) rightr + ok left rightr ;; -let rec demodulate_term metasenv context ugraph table lift_amount term = +let rec demodulation_aux metasenv context ugraph table lift_amount term = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -437,7 +449,7 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = (res, tl @ [S.lift 1 t]) else let r = - demodulate_term metasenv context ugraph table + demodulation_aux metasenv context ugraph table lift_amount t in match r with @@ -452,11 +464,11 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = ) | C.Prod (nn, s, t) -> let r1 = - demodulate_term metasenv context ugraph table lift_amount s in ( + demodulation_aux metasenv context ugraph table lift_amount s in ( match r1 with | None -> let r2 = - demodulate_term metasenv + demodulation_aux metasenv ((Some (nn, C.Decl s))::context) ugraph table (lift_amount+1) t in ( @@ -472,11 +484,11 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = ) | C.Lambda (nn, s, t) -> let r1 = - demodulate_term metasenv context ugraph table lift_amount s in ( + demodulation_aux metasenv context ugraph table lift_amount s in ( match r1 with | None -> let r2 = - demodulate_term metasenv + demodulation_aux metasenv ((Some (nn, C.Decl s))::context) ugraph table (lift_amount+1) t in ( @@ -510,7 +522,7 @@ let build_newtarget_time = ref 0.;; let demod_counter = ref 1;; -let rec demodulation newmeta env table sign target = +let rec demodulation_equality newmeta env table sign target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -629,7 +641,7 @@ let rec demodulation newmeta env table sign target = in !maxmeta, res in - let res = demodulate_term metasenv' context ugraph table 0 left in + let res = demodulation_aux metasenv' context ugraph table 0 left in match res with | Some t -> let newmeta, newtarget = build_newtarget true t in @@ -640,9 +652,9 @@ let rec demodulation newmeta env table sign target = (* if subsumption env table newtarget then *) (* newmeta, build_identity newtarget *) (* else *) - demodulation newmeta env table sign newtarget + demodulation_equality newmeta env table sign newtarget | None -> - let res = demodulate_term metasenv' context ugraph table 0 right in + let res = demodulation_aux metasenv' context ugraph table 0 right in match res with | Some t -> let newmeta, newtarget = build_newtarget false t in @@ -653,7 +665,7 @@ let rec demodulation newmeta env table sign target = (* if subsumption env table newtarget then *) (* newmeta, build_identity newtarget *) (* else *) - demodulation newmeta env table sign newtarget + demodulation_equality newmeta env table sign newtarget | None -> newmeta, target ;; @@ -998,8 +1010,13 @@ let rec demodulation_goal newmeta env table goal = let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) = let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in let what, other = if pos = Utils.Left then what, other else other, what in + let ty = + try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) + with CicUtil.Meta_not_found _ -> ty + in let newterm, newproof = let bo = (* M. *)apply_subst subst (S.subst other t) in + let bo' = apply_subst subst t in let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in incr demod_counter; let metaproof = @@ -1025,29 +1042,35 @@ let rec demodulation_goal newmeta env table goal = in let goal_proof = let pb = - Inference.ProofBlock (subst, eq_URI, (name, ty), bo, + Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, Inference.BasicProof metaproof) in - match proof with - | Inference.NoProof -> - debug_print (lazy "replacing a NoProof"); - pb - | Inference.BasicProof _ -> - debug_print (lazy "replacing a BasicProof"); - pb - | Inference.ProofGoalBlock (_, parent_proof) -> - debug_print (lazy "replacing another ProofGoalBlock"); - Inference.ProofGoalBlock (pb, parent_proof) - | _ -> assert false + let rec repl = function + | Inference.NoProof -> + debug_print (lazy "replacing a NoProof"); + pb + | Inference.BasicProof _ -> + debug_print (lazy "replacing a BasicProof"); + pb + | Inference.ProofGoalBlock (_, parent_proof) -> + debug_print (lazy "replacing another ProofGoalBlock"); + Inference.ProofGoalBlock (pb, parent_proof) + | (Inference.SubProof (term, meta_index, p) as subproof) -> + debug_print + (lazy + (Printf.sprintf "replacing %s" + (Inference.string_of_proof subproof))); + Inference.SubProof (term, meta_index, repl p) + | _ -> assert false + in repl proof in bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof) in let m = Inference.metas_of_term newterm in let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in !maxmeta, (newproof, newmetasenv, newterm) - in - - let res = demodulate_term metasenv' context ugraph table 0 term in + in + let res = demodulation_aux metasenv' context ugraph table 0 term in match res with | Some t -> let newmeta, newgoal = build_newgoal t in @@ -1059,3 +1082,46 @@ let rec demodulation_goal newmeta env table goal = | None -> newmeta, goal ;; + + +let rec demodulation_theorem newmeta env table theorem = + let module C = Cic in + let module S = CicSubstitution in + let module M = CicMetaSubst in + let module HL = HelmLibraryObjects in + let metasenv, context, ugraph = env in + let maxmeta = ref newmeta in + let proof, metas, term = theorem in + let term, termty, metas = theorem in + let metasenv' = metasenv @ metas in + + let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) = + let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in + let what, other = if pos = Utils.Left then what, other else other, what in + let newterm, newty = + let bo = apply_subst subst (S.subst other t) in + let bo' = apply_subst subst t in + let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in + incr demod_counter; + let newproof = + Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, + Inference.BasicProof term) + in + (Inference.build_proof_term newproof, bo) + in + let m = Inference.metas_of_term newterm in + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in + !maxmeta, (newterm, newty, newmetasenv) + in + let res = demodulation_aux metasenv' context ugraph table 0 termty in + match res with + | Some t -> + let newmeta, newthm = build_newtheorem t in + let newt, newty, _ = newthm in + if Inference.meta_convertibility termty newty then + newmeta, newthm + else + demodulation_theorem newmeta env table newthm + | None -> + newmeta, theorem +;; diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 8118c369a..474f0a4d1 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -22,6 +22,7 @@ and proof = (Utils.pos * equality) * proof | ProofGoalBlock of proof * proof (* equality *) | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof + | SubProof of Cic.term * int * proof ;; @@ -44,22 +45,15 @@ let string_of_equality ?env = ;; -let build_proof_term equality = -(* Printf.printf "build_term_proof %s" (string_of_equality equality); *) -(* print_newline (); *) - - let indent = ref 0 in - +let build_proof_term proof = let rec do_build_proof proof = match proof with | NoProof -> Printf.fprintf stderr "WARNING: no proof!\n"; -(* (string_of_equality equality); *) Cic.Implicit None | BasicProof term -> term - | ProofGoalBlock (proofbit, proof (* equality *)) -> + | ProofGoalBlock (proofbit, proof) -> print_endline "found ProofGoalBlock, going up..."; -(* let _, proof, _, _, _ = equality in *) do_build_goal_proof proofbit proof | ProofSymBlock (ens, proof) -> let proof = do_build_proof proof in @@ -68,38 +62,12 @@ let build_proof_term equality = proof ] | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) -> -(* Printf.printf "\nsubst:\n%s\n" (print_subst subst); *) -(* print_newline (); *) - -(* let name, ty, eq_ty, left, right = t' in *) -(* let bo = *) -(* Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); *) -(* eq_ty; left; right] *) -(* in *) let t' = Cic.Lambda (name, ty, bo) in - (* Printf.printf " ProofBlock: eq = %s, eq' = %s" *) - (* (string_of_equality eq) (string_of_equality eq'); *) - (* print_newline (); *) - -(* let s = String.make !indent ' ' in *) -(* incr indent; *) - -(* print_endline (s ^ "build proof'------------"); *) - let proof' = let _, proof', _, _, _ = eq in do_build_proof proof' in -(* print_endline (s ^ "END proof'"); *) - -(* print_endline (s ^ "build eqproof-----------"); *) - let eqproof = do_build_proof eqproof in - -(* print_endline (s ^ "END eqproof"); *) -(* decr indent; *) - - let _, _, (ty, what, other, _), menv', args' = eq in let what, other = if pos = Utils.Left then what, other else other, what @@ -107,6 +75,14 @@ let build_proof_term equality = CicMetaSubst.apply_subst subst (Cic.Appl [Cic.Const (eq_URI, []); ty; what; t'; eqproof; other; proof']) + | SubProof (term, meta_index, proof) -> + let proof = do_build_proof proof in + let eq i = function + | Cic.Meta (j, _) -> i = j + | _ -> false + in + ProofEngineReduction.replace + ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term and do_build_goal_proof proofbit proof = (* match proofbit with *) @@ -135,9 +111,11 @@ let build_proof_term equality = (* let proof' = replace_proof newproof proof in *) (* ProofGoalBlock (pb, (w, proof', t, menv, args)) *) | BasicProof _ -> newproof + | SubProof (term, meta_index, p) -> + SubProof (term, meta_index, replace_proof newproof p) | p -> p in - let _, proof, _, _, _ = equality in +(* let _, proof, _, _, _ = equality in *) do_build_proof proof ;; @@ -474,7 +452,9 @@ let unification_simple metasenv context t1 t2 ugraph = | C.Meta (i, _), C.Meta (j, _) when i > j -> unif subst menv t s | C.Meta _, t when occurs_check subst s t -> - raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif")) + raise + (U.UnificationFailure + (U.failure_msg_of_string "Inference.unification.unif")) | C.Meta (i, l), t -> ( try let _, _, ty = CicUtil.lookup_meta i menv in @@ -486,24 +466,29 @@ let unification_simple metasenv context t1 t2 ugraph = subst, menv with CicUtil.Meta_not_found m -> let names = names_of_context context in - debug_print (lazy ( - Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m - (CicPp.pp t1 names) (CicPp.pp t2 names) - (print_metasenv menv) (print_metasenv metasenv))); + debug_print + (lazy + (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m + (CicPp.pp t1 names) (CicPp.pp t2 names) + (print_metasenv menv) (print_metasenv metasenv))); assert false ) | _, C.Meta _ -> unif subst menv t s | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> - raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif")) + raise (U.UnificationFailure + (U.failure_msg_of_string "Inference.unification.unif")) | C.Appl (hds::tls), C.Appl (hdt::tlt) -> ( try List.fold_left2 (fun (subst', menv) s t -> unif subst' menv s t) (subst, menv) tls tlt with Invalid_argument _ -> - raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif")) + raise (U.UnificationFailure + (U.failure_msg_of_string "Inference.unification.unif")) ) - | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif")) + | _, _ -> + raise (U.UnificationFailure + (U.failure_msg_of_string "Inference.unification.unif")) in let subst, menv = unif [] metasenv t1 t2 in let menv = @@ -521,9 +506,10 @@ let unification metasenv context t1 t2 ugraph = (* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *) let subst, menv, ug = if not (is_simple_term t1) || not (is_simple_term t2) then ( - debug_print (lazy ( - Printf.sprintf "NOT SIMPLE TERMS: %s %s" - (CicPp.ppterm t1) (CicPp.ppterm t2))); + debug_print + (lazy + (Printf.sprintf "NOT SIMPLE TERMS: %s %s" + (CicPp.ppterm t1) (CicPp.ppterm t2))); CicUnification.fo_unif metasenv context t1 t2 ugraph ) else unification_simple metasenv context t1 t2 ugraph @@ -639,7 +625,8 @@ let matching metasenv context t1 t2 ugraph = (* (\* print_newline (); *\) *) (* subst, menv, ug *) (* else *) -(* Printf.printf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2); *) +(* debug_print *) +(* (Printf.sprintf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *) (* print_newline (); *) try let subst, metasenv, ugraph = @@ -1060,9 +1047,10 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = match head with | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) -> - debug_print (lazy ( - Printf.sprintf "OK: %s" (CicPp.ppterm term))); -(* debug_print (lazy ( *) + debug_print + (lazy + (Printf.sprintf "OK: %s" (CicPp.ppterm term))); +(* debug_print ( *) (* Printf.sprintf "args: %s\n" *) (* (String.concat ", " (List.map CicPp.ppterm args)))); *) (* debug_print (lazy ( *) @@ -1088,14 +1076,16 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = match do_find context term with | Some p, newmeta -> let tl, newmeta' = (aux (index+1) newmeta tl) in - p::tl, max newmeta newmeta' + (index, p)::tl, max newmeta newmeta' | None, _ -> aux (index+1) newmeta tl ) | _::tl -> aux (index+1) newmeta tl in - aux 1 newmeta context + let il, maxm = aux 1 newmeta context in + let indexes, equalities = List.split il in + indexes, equalities, maxm ;; @@ -1108,17 +1098,26 @@ let equations_blacklist = "cic:/Coq/Init/Logic/f_equal.con"; "cic:/Coq/Init/Logic/f_equal2.con"; "cic:/Coq/Init/Logic/f_equal3.con"; + "cic:/Coq/Init/Logic/f_equal4.con"; + "cic:/Coq/Init/Logic/f_equal5.con"; "cic:/Coq/Init/Logic/sym_eq.con"; -(* "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *) -(* "cic:/Coq/Init/Peano/mult_n_Sm.con"; *) - + "cic:/Coq/Init/Logic/eq_ind.con"; + "cic:/Coq/Init/Logic/eq_ind_r.con"; + "cic:/Coq/Init/Logic/eq_rec.con"; + "cic:/Coq/Init/Logic/eq_rec_r.con"; + "cic:/Coq/Init/Logic/eq_rect.con"; + "cic:/Coq/Init/Logic/eq_rect_r.con"; + "cic:/Coq/Logic/Eqdep/UIP.con"; + "cic:/Coq/Logic/Eqdep/UIP_refl.con"; + "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con"; + "cic:/Coq/ZArith/Zcompare/rename.con"; (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`... perche' questo cacchio di teorema rompe le scatole :'( *) "cic:/Rocq/SUBST/comparith/mult_n_2.con"; ] ;; -let find_library_equalities ~(dbd:HMysql.dbd) context status maxmeta = +let find_library_equalities dbd context status maxmeta = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in @@ -1133,7 +1132,7 @@ let find_library_equalities ~(dbd:HMysql.dbd) context status maxmeta = let ty, _ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in - (t, ty)::l) + (uri, t, ty)::l) [] (MetadataQuery.equations_for_goal ~dbd status) in @@ -1147,10 +1146,11 @@ let find_library_equalities ~(dbd:HMysql.dbd) context status maxmeta = in let rec aux newmeta = function | [] -> [], newmeta - | (term, termty)::tl -> - debug_print (lazy ( - Printf.sprintf "Examining: %s (%s)" - (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty))); + | (uri, term, termty)::tl -> + debug_print + (lazy + (Printf.sprintf "Examining: %s (%s)" + (CicPp.ppterm term) (CicPp.ppterm termty))); let res, newmeta = match termty with | C.Prod (name, s, t) -> @@ -1166,8 +1166,9 @@ let find_library_equalities ~(dbd:HMysql.dbd) context status maxmeta = match head with | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when (iseq uri) && (ok_types ty newmetas) -> - debug_print (lazy ( - Printf.sprintf "OK: %s" (CicPp.ppterm term))); + debug_print + (lazy + (Printf.sprintf "OK: %s" (CicPp.ppterm term))); let o = !Utils.compare_terms t1 t2 in let w = compute_equality_weight ty t1 t2 in let proof = BasicProof p in @@ -1185,20 +1186,70 @@ let find_library_equalities ~(dbd:HMysql.dbd) context status maxmeta = match res with | Some e -> let tl, newmeta' = aux newmeta tl in - e::tl, max newmeta newmeta' + (uri, e)::tl, max newmeta newmeta' | None -> aux newmeta tl in let found, maxm = aux maxmeta candidates in - (List.fold_left - (fun l e -> - if List.exists (meta_convertibility_eq e) l then ( - debug_print (lazy ( - Printf.sprintf "NO!! %s already there!" (string_of_equality e))); - l - ) - else e::l) - [] found), maxm + let uriset, eqlist = + (List.fold_left + (fun (s, l) (u, e) -> + if List.exists (meta_convertibility_eq e) l then ( + debug_print + (lazy + (Printf.sprintf "NO!! %s already there!" + (string_of_equality e))); + (UriManager.UriSet.add u s, l) + ) else (UriManager.UriSet.add u s, e::l)) + (UriManager.UriSet.empty, []) found) + in + uriset, eqlist, maxm +;; + + +let find_library_theorems dbd env status equalities_uris = + let module C = Cic in + let module S = CicSubstitution in + let module T = CicTypeChecker in + let blacklist = + let refl_equal = + UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in + UriManager.UriSet.remove refl_equal + (UriManager.UriSet.union equalities_uris equations_blacklist) + in + let metasenv, context, ugraph = env in + let candidates = + List.fold_left + (fun l uri -> + if UriManager.UriSet.mem uri blacklist then l + else + let t = CicUtil.term_of_uri uri in + let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in + (t, ty, [])::l) + [] (MetadataQuery.signature_of_goal ~dbd status) + in + candidates +;; + + +let find_context_hypotheses env equalities_indexes = + let metasenv, context, ugraph = env in + let _, res = + List.fold_left + (fun (n, l) entry -> + match entry with + | None -> (n+1, l) + | Some _ -> + if List.mem n equalities_indexes then + (n+1, l) + else + let t = Cic.Rel n in + let ty, _ = + CicTypeChecker.type_of_aux' metasenv context t ugraph in + (n+1, (t, ty, [])::l)) + (1, []) context + in + res ;; @@ -1243,30 +1294,20 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = List.filter (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs in - let table' = Hashtbl.copy table in - let first = List.hd metas in let _ = - Hashtbl.iter - (fun k v -> - if not (List.exists - (function Cic.Meta (i, _) -> i = v | _ -> assert false) - newargs) then - Hashtbl.replace table k first) - table' + if List.length metas > 0 then + let first = List.hd metas in + Hashtbl.iter + (fun k v -> + if not (List.exists + (function Cic.Meta (i, _) -> i = v | _ -> assert false) + newargs) then + Hashtbl.replace table k first) + (Hashtbl.copy table) in -(* debug_print *) -(* (Printf.sprintf "args: %s\nnewargs: %s\n" *) -(* (String.concat "; " (List.map CicPp.ppterm args)) *) -(* (String.concat "; " (List.map CicPp.ppterm newargs))); *) - let rec fix_proof = function | NoProof -> NoProof - | BasicProof term -> -(* let term' = repl term in *) -(* debug_print *) -(* (Printf.sprintf "term was: %s\nterm' is: %s\n" *) -(* (CicPp.ppterm term) (CicPp.ppterm term')); *) - BasicProof (repl term) + | BasicProof term -> BasicProof (repl term) | ProofBlock (subst, eq_URI, namety, bo(* t' *), (pos, eq), p) -> (* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *) @@ -1770,3 +1811,15 @@ let extract_differing_subterms t1 t2 = ;; +let rec string_of_proof = function + | NoProof -> "NoProof" + | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t) + | SubProof (t, i, p) -> + Printf.sprintf "SubProof(%s, %s, %s)" + (CicPp.ppterm t) (string_of_int i) (string_of_proof p) + | ProofSymBlock _ -> "ProofSymBlock" + | ProofBlock _ -> "ProofBlock" + | ProofGoalBlock (p1, p2) -> + Printf.sprintf "ProofGoalBlock(%s, %s)" + (string_of_proof p1) (string_of_proof p2) +;; diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 4bb43ea8f..d0556dd54 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -19,7 +19,7 @@ and proof = (Utils.pos * equality) * proof | ProofGoalBlock of proof * proof (* equality *) | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof - + | SubProof of Cic.term * int * proof type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph @@ -55,7 +55,7 @@ val beta_expand: *) val find_equalities: ?eq_uri:UriManager.uri -> Cic.context -> ProofEngineTypes.proof -> - equality list * int + int list * equality list * int exception TermIsNotAnEquality;; @@ -105,8 +105,17 @@ val fix_metas: int -> equality -> int * equality val extract_differing_subterms: Cic.term -> Cic.term -> (Cic.term * Cic.term) option -val build_proof_term: equality -> Cic.term +val build_proof_term: proof (* equality *) -> Cic.term val find_library_equalities: - dbd:HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> - equality list * int + HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> + UriManager.UriSet.t * equality list * int + +val find_library_theorems: + HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t -> + (Cic.term * Cic.term * Cic.metasenv) list + +val find_context_hypotheses: + environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list + +val string_of_proof: proof -> string diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index 1870a5137..bf9ec6897 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 configuration_file = ref "../helm/matita/matita.conf.xml";; -let core_notation_script = "../../matita/core_notation.moo";; +let core_notation_script = "../helm/matita/core_notation.moo";; let get_from_user ~(dbd:HMysql.dbd) = let rec get () = @@ -28,6 +28,8 @@ let _ = | o -> raise (Arg.Bad ("Unknown term ordering: " ^ o)) and set_fullred b = S.use_fullred := b and set_time_limit v = S.time_limit := float_of_int v + and set_width w = S.maxwidth := w + and set_depth d = S.maxdepth := d in Arg.parse [ "-f", Arg.Bool set_fullred, @@ -47,11 +49,17 @@ let _ = "\tlpo: Lexicographic path ordering"; "-l", Arg.Int set_time_limit, "Time limit in seconds (default: no limit)"; + + "-w", Arg.Int set_width, + Printf.sprintf "Maximal width (default: %d)" !Saturation.maxwidth; + + "-d", Arg.Int set_depth, + Printf.sprintf "Maximal depth (default: %d)" !Saturation.maxdepth; ] (fun a -> ()) "Usage:" in Helm_registry.load_from !configuration_file; CicNotation.load_notation core_notation_script; -CicNotation.load_notation "../../matita/coq.moo"; +CicNotation.load_notation "../helm/matita/coq.ma"; let dbd = HMysql.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 e8afa8032..bc935d7f7 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -38,10 +38,14 @@ let kept_clauses = ref 0;; (* index of the greatest Cic.Meta created - TODO: find a better way! *) let maxmeta = ref 0;; +(* varbiables controlling the search-space *) +let maxdepth = ref 3;; +let maxwidth = ref 3;; + type result = | ParamodulationFailure - | ParamodulationSuccess of Inference.equality option * environment + | ParamodulationSuccess of Inference.proof option * environment ;; @@ -103,8 +107,12 @@ end module EqualitySet = Set.Make(OrderedEquality);; -let select env passive (active, _) = +let select env goals passive (active, _) = processed_clauses := !processed_clauses + 1; + + let goal = + match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false + in let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in let remove eq l = @@ -135,9 +143,13 @@ let select env passive (active, _) = let cardinality map = TermMap.fold (fun k v res -> res + v) map 0 in - match active with - | (Negative, e)::_ -> - let symbols = symbols_of_equality e in +(* match active with *) +(* | (Negative, e)::_ -> *) +(* let symbols = symbols_of_equality e in *) + let symbols = + let _, _, term = goal in + symbols_of_term term + in let card = cardinality symbols in let foldfun k v (r1, r2) = if TermMap.mem k symbols then @@ -179,19 +191,19 @@ let select env passive (active, _) = (([], neg_set), (remove current pos_list, EqualitySet.remove current pos_set), passive_table) - | _ -> - let current = EqualitySet.min_elt pos_set in - let passive_table = - Indexing.remove_index passive_table current -(* if !use_fullred then Indexing.remove_index passive_table current *) -(* else passive_table *) - in - let passive = - (neg_list, neg_set), - (remove current pos_list, EqualitySet.remove current pos_set), - passive_table - in - (Positive, current), passive +(* | _ -> *) +(* let current = EqualitySet.min_elt pos_set in *) +(* let passive_table = *) +(* Indexing.remove_index passive_table current *) +(* (\* if !use_fullred then Indexing.remove_index passive_table current *\) *) +(* (\* else passive_table *\) *) +(* in *) +(* let passive = *) +(* (neg_list, neg_set), *) +(* (remove current pos_list, EqualitySet.remove current pos_set), *) +(* passive_table *) +(* in *) +(* (Positive, current), passive *) ) | _ -> symbols_counter := !symbols_ratio; @@ -288,7 +300,8 @@ let prune_passive howmany (active, _) passive = in let in_weight = round (howmany *. ratio /. (ratio +. 1.)) and in_age = round (howmany /. (ratio +. 1.)) in - debug_print (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age)); + debug_print + (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age)); let symbols, card = match active with | (Negative, e)::_ -> @@ -512,7 +525,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = let demodulate table current = let newmeta, newcurrent = - Indexing.demodulation !maxmeta env table sign current in + Indexing.demodulation_equality !maxmeta env table sign current in maxmeta := newmeta; if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) @@ -601,7 +614,7 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let demodulate sign table target = let newmeta, newtarget = - Indexing.demodulation !maxmeta env table sign target in + Indexing.demodulation_equality !maxmeta env table sign target in maxmeta := newmeta; newtarget in @@ -639,10 +652,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let subs = match passive_table with | None -> - (fun e -> not (Indexing.subsumption env active_table e)) + (fun e -> not (fst (Indexing.subsumption env active_table e))) | Some passive_table -> - (fun e -> not ((Indexing.subsumption env active_table e) || - (Indexing.subsumption env passive_table e))) + (fun e -> not ((fst (Indexing.subsumption env active_table e)) || + (fst (Indexing.subsumption env passive_table e)))) in let t1 = Unix.gettimeofday () in @@ -787,7 +800,545 @@ let get_selection_estimate () = ;; -let rec given_clause env passive active = +let simplify_goal env goal ?passive (active_list, active_table) = + let pl, passive_table = + match passive with + | None -> [], None + | Some ((pn, _), (pp, _), pt) -> + let pn = List.map (fun e -> (Negative, e)) pn + and pp = List.map (fun e -> (Positive, e)) pp in + pn @ pp, Some pt + in + let all = if pl = [] then active_list else active_list @ pl in + + let demodulate table goal = + let newmeta, newgoal = + Indexing.demodulation_goal !maxmeta env table goal in + maxmeta := newmeta; + newgoal + in + let goal = + match passive_table with + | None -> demodulate active_table goal + | Some passive_table -> + let goal = demodulate active_table goal in + demodulate passive_table goal + in + let _ = + let p, _, t = goal in + debug_print + (lazy + (Printf.sprintf "Goal after demodulation: %s, %s" + (string_of_proof p) (CicPp.ppterm t))) + in + goal +;; + + +let simplify_goals env goals ?passive active = + List.map + (fun (d, gl) -> + let gl = List.map (fun g -> simplify_goal env g ?passive active) gl in + d, gl) + goals +;; + + +let simplify_theorems env theorems ?passive (active_list, active_table) = + let pl, passive_table = + match passive with + | None -> [], None + | Some ((pn, _), (pp, _), pt) -> + let pn = List.map (fun e -> (Negative, e)) pn + and pp = List.map (fun e -> (Positive, e)) pp in + pn @ pp, Some pt + in + let all = if pl = [] then active_list else active_list @ pl in + + let demodulate table theorem = + let newmeta, newthm = + Indexing.demodulation_theorem !maxmeta env table theorem in + maxmeta := newmeta; + newthm + in + match passive_table with + | None -> List.map (demodulate active_table) theorems + | Some passive_table -> + let theorems = List.map (demodulate active_table) theorems in + List.map (demodulate passive_table) theorems +;; + + +let apply_equality_to_goal env equality goal = + let module C = Cic in + let module HL = HelmLibraryObjects in + let module I = Inference in + let metasenv, context, ugraph = env in + let _, proof, (ty, left, right, _), metas, args = equality in + let eqterm = C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); ty; left; right] in + let gproof, gmetas, gterm = goal in + try + let subst, metasenv', _ = + let menv = metasenv @ metas @ gmetas in + Inference.unification menv context eqterm gterm ugraph + in + let newproof = + match proof with + | I.BasicProof t -> I.BasicProof (CicMetaSubst.apply_subst subst t) + | I.ProofBlock (s, uri, nt, t, pe, p) -> + I.ProofBlock (subst @ s, uri, nt, t, pe, p) + | _ -> assert false + in + let newgproof = + let rec repl = function + | I.ProofGoalBlock (_, gp) -> I.ProofGoalBlock (newproof, gp) + | I.NoProof -> newproof + | I.BasicProof p -> newproof + | I.SubProof (t, i, p) -> I.SubProof (t, i, repl p) + | _ -> assert false + in + repl gproof + in + true, subst, newgproof + with CicUnification.UnificationFailure _ -> + false, [], I.NoProof +;; + + +(* +let apply_to_goal env theorems active (depth, goals) = + let _ = + debug_print ("apply_to_goal: " ^ (string_of_int (List.length goals))) + in + let metasenv, context, ugraph = env in + let goal = List.hd goals in + let proof, metas, term = goal in +(* debug_print *) +(* (Printf.sprintf "apply_to_goal with goal: %s" (CicPp.ppterm term)); *) + let newmeta = CicMkImplicit.new_meta metasenv [] in + let metasenv = (newmeta, context, term)::metasenv @ metas in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + let status = + ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta) + in + let rec aux = function + | [] -> false, [] (* goals *) (* None *) + | (theorem, thmty, _)::tl -> + try + let subst_in, (newproof, newgoals) = + PrimitiveTactics.apply_tac_verbose ~term:theorem status + in + if newgoals = [] then + let _, _, p, _ = newproof in + let newp = + let rec repl = function + | Inference.ProofGoalBlock (_, gp) -> + Inference.ProofGoalBlock (Inference.BasicProof p, gp) + | Inference.NoProof -> Inference.BasicProof p + | Inference.BasicProof _ -> Inference.BasicProof p + | Inference.SubProof (t, i, p2) -> + Inference.SubProof (t, i, repl p2) + | _ -> assert false + in + repl proof + in + true, [[newp, metas, term]] (* Some newp *) + else if List.length newgoals = 1 then + let _, menv, p, _ = newproof in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let goals = + List.map + (fun i -> + let _, _, ty = CicUtil.lookup_meta i menv in + let proof = + Inference.SubProof + (p, i, Inference.BasicProof (Cic.Meta (i, irl))) + in (proof, menv, ty)) + newgoals + in + let res, others = aux tl in + if res then (true, others) else (false, goals::others) + else + aux tl + with ProofEngineTypes.Fail msg -> + (* debug_print ("FAIL!!:" ^ msg); *) + aux tl + in + let r, l = + if Inference.term_is_equality term then + let rec appleq = function + | [] -> false, [] + | (Positive, equality)::tl -> + let ok, _, newproof = apply_equality_to_goal env equality goal in + if ok then true, [(depth, [newproof, metas, term])] else appleq tl + | _::tl -> appleq tl + in + let al, _ = active in + appleq al + else + false, [] + in + if r = true then r, l else + let r, l = aux theorems in + if r = true then + r, List.map (fun l -> (depth+1, l)) l + else + r, (depth, goals)::(List.map (fun l -> (depth+1, l)) l) +;; +*) + + +let new_meta () = + incr maxmeta; !maxmeta +;; + + +let apply_to_goal env theorems active goal = + let metasenv, context, ugraph = env in + let proof, metas, term = goal in + debug_print + (lazy + (Printf.sprintf "apply_to_goal with goal: %s, %s" + (string_of_proof proof) (CicPp.ppterm term))); + let status = + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let proof', newmeta = + let rec get_meta = function + | SubProof (t, i, _) -> t, i + | ProofGoalBlock (_, p) -> get_meta p + | _ -> + let n = new_meta () in (* CicMkImplicit.new_meta metasenv [] in *) + Cic.Meta (n, irl), n + in + get_meta proof + in +(* let newmeta = CicMkImplicit.new_meta metasenv [] in *) + let metasenv = (newmeta, context, term)::metasenv @ metas in + ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta) +(* ((None, metasenv, proof', term), newmeta) *) + in + let rec aux = function + | [] -> `No (* , [], [] *) + | (theorem, thmty, _)::tl -> + try + let subst, (newproof, newgoals) = + PrimitiveTactics.apply_tac_verbose_with_subst ~term:theorem status + in + if newgoals = [] then + let _, _, p, _ = newproof in + let newp = + let rec repl = function + | Inference.ProofGoalBlock (_, gp) -> + Inference.ProofGoalBlock (Inference.BasicProof p, gp) + | Inference.NoProof -> Inference.BasicProof p + | Inference.BasicProof _ -> Inference.BasicProof p + | Inference.SubProof (t, i, p2) -> + Inference.SubProof (t, i, repl p2) + | _ -> assert false + in + repl proof + in + let _, m = status in + let subst = List.filter (fun (i, _) -> i = m) subst in +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "m = %d\nsubst = %s\n" *) +(* m (print_subst subst))); *) + `Ok (subst, [newp, metas, term]) + else + let _, menv, p, _ = newproof in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let goals = + List.map + (fun i -> + let _, _, ty = CicUtil.lookup_meta i menv in + let p' = + let rec gp = function + | SubProof (t, i, p) -> + SubProof (t, i, gp p) + | ProofGoalBlock (sp1, sp2) -> +(* SubProof (p, i, sp) *) + ProofGoalBlock (sp1, gp sp2) +(* gp sp *) + | BasicProof _ + | NoProof -> + SubProof (p, i, BasicProof (Cic.Meta (i, irl))) + | ProofSymBlock (s, sp) -> + ProofSymBlock (s, gp sp) + | ProofBlock (s, u, nt, t, pe, sp) -> + ProofBlock (s, u, nt, t, pe, gp sp) +(* | _ -> assert false *) + in gp proof + in + debug_print + (lazy + (Printf.sprintf "new sub goal: %s, %s" + (string_of_proof p') (CicPp.ppterm ty))); + (p', menv, ty)) + newgoals + in +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "\nGoOn with subst: %s" (print_subst subst))); *) + let best = aux tl in + match best with + | `Ok (_, _) -> best + | `No -> `GoOn ([subst, goals]) + | `GoOn sl(* , subst', goals' *) -> +(* if (List.length goals') < (List.length goals) then best *) +(* else `GoOn, subst, goals *) + `GoOn ((subst, goals)::sl) + with ProofEngineTypes.Fail msg -> + aux tl + in + let r, s, l = + if Inference.term_is_equality term then + let rec appleq = function + | [] -> false, [], [] + | (Positive, equality)::tl -> + let ok, s, newproof = apply_equality_to_goal env equality goal in + if ok then true, s, [newproof, metas, term] else appleq tl + | _::tl -> appleq tl + in + let al, _ = active in + appleq al + else + false, [], [] + in + if r = true then `Ok (s, l) else aux theorems +;; + + +let apply_to_goal_conj env theorems active (depth, goals) = + let rec aux = function + | goal::tl -> + let propagate_subst subst (proof, metas, term) = + debug_print + (lazy + (Printf.sprintf "\npropagate_subst:\n%s\n%s, %s\n" + (print_subst subst) (string_of_proof proof) + (CicPp.ppterm term))); + let rec repl = function + | NoProof -> NoProof + | BasicProof t -> + BasicProof (CicMetaSubst.apply_subst subst t) + | ProofGoalBlock (p, pb) -> + debug_print (lazy "HERE"); + let pb' = repl pb in + ProofGoalBlock (p, pb') + | SubProof (t, i, p) -> + let t' = CicMetaSubst.apply_subst subst t in + debug_print + (lazy + (Printf.sprintf + "SubProof %d\nt = %s\nsubst = %s\nt' = %s\n" + i (CicPp.ppterm t) (print_subst subst) + (CicPp.ppterm t'))); + let p = repl p in + SubProof (t', i, p) + | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p) + | ProofBlock (s, u, nty, t, pe, p) -> + ProofBlock (subst @ s, u, nty, t, pe, p) + in (repl proof, metas, term) + in + let r = apply_to_goal env theorems active goal in ( + match r with + | `No -> `No (depth, goals) + | `GoOn sl (* (subst, gl) *) -> +(* let tl = List.map (propagate_subst subst) tl in *) + debug_print (lazy "GO ON!!!"); + let l = + List.map + (fun (s, gl) -> + (depth+1, gl @ (List.map (propagate_subst s) tl))) sl + in + debug_print + (lazy + (Printf.sprintf "%s\n" + (String.concat "; " + (List.map + (fun (s, gl) -> + (Printf.sprintf "[%s]" + (String.concat "; " + (List.map + (fun (p, _, g) -> + (Printf.sprintf "<%s, %s>" + (string_of_proof p) + (CicPp.ppterm g))) gl)))) l)))); + `GoOn l (* (depth+1, gl @ tl) *) + | `Ok (subst, gl) -> + if tl = [] then +(* let _ = *) +(* let p, _, t = List.hd gl in *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "OK: %s, %s\n" *) +(* (string_of_proof p) (CicPp.ppterm t))) *) +(* in *) + `Ok (depth, gl) + else + let p, _, _ = List.hd gl in + let subproof = + let rec repl = function + | SubProof (_, _, p) -> repl p + | ProofGoalBlock (p1, p2) -> + ProofGoalBlock (repl p1, repl p2) + | p -> p + in + build_proof_term (repl p) + in + let i = + let rec get_meta = function + | SubProof (_, i, p) -> max i (get_meta p) + | ProofGoalBlock (_, p) -> get_meta p + | _ -> -1 (* assert false *) + in + get_meta p + in + let subst = + let _, (context, _, _) = List.hd subst in + [i, (context, subproof, Cic.Implicit None)] + in + let tl = List.map (propagate_subst subst) tl in + `GoOn ([depth+1, tl]) + ) + | _ -> assert false + in + debug_print + (lazy + (Printf.sprintf "apply_to_goal_conj (%d, [%s])" + depth + (String.concat "; " + (List.map (fun (_, _, t) -> CicPp.ppterm t) goals)))); + if depth > !maxdepth || (List.length goals) > !maxwidth then ( + debug_print + (lazy (Printf.sprintf "Pruning because depth = %d, width = %d" + depth (List.length goals))); + `No (depth, goals) + ) else + aux goals +;; + + +module OrderedGoals = struct + type t = int * (Inference.proof * Cic.metasenv * Cic.term) list + + let compare g1 g2 = + let d1, l1 = g1 + and d2, l2 = g2 in + let r = d2 - d1 in + if r <> 0 then r + else let r = (List.length l1) - (List.length l2) in + if r <> 0 then r + else + let res = ref 0 in + let _ = + List.exists2 + (fun (_, _, t1) (_, _, t2) -> + let r = Pervasives.compare t1 t2 in + if r <> 0 then ( + res := r; + true + ) else + false) l1 l2 + in !res +(* let res = Pervasives.compare g1 g2 in *) +(* let _ = *) +(* let print_goals (d, gl) = *) +(* let gl' = List.map (fun (_, _, t) -> CicPp.ppterm t) gl in *) +(* Printf.sprintf "%d, [%s]" d (String.concat "; " gl') *) +(* in *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "comparing g1:%s and g2:%s, res: %d\n" *) +(* (print_goals g1) (print_goals g2) res)) *) +(* in *) +(* res *) +end + +module GoalsSet = Set.Make(OrderedGoals);; + + +exception SearchSpaceOver;; + + +let apply_to_goals env is_passive_empty theorems active goals = + debug_print (lazy "\n\n\tapply_to_goals\n\n"); + let add_to set goals = + List.fold_left (fun s g -> GoalsSet.add g s) set goals + in + let rec aux set = function + | [] -> + debug_print (lazy "HERE!!!"); + if is_passive_empty then raise SearchSpaceOver else false, set + | goals::tl -> + let res = apply_to_goal_conj env theorems active goals in + match res with + | `Ok newgoals -> + let _ = + let d, p, t = + match newgoals with + | (d, (p, _, t)::_) -> d, p, t + | _ -> assert false + in + debug_print + (lazy + (Printf.sprintf "\nOK!!!!\ndepth: %d\nProof: %s\ngoal: %s\n" + d (string_of_proof p) (CicPp.ppterm t))) + in + true, GoalsSet.singleton newgoals + | `GoOn newgoals -> + let print_set set msg = + debug_print + (lazy + (Printf.sprintf "%s:\n%s" msg + (String.concat "\n" + (GoalsSet.fold + (fun (d, gl) l -> + let gl' = + List.map (fun (_, _, t) -> CicPp.ppterm t) gl + in + let s = + Printf.sprintf "%d, [%s]" d + (String.concat "; " gl') + in + s::l) set [])))) + in + let set = add_to set (goals::tl) in +(* print_set set "SET BEFORE"; *) + let n = GoalsSet.cardinal set in + let set = add_to set newgoals in +(* print_set set "SET AFTER"; *) + let m = GoalsSet.cardinal set in +(* if n < m then *) + false, set +(* else *) +(* let _ = print_set set "SET didn't change" in *) +(* aux set tl *) + | `No newgoals -> + aux set tl +(* let set = add_to set (newgoals::goals::tl) in *) +(* let res, set = aux set tl in *) +(* res, set *) + in + let n = List.length goals in + let res, goals = aux (add_to GoalsSet.empty goals) goals in + let goals = GoalsSet.elements goals in + debug_print (lazy "\n\tapply_to_goals end\n"); + let m = List.length goals in + if m = n && is_passive_empty then + raise SearchSpaceOver + else + res, goals +;; + + +let rec given_clause env goals theorems passive active = let time1 = Unix.gettimeofday () in let selection_estimate = get_selection_estimate () in @@ -797,12 +1348,13 @@ let rec given_clause env passive active = passive else if !elapsed_time > !time_limit then ( debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time)); + !time_limit !elapsed_time)); make_passive [] [] ) else if kept > selection_estimate then ( - debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ - "(kept: %d, selection_estimate: %d)\n") - kept selection_estimate)); + debug_print + (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ + "(kept: %d, selection_estimate: %d)\n") + kept selection_estimate)); prune_passive selection_estimate active passive ) else passive @@ -813,67 +1365,95 @@ let rec given_clause env passive active = kept_clauses := (size_of_passive passive) + (size_of_active active); - match passive_is_empty passive with - | true -> ParamodulationFailure - | false -> - let (sign, current), passive = select env passive active in - let time1 = Unix.gettimeofday () in - let res = forward_simplify env (sign, current) ~passive active in - let time2 = Unix.gettimeofday () in - forward_simpl_time := !forward_simpl_time +. (time2 -. time1); - match res with - | None -> - given_clause env passive active - | Some (sign, current) -> - if (sign = Negative) && (is_identity env current) then ( - debug_print (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current))); - ParamodulationSuccess (Some current, env) - ) else ( - debug_print (lazy "\n================================================"); - debug_print (lazy (Printf.sprintf "selected: %s %s" - (string_of_sign sign) +(* let refl_equal = *) +(* CicUtil.term_of_uri *) +(* (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *) +(* in *) + let goals = simplify_goals env goals active in + let theorems = simplify_theorems env theorems active in + let is_passive_empty = passive_is_empty passive in + try + let ok, goals = apply_to_goals env is_passive_empty theorems active goals in + if ok then + let proof = + match goals with + | (_, [proof, _, _])::_ -> Some proof + | _ -> assert false + in + ParamodulationSuccess (proof, env) + else + match is_passive_empty (* passive_is_empty passive *) with + | true -> (* ParamodulationFailure *) + given_clause env goals theorems passive active + | false -> + let (sign, current), passive = select env goals passive active in + let time1 = Unix.gettimeofday () in + let res = forward_simplify env (sign, current) ~passive active in + let time2 = Unix.gettimeofday () in + forward_simpl_time := !forward_simpl_time +. (time2 -. time1); + match res with + | None -> + given_clause env goals theorems passive active + | Some (sign, current) -> + if (sign = Negative) && (is_identity env current) then ( + debug_print + (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current))); - - let t1 = Unix.gettimeofday () in - let new' = infer env sign current active in - let t2 = Unix.gettimeofday () in - infer_time := !infer_time +. (t2 -. t1); - - let res, goal = contains_empty env new' in - if res then - ParamodulationSuccess (goal, env) - else - let t1 = Unix.gettimeofday () in - let new' = forward_simplify_new env new' (* ~passive *) active in - let t2 = Unix.gettimeofday () in - let _ = - forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1) - in - let active = - match sign with - | Negative -> active - | Positive -> - let t1 = Unix.gettimeofday () in - let active, _, newa, _ = - backward_simplify env ([], [current]) active - in - let t2 = Unix.gettimeofday () in - backward_simpl_time := !backward_simpl_time +. (t2 -. t1); - match newa with - | None -> active - | Some (n, p) -> - let al, tbl = active in - let nn = List.map (fun e -> Negative, e) n in - let pp, tbl = - List.fold_right - (fun e (l, t) -> - (Positive, e)::l, - Indexing.index tbl e) - p ([], tbl) + let _, proof, _, _, _ = current in + ParamodulationSuccess (Some proof (* current *), env) + ) else ( + debug_print + (lazy "\n================================================"); + debug_print (lazy (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 + let t2 = Unix.gettimeofday () in + infer_time := !infer_time +. (t2 -. t1); + + let res, goal' = contains_empty env new' in + if res then + let proof = + match goal' with + | Some goal -> let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof (* goal *), env) + else + let t1 = Unix.gettimeofday () in + let new' = forward_simplify_new env new' active in + let t2 = Unix.gettimeofday () in + let _ = + forward_simpl_new_time := + !forward_simpl_new_time +. (t2 -. t1) + in + let active = + match sign with + | Negative -> active + | Positive -> + let t1 = Unix.gettimeofday () in + let active, _, newa, _ = + backward_simplify env ([], [current]) active in - nn @ al @ pp, tbl - in + let t2 = Unix.gettimeofday () in + backward_simpl_time := + !backward_simpl_time +. (t2 -. t1); + match newa with + | None -> active + | Some (n, p) -> + let al, tbl = active in + let nn = List.map (fun e -> Negative, e) n in + let pp, tbl = + List.fold_right + (fun e (l, t) -> + (Positive, e)::l, + Indexing.index tbl e) + p ([], tbl) + in + nn @ al @ pp, tbl + in (* let _ = *) (* Printf.printf "active:\n%s\n" *) (* (String.concat "\n" *) @@ -895,17 +1475,17 @@ let rec given_clause env passive active = (* (string_of_equality ~env e)) pos))); *) (* print_newline (); *) (* in *) - match contains_empty env new' with - | false, _ -> - let active = - let al, tbl = active in - match sign with - | Negative -> (sign, current)::al, tbl - | Positive -> - al @ [(sign, current)], Indexing.index tbl current - in - let passive = add_to_passive passive new' in - let (_, ns), (_, ps), _ = passive in + match contains_empty env new' with + | false, _ -> + let active = + let al, tbl = active in + match sign with + | Negative -> (sign, current)::al, tbl + | Positive -> + al @ [(sign, current)], Indexing.index tbl current + in + let passive = add_to_passive passive new' in + let (_, ns), (_, ps), _ = passive in (* Printf.printf "passive:\n%s\n" *) (* (String.concat "\n" *) (* ((List.map (fun e -> "Negative " ^ *) @@ -915,14 +1495,22 @@ let rec given_clause env passive active = (* (string_of_equality ~env e)) *) (* (EqualitySet.elements ps)))); *) (* print_newline (); *) - given_clause env passive active - | true, goal -> - ParamodulationSuccess (goal, env) - ) + given_clause env goals theorems passive active + | true, goal -> + let proof = + match goal with + | Some goal -> + let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof (* goal *), env) + ) + with SearchSpaceOver -> + ParamodulationFailure ;; -let rec given_clause_fullred env passive active = +let rec given_clause_fullred env goals theorems passive active = let time1 = Unix.gettimeofday () in let selection_estimate = get_selection_estimate () in @@ -932,12 +1520,13 @@ let rec given_clause_fullred env passive active = passive else if !elapsed_time > !time_limit then ( debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time)); + !time_limit !elapsed_time)); make_passive [] [] ) else if kept > selection_estimate then ( - debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ - "(kept: %d, selection_estimate: %d)\n") - kept selection_estimate)); + debug_print + (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ + "(kept: %d, selection_estimate: %d)\n") + kept selection_estimate)); prune_passive selection_estimate active passive ) else passive @@ -948,91 +1537,133 @@ 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 -> ParamodulationFailure - | false -> - let (sign, current), passive = select env passive active in - let time1 = Unix.gettimeofday () in - let res = forward_simplify env (sign, current) ~passive active in - let time2 = Unix.gettimeofday () in - forward_simpl_time := !forward_simpl_time +. (time2 -. time1); - match res with - | None -> - given_clause_fullred env passive active - | Some (sign, current) -> - if (sign = Negative) && (is_identity env current) then ( - debug_print (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current))); - ParamodulationSuccess (Some current, env) - ) else ( - debug_print (lazy "\n================================================"); - debug_print (lazy (Printf.sprintf "selected: %s %s" - (string_of_sign sign) +(* let refl_equal = *) +(* CicUtil.term_of_uri *) +(* (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *) +(* in *) + let goals = simplify_goals env goals ~passive active in + let theorems = simplify_theorems env theorems ~passive active in + let is_passive_empty = passive_is_empty passive in + try + let ok, goals = apply_to_goals env is_passive_empty theorems active goals in + if ok then + let proof = + match goals with + | (_, [proof, _, _])::_ -> Some proof + | _ -> assert false + in + ParamodulationSuccess (proof, env) + else + let _ = + debug_print + (lazy ("new_goals: " ^ (string_of_int (List.length goals)))); + debug_print + (lazy + (String.concat "\n" + (List.map + (fun (d, gl) -> + let gl' = + List.map + (fun (p, _, t) -> + (string_of_proof p) ^ ", " ^ (CicPp.ppterm t)) gl + in + Printf.sprintf "%d: %s" d (String.concat "; " gl')) + goals))); + in + match is_passive_empty (* passive_is_empty passive *) with + | true -> (* ParamodulationFailure *) + given_clause_fullred env goals theorems passive active + | false -> + let (sign, current), passive = select env goals passive active in + let time1 = Unix.gettimeofday () in + let res = forward_simplify env (sign, current) ~passive active in + let time2 = Unix.gettimeofday () in + forward_simpl_time := !forward_simpl_time +. (time2 -. time1); + match res with + | None -> + given_clause_fullred env goals theorems passive active + | Some (sign, current) -> + if (sign = Negative) && (is_identity env current) then ( + debug_print + (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current))); + let _, proof, _, _, _ = current in + ParamodulationSuccess (Some proof (* current *), env) + ) else ( + debug_print + (lazy "\n================================================"); + debug_print (lazy (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 + let t2 = Unix.gettimeofday () in + infer_time := !infer_time +. (t2 -. t1); + + let active = + if is_identity env current then active + else + let al, tbl = active in + match sign with + | Negative -> (sign, current)::al, tbl + | Positive -> + al @ [(sign, current)], Indexing.index tbl current + in + let rec simplify new' active passive = + let t1 = Unix.gettimeofday () in + let new' = forward_simplify_new env new' ~passive active in + let t2 = Unix.gettimeofday () in + forward_simpl_new_time := + !forward_simpl_new_time +. (t2 -. t1); + let t1 = Unix.gettimeofday () in + let active, passive, newa, retained = + backward_simplify env new' ~passive active in + let t2 = Unix.gettimeofday () in + backward_simpl_time := !backward_simpl_time +. (t2 -. t1); + match newa, retained with + | None, None -> active, passive, new' + | Some (n, p), None + | None, Some (n, p) -> + let nn, np = new' in + simplify (nn @ n, np @ p) active passive + | Some (n, p), Some (rn, rp) -> + let nn, np = new' in + simplify (nn @ n @ rn, np @ p @ rp) active passive + in + let active, passive, new' = simplify new' active passive in - let t1 = Unix.gettimeofday () in - let new' = infer env sign current active in - let t2 = Unix.gettimeofday () in - infer_time := !infer_time +. (t2 -. t1); - - let active = - if is_identity env current then active - else - let al, tbl = active in - match sign with - | Negative -> (sign, current)::al, tbl - | Positive -> al @ [(sign, current)], Indexing.index tbl current - in - let rec simplify new' active passive = - let t1 = Unix.gettimeofday () in - let new' = forward_simplify_new env new' ~passive active in - let t2 = Unix.gettimeofday () in - forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1); - let t1 = Unix.gettimeofday () in - let active, passive, newa, retained = - backward_simplify env new' ~passive active in - let t2 = Unix.gettimeofday () in - backward_simpl_time := !backward_simpl_time +. (t2 -. t1); - match newa, retained with - | None, None -> active, passive, new' - | Some (n, p), None - | None, Some (n, p) -> - let nn, np = new' in - simplify (nn @ n, np @ p) active passive - | Some (n, p), Some (rn, rp) -> - let nn, np = new' in - simplify (nn @ n @ rn, np @ p @ rp) active passive - in - let active, passive, new' = simplify new' active passive in - - let k = size_of_passive passive in - if k < (kept - 1) then - processed_clauses := !processed_clauses + (kept - 1 - k); - - let _ = - debug_print (lazy ( - 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 (lazy ( - 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 k = size_of_passive passive in + if k < (kept - 1) then + processed_clauses := !processed_clauses + (kept - 1 - k); + + let _ = + debug_print + (lazy + (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 + (lazy + (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 *) (* Printf.printf "passive:\n%s\n" *) (* (String.concat "\n" *) @@ -1043,15 +1674,21 @@ let rec given_clause_fullred env passive active = (* (string_of_equality ~env e)) *) (* (EqualitySet.elements ps)))); *) (* print_newline (); *) - given_clause_fullred env passive active - | true, goal -> - ParamodulationSuccess (goal, env) - ) + given_clause_fullred env goals theorems passive active + | true, goal -> + let proof = + match goal with + | Some goal -> let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof (* goal *), env) + ) + with SearchSpaceOver -> + ParamodulationFailure ;; -let given_clause_ref = ref given_clause;; - +(* let given_clause_ref = ref given_clause;; *) let main dbd term metasenv ugraph = let module C = Cic in @@ -1064,9 +1701,9 @@ let main dbd term metasenv ugraph = let goal' = List.nth goals 0 in 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+2) + let eq_indexes, equalities, maxm = find_equalities context proof in + let lib_eq_uris, 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 @@ -1080,28 +1717,45 @@ let main dbd term metasenv ugraph = in (* let new_meta_goal = Cic.Meta (goal', irl) in *) let env = (metasenv, context, ugraph) in + let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in + let context_hyp = find_context_hypotheses env eq_indexes in + let theorems = context_hyp @ theorems in + let _ = + debug_print + (lazy + (Printf.sprintf + "Theorems:\n-------------------------------------\n%s\n" + (String.concat "\n" + (List.map + (fun (t, ty, _) -> + Printf.sprintf + "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) + theorems)))) + in try - let term_equality = equality_of_term new_meta_goal goal in - let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in - 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 goal = Inference.BasicProof new_meta_goal, [], goal in +(* let term_equality = equality_of_term new_meta_goal goal in *) +(* let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *) +(* 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 equalities = let equalities = equalities @ library_equalities in - debug_print (lazy ( - Printf.sprintf "equalities:\n%s\n" - (String.concat "\n" - (List.map string_of_equality equalities)))); + debug_print + (lazy + (Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities)))); debug_print (lazy "SIMPLYFYING EQUALITIES..."); let rec simpl e others others_simpl = let active = others @ others_simpl in @@ -1130,16 +1784,18 @@ let main dbd term metasenv ugraph = let res = List.rev (List.map snd (simpl (Positive, hd) others [])) in - debug_print (lazy ( - Printf.sprintf "equalities AFTER:\n%s\n" - (String.concat "\n" - (List.map string_of_equality res)))); + debug_print + (lazy + (Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res)))); res in let active = make_active () in - let passive = make_passive [term_equality] equalities in + let passive = make_passive [] (* [term_equality] *) equalities in Printf.printf "\ncurrent goal: %s\n" - (string_of_equality ~env term_equality); + (let _, _, g = goal in CicPp.ppterm g); +(* (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" @@ -1153,28 +1809,22 @@ let main dbd term metasenv ugraph = start_time := Unix.gettimeofday (); let res = (if !use_fullred then given_clause_fullred else given_clause) - env passive active + env [0, [goal]] theorems 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 proof = *) -(* (\* let p = CicSubstitution.lift 1 proof in *\) *) -(* let rec repl i = function *) -(* | C.Meta _ -> C.Rel i *) -(* | C.Appl l -> C.Appl (List.map (repl i) l) *) -(* | C.Prod (n, s, t) -> C.Prod (n, s, repl (i+1) t) *) -(* | C.Lambda (n, s, t) -> C.Lambda (n, s, repl (i+1) t) *) -(* | t -> t *) -(* in *) -(* let p = repl 1 proof in *) -(* p *) -(* (\* C.Lambda (C.Anonymous, C.Rel 9, p) *\) *) -(* in *) + | ParamodulationSuccess (Some proof (* goal *), env) -> +(* let proof = Inference.build_proof_term goal in *) + let proof = Inference.build_proof_term proof 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); let newmetasenv = List.fold_left (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities @@ -1238,108 +1888,124 @@ let main dbd term metasenv ugraph = ;; -let saturate dbd ?(full=false) ?(depth=0) ?(width=0) (proof, goal) = +let default_depth = !maxdepth +and default_width = !maxwidth;; + +let saturate + dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in maxmeta := 0; + maxdepth := depth; + maxwidth := width; + let proof, goal = status 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 + let eq_indexes, equalities, maxm = find_equalities context proof in 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 (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty))); + debug_print + (lazy (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 goal = Inference.BasicProof new_meta_goal, [], goal in let res, time = - 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), 0.) - else - let library_equalities, maxm = - find_library_equalities ~dbd context (proof, goal') (maxm+2) + let lib_eq_uris, library_equalities, maxm = + find_library_equalities dbd context (proof, goal') (maxm+2) + in + maxmeta := maxm+2; + let equalities = + let equalities = equalities @ library_equalities in + debug_print + (lazy + (Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities)))); + debug_print (lazy "SIMPLYFYING EQUALITIES..."); + let rec simpl e others others_simpl = + let active = others @ others_simpl in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + (Indexing.empty_table ()) active + in + let res = forward_simplify env e (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl (e::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> e::others_simpl + ) in - maxmeta := maxm+2; - let equalities = - let equalities = equalities @ library_equalities in - debug_print (lazy ( - Printf.sprintf "equalities:\n%s\n" - (String.concat "\n" - (List.map string_of_equality equalities)))); - debug_print (lazy "SIMPLYFYING EQUALITIES..."); - let rec simpl e others others_simpl = - let active = others @ others_simpl in - let tbl = - List.fold_left - (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + match equalities with + | [] -> [] + | hd::tl -> + let others = List.map (fun e -> (Positive, e)) tl in + let res = + List.rev (List.map snd (simpl (Positive, hd) others [])) in - let res = forward_simplify env e (active, tbl) in - match others with - | hd::tl -> ( - match res with - | None -> simpl hd tl others_simpl - | Some e -> simpl hd tl (e::others_simpl) - ) - | [] -> ( - match res with - | None -> others_simpl - | Some e -> e::others_simpl - ) + debug_print + (lazy + (Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res)))); + res + in + let theorems = + if full then + let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in + let context_hyp = find_context_hypotheses env eq_indexes in + context_hyp @ thms + else + let refl_equal = + UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in - match equalities with - | [] -> [] - | hd::tl -> - let others = List.map (fun e -> (Positive, e)) tl in - let res = - List.rev (List.map snd (simpl (Positive, hd) others [])) - in - debug_print (lazy ( - Printf.sprintf "equalities AFTER:\n%s\n" - (String.concat "\n" - (List.map string_of_equality res)))); - res - in - let active = make_active () in - let passive = make_passive [term_equality] equalities in - let start = Unix.gettimeofday () in - let res = given_clause_fullred env passive active in - let finish = Unix.gettimeofday () in - (res, finish -. start) + let t = CicUtil.term_of_uri refl_equal in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + [(t, ty, [])] + in + let _ = + debug_print + (lazy + (Printf.sprintf + "Theorems:\n-------------------------------------\n%s\n" + (String.concat "\n" + (List.map + (fun (t, ty, _) -> + Printf.sprintf + "Term: %s, type: %s" + (CicPp.ppterm t) (CicPp.ppterm ty)) + theorems)))) + in + let active = make_active () in + let passive = make_passive [(* term_equality *)] equalities in + let start = Unix.gettimeofday () in + let res = given_clause_fullred env [0, [goal]] theorems passive active in + let finish = Unix.gettimeofday () in + (res, finish -. start) in match res with - | ParamodulationSuccess (Some goal, env) -> + | ParamodulationSuccess (Some proof (* goal *), env) -> debug_print (lazy "OK, found a proof!"); - let proof = Inference.build_proof_term goal in +(* let proof = Inference.build_proof_term goal in *) + let proof = Inference.build_proof_term proof 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 = @@ -1348,13 +2014,14 @@ let saturate dbd ?(full=false) ?(depth=0) ?(width=0) (proof, goal) = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in debug_print (lazy (CicPp.pp proof [](* names *))); - debug_print (lazy - (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))))); + debug_print + (lazy + (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 @@ -1366,13 +2033,14 @@ let saturate dbd ?(full=false) ?(depth=0) ?(width=0) (proof, goal) = ~what:[goal'] ~with_what:[proof] ~where:meta_proof in - debug_print (lazy ( - 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))); + debug_print + (lazy + (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 (lazy "THE PROOF DOESN'T TYPECHECK!!!"); @@ -1384,11 +2052,8 @@ let saturate dbd ?(full=false) ?(depth=0) ?(width=0) (proof, goal) = newstatus | _ -> raise (ProofEngineTypes.Fail "NO proof found") -(* with e -> *) -(* raise (Failure "saturation failed") *) ;; - (* dummy function called within matita to trigger linkage *) let init () = ();; @@ -1398,3 +2063,4 @@ if connect_to_auto then ( AutoTactic.paramodulation_tactic := saturate; AutoTactic.term_is_equality := Inference.term_is_equality; );; + diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 681a371e1..2d5ee24ce 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -289,9 +289,10 @@ let rec aux_ordering ?(recursion=true) t1 t2 = aux_ordering h1 h2 | t1, t2 -> - debug_print (lazy ( - Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n" - (CicPp.ppterm t1) (CicPp.ppterm t2))); + debug_print + (lazy + (Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n" + (CicPp.ppterm t1) (CicPp.ppterm t2))); Incomparable ;; -- 2.39.2