Fixing indexing (commit parziale di Claudio?)

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 89673e7d75dae131b867114380e98b37fec483f6..fe2da884d4c1f02c2c808e97b2c40fe9fa522a88 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -530,9 +530,16 @@ let record_index_obj =
    end
 ;;
 
-let compute_keys uri height kind = 
- let mk_item orig_ty spec =
-  let keys = NnAuto.keys_of_cic_term [] [] [] orig_ty in
+let compute_keys status uri height kind = 
+ let mk_item ty spec =
+   let orig_ty = NTacStatus.mk_cic_term [] ty in
+   let status,keys = NnAuto.keys_of_type status orig_ty in
+   let keys =  
+     List.map 
+       (fun t -> 
+         snd (NTacStatus.term_of_cic_term status t (NTacStatus.ctx_of t)))
+       keys
+   in
    keys,NCic.Const(NReference.reference_of_spec uri spec)
  in
  let data = 
@@ -578,12 +585,12 @@ let compute_keys uri height kind =
           NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
         None
       end)
-   data
+    data
 ;;
 
 let index_obj_for_auto status (uri, height, _, _, kind) = 
  (*prerr_endline (string_of_int height);*)
-  let data = compute_keys uri height kind in
+  let data = compute_keys status uri height kind in
   let status = basic_index_obj data status in
   let dump = record_index_obj data :: status#dump in   
   status#set_dump dump

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index baa38195ae6fd690bd8ab34e3015f7e0d817d781..b6bfbc6a38b7acfd880ea07a671edb35cdbd8c16 100644 (file)
--- 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)
 
@@ -535,8 +584,7 @@ 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
+let keys_of_type status orig_ty =
   let _, ty, _ = saturate ~delta:max_int status orig_ty in
   let keys = [ty] in
   let keys = 
@@ -552,6 +600,11 @@ let keys_of_term status t =
   status, keys
 ;;
 
+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 ->
@@ -1117,8 +1170,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,6 +1554,7 @@ 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 stack = 
@@ -1510,6 +1566,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

diff --git a/helm/software/components/ng_tactics/nnAuto.mli b/helm/software/components/ng_tactics/nnAuto.mli
index bc71db5c6d5cfa4e3d573b455838128736c7d5db..8f56541e3d95732e3cbd732e1e4cd556b3538623 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.mli
+++ b/helm/software/components/ng_tactics/nnAuto.mli
@@ -31,3 +31,7 @@ val auto_tac:
   params:(NTacStatus.tactic_term list option * (string * string) list) -> 
    's NTacStatus.tactic
 
+val keys_of_type: 
+  (#NTacStatus.pstatus as 'a) ->
+  NTacStatus.cic_term -> 'a * NTacStatus.cic_term list
+