X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=7a9c20f0f85ce0b6106db7819162bf470c9d9793;hb=HEAD;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..7a9c20f0f 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -19,8 +19,67 @@ 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 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 + 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.NCic (NCic.Const a)) ^ ": rel = " ^ + (string_of_float (relevance v)) ^ + "; 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) @@ -117,7 +176,7 @@ let fast_height_of_term t = | NCic.Rel _ | NCic.Sort _ -> () | NCic.Implicit _ -> assert false - | NCic.Const nref as t -> + | NCic.Const nref -> (* prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref)); @@ -195,12 +254,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 @@ -210,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 @@ -225,16 +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_of ngty) in let c = ref 0 in List.fold_left (fun eq_cache _ -> @@ -470,7 +528,7 @@ let saturate_to_ref metasenv subst ctx nref ty = | NCic.Const(NReference.Ref (_,NReference.Def _) as nre) when nre<>nref -> let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in - aux metasenv ty (args@moreargs) + aux metasenv bo (args@moreargs) | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl) when nre<>nref -> let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in @@ -520,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 = @@ -535,10 +595,95 @@ 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 status, t = apply_subst status context 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 _, ty = apply_subst status (ctx_of ty) 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 +697,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 -> @@ -630,7 +785,7 @@ let search_in_th gty th = | [] -> (* Ncic_termSet.elements *) acc | (_::tl) as k -> try - let idx = List.assq k th in + let idx = List.assoc(*q*) k th in let acc = Ncic_termSet.union acc (InvRelDiscriminationTree.retrieve_unifiables idx gty) in @@ -755,7 +910,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status else (* smart = 2: both *) try NTactics.apply_tac ("",0,t) status - with Error _ as exc -> + with Error _ -> smart_apply_auto ("",0,t) eq_cache status in (* @@ -839,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 @@ -875,11 +1033,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 = @@ -938,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 @@ -1043,10 +1240,22 @@ let rec guess_name name ctx = let is_prod status = let _, ctx, gty = current_goal status in + let status, gty = apply_subst status ctx gty in let _, raw_gty = term_of_cic_term status gty ctx in match raw_gty with - | NCic.Prod (name,_,_) -> Some (guess_name name ctx) - | _ -> None + | NCic.Prod (name,src,_) -> + 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)) + | _ -> `Some (guess_name name ctx)) + | _ -> `None let intro ~depth status facts name = let status = NTactics.intro_tac name status in @@ -1060,33 +1269,46 @@ 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 - | Some(name) -> + | `Inductive name + | `Some(name) -> let status,facts = intro ~depth status facts name - in intros_facts ~depth status facts + in intros_facts ~depth status facts +(* | `Inductive name -> + let status = NTactics.case1_tac name status in + intros_facts ~depth status facts *) | _ -> status, facts ;; -let rec intros ~depth status cache = +let intros ~depth status cache = match is_prod status with - | Some _ -> + | `Inductive _ + | `Some _ -> let trace = cache.trace in let status,facts = intros_facts ~depth status cache.facts in + if head_goals status#stack = [] then + let status = NTactics.merge_tac status in + [(0,Ast.Ident("__intros",None)),status], cache + else (* we reindex the equation from scratch *) - let unit_eq = - index_local_equations status#eq_cache status in - status, init_cache ~facts ~unit_eq () ~trace - | _ -> status, cache + let unit_eq = index_local_equations status#eq_cache status in + let status = NTactics.merge_tac status in + [(0,Ast.Ident("__intros",None)),status], + init_cache ~facts ~unit_eq () ~trace + | _ -> [],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 @@ -1103,8 +1325,11 @@ let reduce ~depth status g = ;; let do_something signature flags status g depth gty cache = + let l0, cache = intros ~depth status cache in + if l0 <> [] then l0, cache + else (* 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 +1342,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))))); @@ -1374,7 +1601,6 @@ auto_main flags signature cache depth status: unit = raise (Gaveup IntSet.empty) else let status = NTactics.branch_tac ~force:true status in - let status, cache = intros ~depth status cache in let g,gctx, gty = current_goal status in let ctx,ty = close status g in let closegty = mk_cic_term ctx ty in @@ -1402,7 +1628,9 @@ auto_main flags signature cache depth status: unit = debug_print (~depth:depth) (lazy ("Case: " ^ CicNotationPp.pp_term t)); let depth,cache = - if t=Ast.Ident("__whd",None) then depth, cache + if t=Ast.Ident("__whd",None) || + t=Ast.Ident("__intros",None) + then depth, cache else depth+1,loop_cache in let cache = add_to_trace ~depth cache t in try @@ -1436,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 @@ -1499,17 +1727,20 @@ 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 | _ -> 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 + debug_print (print_stat statistics); debug_print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); debug_print(lazy