From b24260fd5c00791ad04042405e3942f288f54ab2 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Mon, 18 Jul 2005 09:15:55 +0000 Subject: [PATCH] adding library support (not ready yet) --- helm/ocaml/paramodulation/inference.ml | 62 ++++++++++++++++ helm/ocaml/paramodulation/inference.mli | 4 +- helm/ocaml/paramodulation/saturation.ml | 85 +++++++++++++++++++++- helm/ocaml/paramodulation/test_indexing.ml | 19 ++++- 4 files changed, 161 insertions(+), 9 deletions(-) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 38bc6abe5..1252c6069 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1117,6 +1117,66 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = ;; +let find_library_equalities ~(dbd:Mysql.dbd) status maxmeta = + let module C = Cic in + let module S = CicSubstitution in + let module T = CicTypeChecker in + let candidates = + List.map + (fun uri -> + let t = CicUtil.term_of_uri uri in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + t, ty) + (MetadataQuery.equations_for_goal ~dbd status) + in + let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI + and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in + let iseq uri = + uri == eq_uri1 || uri == eq_uri2 + in + let rec aux newmeta = function + | [] -> [], newmeta + | (term, termty)::tl -> + let res, newmeta = + match termty with + | C.Prod (name, s, t) -> + let head, newmetas, args, newmeta = + ProofEngineHelpers.saturate_term newmeta [] [] termty + in + let p = + if List.length args = 0 then + term + else + C.Appl (term::args) + in ( + match head with + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> + Printf.printf "OK: %s\n" (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 + let e = (w, proof, (ty, t1, t2, o), newmetas, args) in + Some e, (newmeta+1) + | _ -> None, newmeta + ) + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> + let o = !Utils.compare_terms t1 t2 in + let w = compute_equality_weight ty t1 t2 in + let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in + Some e, (newmeta+1) + | _ -> None, newmeta + in + match res with + | Some e -> + let tl, newmeta' = aux newmeta tl in + e::tl, max newmeta newmeta' + | None -> + aux newmeta tl + in + aux maxmeta candidates +;; + + let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = (* print_endline ("fix_metas " ^ (string_of_int newmeta)); *) let table = Hashtbl.create (List.length args) in @@ -1667,3 +1727,5 @@ let extract_differing_subterms t1 t2 = | hd::[] -> Some hd | _ -> None ;; + + diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 76d48603d..0695fbc9e 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -100,5 +100,7 @@ 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 find_library_equalities: + dbd:Mysql.dbd -> ProofEngineTypes.status -> int -> equality list * int diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index a6c4fc8ad..94f26a7e6 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -986,9 +986,7 @@ let rec given_clause_fullred env passive active = ;; -let get_from_user () = - let dbd = Mysql.quick_connect - ~host:"localhost" ~user:"helm" ~database:"mowgli" () in +let get_from_user ~(dbd:Mysql.dbd) = let rec get () = match read_line () with | "" -> [] @@ -1010,7 +1008,9 @@ let main () = let module T = CicTypeChecker in let module PET = ProofEngineTypes in let module PP = CicPp in - let term, metasenv, ugraph = get_from_user () 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,6 +1018,8 @@ 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 maxmeta := maxm+2; (* TODO ugly!! *) let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let new_meta_goal, metasenv, type_of_goal = @@ -1113,6 +1115,81 @@ let main () = ;; +let saturation_tactic status = + 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 + 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 + in + let i2 = + match meta_proof with + | C.Meta (i, _) -> i | _ -> assert 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 configuration_file = ref "../../matita/matita.conf.xml";; let _ = diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml index 7391812f3..5681a5d08 100644 --- a/helm/ocaml/paramodulation/test_indexing.ml +++ b/helm/ocaml/paramodulation/test_indexing.ml @@ -210,11 +210,11 @@ let test_refl () = ] ] in let ens = [ - (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", + (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", C.Rel 4); - (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", + (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", C.Rel 3); - (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", + (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", C.Rel 2); ] in let term2 = C.Appl [ @@ -231,10 +231,21 @@ let test_refl () = Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term2) (CicPp.ppterm ty); ;; + +let test_lib () = + let uri = Sys.argv.(1) in + let t = CicUtil.term_of_uri (UriManager.uri_of_string uri) in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + Printf.printf "Term of %s: %s\n" uri (CicPp.ppterm t); + Printf.printf "type: %s\n" (CicPp.ppterm ty); +;; + + (* differing ();; *) (* next_after ();; *) (* discrimination_tree_test ();; *) (* path_indexing_test ();; *) (* test_subst ();; *) Helm_registry.load_from "../../matita/matita.conf.xml"; -test_refl ();; +(* test_refl ();; *) +test_lib ();; -- 2.39.2