X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=aed51e35bd2d66bd1b3c44289d75d229f50538ae;hb=246f3c2f2d26655129efacf830ecff47094795b4;hp=b2970d209c39c5edbd3e2d5057b933bc4942ef42;hpb=6bd49a71cfff3f29ee79da975678292861f9be0d;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index b2970d209..aed51e35b 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -125,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 @@ -134,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 *) @@ -773,7 +777,7 @@ let simplify_equalities bag eq_uri env equalities = (Printf.sprintf "equalities:\n%s\n" (String.concat "\n" (List.map Equality.string_of_equality equalities)))); - Utils.debug_print (lazy "SIMPLYFYING EQUALITIES..."); +Utils.debug_print (lazy "SIMPLYFYING EQUALITIES..."); match equalities with | [] -> [] | hd::tl -> @@ -820,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 @@ -862,7 +866,8 @@ let find_all_subsumed bag maxm env table (goalproof,menv,ty) = 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 ;; @@ -882,7 +887,7 @@ let check_if_goal_is_identity env = function 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 ;; @@ -934,17 +939,16 @@ let infer_goal_set bag env active goals = | [] -> active_goals, [] | hd::tl -> let changed,selected = simplify_goal bag env hd active in -(* - if changed then - prerr_endline ("--------------- goal semplificato"); -*) let (_,_,t1) = selected in + (* + if changed && Utils.debug then + prerr_endline ("goal semplificato: " ^ CicPp.ppterm t1); *) let already_in = List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) active_goals in if already_in then - aux tl + aux tl else let passive_goals = tl in let new_passive_goals = @@ -1436,7 +1440,6 @@ let build_proof (* replacing fake mets with real ones *) (* prerr_endline "replacing metas..."; *) let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in - if proof_menv = [] then prerr_endline "VUOTA"; CicMetaSubst.ppmetasenv [] proof_menv; let what, with_what = List.fold_left @@ -1485,7 +1488,6 @@ let build_proof ~where:type_of_goal in let goal_proof,goal_ty,real_menv,_ = - prerr_endline "parte la refine"; try CicRefine.type_of_aux' metasenv context goal_proof CicUniv.empty_ugraph @@ -1592,7 +1594,7 @@ let all_subsumed bag maxm status active passive = 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)); + (* 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 debug_print (lazy (string_of_int (List.length (fst active)))); @@ -1612,6 +1614,7 @@ let all_subsumed bag maxm status active passive = 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 @@ -1621,9 +1624,15 @@ let all_subsumed bag maxm status active passive = 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 + 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 + in + res, !maxmeta let given_clause @@ -1650,9 +1659,12 @@ let given_clause 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)); + (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *) Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *) - let canonical_menv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in + let canonical_menv = + List.map + (fun (i,_,ty)-> (i,[],Utils.remove_local_context 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