From c1a270db687e5cea3410b10634728c6ec57d2caa Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Wed, 21 Sep 2005 12:03:32 +0000 Subject: [PATCH] bugfix on proof construction --- helm/ocaml/paramodulation/Makefile | 2 +- helm/ocaml/paramodulation/indexing.ml | 328 +++++++++++++++------ helm/ocaml/paramodulation/inference.ml | 120 ++++---- helm/ocaml/paramodulation/inference.mli | 7 +- helm/ocaml/paramodulation/saturate_main.ml | 4 +- helm/ocaml/paramodulation/saturation.ml | 33 ++- 6 files changed, 335 insertions(+), 159 deletions(-) diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index 1d47d3cb0..88d313d3c 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -1,6 +1,6 @@ PACKAGE = paramodulation -REQUIRES = helm-tactics +REQUIRES = helm-tactics helm-cic_disambiguation INTERFACE_FILES = \ utils.mli \ diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 5b84bb72a..3361f5a3b 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -1,3 +1,27 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) let debug_print = Utils.debug_print;; @@ -187,7 +211,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = (* (\* (CicPp.pp termty names) (CicPp.pp ty names))); *\) *) (* find_matches metasenv context ugraph lift_amount term termty tl *) (* ) else *) - let do_match c other eq_URI = + let do_match c (* other *) eq_URI = let subst', metasenv', ugraph' = let t1 = Unix.gettimeofday () in try @@ -211,12 +235,12 @@ let rec find_matches metasenv context ugraph lift_amount term termty = in if o <> U.Incomparable then try - do_match c other eq_URI + do_match c (* other *) eq_URI with Inference.MatchingFailure -> find_matches metasenv context ugraph lift_amount term termty tl else let res = - try do_match c other eq_URI + try do_match c (* other *) eq_URI with Inference.MatchingFailure -> None in match res with @@ -246,6 +270,11 @@ let rec find_all_matches ?(unif_fun=Inference.unification) (* let names = Utils.names_of_context context in *) (* let termty, ugraph = *) (* CicTypeChecker.type_of_aux' metasenv context term ugraph *) +(* in *) +(* let _ = *) +(* match term with *) +(* | C.Meta _ -> assert false *) +(* | _ -> () *) (* in *) function | [] -> [] @@ -259,7 +288,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) (* find_all_matches ~unif_fun metasenv context ugraph *) (* lift_amount term termty tl *) (* ) else *) - let do_match c other eq_URI = + let do_match c (* other *) eq_URI = let subst', metasenv', ugraph' = let t1 = Unix.gettimeofday () in try @@ -286,7 +315,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) in if o <> U.Incomparable then try - let res = do_match c other eq_URI in + let res = do_match c (* other *) eq_URI in res::(find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl) with @@ -297,7 +326,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) lift_amount term termty tl else try - let res = do_match c other eq_URI in + let res = do_match c (* other *) eq_URI in match res with | _, s, _, _, _ -> let c' = (* M. *)apply_subst s c @@ -441,6 +470,26 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = Some (C.Prod (nn, s', (S.lift 1 t)), subst, menv, ug, eq_found) ) + | C.Lambda (nn, s, t) -> + let r1 = + demodulate_term metasenv context ugraph table lift_amount s in ( + match r1 with + | None -> + let r2 = + demodulate_term metasenv + ((Some (nn, C.Decl s))::context) ugraph + table (lift_amount+1) t + in ( + match r2 with + | None -> None + | Some (t', subst, menv, ug, eq_found) -> + Some (C.Lambda (nn, (S.lift 1 s), t'), + subst, menv, ug, eq_found) + ) + | Some (s', subst, menv, ug, eq_found) -> + Some (C.Lambda (nn, s', (S.lift 1 t)), + subst, menv, ug, eq_found) + ) | t -> None ;; @@ -476,19 +525,30 @@ let rec demodulation newmeta env table sign target = let time1 = Unix.gettimeofday () in let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in + let ty, _ = + CicTypeChecker.type_of_aux' metasenv context what ugraph + in let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newproof = let bo = (* M. *)apply_subst subst (S.subst other t) in - let t' = - let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in - incr demod_counter; - let l, r = - if is_left then t, S.lift 1 right else S.lift 1 left, t in - (name, ty, S.lift 1 eq_ty, l, r) +(* let t' = *) +(* let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in *) +(* incr demod_counter; *) +(* let l, r = *) +(* if is_left then t, S.lift 1 right else S.lift 1 left, t in *) +(* (name, ty, S.lift 1 eq_ty, l, r) *) +(* in *) + let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in + incr demod_counter; + let bo' = + let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in + C.Appl [C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + S.lift 1 eq_ty; l; r] in if sign = Utils.Positive then (bo, - Inference.ProofBlock (subst, eq_URI, t', eq_found, proof)) + Inference.ProofBlock ( + subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof)) else let metaproof = incr maxmeta; @@ -498,7 +558,7 @@ let rec demodulation newmeta env table sign target = print_newline (); C.Meta (!maxmeta, irl) in - let target' = +(* let target' = *) let eq_found = let proof' = let ens = @@ -517,35 +577,45 @@ let rec demodulation newmeta env table sign target = in let target_proof = let pb = - Inference.ProofBlock (subst, eq_URI, t', eq_found, - Inference.BasicProof metaproof) + Inference.ProofBlock (subst, eq_URI, (name, ty), bo'(* t' *), + eq_found, Inference.BasicProof metaproof) in match proof with | Inference.BasicProof _ -> print_endline "replacing a BasicProof"; pb - | Inference.ProofGoalBlock (_, parent_eq) -> + | Inference.ProofGoalBlock (_, parent_proof(* parent_eq *)) -> print_endline "replacing another ProofGoalBlock"; - Inference.ProofGoalBlock (pb, parent_eq) + Inference.ProofGoalBlock (pb, parent_proof(* parent_eq *)) | _ -> assert false in - (0, target_proof, (eq_ty, left, right, order), metas, args) - in +(* (0, target_proof, (eq_ty, left, right, order), metas, args) *) +(* in *) let refl = C.Appl [C.MutConstruct (* reflexivity *) (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); eq_ty; if is_left then right else left] in (bo, - Inference.ProofGoalBlock (Inference.BasicProof refl, target')) + Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof(* target' *))) in let left, right = if is_left then newterm, right else left, newterm in let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas - and newargs = - List.filter - (function C.Meta (i, _) -> List.mem i m | _ -> assert false) - args + and newargs = args +(* let a = *) +(* List.filter *) +(* (function C.Meta (i, _) -> List.mem i m | _ -> assert false) args in *) +(* let delta = (List.length args) - (List.length a) in *) +(* if delta > 0 then *) +(* let first = List.hd a in *) +(* let rec aux l = function *) +(* | 0 -> l *) +(* | d -> let l = aux l (d-1) in l @ [first] *) +(* in *) +(* aux a delta *) +(* else *) +(* a *) in let ordering = !Utils.compare_terms left right in @@ -556,19 +626,9 @@ let rec demodulation newmeta env table sign target = let w = Utils.compute_equality_weight eq_ty left right in (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs) in -(* if sign = Utils.Positive then ( *) -(* let newm, res = Inference.fix_metas !maxmeta res in *) -(* maxmeta := newm; *) -(* !maxmeta, res *) -(* ) else *) - !maxmeta(* newmeta *), res + !maxmeta, res in let res = demodulate_term metasenv' context ugraph table 0 left in -(* let build_identity (w, p, (t, l, r, o), m, a) = *) -(* match o with *) -(* | Utils.Gt -> (w, p, (t, r, r, Utils.Eq), m, a) *) -(* | _ -> (w, p, (t, l, l, Utils.Eq), m, a) *) -(* in *) match res with | Some t -> let newmeta, newtarget = build_newtarget true t in @@ -607,7 +667,7 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = let res, lifted_term = match term with | C.Meta (i, l) -> - let l', lifted_l = + let l', lifted_l = List.fold_right (fun arg (res, lifted_tl) -> match arg with @@ -630,11 +690,11 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = | None -> (List.map (fun (r, s, m, ug, eq_found) -> - None::r, s, m, ug, eq_found) res, + None::r, s, m, ug, eq_found) res, None::lifted_tl) ) l ([], []) in - let e = + let e = List.map (fun (l, s, m, ug, eq_found) -> (C.Meta (i, l), s, m, ug, eq_found)) l' @@ -660,6 +720,22 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in l1' @ l2', C.Prod (nn, lifted_s, lifted_t) + | C.Lambda (nn, s, t) -> + let l1, lifted_s = + betaexpand_term metasenv context ugraph table lift_amount s in + let l2, lifted_t = + betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph + table (lift_amount+1) t in + let l1' = + List.map + (fun (t, s, m, ug, eq_found) -> + C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1 + and l2' = + List.map + (fun (t, s, m, ug, eq_found) -> + C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in + l1' @ l2', C.Lambda (nn, lifted_s, lifted_t) + | C.Appl l -> let l', lifted_l = List.fold_right @@ -688,7 +764,7 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = | t -> [], (S.lift lift_amount t) in match term with - | C.Meta _ -> res, lifted_term + | C.Meta (i, l) -> res, lifted_term | term -> let termty, ugraph = C.Implicit None, ugraph @@ -727,32 +803,27 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = let what, other = if pos = Utils.Left then what, other else other, what in let newgoal, newproof = let bo' = (* M. *)apply_subst s (S.subst other bo) in - let t' = - let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in - incr sup_l_counter; - let l, r = - if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in - (name, ty, S.lift 1 eq_ty, l, r) - in -(* let bo'' = *) -(* C.Appl ( *) -(* [C.MutInd (HL.Logic.eq_URI, 0, []); *) -(* S.lift 1 eq_ty] @ *) -(* if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *) -(* else [S.lift 1 left; S.lift 1 bo']) *) -(* in *) (* let t' = *) (* let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in *) (* incr sup_l_counter; *) -(* C.Lambda (name, ty, bo'') *) +(* let l, r = *) +(* if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in *) +(* (name, ty, S.lift 1 eq_ty, l, r) *) (* in *) + let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in + incr sup_l_counter; + let bo'' = + let l, r = + if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in + C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty; l; r] + in incr maxmeta; let metaproof = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in C.Meta (!maxmeta, irl) in - let target' = +(* let target' = *) let eq_found = let proof' = let ens = @@ -770,27 +841,27 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = in let target_proof = let pb = - Inference.ProofBlock (s, eq_URI, t', eq_found, + Inference.ProofBlock (s, eq_URI, (name, ty), bo''(* t' *), eq_found, Inference.BasicProof metaproof) in match proof with | Inference.BasicProof _ -> print_endline "replacing a BasicProof"; pb - | Inference.ProofGoalBlock (_, parent_eq) -> + | Inference.ProofGoalBlock (_, parent_proof(* parent_eq *)) -> print_endline "replacing another ProofGoalBlock"; - Inference.ProofGoalBlock (pb, parent_eq) + Inference.ProofGoalBlock (pb, parent_proof(* parent_eq *)) | _ -> assert false in - (weight, target_proof, (eq_ty, left, right, ordering), [], []) - in +(* (weight, target_proof, (eq_ty, left, right, ordering), [], []) *) +(* in *) let refl = C.Appl [C.MutConstruct (* reflexivity *) (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); eq_ty; if ordering = U.Gt then right else left] in (bo', - Inference.ProofGoalBlock (Inference.BasicProof refl, target')) + Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof(* target' *))) in let left, right = if ordering = U.Gt then newgoal, right else left, newgoal in @@ -851,22 +922,16 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in (name, ty, S.lift 1 eq_ty, l, r) in -(* let bo'' = *) -(* C.Appl ( *) -(* [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ *) -(* if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *) -(* else [S.lift 1 left; S.lift 1 bo']) *) -(* in *) -(* let t' = *) -(* let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in *) -(* incr sup_r_counter; *) -(* C.Lambda (name, ty, bo'') *) -(* in *) + let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in + incr sup_r_counter; + let bo'' = + let l, r = + if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in + C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty; l; r] + in bo', - Inference.ProofBlock (s, eq_URI, t', eq_found, eqproof(* target *)) -(* (\* M. *\)apply_subst s *) -(* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *) -(* eqproof; other; proof']) *) + Inference.ProofBlock ( + s, eq_URI, (name, ty), bo''(* t' *), eq_found, eqproof) in let newmeta, newequality = let left, right = @@ -875,6 +940,24 @@ 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 m = *) +(* (Inference.metas_of_term left) @ (Inference.metas_of_term right) in *) +(* let a = *) +(* List.filter *) +(* (function C.Meta (i, _) -> List.mem i m | _ -> assert false) *) +(* (args @ args') *) +(* in *) +(* let delta = (List.length args) - (List.length a) in *) +(* if delta > 0 then *) +(* let first = List.hd a in *) +(* let rec aux l = function *) +(* | 0 -> l *) +(* | d -> let l = aux l (d-1) in l @ [first] *) +(* in *) +(* aux a delta *) +(* else *) +(* a *) +(* in *) let eq' = let w = Utils.compute_equality_weight eq_ty left right in (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) @@ -889,18 +972,89 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = newequality in - -(* let build_new = *) -(* let profile = CicUtil.profile "Indexing.superposition_right.build_new" in *) -(* (fun o e -> profile.profile (build_new o) e) *) -(* in *) - let new1 = List.map (build_new U.Gt) res1 and new2 = List.map (build_new U.Lt) res2 in - let ok = function - | _, _, (_, left, right, _), _, _ -> - not (fst (CR.are_convertible context left right ugraph)) - in +(* let ok = function *) +(* | _, _, (_, left, right, _), _, _ -> *) +(* not (fst (CR.are_convertible context left right ugraph)) *) +(* in *) + let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in (!maxmeta, (List.filter ok (new1 @ new2))) ;; + + +let rec demodulation_goal newmeta env table goal = + 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 = goal in + let metasenv' = metasenv @ metas in + + 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 newterm, newproof = + let bo = (* M. *)apply_subst subst (S.subst other t) in + let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in + incr demod_counter; + let metaproof = + incr maxmeta; + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + Printf.printf "\nADDING META: %d\n" !maxmeta; + print_newline (); + C.Meta (!maxmeta, irl) + in + let eq_found = + let proof' = + let ens = + if pos = Utils.Left then build_ens_for_sym_eq ty what other + else build_ens_for_sym_eq ty other what + in + Inference.ProofSymBlock (ens, proof') + in + let what, other = + if pos = Utils.Left then what, other else other, what + in + pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args') + in + let goal_proof = + let pb = + Inference.ProofBlock (subst, eq_URI, (name, ty), bo, + eq_found, Inference.BasicProof metaproof) + in + match proof with + | Inference.NoProof -> + debug_print "replacing a NoProof"; + pb + | Inference.BasicProof _ -> + debug_print "replacing a BasicProof"; + pb + | Inference.ProofGoalBlock (_, parent_proof) -> + debug_print "replacing another ProofGoalBlock"; + Inference.ProofGoalBlock (pb, parent_proof) + | _ -> assert false + 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 + match res with + | Some t -> + let newmeta, newgoal = build_newgoal t in + let _, _, newg = newgoal in + if Inference.meta_convertibility term newg then + newmeta, newgoal + else + demodulation_goal newmeta env table newgoal + | None -> + newmeta, goal +;; diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index a0cf2bb21..4f1b43bdb 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -16,10 +16,11 @@ and proof = | BasicProof of Cic.term | ProofBlock of Cic.substitution * UriManager.uri * + (Cic.name * Cic.term) * Cic.term * (* name, ty, eq_ty, left, right *) - (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * +(* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *) (Utils.pos * equality) * proof - | ProofGoalBlock of proof * equality + | ProofGoalBlock of proof * proof (* equality *) | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof ;; @@ -56,9 +57,9 @@ let build_proof_term equality = (* (string_of_equality equality); *) Cic.Implicit None | BasicProof term -> term - | ProofGoalBlock (proofbit, equality) -> + | ProofGoalBlock (proofbit, proof (* equality *)) -> print_endline "found ProofGoalBlock, going up..."; - let _, proof, _, _, _ = equality in +(* let _, proof, _, _, _ = equality in *) do_build_goal_proof proofbit proof | ProofSymBlock (ens, proof) -> let proof = do_build_proof proof in @@ -66,16 +67,16 @@ let build_proof_term equality = Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *) proof ] - | ProofBlock (subst, eq_URI, t', (pos, eq), eqproof) -> + | 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, (* CicSubstitution.lift 1 *) bo) in +(* 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 (); *) @@ -112,8 +113,8 @@ let build_proof_term equality = (* | BasicProof _ -> do_build_proof proof *) (* | proofbit -> *) match proof with - | ProofGoalBlock (pb, eq) -> - do_build_proof (ProofGoalBlock (replace_proof proofbit pb, eq)) + | ProofGoalBlock (pb, p(* eq *)) -> + do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p(* eq *))) (* let _, proof, _, _, _ = eq in *) (* let newproof = replace_proof proofbit proof in *) (* do_build_proof newproof *) @@ -124,19 +125,12 @@ let build_proof_term equality = | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *) and replace_proof newproof = function - | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> - let uri = eq_URI in -(* if eq_URI = HelmLibraryObjects.Logic.eq_ind_URI then *) -(* HelmLibraryObjects.Logic.eq_ind_r_URI *) -(* else *) -(* HelmLibraryObjects.Logic.eq_ind_URI *) -(* in *) + | ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof) -> let eqproof' = replace_proof newproof eqproof in - ProofBlock (subst, uri(* eq_URI *), t', poseq, eqproof') -(* ProofBlock (subst, eq_URI, t', poseq, newproof) *) - | ProofGoalBlock (pb, equality) -> + ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof') + | ProofGoalBlock (pb, p(* equality *)) -> let pb' = replace_proof newproof pb in - ProofGoalBlock (pb', equality) + ProofGoalBlock (pb', p(* equality *)) (* let w, proof, t, menv, args = equality in *) (* let proof' = replace_proof newproof proof in *) (* ProofGoalBlock (pb, (w, proof', t, menv, args)) *) @@ -1122,7 +1116,7 @@ let equations_blacklist = perche' questo cacchio di teorema rompe le scatole :'( *) "cic:/Rocq/SUBST/comparith/mult_n_2.con"; ] -;; + ;; let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = let module C = Cic in @@ -1217,14 +1211,12 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = (fun t (newargs, index) -> match t with | Cic.Meta (i, l) -> - Hashtbl.add table i index; -(* if index = 5469 then ( *) -(* Printf.printf "?5469 COMES FROM (%d): %s\n" *) -(* i (string_of_equality equality); *) -(* print_newline (); *) -(* is_this_case := true *) -(* ); *) - ((Cic.Meta (index, l))::newargs, index+1) + if Hashtbl.mem table i then + let idx = Hashtbl.find table i in + ((Cic.Meta (idx, l))::newargs, index+1) + else + let _ = Hashtbl.add table i index in + ((Cic.Meta (index, l))::newargs, index+1) | _ -> assert false) args ([], newmeta+1) in @@ -1246,19 +1238,44 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = and left = repl left and right = repl right in let metas = (metas_of_term left) @ (metas_of_term right) in - let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' - and newargs = + let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in + let newargs = 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' + 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 -> BasicProof (repl term) - | ProofBlock (subst, eq_URI, t', (pos, eq), p) -> + | 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) + | ProofBlock (subst, eq_URI, namety, bo(* t' *), (pos, eq), p) -> (* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *) (* (string_of_equality equality) (print_subst subst); *) - + +(* debug_print "table is:"; *) +(* Hashtbl.iter *) +(* (fun k v -> debug_print (Printf.sprintf "%d: %d" k v)) *) +(* table; *) let subst' = List.fold_left (fun s arg -> @@ -1269,42 +1286,24 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = if List.mem_assoc i subst then s else -(* let _, context, ty = CicUtil.lookup_meta j menv' in *) -(* (i, (context, Cic.Meta (j, l), ty))::s *) let _, context, ty = CicUtil.lookup_meta i menv in (i, (context, Cic.Meta (j, l), ty))::s - with Not_found -> s + with Not_found -> +(* debug_print ("Not_found meta ?" ^ (string_of_int i)); *) + s ) | _ -> assert false) [] args in -(* let subst'' = *) -(* List.map *) -(* (fun (i, e) -> *) -(* try let j = Hashtbl.find table i in (j, e) *) -(* with _ -> (i, e)) subst *) -(* in *) (* Printf.printf "subst' is:\n%s\n" (print_subst subst'); *) (* print_newline (); *) - ProofBlock (subst' @ subst, eq_URI, t', (pos, eq), p) -(* | ProofSymBlock (ens, p) -> *) -(* let ens' = List.map (fun (u, t) -> (u, repl t)) ens in *) -(* ProofSymBlock (ens', fix_proof p) *) + ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p) | p -> assert false in -(* (newmeta + (List.length newargs) + 2, *) let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in -(* if !is_this_case then ( *) -(* print_endline "\nTHIS IS THE TROUBLE!!!"; *) -(* let pt = build_proof_term neweq in *) -(* Printf.printf "equality: %s\nproof: %s\n" *) -(* (string_of_equality neweq) (CicPp.ppterm pt); *) -(* print_endline (String.make 79 '-'); *) -(* ); *) (newmeta + 1, neweq) -(* (w, fix_proof p, (ty, left, right, o), menv', newargs)) *) ;; @@ -1543,6 +1542,7 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = let is_identity ((_, context, ugraph) as env) = function | ((_, _, (ty, left, right, _), _, _) as equality) -> (left = right || + (meta_convertibility left right) || (fst (CicReduction.are_convertible context left right ugraph))) ;; diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index b7a10fe34..2011dd979 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -13,10 +13,11 @@ and proof = | BasicProof of Cic.term | ProofBlock of Cic.substitution * UriManager.uri * + (Cic.name * Cic.term) * Cic.term * (* name, ty, eq_ty, left, right *) - (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * +(* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *) (Utils.pos * equality) * proof - | ProofGoalBlock of proof * equality + | ProofGoalBlock of proof * proof (* equality *) | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof @@ -87,6 +88,8 @@ val term_is_equality: ?eq_uri:UriManager.uri -> Cic.term -> bool (* val demodulation: int -> environment -> equality -> equality -> int * equality *) +val meta_convertibility: Cic.term -> Cic.term -> bool + val meta_convertibility_eq: equality -> equality -> bool val is_identity: environment -> equality -> bool diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index 6f1ea3f2b..9766b79f6 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -42,8 +42,8 @@ let _ = "-o", Arg.String set_ordering, "Term ordering. Possible values are:\n" ^ - "\tkbo: Knuth-Bendix ordering (default)\n" ^ - "\tnr-kbo: Non-recursive variant of kbo\n" ^ + "\tkbo: Knuth-Bendix ordering\n" ^ + "\tnr-kbo: Non-recursive variant of kbo (default)\n" ^ "\tlpo: Lexicographic path ordering"; "-l", Arg.Int set_time_limit, "Time limit in seconds (default: no limit)"; diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index a3dff3eb3..197ceffbb 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -1161,22 +1161,41 @@ let main dbd term metasenv ugraph = | ParamodulationFailure -> Printf.printf "NO proof found! :-(\n\n" | ParamodulationSuccess (Some goal, env) -> - let proof = Inference.build_proof_term goal in + 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 *) let newmetasenv = List.fold_left (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities in let _ = + 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); try let ty, ug = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in - Printf.printf "OK, found a proof!\n"; - (* REMEMBER: we have to instantiate meta_proof, we should use - apply the "apply" tactic to proof and status - *) - let names = names_of_context context in - print_endline (PP.pp proof names); +(* Printf.printf "OK, found a proof!\n"; *) +(* (\* REMEMBER: we have to instantiate meta_proof, we should use *) +(* apply the "apply" tactic to proof and status *) +(* *\) *) +(* let names = names_of_context context in *) +(* print_endline (PP.pp proof names); *) (* print_endline (PP.ppterm proof); *) print_endline (string_of_float (finish -. start)); -- 2.39.2