From 4b0c8ab87297a2bcf9998c098fafbba44e8b641b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 May 2006 12:19:04 +0000 Subject: [PATCH] - metas_of_term moved to cicUtil - fixed proof generation - added again typechecking of generated proof --- components/binaries/tptp2grafite/main.ml | 2 +- components/cic/cicUtil.ml | 26 +++++++++++ components/cic/cicUtil.mli | 1 + components/tactics/paramodulation/equality.ml | 20 +++++---- .../tactics/paramodulation/saturation.ml | 44 +++++++++++++------ components/tactics/paramodulation/utils.ml | 28 ++---------- 6 files changed, 74 insertions(+), 47 deletions(-) diff --git a/components/binaries/tptp2grafite/main.ml b/components/binaries/tptp2grafite/main.ml index 315bfc100..18fa713a9 100644 --- a/components/binaries/tptp2grafite/main.ml +++ b/components/binaries/tptp2grafite/main.ml @@ -151,7 +151,7 @@ let convert_ast statements context = function statements, f::context | A.Negated_conjecture -> if collect_fv_from_formulae f <> [] then - (*prerr_endline "CONTIENE FV";*)(); + prerr_endline "CONTIENE FV"; let f = PT.Binder (`Forall, diff --git a/components/cic/cicUtil.ml b/components/cic/cicUtil.ml index 7c6e3eabe..51d84392b 100644 --- a/components/cic/cicUtil.ml +++ b/components/cic/cicUtil.ml @@ -363,3 +363,29 @@ let rehash_obj = in C.InductiveDefinition (tl', params', paramsno, attrs) +let rec metas_of_term = function + | Cic.Meta (i, c) -> [i,c] + | Cic.Var (_, ens) + | Cic.Const (_, ens) + | Cic.MutInd (_, _, ens) + | Cic.MutConstruct (_, _, _, ens) -> + List.flatten (List.map (fun (u, t) -> metas_of_term t) ens) + | Cic.Cast (s, t) + | Cic.Prod (_, s, t) + | Cic.Lambda (_, s, t) + | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t) + | Cic.Appl l -> List.flatten (List.map metas_of_term l) + | Cic.MutCase (uri, i, s, t, l) -> + (metas_of_term s) @ (metas_of_term t) @ + (List.flatten (List.map metas_of_term l)) + | Cic.Fix (i, il) -> + List.flatten + (List.map (fun (s, i, t1, t2) -> + (metas_of_term t1) @ (metas_of_term t2)) il) + | Cic.CoFix (i, il) -> + List.flatten + (List.map (fun (s, t1, t2) -> + (metas_of_term t1) @ (metas_of_term t2)) il) + | _ -> [] +;; + diff --git a/components/cic/cicUtil.mli b/components/cic/cicUtil.mli index b6fd7459d..4391efc82 100644 --- a/components/cic/cicUtil.mli +++ b/components/cic/cicUtil.mli @@ -35,6 +35,7 @@ val clean_up_local_context : val is_closed : Cic.term -> bool val is_meta_closed : Cic.term -> bool +val metas_of_term : Cic.term -> (int * Cic.term option list) list (** @raise Failure "not enough prods" *) val strip_prods: int -> Cic.term -> Cic.term diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 34b69718f..521c7635c 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -468,14 +468,18 @@ let pp_proof names goalproof proof = let build_goal_proof l initial ty se = let se = List.map (fun i -> Cic.Meta (i,[])) se in let proof,se = - List.fold_left - (fun (current_proof,se) (pos,id,subst,pred) -> - let p,l,r = proof_of_id id in - let p = build_proof_term p in - let pos = if pos = Utils.Left then Utils.Right else Utils.Left in - build_proof_step subst current_proof p pos l r pred, - List.map (fun x -> Subst.apply_subst subst x) se) - (initial,se) l + let rec aux se current_proof = function + | [] -> current_proof,se + | (pos,id,subst,pred)::tl -> + let p,l,r = proof_of_id id in + let p = build_proof_term p in + let pos = if pos = Utils.Left then Utils.Right else Utils.Left in + let proof = build_proof_step subst current_proof p pos l r pred in + let proof,se = aux se proof tl in + Subst.apply_subst subst proof, + List.map (fun x -> Subst.apply_subst subst x) se + in + aux se initial l in canonical (contextualize_rewrites proof ty), se ;; diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index b93f6b091..cfada5085 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1269,14 +1269,18 @@ let rec check goal = function let simplify_goal_set env goals passive active = let active_goals, passive_goals = goals in + let find (_,_,g) where = + List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where + in let simplified = - HExtlib.filter_map - (fun g -> + List.fold_left + (fun acc g -> match simplify_goal env g ~passive active with - | true, g -> Some g - | false, g -> Some g) - active_goals + | _, g -> if find g acc then acc else g::acc) + [] active_goals in + if List.length active_goals <> List.length simplified then + prerr_endline "SEMPLIFICANDO HO SCARTATO..."; (simplified,passive_goals) (* HExtlib.list_uniq ~eq:(fun (_,_,t1) (_,_,t2) -> t1 = t2) @@ -1300,13 +1304,20 @@ let check_if_goals_set_is_solved env active goals = let infer_goal_set env active goals = let active_goals, passive_goals = goals in - match passive_goals with - | [] -> goals - | hd::tl -> - let selected = hd in - let passive_goals = tl in - let new' = Indexing.superposition_left env (snd active) selected in - selected::active_goals, passive_goals @ new' + let rec aux = function + | [] -> goals + | ((_,_,t1) as hd)::tl when + not (List.exists + (fun (_,_,t) -> Equality.meta_convertibility t t1) + active_goals) + -> + let selected = hd in + let passive_goals = tl in + let new' = Indexing.superposition_left env (snd active) selected in + selected::active_goals, passive_goals @ new' + | _::tl -> aux tl + in + aux passive_goals ;; let infer_goal_set_with_current env current goals = @@ -1791,6 +1802,7 @@ let saturate let goal_proof = replace goal_proof in (* ok per le meta libere... ma per quelle che c'erano e sono rimaste? * what mi pare buono, sostituisce solo le meta farlocche *) + prerr_endline (CicPp.pp goal_proof names); let side_effects_t = List.map replace side_effects_t in (* check/refine/... build the new proof *) let replaced_goal = @@ -1813,10 +1825,16 @@ let saturate | CicUnification.AssertFailure s -> fail "Maybe the local context of metas in the goal was not an IRL" s in - let final_subst = (goalno,(context,goal_proof,type_of_goal))::subst_side_effects in + let _ = + let ty,_ = + CicTypeChecker.type_of_aux' real_menv context goal_proof + CicUniv.empty_ugraph + in + ty + in let proof, real_metasenv = ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof goalno (CicMetaSubst.apply_subst final_subst) real_menv diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index 6a32e2595..072d64f66 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -733,29 +733,7 @@ let eq_XURI () = UriManager.uri_of_string (s ^ "#xpointer(1/1/1)") let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ()) -let rec metas_of_term = function - | Cic.Meta (i, c) -> [i] - | Cic.Var (_, ens) - | Cic.Const (_, ens) - | Cic.MutInd (_, _, ens) - | Cic.MutConstruct (_, _, _, ens) -> - List.flatten (List.map (fun (u, t) -> metas_of_term t) ens) - | Cic.Cast (s, t) - | Cic.Prod (_, s, t) - | Cic.Lambda (_, s, t) - | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t) - | Cic.Appl l -> List.flatten (List.map metas_of_term l) - | Cic.MutCase (uri, i, s, t, l) -> - (metas_of_term s) @ (metas_of_term t) @ - (List.flatten (List.map metas_of_term l)) - | Cic.Fix (i, il) -> - List.flatten - (List.map (fun (s, i, t1, t2) -> - (metas_of_term t1) @ (metas_of_term t2)) il) - | Cic.CoFix (i, il) -> - List.flatten - (List.map (fun (s, t1, t2) -> - (metas_of_term t1) @ (metas_of_term t2)) il) - | _ -> [] -;; +let metas_of_term t = + List.map fst (CicUtil.metas_of_term t) +;; -- 2.39.2