X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=fe63c7d669abed002c73b8876b60bba5abd0f834;hb=b09b0e4b30c429d8e050150cc4e9b94d7c205368;hp=b3a53d92953f61e2f86dad7baf146deab69dec79;hpb=027d780050fc28643896c08cc82fd47e30835a76;p=helm.git diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index b3a53d929..fe63c7d66 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -708,7 +708,6 @@ let backward_simplify env new' ?passive active = active, passive, newa, newp *) ;; - let close env new' given = let new_pos, new_table, min_weight = List.fold_left @@ -889,7 +888,7 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = *) match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] - when UriManager.eq uri (LibraryObjects.eq_URI ()) -> + when UriManager.eq uri (Utils.eq_URI ()) -> (let goal_equation = Equality.mk_equality (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) @@ -946,7 +945,7 @@ let rec given_clause_fullred dbd env goals theorems ~passive active = (* in *) let ok, proof = (* apply_goal_to_theorems dbd env theorems ~passive active goals in *) - let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in + let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in match fst goals with | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])::_ when left = right && iseq uri -> @@ -1195,13 +1194,24 @@ let given_clause_fullred dbd env goals theorems passive active = (given_clause_fullred dbd env goals theorems passive) active *) -let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ());; +let iseq uri = UriManager.eq uri (Utils.eq_URI ());; let check_if_goal_is_identity env = function | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) when left = right && iseq uri -> let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in Some (goalproof, reflproof, 0, Subst.empty_subst,m) + | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) + when iseq uri -> + (let _,context,_ = env in + try + let s,m,_ = + Inference.unification m m context left right CicUniv.empty_ugraph + in + let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in + let m = Subst.apply_subst_metasenv s m in + Some (goalproof, reflproof, 0, s,m) + with _ -> None) | _ -> None ;; @@ -1223,6 +1233,7 @@ let simplify_goal_set env goals passive active = (fun acc goal -> match simplify_goal env goal ~passive active with | _, g -> if find g acc then acc else g::acc) + (* active_goals active_goals *) [] active_goals in if List.length active_goals <> List.length simplified then @@ -1269,10 +1280,16 @@ let infer_goal_set env active goals = let infer_goal_set_with_current env current goals = let active_goals, passive_goals = goals in let _,table,_ = build_table [current] in + let _,_,_,_,id = Equality.open_equality current in active_goals, List.fold_left (fun acc g -> let new' = Indexing.superposition_left env table g in + if id = 2 then + begin + prerr_endline "XXXXXXX"; + List.iter (fun _,_,e -> prerr_endline (CicPp.ppterm e)) new' ; + end; acc @ new') passive_goals active_goals ;; @@ -1287,6 +1304,7 @@ let size_of_goal_set_p (_,l) = List.length l;; let given_clause ((_,context,_) as env) goals theorems passive active max_iterations max_time = + let names = names_of_context context in let initial_time = Unix.gettimeofday () in let iterations_left iterno = let now = Unix.gettimeofday () in @@ -1305,7 +1323,9 @@ let given_clause (ParamodulationFailure "No more time to spend") else let _ = prerr_endline "simpl goal with active" in + let _ = <:start> in let goals = simplify_goal_set env goals passive active in + let _ = <:stop> in match check_if_goals_set_is_solved env active goals with | Some p -> prerr_endline @@ -1336,13 +1356,18 @@ let given_clause ParamodulationFailure "No more passive"(*maybe this is a success! *) else begin + let goals = infer_goal_set env active goals in + let goals = infer_goal_set env active goals in let goals = infer_goal_set env active goals in let current, passive = select env goals passive in + let _,_,goaltype = List.hd (fst goals) in + prerr_endline (Printf.sprintf "Current goal = %s\n" + (CicPp.pp goaltype names)); prerr_endline (Printf.sprintf "Selected = %s\n" (Equality.string_of_equality ~env current)); (* SIMPLIFICATION OF CURRENT *) let res = - forward_simplify env (Positive, current) ~passive active + forward_simplify env (Positive, current) (*~passive*) active in match res with | None -> step goals theorems passive active (iterno+1) @@ -1373,10 +1398,21 @@ let given_clause | Some p, Some rp -> simplify (new' @ p @ rp) active passive in let active, passive, new' = simplify new' active passive in + if iterno = 36 || iterno = 654 then + begin + prerr_endline "..................."; + List.iter + (fun x -> prerr_endline (Equality.string_of_equality +~env:env x)) new'; + prerr_endline "FINE..................."; + end; prerr_endline "simpl goal with new"; let goals = let a,b,_ = build_table new' in + let _ = <:start> in + <:stop> in let passive = add_to_passive passive new' in step goals theorems passive active (iterno+1) @@ -1665,7 +1701,7 @@ let saturate context_hyp @ thms, [] else let refl_equal = - let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + let us = UriManager.string_of_uri (Utils.eq_URI ()) in UriManager.uri_of_string (us ^ "#xpointer(1/1/1)") in let t = CicUtil.term_of_uri refl_equal in @@ -1723,11 +1759,14 @@ let saturate ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in let goal_proof, side_effects_t = - let initial = newproof in + let initial = Equality.add_subst subsumption_subst newproof in Equality.build_goal_proof goalproof initial type_of_goal side_effects in -(*prerr_endline (CicPp.pp goal_proof names);*) let goal_proof = Subst.apply_subst subsumption_subst goal_proof in + let metas_still_open_in_proof = Utils.metas_of_term goal_proof in +(*prerr_endline (CicPp.pp goal_proof names);*) + (* ?? *) + let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in let side_effects_t = List.map (Subst.apply_subst subsumption_subst) side_effects_t in @@ -1743,7 +1782,10 @@ let saturate | None -> [i,context,ty], (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) - ([],[],[],None) proof_menv + ([],[],[],None) + (List.filter + (fun (i,_,_) -> List.mem i metas_still_open_in_proof) + proof_menv) in let replace where = (* we need this fake equality since the metas of the hypothesis may be