From: Enrico Tassi Date: Mon, 2 Oct 2006 15:18:35 +0000 (+0000) Subject: returns the right list of goals X-Git-Tag: 0.4.95@7852~955 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=59895ae358dff2a57a9fd1ea6924690a0862e036;p=helm.git returns the right list of goals --- diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 69634a830..655939851 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -858,15 +858,21 @@ exception NotMetaConvertible;; let meta_convertibility_aux table t1 t2 = let module C = Cic in - let rec aux table t1 t2 = + let rec aux ((table_l,table_r) as table) t1 t2 = match t1, t2 with + | C.Meta (m1, tl1), C.Meta (m2, tl2) when m1 = m2 -> table + | C.Meta (m1, tl1), C.Meta (m2, tl2) when m1 < m2 -> aux table t2 t1 | C.Meta (m1, tl1), C.Meta (m2, tl2) -> - (try - if List.assoc m1 table = m2 then table - else raise NotMetaConvertible - with Not_found -> - try ignore(List.assoc m2 table);raise NotMetaConvertible - with Not_found -> (m1,m2)::table) + let m1_binding, table_l = + try List.assoc m1 table_l, table_l + with Not_found -> m2, (m1, m2)::table_l + and m2_binding, table_r = + try List.assoc m2 table_r, table_r + with Not_found -> m1, (m2, m1)::table_r + in + if (m1_binding <> m2) || (m2_binding <> m1) then + raise NotMetaConvertible + else table_l,table_r | C.Var (u1, ens1), C.Var (u2, ens2) | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) -> aux_ens table ens1 ens2 @@ -942,12 +948,12 @@ let meta_convertibility_eq eq1 eq2 = true else try - let table = meta_convertibility_aux [] left left' in + let table = meta_convertibility_aux ([],[]) left left' in let _ = meta_convertibility_aux table right right' in true with NotMetaConvertible -> try - let table = meta_convertibility_aux [] left right' in + let table = meta_convertibility_aux ([],[]) left right' in let _ = meta_convertibility_aux table right left' in true with NotMetaConvertible -> @@ -960,7 +966,7 @@ let meta_convertibility t1 t2 = true else try - ignore(meta_convertibility_aux [] t1 t2); + ignore(meta_convertibility_aux ([],[]) t1 t2); true with NotMetaConvertible -> false @@ -990,7 +996,8 @@ let equality_of_term bag proof term = let is_weak_identity eq = let _,_,(_,left, right,_),_,_ = open_equality eq in - left = right (* doing metaconv here is meaningless *) + left = right + (* doing metaconv here is meaningless *) ;; let is_identity (_, context, ugraph) eq = diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 625beb839..1d5d9783f 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1249,31 +1249,33 @@ let build_proof eq_uri goalproof initial type_of_goal side_effects context proof_menv in -(* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *) + (* prerr_endline ("PROOF: " ^ 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);*) - (* ?? *) + (* 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 (* replacing fake mets with real ones *) -(* prerr_endline "replacing metas..."; *) + (* prerr_endline "replacing metas..."; *) let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in let goal_proof_menv, what, with_what,free_meta = List.fold_left (fun (acc1,acc2,acc3,uniq) (i,_,ty) -> match uniq with | Some m -> -(* acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq *) - (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl))::acc3, uniq +(* acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq *) + (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2, + (Cic.Meta(i,irl))::acc3, uniq | None -> [i,context,ty], (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) ([],[],[],None) (List.filter - (fun (i,_,_) -> List.mem i metas_still_open_in_proof) + (fun (i,_,_) -> + List.mem i metas_still_open_in_proof + (*&& not(List.mem i metas_still_open_in_goal)*)) proof_menv) in let replace where = @@ -1293,8 +1295,9 @@ let build_proof (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv) in -(* prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int - * free_metas) ); *) + (* prerr_endline + * ("freemetas: " ^ + * String.concat "," (List.map string_of_int free_metas) ); *) (* check/refine/... build the new proof *) let replaced_goal = ProofEngineReduction.replace @@ -1340,13 +1343,20 @@ let build_proof prerr_endline "THE PROOF DOES NOT TYPECHECK!"; raise exn in + + let metas_of_proof = Utils.metas_of_term goal_proof in + let proof, real_metasenv = ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof goalno (CicMetaSubst.apply_subst final_subst) real_menv in let open_goals = + HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof) + in +(* match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] in +*) (* Printf.eprintf "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index 6ac2132aa..81c84af35 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -346,7 +346,7 @@ let compute_equality_weight (ty,left,right,o) = let compute_equality_weight e = let w = compute_equality_weight e in - let d = distance !goal_symbols (symbols_of_eq e) in + let d = 0 in (* distance !goal_symbols (symbols_of_eq e) in *) (* prerr_endline (Printf.sprintf "dist %s --- %s === %d" (String.concat ", " (List.map (CicPp.ppterm) (TermSet.elements