From c9d7e6a946744890def5b5471c93b4dbd78c4ac9 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Thu, 30 Jun 2005 16:05:34 +0000 Subject: [PATCH] proofs are now built lazily at the end of the computation --- helm/ocaml/paramodulation/Makefile | 1 + helm/ocaml/paramodulation/indexing.ml | 26 +++++--- helm/ocaml/paramodulation/inference.ml | 83 ++++++++++++++++++++----- helm/ocaml/paramodulation/inference.mli | 18 +++++- helm/ocaml/paramodulation/saturation.ml | 79 ++++++++++++++--------- 5 files changed, 151 insertions(+), 56 deletions(-) diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index a34ec0c2b..9d30e7020 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -31,6 +31,7 @@ INTERFACE_FILES = \ DEPOBJS = \ $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \ + trie.ml \ path_indexing.ml \ discrimination_tree.ml \ test_indexing.ml \ diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 5a8960101..6425e3c82 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -399,7 +399,7 @@ let rec demodulation newmeta env table target = in let t' = C.Lambda (C.Anonymous, ty, bo'') in bo, - C.Implicit None + Inference.ProofBlock (subst, eq_URI, t', eq_found, target) (* (\* M. *\)apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t'; *) (* proof; other; proof']) *) in @@ -417,8 +417,12 @@ let rec demodulation newmeta env table target = let time2 = Unix.gettimeofday () in build_newtarget_time := !build_newtarget_time +. (time2 -. time1); - - newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs) + + let res = + (C.Implicit None, (eq_ty, left, right, ordering), newmetasenv, newargs) + in + Inference.store_proof res newproof; + newmeta, res in (* let build_newtarget = *) (* let profile = CicUtil.profile "Indexing.demodulation.build_newtarget" in *) @@ -586,7 +590,7 @@ let superposition_left (metasenv, context, ugraph) table target = in let t' = C.Lambda (C.Anonymous, ty, bo'') in bo', - C.Implicit None + Inference.ProofBlock (s, eq_URI, t', eq_found, target) (* (\* M. *\)apply_subst s *) (* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *) (* proof; other; proof']) *) @@ -597,8 +601,10 @@ let superposition_left (metasenv, context, ugraph) table target = let time2 = Unix.gettimeofday () in build_newtarget_time := !build_newtarget_time +. (time2 -. time1); - - (newproof, (eq_ty, left, right, neworder), [], []) + + let res = (C.Implicit None, (eq_ty, left, right, neworder), [], []) in + Inference.store_proof res newproof; + res in (* let build_new = *) (* let profile = CicUtil.profile "Inference.superposition_left.build_new" in *) @@ -649,7 +655,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = in let t' = C.Lambda (C.Anonymous, ty, bo'') in bo', - C.Implicit None + Inference.ProofBlock (s, eq_URI, t', eq_found, target) (* (\* M. *\)apply_subst s *) (* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *) (* eqproof; other; proof']) *) @@ -661,7 +667,8 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let neworder = !Utils.compare_terms left right and newmenv = newmetas @ menv' and newargs = args @ args' in - let eq' = (newproof, (eq_ty, left, right, neworder), newmenv, newargs) + let eq' = + (C.Implicit None, (eq_ty, left, right, neworder), newmenv, newargs) and env = (metasenv, context, ugraph) in let newm, eq' = Inference.fix_metas !maxmeta eq' in newm, eq' @@ -670,7 +677,8 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let time2 = Unix.gettimeofday () in build_newtarget_time := !build_newtarget_time +. (time2 -. time1); - + + Inference.store_proof newequality newproof; newequality in diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index d8ff4a7d9..163fabddb 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1,6 +1,26 @@ open Utils;; +type equality = + Cic.term * (* proof *) + (Cic.term * (* type *) + Cic.term * (* left side *) + Cic.term * (* right side *) + Utils.comparison) * (* ordering *) + Cic.metasenv * (* environment for metas *) + Cic.term list (* arguments *) +;; + + +type proof = + | BasicProof of Cic.term + | ProofBlock of + Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) * + equality + | NoProof +;; + + let string_of_equality ?env = match env with | None -> ( @@ -20,6 +40,45 @@ let string_of_equality ?env = ;; +let prooftable = Hashtbl.create 2001;; + +let store_proof equality proof = + if not (Hashtbl.mem prooftable equality) then + Hashtbl.add prooftable equality proof +;; + + +let delete_proof equality = +(* Printf.printf "| Removing proof of %s" (string_of_equality equality); *) +(* print_newline (); *) + Hashtbl.remove prooftable equality +;; + + +let rec build_term_proof equality = +(* Printf.printf "build_term_proof %s" (string_of_equality equality); *) +(* print_newline (); *) + let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in + match proof with + | NoProof -> + Printf.fprintf stderr "WARNING: no proof for %s\n" + (string_of_equality equality); + Cic.Implicit None + | BasicProof term -> term + | ProofBlock (subst, eq_URI, t', (pos, eq), eq') -> +(* Printf.printf " ProofBlock: eq = %s, eq' = %s" *) +(* (string_of_equality eq) (string_of_equality eq'); *) +(* print_newline (); *) + let proof' = build_term_proof eq in + let eqproof = build_term_proof eq' in + let _, (ty, what, other, _), menv', args' = eq in + let what, other = if pos = Utils.Left then what, other else other, what in + CicMetaSubst.apply_subst subst + (Cic.Appl [Cic.Const (eq_URI, []); ty; + what; t'; eqproof; other; proof']) +;; + + let rec metas_of_term = function | Cic.Meta (i, c) -> [i] | Cic.Var (_, ens) @@ -933,17 +992,6 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) ;; -type equality = - Cic.term * (* proof *) - (Cic.term * (* type *) - Cic.term * (* left side *) - Cic.term * (* right side *) - Utils.comparison) * (* ordering *) - Cic.metasenv * (* environment for metas *) - Cic.term list (* arguments *) -;; - - let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = let module C = Cic in let module S = CicSubstitution in @@ -978,14 +1026,18 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> Printf.printf "OK: %s\n" (CicPp.ppterm term); let o = !Utils.compare_terms t1 t2 in - Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1) + let e = (p, (ty, t1, t2, o), newmetas, args) in + store_proof e (BasicProof p); + Some e, (newmeta+1) | _ -> None, newmeta ) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> let t1 = S.lift index t1 and t2 = S.lift index t2 in let o = !Utils.compare_terms t1 t2 in - Some (C.Rel index, (ty, t1, t2, o), [], []), (newmeta+1) + let e = (C.Rel index, (ty, t1, t2, o), [], []) in + store_proof e (BasicProof (C.Rel index)); + Some e, (newmeta+1) | _ -> None, newmeta in ( match do_find context term with @@ -1047,7 +1099,10 @@ exception TermIsNotAnEquality;; let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> let o = !Utils.compare_terms t1 t2 in - (proof, (ty, t1, t2, o), [], []) + let e = (proof, (ty, t1, t2, o), [], []) in + store_proof e (BasicProof proof); + e +(* (proof, (ty, t1, t2, o), [], []) *) | _ -> raise TermIsNotAnEquality ;; diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 42fc39bf3..74194e84a 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -6,9 +6,16 @@ type equality = Utils.comparison) * (* ordering *) Cic.metasenv * (* environment for metas *) Cic.term list (* arguments *) -;; -type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; +type proof = + | BasicProof of Cic.term + | ProofBlock of + Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) * + equality + | NoProof + + +type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph exception MatchingFailure @@ -87,3 +94,10 @@ val fix_metas: int -> equality -> int * equality val extract_differing_subterms: Cic.term -> Cic.term -> (Cic.term * Cic.term) option + + +val store_proof: equality -> proof -> unit + +val delete_proof: equality -> unit + +val build_term_proof: equality -> Cic.term diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index d8019cae8..793e48423 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -34,7 +34,7 @@ let maxmeta = ref 0;; type result = | Failure - | Success of Cic.term option * environment + | Success of Inference.equality option * environment ;; @@ -415,13 +415,13 @@ let infer env sign current (active_list, active_table) = let contains_empty env (negative, positive) = let metasenv, context, ugraph = env in try - let (proof, _, _, _) = + let found = List.find (fun (proof, (ty, left, right, ordering), m, a) -> fst (CicReduction.are_convertible context left right ugraph)) negative in - true, Some proof + true, Some found with Not_found -> false, None ;; @@ -461,7 +461,8 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = Indexing.demodulation !maxmeta env table current in maxmeta := newmeta; if is_identity env newcurrent then - if sign = Negative then Some (sign, newcurrent) else None + if sign = Negative then Some (sign, newcurrent) + else (Inference.delete_proof newcurrent; None) else Some (sign, newcurrent) in @@ -485,12 +486,14 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = if ok then res else None | Some (Positive, c) -> if Indexing.in_index active_table c then - None + (Inference.delete_proof c; None) else match passive_table with | None -> res | Some passive_table -> - if Indexing.in_index passive_table c then None else res + if Indexing.in_index passive_table c then + (Inference.delete_proof c; None) + else res (* | Some (s, c) -> if find_duplicate s c all then None else res *) @@ -571,7 +574,13 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let new_pos_set = List.fold_left (fun s e -> - if not (Inference.is_identity env e) then EqualitySet.add e s else s) + if not (Inference.is_identity env e) then + if EqualitySet.mem e s then + (Inference.delete_proof e; s) + else + EqualitySet.add e s + else + (Inference.delete_proof e; s)) EqualitySet.empty new_pos in let new_pos = EqualitySet.elements new_pos_set in @@ -602,10 +611,17 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let is_duplicate = match passive_table with - | None -> (fun e -> not (Indexing.in_index active_table e)) + | None -> + (fun e -> + let ok = not (Indexing.in_index active_table e) in + if not ok then Inference.delete_proof e; + ok) | Some passive_table -> - (fun e -> not ((Indexing.in_index active_table e) || - (Indexing.in_index passive_table e))) + (fun e -> + let ok = not ((Indexing.in_index active_table e) || + (Indexing.in_index passive_table e)) in + if not ok then Inference.delete_proof e; + ok) in new_neg, List.filter is_duplicate new_pos @@ -639,16 +655,22 @@ let backward_simplify_active env new_pos new_table active = let active, newa = List.fold_right (fun (s, eq) (res, tbl) -> - if (is_identity env eq) || (find eq res) then + if List.mem (s, eq) res then res, tbl + else if (is_identity env eq) || (find eq res) then ( + Inference.delete_proof eq; + res, tbl + ) (* else if (find eq res) then *) +(* res, tbl *) else (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) active_list ([], Indexing.empty_table ()), List.fold_right (fun (s, eq) (n, p) -> - if (s <> Negative) && (is_identity env eq) then + if (s <> Negative) && (is_identity env eq) then ( + Inference.delete_proof eq; (n, p) - else + ) else if s = Negative then eq::n, p else n, eq::p) newa ([], []) @@ -750,8 +772,7 @@ let rec given_clause env passive active = Printf.printf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current); print_newline (); - let proof, _, _, _ = current in - Success (Some proof, env) + Success (Some current, env) ) else ( print_endline "\n================================================"; Printf.printf "selected: %s %s" @@ -763,9 +784,9 @@ let rec given_clause env passive active = let t2 = Unix.gettimeofday () in infer_time := !infer_time +. (t2 -. t1); - let res, proof = contains_empty env new' in + let res, goal = contains_empty env new' in if res then - Success (proof, env) + Success (goal, env) else let t1 = Unix.gettimeofday () in let new' = forward_simplify_new env new' (* ~passive *) active in @@ -839,8 +860,8 @@ let rec given_clause env passive active = (* (EqualitySet.elements ps)))); *) (* print_newline (); *) given_clause env passive active - | true, proof -> - Success (proof, env) + | true, goal -> + Success (goal, env) ) ;; @@ -886,8 +907,7 @@ let rec given_clause_fullred env passive active = Printf.printf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current); print_newline (); - let proof, _, _, _ = current in - Success (Some proof, env) + Success (Some current, env) ) else ( print_endline "\n================================================"; Printf.printf "selected: %s %s" @@ -958,8 +978,8 @@ let rec given_clause_fullred env passive active = | false, _ -> let passive = add_to_passive passive new' in given_clause_fullred env passive active - | true, proof -> - Success (proof, env) + | true, goal -> + Success (goal, env) ) ;; @@ -1025,14 +1045,11 @@ let main () = match res with | Failure -> Printf.printf "NO proof found! :-(\n\n" - | Success (Some proof, env) -> - Printf.printf "OK, found a proof!:\n%s\n%.9f\n" - (PP.pp proof (names_of_context context)) - (finish -. start); -(* Printf.printf ("forward_simpl_details:\n build_all: %.9f\n" ^^ *) -(* " demodulate: %.9f\n subsumption: %.9f\n") *) -(* fs_time_info.build_all fs_time_info.demodulate *) -(* fs_time_info.subsumption; *) + | Success (Some goal, env) -> + Printf.printf "OK, found a proof!\n"; + let proof = Inference.build_term_proof goal in + print_endline (PP.pp proof (names_of_context context)); + print_endline (string_of_float (finish -. start)); | Success (None, env) -> Printf.printf "Success, but no proof?!?\n\n" in -- 2.39.2