X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=5fa1dafeb288c537e1d67a98d2b7ebd6ec6880b1;hb=456ea05ac26bf48e4cdc0d745a92de0d14b3ff80;hp=f8b0ff45fcc088dcc5c799c93e8831c9be2f3b2b;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index f8b0ff45f..5fa1dafeb 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -31,6 +31,7 @@ let connect_to_auto = true;; +let debug_print = Utils.debug_print;; (* profiling statistics... *) let infer_time = ref 0.;; @@ -124,8 +125,11 @@ let make_passive eq_list = let set = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list in - (*EqualitySet.elements set*) eq_list, set (* see applys.ma *) + (* we have the invariant that the list and the set have the same + * cardinality *) + EqualitySet.elements set, set ;; + let make_empty_active () = [], Indexing.empty ;; let make_active eq_list = eq_list, List.fold_left Indexing.index Indexing.empty eq_list @@ -133,6 +137,7 @@ let make_active eq_list = let size_of_passive (passive_list, _) = List.length passive_list;; let size_of_active (active_list, _) = List.length active_list;; + let passive_is_empty = function | [], s when EqualitySet.is_empty s -> true | [], s -> assert false (* the set and the list should be in sync *) @@ -710,7 +715,7 @@ let activate_theorem (active, passive) = ;; - +(* let simplify_theorems bag env theorems ?passive (active_list, active_table) = let pl, passive_table = match passive with @@ -740,7 +745,7 @@ let simplify_theorems bag env theorems ?passive (active_list, active_table) = let p_theorems = List.map (mapfun passive_table) p_theorems in List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems ;; - +*) let rec simpl bag eq_uri env e others others_simpl = let active = others @ others_simpl in @@ -801,13 +806,13 @@ let print_goals goals = let pp_goal_set msg goals names = let active_goals, passive_goals = goals in - prerr_endline ("////" ^ msg); - prerr_endline ("ACTIVE G: " ^ + debug_print (lazy ("////" ^ msg)); + debug_print (lazy ("ACTIVE G: " ^ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names) - active_goals))); - prerr_endline ("PASSIVE G: " ^ + active_goals)))); + debug_print (lazy ("PASSIVE G: " ^ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names) - passive_goals))) + passive_goals)))) ;; let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = @@ -819,8 +824,8 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = Equality.mk_equality bag (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) in -(* match Indexing.subsumption env table goal_equation with*) - match Indexing.unification env table goal_equation with + match Indexing.subsumption env table goal_equation with + (* match Indexing.unification env table goal_equation with *) | Some (subst, equality, swapped ) -> (* prerr_endline @@ -842,25 +847,27 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = | _ -> None ;; -let find_all_subsumed bag env table (goalproof,menv,ty) = +let find_all_subsumed bag maxm env table (goalproof,menv,ty) = match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] when LibraryObjects.is_eq_URI uri -> let goal_equation = - Equality.mk_equality bag - (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) + (Equality.mk_equality bag + (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv)) in - List.map + List.map (fun (subst, equality, swapped ) -> let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in + Indexing.check_for_duplicates cicmenv "from subsumption"; let p = if swapped then Equality.symmetric bag eq_ty l id uri m else p in (goalproof, p, id, subst, cicmenv)) - (Indexing.unification_all env table goal_equation) + (Indexing.subsumption_all env table goal_equation) + (* (Indexing.unification_all env table goal_equation) *) | _ -> assert false ;; @@ -875,12 +882,12 @@ let check_if_goal_is_identity env = function (let _,context,_ = env in try let s,m,_ = - Founif.unification m m context left right CicUniv.empty_ugraph + Founif.unification [] m context left right CicUniv.empty_ugraph in let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in let m = Subst.apply_subst_metasenv s m in Some (goalproof, reflproof, 0, s,m) - with _ -> None) + with CicUnification.UnificationFailure _ -> None) | _ -> None ;; @@ -990,21 +997,21 @@ let pp_goals label goals context = let names = Utils.names_of_context context in List.iter (fun _,_,g -> - prerr_endline - (Printf.sprintf "Current goal: %s = %s\n" label (CicPp.pp g names))) + debug_print (lazy + (Printf.sprintf "Current goal: %s = %s\n" label (CicPp.pp g names)))) (fst goals); List.iter (fun _,_,g -> - prerr_endline - (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))) + debug_print (lazy + (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names)))) (snd goals); ;; let print_status iterno goals active passive = - prerr_endline + debug_print (lazy (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)" iterno (size_of_active active) (size_of_passive passive) - (size_of_goal_set_a goals) (size_of_goal_set_p goals)) + (size_of_goal_set_a goals) (size_of_goal_set_p goals))) ;; (** given-clause algorithm with full reduction strategy: NEW implementation *) @@ -1055,9 +1062,9 @@ let given_clause in match check_if_goals_set_is_solved bag env active goals with | Some p -> - prerr_endline + debug_print (lazy (Printf.sprintf "\nFound a proof in: %f\n" - (Unix.gettimeofday() -. initial_time)); + (Unix.gettimeofday() -. initial_time))); ParamodulationSuccess (p,active,passive) | None -> (* SELECTION *) @@ -1083,9 +1090,9 @@ let given_clause if s_iterno < saturation_steps then let current, passive = select env goals passive in (* SIMPLIFICATION OF CURRENT *) - prerr_endline + debug_print (lazy ("Selected : " ^ - Equality.string_of_equality ~env current); + Equality.string_of_equality ~env current)); forward_simplify bag eq_uri env current active, passive else None, passive @@ -1255,7 +1262,7 @@ let fix_proof metasenv context all_implicits p = try let _ = CicUtil.lookup_meta i metasenv in metasenv with CicUtil.Meta_not_found _ -> - prerr_endline ("not found: "^(string_of_int i)); + debug_print (lazy ("not found: "^(string_of_int i))); let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in (i,context,Cic.Meta(j,irl))::metasenv in @@ -1276,10 +1283,11 @@ let fix_proof metasenv context all_implicits p = let metasenv,s = aux metasenv n s in let metasenv,t = aux metasenv (n+1) t in metasenv,Cic.Prod(name,s,t) - | Cic.LetIn(name,s,t) -> + | Cic.LetIn(name,s,ty,t) -> let metasenv,s = aux metasenv n s in + let metasenv,ty = aux metasenv n ty in let metasenv,t = aux metasenv (n+1) t in - metasenv,Cic.LetIn(name,s,t) + metasenv,Cic.LetIn(name,s,ty,t) | Cic.Const(uri,ens) -> let metasenv,ens = List.fold_right @@ -1294,15 +1302,16 @@ let fix_proof metasenv context all_implicits p = aux metasenv 0 p ;; -let fix_metasenv metasenv = +let fix_metasenv context metasenv = List.fold_left (fun m (i,c,t) -> - let m,t = fix_proof m c false t in + let m,t = fix_proof m context false t in let m = List.filter (fun (j,_,_) -> j<>i) m in - (i,c,t)::m) + (i,context,t)::m) metasenv metasenv ;; + (* status: input proof status * goalproof: forward steps on goal * newproof: backward steps @@ -1316,17 +1325,17 @@ let build_proof bag status goalproof newproof subsumption_id subsumption_subst proof_menv = - if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA" - else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv); + if proof_menv = [] then debug_print (lazy "+++++++++++++++VUOTA") + else debug_print (lazy (CicMetaSubst.ppmetasenv [] proof_menv)); let proof, goalno = status in let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in let names = Utils.names_of_context context in - prerr_endline "Proof:"; - prerr_endline + debug_print (lazy "Proof:"); + debug_print (lazy (Equality.pp_proof bag names goalproof newproof subsumption_subst - subsumption_id type_of_goal); + subsumption_id type_of_goal)); (* prerr_endline ("max weight: " ^ (string_of_int (Equality.max_weight goalproof newproof))); @@ -1345,7 +1354,8 @@ let build_proof in (* Equality.draw_proof bag names goalproof newproof subsumption_id; *) let goal_proof = Subst.apply_subst subsumption_subst goal_proof in - let real_menv = fix_metasenv (proof_menv@metasenv) in + (* assert (metasenv=[]); *) + let real_menv = fix_metasenv context (proof_menv@metasenv) in let real_menv,goal_proof = fix_proof real_menv context false goal_proof in (* @@ -1360,20 +1370,33 @@ let build_proof prerr_endline "THE PROOF DOES NOT TYPECHECK! "; raise exn in + let old_insert_coercions = !CicRefine.insert_coercions in let goal_proof,goal_ty,real_menv,_ = (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *) try - prerr_endline (CicPp.ppterm goal_proof); - CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph + debug_print (lazy (CicPp.ppterm goal_proof)); + CicRefine.insert_coercions := false; + let res = + CicRefine.type_of_aux' + real_menv context goal_proof CicUniv.empty_ugraph + in + CicRefine.insert_coercions := old_insert_coercions; + res with | CicRefine.RefineFailure s | CicRefine.Uncertain s | CicRefine.AssertFailure s as exn -> + CicRefine.insert_coercions := old_insert_coercions; pp_error goal_proof names (Lazy.force s) exn | CicUtil.Meta_not_found i as exn -> + CicRefine.insert_coercions := old_insert_coercions; pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn | Invalid_argument "list_fold_left2" as exn -> + CicRefine.insert_coercions := old_insert_coercions; pp_error goal_proof names "Invalid_argument: list_fold_left2" exn + | exn -> + CicRefine.insert_coercions := old_insert_coercions; + raise exn in let subst_side_effects,real_menv,_ = try @@ -1385,7 +1408,7 @@ let build_proof | CicUnification.AssertFailure s -> assert false (* fail "Maybe the local context of metas in the goal was not an IRL" s *) in - prerr_endline "+++++++++++++ FINE UNIF"; + Utils.debug_print (lazy "+++++++++++++ FINE UNIF"); let final_subst = (goalno,(context,goal_proof,type_of_goal))::subst_side_effects in @@ -1572,28 +1595,46 @@ let all_subsumed bag maxm status active passive = let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let env = metasenv,context,CicUniv.empty_ugraph in let cleaned_goal = Utils.remove_local_context type_of_goal in + let canonical_menv,other_menv = + List.partition (fun (_,c,_) -> c = context) metasenv in + (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *) + let metasenv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in - prerr_endline (string_of_int (List.length (fst active))); + debug_print (lazy (string_of_int (List.length (fst active)))); (* we simplify using both actives passives *) let table = List.fold_left (fun (l,tbl) eq -> eq::l,(Indexing.index tbl eq)) active (list_of_passive passive) in + let (_,_,ty) = goal in + debug_print (lazy ("prima " ^ CicPp.ppterm ty)); let _,goal = simplify_goal bag env goal table in let (_,_,ty) = goal in - prerr_endline (CicPp.ppterm ty); - let subsumed = find_all_subsumed bag env (snd table) goal in + debug_print (lazy ("in mezzo " ^ CicPp.ppterm ty)); + let subsumed = find_all_subsumed bag !maxmeta env (snd table) goal in + debug_print (lazy ("dopo " ^ CicPp.ppterm ty)); let subsumed_or_id = match (check_if_goal_is_identity env goal) with None -> subsumed | Some id -> id::subsumed in + debug_print (lazy "dopo subsumed"); let res = List.map (fun (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) -> + let subst, proof, gl = build_proof bag - status goalproof newproof subsumption_id subsumption_subst proof_menv) - subsumed_or_id in + status goalproof newproof subsumption_id subsumption_subst proof_menv + in + let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in + let newmetasenv = + other_menv @ + List.filter + (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv + in + let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in + (subst, proof,gl)) subsumed_or_id + in res, !maxmeta @@ -1619,17 +1660,20 @@ let given_clause let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in let cleaned_goal = Utils.remove_local_context type_of_goal in + let canonical_menv,other_menv = + List.partition (fun (_,c,_) -> c = context) metasenv in + (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *) Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *) - let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in + let canonical_menv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in + let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in let goal = [], metasenv', cleaned_goal in let env = metasenv,context,CicUniv.empty_ugraph in - prerr_endline ">>>>>> ACTIVES >>>>>>>>"; - List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e)) + debug_print (lazy ">>>>>> ACTIVES >>>>>>>>"); + List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e))) active_l; - prerr_endline ">>>>>>>>>>>>>>"; + debug_print (lazy ">>>>>>>>>>>>>>"); let goals = make_goal_set goal in match -(* given_caluse non prende in input maxm ????? *) given_clause bag eq_uri env goals passive active goal_steps saturation_steps max_time with @@ -1641,9 +1685,12 @@ let given_clause build_proof bag status goalproof newproof subsumption_id subsumption_subst proof_menv in + let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in + let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in Some (subst, proof,gl),a,p, !maxmeta ;; + let add_to_passive eql passives = add_to_passive passives eql eql ;;