]> matita.cs.unibo.it Git - helm.git/commitdiff
some experiment filtering with height
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 11 Feb 2010 09:49:47 +0000 (09:49 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 11 Feb 2010 09:49:47 +0000 (09:49 +0000)
helm/software/components/ng_tactics/nnAuto.ml
helm/software/matita/nlibrary/arithmetics/nat.ma
helm/software/matita/nlibrary/depends

index ce0a1b00ee2c2e45b20ef04ea6473c96a156dae1..0d8655f541d3be63752ea9cf9b414968ae3dea9c 100644 (file)
@@ -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;
index d8ac55049f19e5c3d16008f4f4387f1b28442131..393f16189a9001d8dacab469c43f285ce8123533 100644 (file)
@@ -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.
index 9f5c28b24c7ca4f041989e310e3480f185898f45..31dd702c8110a7dbfe34a537e5d6bba2d8d07da2 100644 (file)
@@ -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