From: Enrico Tassi Date: Thu, 11 Feb 2010 09:49:47 +0000 (+0000) Subject: some experiment filtering with height X-Git-Tag: make_still_working~3046 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3f3d273d3b515a8b78c4aca2b28fa00ed26e0395;p=helm.git some experiment filtering with height --- diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index ce0a1b00e..0d8655f54 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -1409,6 +1409,65 @@ exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive atoms of the input goals *) exception Proved of NTacStatus.tac_status +let height_of_ref (NReference.Ref (uri, x)) = + match x with + | NReference.Decl + | NReference.Ind _ + | NReference.Con _ + | NReference.CoFix _ -> + let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in + height + | NReference.Def h -> h + | NReference.Fix (_,_,h) -> h +;; + +let fast_height_of_term t = + let h = ref 0 in + let rec aux = + function + NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l + | NCic.Meta _ -> () + | NCic.Rel _ + | NCic.Sort _ -> () + | NCic.Implicit _ -> assert false + | NCic.Const nref as t -> +(* + prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] + ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref)); +*) + h := max !h (height_of_ref nref) + | NCic.Prod (_,t1,t2) + | NCic.Lambda (_,t1,t2) -> aux t1; aux t2 + | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t + | NCic.Appl l -> List.iter aux l + | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl + in + aux t; !h +;; + +let height_of_goals status = + let open_goals = head_goals status#stack in + assert (List.length open_goals > 0); + let h = ref 0 in + List.iter + (fun open_goal -> + let ty = get_goalty status open_goal in + let context = ctx_of ty in + let _, ty = term_of_cic_term status ty (ctx_of ty) in + h := max !h (fast_height_of_term ty); + List.iter + (function + | _, NCic.Decl ty -> h := max !h (fast_height_of_term ty) + | _, NCic.Def (bo,ty) -> + h := max !h (fast_height_of_term ty); + h := max !h (fast_height_of_term bo); + ) + context) + open_goals; + prerr_endline ("altezza sequente: " ^ string_of_int !h); + !h +;; + (* let close_failures _ c = c;; *) (* let prunable _ _ _ = false;; *) (* let cache_examine cache gty = `Notfound;; *) @@ -1423,7 +1482,22 @@ let init_cache ?(facts=[]) ?(under_inspection=[]) unit_eq = unit_eq } -let only _ _ _ = true;; +let only signature _context candidate = + (* TASSI: nel trie ci mettiamo solo il body, non il ty *) + let candidate_ty = + NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate + in + let height = fast_height_of_term candidate_ty in + let rc = signature >= height in + if rc = false then + prerr_endline ("Filtro: " ^ NCicPp.ppterm ~context:[] ~subst:[] + ~metasenv:[] candidate ^ ": " ^ string_of_int height) + else + prerr_endline ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[] + ~metasenv:[] candidate ^ ": " ^ string_of_int height); + + rc +;; let candidate_no = ref 0;; @@ -1912,8 +1986,8 @@ let auto_tac ~params:(_univ,flags) status = let size = int "size" flags 10 in let width = int "width" flags 4 (* (3+List.length goals)*) in (* XXX fix sort *) - let goals = List.map (fun i -> (i,P)) goals in - let signature = () in +(* let goals = List.map (fun i -> (i,P)) goals in *) + let signature = height_of_goals status in let flags = { last = true; maxwidth = width; diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma index d8ac55049..393f16189 100644 --- a/helm/software/matita/nlibrary/arithmetics/nat.ma +++ b/helm/software/matita/nlibrary/arithmetics/nat.ma @@ -259,13 +259,18 @@ ntheorem le_n_Sn : ∀n:nat. n ≤ S n. ntheorem le_pred_n : ∀n:nat. pred n ≤ n. #n; nelim n; //; nqed. +(* XXX global problem *) +nlemma my_trans_le : ∀x,y,z:nat.x ≤ y → y ≤ z → x ≤ z. +napply transitive_le. +nqed. + ntheorem monotonic_pred: monotonic ? le pred. -#n; #m; #lenm; nelim lenm; //; /2/; nqed. +#n; #m; #lenm; nelim lenm; /2/; nqed. ntheorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m. -/2/; nqed. +(* XXX *) nletin hint ≝ monotonic. /2/; nqed. -ntheorem lt_S_S_to_lt: ∀n,m. S n < S m \to n < m. +ntheorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m. /2/; nqed. ntheorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m. @@ -835,7 +840,7 @@ ntheorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m). #n; #m; #lenm; nelim lenm; napplyS refl_eq. *) napply nat_elim2; ##[// - ##|#n; #abs; napply False_ind;/2/; + ##|#n; #abs; napply False_ind; (* XXX *) napply not_le_Sn_O; /2/. ##|#n; #m; #Hind; #c; napplyS Hind; /2/; ##] nqed. @@ -854,7 +859,7 @@ ntheorem plus_minus: ∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m. napply nat_elim2; ##[// - ##|#n; #p; #abs; napply False_ind;/2/; + ##|#n; #p; #abs; napply False_ind; (* XXX *) napply not_le_Sn_O; /2/; ##|nnormalize;/3/; ##] nqed. @@ -1026,9 +1031,9 @@ ntheorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop. (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). napply nat_elim2; ##[#n; ncases n; nnormalize; /3/; - ##|nnormalize; /3/; - ##|nnormalize; /4/; - ##] + ##|nnormalize; (* XXX *) nletin hint ≝ not_eq_O_S; /3/; + ##|nnormalize; /4/; + ##] (* XXX rimane aperto *) #m; #P; #_; #H; napply H; napply not_eq_O_S. nqed. ntheorem eqb_n_n: ∀n. eqb n n = true. @@ -1037,7 +1042,7 @@ nqed. ntheorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m. #n; #m; napply (eqb_elim n m);//; -#_; #abs; napply False_ind;/2/; +#_; #abs; napply False_ind; (* XXX *) nletin hint ≝ not_eq_true_false; /2/; nqed. ntheorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m. @@ -1067,7 +1072,7 @@ ntheorem leb_elim: ∀n,m:nat. ∀P:bool → Prop. (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m). napply nat_elim2; nnormalize; ##[/2/ - ##|/3/; + ##| (* XXX *) nletin hint ≝ not_le_Sn_O; /3/; ##|#n; #m; #Hind; #P; #Pt; #Pf; napply Hind; ##[#lenm; napply Pt; napply le_S_S;//; ##|#nlenm; napply Pf; #leSS; /3/; @@ -1078,14 +1083,14 @@ nqed. ntheorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m. #n; #m; napply leb_elim; ##[//; - ##|#_; #abs; napply False_ind; /2/; + ##|#_; #abs; napply False_ind; (* XXX *) nletin hint ≝ not_eq_true_false; /2/; ##] nqed. ntheorem leb_false_to_not_le:∀n,m. leb n m = false → n ≰ m. #n; #m; napply leb_elim; - ##[#_; #abs; napply False_ind; /2/; + ##[#_; #abs; napply False_ind; (* XXX *) nletin hint ≝ not_eq_true_false; /2/; ##|/2/; ##] nqed. diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 9f5c28b24..31dd702c8 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,40 +1,44 @@ -overlap/o-algebra.ma sets/categories2.ma algebra/bool.ma logic/connectives.ma +overlap/o-algebra.ma sets/categories2.ma algebra/abelian_magmas.ma algebra/magmas.ma basics/functions.ma Plogic/connectives.ma Plogic/equality.ma Plogic/connectives.ma Plogic/equality.ma -arithmetics/nat.ma basics/eq.ma basics/functions.ma -datatypes/bool.ma logic/pts.ma +arithmetics/nat.ma basics/bool.ma basics/eq.ma basics/functions.ma hints_declaration.ma logic/destruct_bb.ma logic/equality.ma +datatypes/bool.ma logic/pts.ma logic/equality.ma logic/connectives.ma properties/relations.ma sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma logic/cprop.ma hints_declaration.ma sets/setoids1.ma +basics/bool.ma basics/eq.ma basics/functions.ma topology/igft.ma logic/equality.ma sets/sets.ma -nat/minus.ma nat/order.ma +foo.ma logic/equality.ma logic/pts.ma nat/nat.ma algebra/magmas.ma sets/sets.ma +nat/minus.ma nat/order.ma hints_declaration.ma logic/pts.ma -Plogic/equality.ma logic/pts.ma properties/relations1.ma logic/pts.ma -algebra/unital_magmas.ma algebra/magmas.ma -nat/compare.ma datatypes/bool.ma nat/order.ma +Plogic/equality.ma logic/pts.ma sets/categories.ma sets/sets.ma properties/relations2.ma logic/pts.ma +algebra/unital_magmas.ma algebra/magmas.ma +nat/compare.ma datatypes/bool.ma nat/order.ma nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma logic/connectives.ma logic/pts.ma basics/relations.ma Plogic/connectives.ma -topology/igft-setoid.ma sets/sets.ma +basics/list.ma basics/bool.ma basics/eq.ma sets/categories2.ma sets/categories.ma sets/setoids2.ma sets/sets.ma +topology/igft-setoid.ma sets/sets.ma sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma -datatypes/pairs.ma logic/pts.ma -nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma -nat/order.ma nat/nat.ma sets/sets.ma logic/pts.ma -topology/cantor.ma nat/nat.ma topology/igft.ma +nat/order.ma nat/nat.ma sets/sets.ma +nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma +datatypes/pairs.ma logic/pts.ma sets/setoids1.ma hints_declaration.ma properties/relations1.ma sets/setoids.ma -nat/big_ops.ma algebra/magmas.ma nat/order.ma +topology/cantor.ma nat/nat.ma topology/igft.ma sets/setoids2.ma properties/relations2.ma sets/setoids1.ma +nat/big_ops.ma algebra/magmas.ma nat/order.ma topology/igft2.ma arithmetics/nat.ma topology/igft.ma -topology/igft3.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma properties/relations.ma logic/pts.ma +topology/igft3.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma +topology/igft4.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma basics/eq.ma basics/relations.ma sets/setoids.ma hints_declaration.ma logic/connectives.ma properties/relations.ma