X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=7a9c20f0f85ce0b6106db7819162bf470c9d9793;hb=72e835f5e6848c09faf6343fb7e276c88bfc1f2e;hp=323777d18846e895eabfcaaeff3ae7e3e6c2ecfa;hpb=d0c7735ccdde99179105d56a8fafa22060aa6184;p=helm.git diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 323777d18..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) @@ -166,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)); @@ -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,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 _ -> @@ -519,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 @@ -569,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 = @@ -641,6 +652,7 @@ let all_keys_of_cic_type metasenv subst context ty = 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)) @@ -660,6 +672,7 @@ 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 _, ty = apply_subst status (ctx_of ty) ty in let keys = (* let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in @@ -772,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 @@ -897,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 (* @@ -981,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 @@ -1097,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 @@ -1202,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 @@ -1219,26 +1269,37 @@ 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 ~whd ~depth status g = @@ -1264,6 +1325,9 @@ let reduce ~whd ~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 ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in (* if l <> [] then l,cache else *) @@ -1537,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 @@ -1565,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 @@ -1599,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 @@ -1671,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