From cae7dd50468e5ba0dec9d3cf4fa14daee2c3da2e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Oct 2006 16:08:31 +0000 Subject: [PATCH] commented out are_convertible in is_identity fixed metadataquery so that only are calculated without the DB (but are calculated) removed is_meta_convertible left right in is_weak_identity added extra dependencies between gcd < relevant_equations < ord to make paramodulation happy. In the past this used to be the order used by make. added an hack in applys.ma, since it used to work due to convertibility. --- components/tactics/metadataQuery.ml | 25 +++++++++++++------ components/tactics/paramodulation/equality.ml | 4 ++- .../paramodulation/equality_retrieval.ml | 17 ++++++------- matita/library/nat/ord.ma | 1 + matita/library/nat/relevant_equations.ma | 2 ++ matita/tests/applys.ma | 6 ++--- 6 files changed, 34 insertions(+), 21 deletions(-) diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml index cd14f3f5e..be68c31f7 100644 --- a/components/tactics/metadataQuery.ml +++ b/components/tactics/metadataQuery.ml @@ -212,6 +212,11 @@ let only constants uri = let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *) let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in let consts = Constr.constants_of ty in +(* prerr_endline ("XXX " ^ UriManager.string_of_uri uri);*) +(* Constr.UriManagerSet.iter (fun u -> prerr_endline (" - " ^*) +(* UriManager.string_of_uri u)) consts;*) +(* Constr.UriManagerSet.iter (fun u -> prerr_endline (" + " ^*) +(* UriManager.string_of_uri u)) constants;*) Constr.UriManagerSet.subset consts constants ;; @@ -236,6 +241,7 @@ let universe_of_goals ~(dbd:HMysql.dbd) proof goals = let predicates, rest = Constr.UriManagerSet.partition is_predicate all_constants_closed in + prerr_endline ("FOO!1"); let uris = Constr.UriManagerSet.fold (fun u acc -> @@ -246,6 +252,7 @@ let universe_of_goals ~(dbd:HMysql.dbd) proof goals = acc @ uris) predicates [] in + prerr_endline ("FOO!2"); (* let uris = sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) @@ -262,13 +269,13 @@ let filter_out_predicate set ctx menv = ;; let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) = -(* let to_string set = - "{ " ^ - (String.concat ", " + let to_string set = + "{\n" ^ + (String.concat "\n" (Constr.UriManagerSet.fold - (fun u l -> (UriManager.string_of_uri u)::l) set [])) - ^ " }" - in *) + (fun u l -> (" "^UriManager.string_of_uri u)::l) set [])) + ^ "\n}" + in let (_, metasenv, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let main, sig_constants = @@ -306,11 +313,13 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) = (* Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *) let set = close_with_constructors set metasenv context in (* Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *) - let set = List.fold_right Constr.UriManagerSet.remove l set in + let set_for_sigmatch = List.fold_right Constr.UriManagerSet.remove l set in let uris = - sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in + sigmatch ~dbd ~facts:false ~where:`Statement (main,set_for_sigmatch) in let uris = List.filter nonvar (List.map snd uris) in let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in + let set = List.fold_right Constr.UriManagerSet.add l set in + let uris = List.filter (only set) uris in uris (* ) *) (* else raise Goal_is_not_an_equation *) diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 655939851..7123c134a 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -1003,7 +1003,9 @@ let is_weak_identity eq = let is_identity (_, context, ugraph) eq = let _,_,(ty,left,right,_),menv,_ = open_equality eq in (* doing metaconv here is meaningless *) - fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph) + left = right +(* fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph) + * *) ;; diff --git a/components/tactics/paramodulation/equality_retrieval.ml b/components/tactics/paramodulation/equality_retrieval.ml index 886cc7ffe..e0e92b408 100644 --- a/components/tactics/paramodulation/equality_retrieval.ml +++ b/components/tactics/paramodulation/equality_retrieval.ml @@ -210,10 +210,10 @@ let find_context_equalities let module T = CicTypeChecker in let _,metasenv,_,_ = proof in let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in - let use_auto, auto = + let auto = match auto with - | None -> false, default_auto - | Some auto -> true, auto in + | None -> default_auto + | Some auto -> auto in (* if use_auto is true, we try to close the hypothesis of equational statements using auto; a naif, and probably wrong approach *) let rec aux cache index newmeta = function @@ -224,7 +224,7 @@ let find_context_equalities (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term))); let do_find context term = match term with - | C.Prod (name, s, t) when (is_an_equality t && use_auto) -> + | C.Prod (name, s, t) when is_an_equality t -> (try let term = S.lift index term in let saturated,cache,newmeta = @@ -302,10 +302,10 @@ let find_library_equalities bag let candidates = List.map utty_of_u eqs in let candidates = List.filter is_monomorphic_eq candidates in let candidates = List.filter is_var_free candidates in - let use_auto, auto = + let auto = match auto with - | None -> false, default_auto - | Some auto -> true, auto in + | None -> default_auto + | Some auto -> auto in (* if use_auto is true, we try to close the hypothesis of equational statements using auto; a naif, and probably wrong approach *) let rec aux cache newmeta = function @@ -317,7 +317,7 @@ let find_library_equalities bag (CicPp.ppterm term) (CicPp.ppterm termty))); let res, newmeta, cache = match termty with - | C.Prod (name, s, t) when use_auto -> + | C.Prod (name, s, t) -> (try let saturated,cache,newmeta = close_hypothesis_of_term context metasenv newmeta termty @@ -341,7 +341,6 @@ let find_library_equalities bag eqs, newmeta , cache with AutoFailure (cache,newmeta) -> [], newmeta , cache) - | C.Prod _ -> [], newmeta, cache | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in [e], newmeta+1, cache diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma index e9353ba5b..1ec8f68c5 100644 --- a/matita/library/nat/ord.ma +++ b/matita/library/nat/ord.ma @@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/nat/ord". include "datatypes/constructors.ma". include "nat/exp.ma". include "nat/gcd.ma". +include "nat/relevant_equations.ma". (* required by auto paramod *) (* this definition of log is based on pairs, with a remainder *) diff --git a/matita/library/nat/relevant_equations.ma b/matita/library/nat/relevant_equations.ma index f4cf43775..af8f68d5b 100644 --- a/matita/library/nat/relevant_equations.ma +++ b/matita/library/nat/relevant_equations.ma @@ -16,6 +16,8 @@ set "baseuri" "cic:/matita/nat/relevant_equations.ma". include "nat/times.ma". include "nat/minus.ma". +include "nat/gcd.ma". +(* if gcd is compiled before this, the applys will take too much *) theorem times_plus_l: \forall n,m,p:nat. (n+m)*p = n*p + m*p. intros. diff --git a/matita/tests/applys.ma b/matita/tests/applys.ma index c929e5be5..1115eaf92 100644 --- a/matita/tests/applys.ma +++ b/matita/tests/applys.ma @@ -30,10 +30,10 @@ qed. theorem prova2 : \forall n. S n \divides (S n)!. intros. -(* o fare una List.rev quando si fa la make_passives... la tira su, - ma tardi.... +(* se non trova subito sym_times poi si perde! *) +(* alternativamente si puo' abilitare la are_convertible nella + is_identity, ma poi va peggio nel resto (conv lunghe) *) letin www \def sym_times. clearbody www. -*) applyS (witness ? ? ? (refl_eq ? ?)). qed. -- 2.39.2