From: Andrea Asperti Date: Thu, 8 Apr 2010 13:02:05 +0000 (+0000) Subject: Fixing indexing (commit parziale di Claudio?) X-Git-Tag: make_still_working~2942 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dd29593d12cffd332c9d546167215f42a90fa9f7;p=helm.git Fixing indexing (commit parziale di Claudio?) From: asperti --- diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 89673e7d7..fe2da884d 100644 --- 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 baa38195a..b6bfbc6a3 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) @@ -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 bc71db5c6..8f56541e3 100644 --- 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 +