X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=d492b1cb41b3398f44be46b924931b832e8ea91c;hb=95639a0a6e187e8ba8c08e71688d8065ef319408;hp=320f4f630c07c5787be6e7211ebcbd7132b56c1a;hpb=df2f819793eaf676cb2aef27c9518f740fcae3f6;p=helm.git diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 320f4f630..d492b1cb4 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -26,9 +26,9 @@ let app_counter = ref 0 module RHT = struct type t = NReference.reference - let equal = (==) - let compare = Pervasives.compare - let hash = Hashtbl.hash + let equal = NReference.eq + let compare = NReference.compare + let hash = NReference.hash end;; module RefHash = Hashtbl.Make(RHT);; @@ -72,8 +72,12 @@ let print_stat status tbl = let vcompare (_,v1) (_,v2) = Pervasives.compare (relevance v1) (relevance v2) in let l = List.sort vcompare l in + let short_name r = + Filename.chop_extension + (Filename.basename (NReference.string_of_reference r)) + in let vstring (a,v)= - NotationPp.pp_term status (Ast.NCic (NCic.Const a)) ^ ": rel = " ^ + short_name a ^ ": rel = " ^ (string_of_float (relevance v)) ^ "; uses = " ^ (string_of_int !(v.uses)) ^ "; nom = " ^ (string_of_int !(v.nominations)) in @@ -263,6 +267,7 @@ let solve f status eq_cache goal = Lazy.force msg ^ "\n in the environment\n" ^ status#ppmetasenv subst metasenv)); None + | Sys.Break as e -> raise e | _ -> None in HExtlib.filter_map build_status @@ -288,10 +293,11 @@ let auto_eq_check eq_cache status = ;; let index_local_equations eq_cache status = + noprint (lazy "indexing equations"); let open_goals = head_goals status#stack in let open_goal = List.hd open_goals in - debug_print (lazy ("indexing equations for " ^ string_of_int open_goal)); let ngty = get_goalty status open_goal in + let _,_,metasenv,subst,_ = status#obj in let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in let c = ref 0 in List.fold_left @@ -299,12 +305,12 @@ let index_local_equations eq_cache status = c:= !c+1; let t = NCic.Rel !c in try - let ty = NCicTypeChecker.typeof status [] [] ctx t in + let ty = NCicTypeChecker.typeof status subst metasenv ctx t in if is_a_fact status (mk_cic_term ctx ty) then - (debug_print(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty))); - NCicParamod.forward_infer_step eq_cache t ty) + (debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty))); + NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty) else - (noprint (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty))); + (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty))); eq_cache) with | NCicTypeChecker.TypeCheckerFailure _ @@ -431,7 +437,9 @@ let close_metasenv status metasenv subst = (* prerr_endline (status#ppterm ctx [] [] iterm); *) let s_entry = i, ([], ctx, iterm, ty) in s_entry::subst,okind::objs - with _ -> assert false) + with + Sys.Break as e -> raise e + | _ -> assert false) (subst,[]) metasenv ;; @@ -973,6 +981,9 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = with Error _ -> smart_apply_auto ("",0,t) eq_cache status in +(* FG: this optimization rules out some applications of + * lift_bind (from contribs/lambda_delta/Basic_2/substitution/lift.ma) + * (* we compare the expected branching with the actual one and prune the candidate when the latter is larger. The optimization is meant to rule out stange applications of flexible terms, @@ -993,7 +1004,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no))); debug_print ~depth (lazy "strange application"); None) else - (incr candidate_no; Some ((!candidate_no,t),status)) +*) (incr candidate_no; Some ((!candidate_no,t),status)) with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None ;; @@ -1011,7 +1022,7 @@ let perforate_small status subst metasenv context t = let rec aux = function | NCic.Appl (hd::tl) -> let map t = - let s = sort_of status subst metasenv context t in + let s = sort_of status subst metasenv context t in match s with | NCic.Sort(NCic.Type [`Type,u]) when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0)) @@ -1032,7 +1043,7 @@ let get_cands retrieve_for diff empty gty weak_gty = cands, diff more_cands cands ;; -let get_candidates ?(smart=true) depth flags status cache signature gty = +let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty = let universe = status#auto_cache in let _,_,metasenv,subst,_ = status#obj in let context = ctx_of gty in @@ -1057,7 +1068,7 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = let raw_weak = perforate_small status subst metasenv context raw_gty in let weak = mk_cic_term context raw_weak in - debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak)); + noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak)); Some raw_weak, Some (weak) | _ -> None,None else None,None @@ -1102,10 +1113,11 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = let candidates_facts,candidates_other = let gl1,gl2 = List.partition test global_cands in let ll1,ll2 = List.partition test local_cands in - (* if the goal is an equation we avoid to apply unit equalities, - since superposition should take care of them; refl is an + (* if the goal is an equation and paramodulation did not fail + we avoid to apply unit equalities; refl is an exception since it prompts for convertibility *) - let l1 = if is_eq then [Ast.Ident("refl",None)] else gl1@ll1 in + let l1 = if is_eq && (not pfailed) + then [Ast.Ident("refl",None)] else gl1@ll1 in let l2 = (* if smart given candidates are applied in smart mode *) if by && smart then ll2 @@ -1133,7 +1145,7 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = sort_candidates status context (smart_candidates_other) ;; -let applicative_case depth signature status flags gty cache = +let applicative_case ~pfailed depth signature status flags gty cache = app_counter:= !app_counter+1; let _,_,metasenv,subst,_ = status#obj in let context = ctx_of gty in @@ -1149,7 +1161,7 @@ let applicative_case depth signature status flags gty cache = (* new *) let candidates_facts, smart_candidates_facts, candidates_other, smart_candidates_other = - get_candidates ~smart:true depth + get_candidates ~smart:true ~pfailed depth flags status tcache signature gty in let sm = if is_eq || is_prod then 0 else 2 in @@ -1183,7 +1195,6 @@ let applicative_case depth signature status flags gty cache = exception Found ;; - (* gty is supposed to be meta-closed *) let is_subsumed depth filter_depth status gty cache = if cache=[] then false else ( @@ -1354,7 +1365,7 @@ let is_meta status gty = let do_something signature flags status g depth gty cache = (* if the goal is meta we close it with I:True. This should work - thnaks to the toplogical sorting of goals. *) + thanks to the toplogical sorting of goals. *) if is_meta status gty then let t = Ast.Ident("I",None) in debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t)); @@ -1377,7 +1388,7 @@ let do_something signature flags status g depth gty cache = in let l2 = if ((l1 <> []) && flags.last) then [] else - applicative_case depth signature status flags gty cache + applicative_case ~pfailed:(l1=[]) depth signature status flags gty cache in (* statistics *) List.iter