X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=323777d18846e895eabfcaaeff3ae7e3e6c2ecfa;hb=ce0e8e7fc59e6a1f7ed6038370bdc1de096cdc01;hp=baa38195ae6fd690bd8ab34e3015f7e0d817d781;hpb=a14adba81c00c9dcb9996d7af39e4803214606f1;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index baa38195a..323777d18 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -19,8 +19,57 @@ let debug_print = noprint
 open Continuationals.Stack
 open NTacStatus
 module Ast = CicNotationPt
+
+(* ======================= statistics  ========================= *)
+
 let app_counter = ref 0
 
+module RHT = struct
+  type t = NReference.reference
+  let equal = (==)
+  let compare = Pervasives.compare
+  let hash = Hashtbl.hash
+end;;
+
+module RefHash = Hashtbl.Make(RHT);;
+
+type info = {
+  nominations : int ref;
+  uses: int ref;
+}
+
+let statistics: info RefHash.t = RefHash.create 503
+
+let incr_nominations tbl item =
+  try
+    let v = RefHash.find tbl item in incr v.nominations
+  with Not_found ->
+    RefHash.add tbl item {nominations = ref 1; uses = ref 0}
+
+let incr_uses tbl item =
+  try
+    let v = RefHash.find tbl item in incr v.uses
+  with Not_found -> assert false
+
+let toref f tbl t =
+  match t with
+    | Ast.NRef n -> 
+	f tbl n
+    | Ast.NCic _  (* local candidate *)
+    | _  ->  ()
+
+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
+  let vcompare (_,v1) (_,v2) =
+    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 = " ^
+      (string_of_float (relevance v)) ^
+      "; uses = " ^ (string_of_int !(v.uses)) in
+  lazy (String.concat "\n" (List.map vstring l)) 
+
 (* ======================= utility functions ========================= *)
 module IntSet = Set.Make(struct type t = int let compare = compare end)
 
@@ -195,12 +244,12 @@ let solve f status eq_cache goal =
     with 
         NCicRefiner.RefineFailure msg 
       | NCicRefiner.Uncertain msg ->
-          print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
+          debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
                         snd (Lazy.force msg) ^	
 			"\n in the environment\n" ^ 
 			NCicPp.ppmetasenv subst metasenv)); None
       | NCicRefiner.AssertFailure msg -> 
-          print (lazy ("WARNING: refining in fast_eq_check failed" ^
+          debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
                         Lazy.force msg ^
 			"\n in the environment\n" ^ 
 			NCicPp.ppmetasenv subst metasenv)); None
@@ -535,10 +584,93 @@ let smart_apply_auto t eq_cache =
 
 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
 
-let keys_of_term status t =
-  let status, orig_ty = typeof status (ctx_of t) t in
+(* cartesian: term set list -> term list set *)
+let rec cartesian =
+ function
+    [] -> NDiscriminationTree.TermListSet.empty
+  | [l] ->
+     NDiscriminationTree.TermSet.fold
+      (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
+  | he::tl ->
+     let rest = cartesian tl in
+      NDiscriminationTree.TermSet.fold
+       (fun x acc ->
+         NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
+       ) he NDiscriminationTree.TermListSet.empty
+;;
+
+(* all_keys_of_cic_type: term -> term set *)
+let all_keys_of_cic_type metasenv subst context ty =
+ let saturate ty =
+  (* Here we are dropping the metasenv, but this should not raise any
+     exception (hopefully...) *)
+  let ty,_,hyps =
+   NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0
+  in
+   ty,List.length hyps
+ in
+ let rec aux ty =
+  match ty with
+     NCic.Appl (he::tl) ->
+      let tl' =
+       List.map (fun ty ->
+        let wty = NCicReduction.whd ~delta:0 ~subst context ty in
+         if ty = wty then
+          NDiscriminationTree.TermSet.add ty (aux ty)
+         else
+          NDiscriminationTree.TermSet.union
+           (NDiscriminationTree.TermSet.add  ty (aux  ty))
+           (NDiscriminationTree.TermSet.add wty (aux wty))
+        ) tl
+      in
+       NDiscriminationTree.TermListSet.fold
+        (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
+        (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
+        NDiscriminationTree.TermSet.empty
+   | _ -> NDiscriminationTree.TermSet.empty
+ in
+  let ty,ity = saturate ty in
+  let wty,iwty = saturate (NCicReduction.whd ~delta:0 ~subst context ty) in
+   if ty = wty then
+    [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
+   else
+    [ity,  NDiscriminationTree.TermSet.add  ty (aux  ty) ;
+     iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
+;;
+
+let all_keys_of_type status t =
+ let _,_,metasenv,subst,_ = status#obj in
+ let context = ctx_of t in
+ let keys =
+  all_keys_of_cic_type metasenv subst context
+   (snd (term_of_cic_term status t context))
+ in
+  status,
+   List.map
+    (fun (intros,keys) ->
+      intros,
+       NDiscriminationTree.TermSet.fold
+        (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
+        keys Ncic_termSet.empty
+    ) keys
+;;
+
+
+let keys_of_type status orig_ty =
+  (* Here we are dropping the metasenv (in the status), but this should not
+     raise any exception (hopefully...) *)
   let _, ty, _ = saturate ~delta:max_int status orig_ty in
-  let keys = [ty] in
+  let keys =
+(*
+    let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
+    if orig_ty' <> orig_ty then
+     let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
+      [ty;ty']
+    else
+     [ty]
+*)
+   [ty] in
+(*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
   let keys = 
     let _, ty = term_of_cic_term status ty (ctx_of ty) in
     match ty with
@@ -552,6 +684,16 @@ let keys_of_term status t =
   status, keys
 ;;
 
+let all_keys_of_term status t =
+ let status, orig_ty = typeof status (ctx_of t) t in
+  all_keys_of_type status orig_ty
+;;
+
+let keys_of_term status t =
+  let status, orig_ty = typeof status (ctx_of t) t in
+    keys_of_type status orig_ty
+;;
+
 let mk_th_cache status gl = 
   List.fold_left 
     (fun (status, acc) g ->
@@ -875,11 +1017,28 @@ let get_candidates ?(smart=true) status cache signature gty =
   let c_ast = function 
     | NCic.Const r -> Ast.NRef r | _ -> assert false in
   let _, raw_gty = term_of_cic_term status gty context in
-  let cands = 
-    NDiscriminationTree.DiscriminationTree.retrieve_unifiables 
-      universe raw_gty 
-  in
+  let keys = all_keys_of_cic_term metasenv subst context raw_gty in
+  (* we only keep those keys that do not require any intros for now *)
+  let no_intros_keys = snd (List.hd keys) in
+  let cands =
+   NDiscriminationTree.TermSet.fold
+    (fun ty acc ->
+      NDiscriminationTree.TermSet.union acc
+       (NDiscriminationTree.DiscriminationTree.retrieve_unifiables 
+         universe ty)
+    ) no_intros_keys NDiscriminationTree.TermSet.empty in
+(* old code:
+  let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables 
+        universe raw_gty in 
+*)
+  let local_cands =
+   NDiscriminationTree.TermSet.fold
+    (fun ty acc ->
+      Ncic_termSet.union acc (search_in_th (mk_cic_term context ty) cache)
+    ) no_intros_keys Ncic_termSet.empty in
+(* old code:
   let local_cands = search_in_th gty cache in
+*)
   debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty));
   debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands)))));
   let together global local = 
@@ -1082,11 +1241,13 @@ let rec intros ~depth status cache =
       | _ -> status, cache
 ;;
 
-let reduce ~depth status g = 
+let reduce ~whd ~depth status g = 
   let n,h,metasenv,subst,o = status#obj in 
   let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
   let ty = NCicUntrusted.apply_subst subst ctx ty in
-  let ty' = NCicReduction.whd ~subst ctx ty in
+  let ty' =
+   (if whd then NCicReduction.whd else NCicTacReduction.normalize) ~subst ctx ty
+  in
   if ty = ty' then []
   else
     (debug_print ~depth 
@@ -1104,7 +1265,7 @@ let reduce ~depth status g =
 
 let do_something signature flags status g depth gty cache =
   (* whd *)
-  let l = reduce ~depth status g in
+  let l = (*reduce ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in
   (* if l <> [] then l,cache else *)
   (* backward aplications *)
   let l1 = 
@@ -1117,8 +1278,10 @@ let do_something signature flags status g depth gty cache =
   let l2 = 
     if ((l1 <> []) && flags.last) then [] else
     applicative_case depth signature status flags gty cache 
-  (* fast paramodulation *) 
   in
+  (* statistics *)
+  List.iter 
+    (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
   (* states in l1 have have an empty set of subgoals: no point to sort them *)
   debug_print ~depth 
     (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
@@ -1499,8 +1662,9 @@ let auto_tac ~params:(univ,flags) status =
           | Gaveup _ -> up_to (x+1) y
           | Proved (s,trace) -> 
               debug_print (lazy ("proved at depth " ^ string_of_int x));
+	      List.iter (toref incr_uses statistics) trace;
               let trace = cleanup_trace s trace in
-	      let _ = print (pptrace trace) in
+	      let _ = debug_print (pptrace trace) in
               let stack = 
                 match s#stack with
                   | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
@@ -1510,6 +1674,7 @@ let auto_tac ~params:(univ,flags) status =
                 oldstatus#set_status s 
   in
   let s = up_to depth depth in
+    debug_print (print_stat statistics);
     debug_print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
     debug_print(lazy