From 439cb54c906ae03dc5f88e907ce2577fe5d6fcf7 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Tue, 11 Oct 2005 15:10:22 +0000 Subject: [PATCH] fixed bugs in Indexing.find_matches and Saturation.apply_equality_to_goal --- helm/ocaml/paramodulation/.depend | 2 + helm/ocaml/paramodulation/indexing.ml | 32 ++++++++++------ helm/ocaml/paramodulation/inference.ml | 12 +++++- helm/ocaml/paramodulation/saturation.ml | 50 ++++++++++++++++--------- 4 files changed, 65 insertions(+), 31 deletions(-) diff --git a/helm/ocaml/paramodulation/.depend b/helm/ocaml/paramodulation/.depend index 8a74093c5..591ad1df8 100644 --- a/helm/ocaml/paramodulation/.depend +++ b/helm/ocaml/paramodulation/.depend @@ -11,3 +11,5 @@ indexing.cmo: utils.cmi inference.cmi discrimination_tree.cmo indexing.cmx: utils.cmx inference.cmx discrimination_tree.cmx saturation.cmo: utils.cmi inference.cmi indexing.cmo saturation.cmx: utils.cmx inference.cmx indexing.cmx +saturate_main.cmo: utils.cmi saturation.cmo +saturate_main.cmx: utils.cmx saturation.cmx diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 497c42636..85ee885cb 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -202,17 +202,18 @@ let rec find_matches metasenv context ugraph lift_amount term termty = (* let termty, ugraph = *) (* CicTypeChecker.type_of_aux' metasenv context term ugraph *) (* in *) + let check = match termty with C.Implicit None -> false | _ -> true in function | [] -> None | candidate::tl -> let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in -(* if not (fst (CicReduction.are_convertible *) -(* ~metasenv context termty ty ugraph)) then ( *) -(* (\* debug_print (lazy ( *\) *) -(* (\* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *) -(* (\* (CicPp.pp termty names) (CicPp.pp ty names))); *\) *) -(* find_matches metasenv context ugraph lift_amount term termty tl *) -(* ) else *) + if check && not (fst (CicReduction.are_convertible + ~metasenv context termty ty ugraph)) then ( +(* debug_print (lazy ( *) +(* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *) +(* (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 subst', metasenv', ugraph' = let t1 = Unix.gettimeofday () in @@ -425,7 +426,8 @@ let subsumption env table target = ;; -let rec demodulation_aux metasenv context ugraph table lift_amount term = +let rec demodulation_aux ?(typecheck=false) + metasenv context ugraph table lift_amount term = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -435,8 +437,10 @@ let rec demodulation_aux metasenv context ugraph table lift_amount term = | C.Meta _ -> None | term -> let termty, ugraph = - C.Implicit None, ugraph -(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) + if typecheck then + CicTypeChecker.type_of_aux' metasenv context term ugraph + else + C.Implicit None, ugraph in let res = find_matches metasenv context ugraph lift_amount term termty candidates @@ -1087,7 +1091,9 @@ let rec demodulation_goal newmeta env table goal = let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in !maxmeta, (newproof, newmetasenv, newterm) in - let res = demodulation_aux metasenv' context ugraph table 0 term in + let res = + demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term + in match res with | Some t -> let newmeta, newgoal = build_newgoal t in @@ -1130,7 +1136,9 @@ let rec demodulation_theorem newmeta env table theorem = 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 + let res = + demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty + in match res with | Some t -> let newmeta, newthm = build_newtheorem t in diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 0556c442d..bf53f5cec 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1180,6 +1180,13 @@ let find_library_equalities dbd context status maxmeta = let ok_types ty menv = List.for_all (fun (_, _, mt) -> mt = ty) menv in + let rec has_vars = function + | C.Meta _ | C.Rel _ | C.Const _ -> false + | C.Var _ -> true + | C.Appl l -> List.exists has_vars l + | C.Prod (_, s, t) -> (has_vars s) || (has_vars t) + | _ -> assert false + in let rec aux newmeta = function | [] -> [], newmeta | (uri, term, termty)::tl -> @@ -1189,7 +1196,7 @@ let find_library_equalities dbd context status maxmeta = (CicPp.ppterm term) (CicPp.ppterm termty))); let res, newmeta = match termty with - | C.Prod (name, s, t) -> + | C.Prod (name, s, t) when not (has_vars termty) -> let head, newmetas, args, newmeta = ProofEngineHelpers.saturate_term newmeta [] context termty 0 in @@ -1212,7 +1219,8 @@ let find_library_equalities dbd context status maxmeta = Some e, (newmeta+1) | _ -> None, newmeta ) - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when iseq uri && not (has_vars termty) -> 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 diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 825d6b8c8..181b4e1d9 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -858,13 +858,13 @@ let simplify_goal env goal ?passive (active_list, active_table) = let changed', goal = demodulate passive_table goal in (changed || changed'), 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 *) + let _ = + let p, _, t = goal in + debug_print + (lazy + (Printf.sprintf "Goal after demodulation: %s, %s" + (string_of_proof p) (CicPp.ppterm t))) + in changed, goal ;; @@ -942,6 +942,10 @@ let apply_equality_to_goal env equality goal = let eqterm = C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in let gproof, gmetas, gterm = goal in + debug_print + (lazy + (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s" + (string_of_equality equality) (CicPp.ppterm gterm))); try let subst, metasenv', _ = let menv = metasenv @ metas @ gmetas in @@ -1060,7 +1064,7 @@ let new_meta () = ;; -let apply_to_goal env theorems active goal = +let apply_to_goal env theorems ?passive active goal = let metasenv, context, ugraph = env in let proof, metas, term = goal in debug_print @@ -1173,15 +1177,25 @@ let apply_to_goal env theorems active goal = in let r, s, l = if Inference.term_is_equality term then - let rec appleq = function + let _ = debug_print (lazy "OK, is equality!!") in + let rec appleq_a = 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 + if ok then true, s, [newproof, metas, term] else appleq_a tl + | _::tl -> appleq_a tl + in + let rec appleq_p = function + | [] -> false, [], [] + | equality::tl -> + let ok, s, newproof = apply_equality_to_goal env equality goal in + if ok then true, s, [newproof, metas, term] else appleq_p tl in let al, _ = active in - appleq al + match passive with + | None -> appleq_a al + | Some (_, (pl, _), _) -> + let r, s, l = appleq_a al in if r then r, s, l else appleq_p pl else false, [], [] in @@ -1189,7 +1203,7 @@ let apply_to_goal env theorems active goal = ;; -let apply_to_goal_conj env theorems active (depth, goals) = +let apply_to_goal_conj env theorems ?passive active (depth, goals) = let rec aux = function | goal::tl -> let propagate_subst subst (proof, metas, term) = @@ -1221,7 +1235,7 @@ let apply_to_goal_conj env theorems active (depth, goals) = ProofBlock (subst @ s, u, nty, t, pe, p) in (repl proof, metas, term) in - let r = apply_to_goal env theorems active goal in ( + let r = apply_to_goal env theorems ?passive active goal in ( match r with | `No -> `No (depth, goals) | `GoOn sl (* (subst, gl) *) -> @@ -1421,7 +1435,7 @@ let apply_to_goals env is_passive_empty theorems active goals = ;; -let apply_goal_to_theorems dbd env theorems active goals = +let apply_goal_to_theorems dbd env theorems ?passive active goals = (* let theorems, _ = theorems in *) let context_hyp, library_thms = theorems in let thm_uris = @@ -1434,7 +1448,7 @@ let apply_goal_to_theorems dbd env theorems active goals = let rec aux = function | [] -> false, (a_goals, p_goals) | theorem::tl -> - let res = apply_to_goal_conj env [theorem] active goal in + let res = apply_to_goal_conj env [theorem] ?passive active goal in match res with | `Ok newgoals -> true, ([newgoals], []) @@ -1752,7 +1766,9 @@ let rec given_clause_fullred dbd env goals theorems passive active = (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" (print_goals (fst goals)) (print_goals (snd goals)))) in - let ok, goals = apply_goal_to_theorems dbd env theorems active goals in + let ok, goals = + apply_goal_to_theorems dbd env theorems ~passive active goals + in if ok then let proof = match (fst goals) with -- 2.39.2