X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=7a9c20f0f85ce0b6106db7819162bf470c9d9793;hb=1c8e230b1d81491b38126900d76201fb84303ced;hp=93078df257ab9aadfc781cbdd8e07d06f1decec1;hpb=4c1ae9c678da6c94c69d3cb6d8cb296c32d324e6;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 93078df25..7a9c20f0f 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -58,6 +58,14 @@ let toref f tbl t =
     | Ast.NCic _  (* local candidate *)
     | _  ->  ()
 
+let is_relevant tbl item =
+  try
+    let v = RefHash.find tbl item in
+      if !(v.nominations) < 60 then true (* not enough info *)
+      else if !(v.uses) = 0 then false
+      else true
+  with Not_found -> true
+
 let print_stat tbl =
   let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
   let relevance v = float !(v.uses) /. float !(v.nominations) in
@@ -65,10 +73,12 @@ let print_stat tbl =
     Pervasives.compare (relevance v1) (relevance v2) in
   let l = List.sort vcompare l in
   let vstring (a,v)=
-    CicNotationPp.pp_term (Ast.NRef a) ^ ": rel = " ^
+      CicNotationPp.pp_term (Ast.NCic (NCic.Const a)) ^ ": rel = " ^
       (string_of_float (relevance v)) ^
-      "; uses = " ^ (string_of_int !(v.uses)) in
-  lazy (String.concat "\n" (List.map vstring l)) 
+      "; uses = " ^ (string_of_int !(v.uses)) ^
+      "; nom = " ^ (string_of_int !(v.nominations)) in
+  lazy ("\n\nSTATISTICS:\n" ^
+	  String.concat "\n" (List.map vstring l)) 
 
 (* ======================= utility functions ========================= *)
 module IntSet = Set.Make(struct type t = int let compare = compare end)
@@ -259,7 +269,7 @@ let solve f status eq_cache goal =
       (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
 ;;
 
-let fast_eq_check eq_cache status goal =
+let fast_eq_check eq_cache status (goal:int) =
   match solve NCicParamod.fast_eq_check status eq_cache goal with
   | [] -> raise (Error (lazy "no proof found",None))
   | s::_ -> s
@@ -274,17 +284,15 @@ let auto_eq_check eq_cache status =
     let s = dist_fast_eq_check eq_cache status in
       [s]
   with
-    | Error _ -> []
+    | Error _ -> debug_print (lazy ("no paramod proof found"));[]
 ;;
 
-(* warning: ctx is supposed to be already instantiated w.r.t subst *)
 let index_local_equations eq_cache status =
   debug_print (lazy "indexing equations");
   let open_goals = head_goals status#stack in
   let open_goal = List.hd open_goals in
   let ngty = get_goalty status open_goal in
-  let ctx = ctx_of ngty in
-  let ctx = apply_subst_context ~fix_projections:true status ctx in
+  let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
   let c = ref 0 in
   List.fold_left 
     (fun eq_cache _ ->
@@ -294,7 +302,6 @@ let index_local_equations eq_cache status =
            let ty = NCicTypeChecker.typeof [] [] ctx t in
            if is_a_fact status (mk_cic_term ctx ty) then
              (debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
-              debug_print(lazy("riprovo " ^ (ppterm status (mk_cic_term ctx ty))));
               NCicParamod.forward_infer_step eq_cache t ty)
            else 
              (debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty)));
@@ -571,6 +578,8 @@ let smart_apply t unit_eq status g =
         debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
         fast_eq_check unit_eq status j
     with
+      | NCicEnvironment.ObjectNotFound s as e ->
+          raise (Error (lazy "eq_coerc non yet defined",Some e))
       | Error _ as e -> debug_print (lazy "error"); raise e
 
 let smart_apply_tac t s =
@@ -985,8 +994,11 @@ let get_candidates ?(smart=true) depth flags status cache signature gty =
       | None -> 
 	  let mapf s = 
 	    let to_ast = function 
-	      | NCic.Const r -> Ast.NRef r | _ -> assert false in
-	      List.map to_ast (NDiscriminationTree.TermSet.elements s) in
+	      | NCic.Const r when true (*is_relevant statistics r*) -> Some (Ast.NRef r)
+	      | NCic.Const _ -> None 
+	      | _ -> assert false in
+	      HExtlib.filter_map 
+		to_ast (NDiscriminationTree.TermSet.elements s) in
 	  let g,l = 
 	    get_cands
 	      (NDiscriminationTree.DiscriminationTree.retrieve_unifiables 
@@ -1101,10 +1113,32 @@ let applicative_case depth signature status flags gty cache =
 	| NCic.Prod _ -> true, false
 	| _ -> false, NCicParamod.is_equation metasenv subst context t 
   in
-  debug_print(lazy (string_of_bool is_eq)); 
+  debug_print~depth (lazy (string_of_bool is_eq)); 
+  (* old 
   let candidates, smart_candidates = 
     get_candidates ~smart:(not is_eq) depth 
-      flags status tcache signature gty in
+      flags status tcache signature gty in 
+    (* if the goal is an equation we avoid to apply unit equalities,
+       since superposition should take care of them; refl is an
+       exception since it prompts for convertibility *)
+  let candidates = 
+    let test x = not (is_a_fact_ast status subst metasenv context x) in
+    if is_eq then 
+      Ast.Ident("refl",None) ::List.filter test candidates 
+    else candidates in *)
+  (* new *)
+  let candidates, smart_candidates = 
+    get_candidates ~smart:true depth 
+      flags status tcache signature gty in 
+    (* if the goal is an equation we avoid to apply unit equalities,
+       since superposition should take care of them; refl is an
+       exception since it prompts for convertibility *)
+  let candidates,smart_candidates = 
+    let test x = not (is_a_fact_ast status subst metasenv context x) in
+    if is_eq then 
+      Ast.Ident("refl",None) ::List.filter test candidates,
+      List.filter test smart_candidates
+    else candidates,smart_candidates in 
   debug_print ~depth
     (lazy ("candidates: " ^ string_of_int (List.length candidates)));
   debug_print ~depth
@@ -1210,13 +1244,13 @@ let is_prod status =
   let _, raw_gty = term_of_cic_term status gty ctx in
   match raw_gty with
     | NCic.Prod (name,src,_) ->
-        let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
+        let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in 
         (match snd (term_of_cic_term status src ctx) with
         | NCic.Const(NReference.Ref (_,NReference.Ind _) as r) 
         | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
             let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys r in
             (match itys with
-            | [_,_,_,[_;_]] 
+            (* | [_,_,_,[_;_]]  con nat va, ovviamente, in loop *)
             | [_,_,_,[_]] 
             | [_,_,_,[]] -> `Inductive (guess_name name ctx)         
             | _ -> `Some (guess_name name ctx))
@@ -1237,13 +1271,14 @@ let intro ~depth status facts name =
 let rec intros_facts ~depth status facts =
   if List.length (head_goals status#stack) <> 1 then status, facts else
   match is_prod status with
+    | `Inductive name 
     | `Some(name) ->
         let status,facts =
           intro ~depth status facts name
-        in intros_facts ~depth status facts 
-    | `Inductive name ->
+        in intros_facts ~depth status facts
+(*    | `Inductive name ->
           let status = NTactics.case1_tac name status in
-          intros_facts ~depth status facts
+          intros_facts ~depth status facts *)
     | _ -> status, facts
 ;; 
 
@@ -1629,7 +1664,7 @@ let cleanup_trace s trace =
 	    | _ -> false) trace
 ;;
 
-let auto_tac ~params:(univ,flags) status =
+let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
   let oldstatus = status in
   let status = (status:> NTacStatus.tac_status) in
   let goals = head_goals status#stack in
@@ -1701,6 +1736,7 @@ let auto_tac ~params:(univ,flags) status =
                   | _ -> assert false
               in
               let s = s#set_stack stack in
+                trace_ref := trace;
                 oldstatus#set_status s 
   in
   let s = up_to depth depth in