From: Andrea Asperti Date: Wed, 29 Oct 2008 15:13:07 +0000 (+0000) Subject: propagation of changes in other paramodulation files. X-Git-Tag: make_still_working~4616 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6bd49a71cfff3f29ee79da975678292861f9be0d;p=helm.git propagation of changes in other paramodulation files. --- diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index a52109e46..b2970d209 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -843,18 +843,19 @@ 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 @@ -876,7 +877,7 @@ 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 @@ -1296,15 +1297,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 @@ -1347,7 +1349,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 (* @@ -1587,6 +1590,10 @@ 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 debug_print (lazy (string_of_int (List.length (fst active)))); (* we simplify using both actives passives *) @@ -1594,10 +1601,13 @@ let all_subsumed bag maxm status active passive = 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 - debug_print (lazy (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 @@ -1606,10 +1616,14 @@ let all_subsumed bag maxm status active passive = 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 - res, !maxmeta + 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 + (subst, proof,gl)) subsumed_or_id + in res, !maxmeta let given_clause @@ -1634,8 +1648,12 @@ 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 debug_print (lazy ">>>>>> ACTIVES >>>>>>>>"); @@ -1644,7 +1662,6 @@ let given_clause 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 @@ -1656,9 +1673,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 ;;