X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=25274de814f7571774f7ee3a5df6054e0ca668b5;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=efb83b81526be0c7abc4737674369f900c4329b1;hpb=3b3c0659bdae6fe088604e00d1f0c0dc1b84202d;p=helm.git diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index efb83b815..25274de81 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 @@ -141,7 +145,7 @@ let is_a_fact_obj s uri = let is_a_fact_ast status subst metasenv ctx cand = noprint ~depth:0 (lazy ("checking facts " ^ NotationPp.pp_term status cand)); - let status, t = disambiguate status ctx ("",0,cand) None in + let status, t = disambiguate status ctx ("",0,cand) `XTNone in let status,t = term_of_cic_term status t ctx in let ty = NCicTypeChecker.typeof status subst metasenv ctx t in is_a_fact status (mk_cic_term ctx ty) @@ -231,7 +235,7 @@ let solve f status eq_cache goal = let gty = NCicUntrusted.apply_subst status subst ctx gty in let build_status (pt, _, metasenv, subst) = try - noprint (lazy ("refining: "^(status#ppterm ctx subst metasenv pt))); + debug_print (lazy ("refining: "^(status#ppterm ctx subst metasenv pt))); let stamp = Unix.gettimeofday () in let metasenv, subst, pt, pty = (* NCicRefiner.typeof status @@ -243,7 +247,7 @@ let solve f status eq_cache goal = NCicUnification.unify status metasenv subst ctx gty pty *) NCicRefiner.typeof (status#set_coerc_db NCicCoercion.empty_db) - metasenv subst ctx pt (Some gty) + metasenv subst ctx pt (`XTSome gty) in noprint (lazy (Printf.sprintf "Refined in %fs" (Unix.gettimeofday() -. stamp))); @@ -254,15 +258,16 @@ let solve f status eq_cache goal = with NCicRefiner.RefineFailure msg | NCicRefiner.Uncertain msg -> - noprint (lazy ("WARNING U: refining in fast_eq_check failed\n" ^ + debug_print (lazy ("WARNING U: refining in fast_eq_check failed\n" ^ snd (Lazy.force msg) ^ "\n in the environment\n" ^ status#ppmetasenv subst metasenv)); None | NCicRefiner.AssertFailure msg -> - noprint (lazy ("WARNING F: refining in fast_eq_check failed" ^ + debug_print (lazy ("WARNING F: refining in fast_eq_check failed" ^ 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 @@ -292,6 +297,7 @@ let index_local_equations eq_cache status = 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 _,_,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 - (noprint(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 _ @@ -312,6 +318,44 @@ let index_local_equations eq_cache status = eq_cache ctx ;; +let index_local_equations2 eq_cache status open_goal lemmas nohyps = + noprint (lazy "indexing equations"); + let eq_cache,lemmas = + match lemmas with + None -> eq_cache,[] + | Some l -> NCicParamod.empty_state,l + in + 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 status,lemmas = + List.fold_left + (fun (status,lemmas) l -> + let status,l = NTacStatus.disambiguate status ctx l `XTNone in + let status,l = NTacStatus.term_of_cic_term status l ctx in + status,l::lemmas) + (status,[]) lemmas in + let local_equations = + if nohyps then [] else + List.map (fun i -> NCic.Rel (i + 1)) + (HExtlib.list_seq 1 (List.length ctx)) in + let lemmas = lemmas @ local_equations in + List.fold_left + (fun eq_cache t -> + try + 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 subst metasenv ty))); + NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty) + else + (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty))); + eq_cache) + with + | NCicTypeChecker.TypeCheckerFailure _ + | NCicTypeChecker.AssertFailure _ -> eq_cache) + eq_cache lemmas +;; + let fast_eq_check_tac ~params s = let unit_eq = index_local_equations s#eq_cache s in dist_fast_eq_check unit_eq s @@ -335,8 +379,11 @@ let demod eq_cache status goal = ;; let demod_tac ~params s = - let unit_eq = index_local_equations s#eq_cache s in - NTactics.distribute_tac (demod unit_eq) s + let unit_eq s i = + index_local_equations2 s#eq_cache s i (fst params) + (List.mem_assoc "nohyps" (snd params)) + in + NTactics.distribute_tac (fun s i -> demod (unit_eq s i) s i) s ;; (* @@ -431,7 +478,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 ;; @@ -541,7 +590,7 @@ let smart_apply t unit_eq status g = let n,h,metasenv,subst,o = status#obj in let gname, ctx, gty = List.assoc g metasenv in (* let ggty = mk_cic_term context gty in *) - let status, t = disambiguate status ctx t None in + let status, t = disambiguate status ctx t `XTNone in let status,t = term_of_cic_term status t ctx in let _,_,metasenv,subst,_ = status#obj in let ty = NCicTypeChecker.typeof status subst metasenv ctx t in @@ -925,7 +974,7 @@ let openg_no status = List.length (head_goals status#stack) let sort_candidates status ctx candidates = let _,_,metasenv,subst,_ = status#obj in let branch cand = - let status,ct = disambiguate status ctx ("",0,cand) None in + let status,ct = disambiguate status ctx ("",0,cand) `XTNone in let status,t = term_of_cic_term status ct ctx in let ty = NCicTypeChecker.typeof status subst metasenv ctx t in let res = branch status (mk_cic_term ctx ty) in @@ -973,6 +1022,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, @@ -987,13 +1039,13 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = let diff = og_no - old_og_no in debug_print (lazy ("expected branching: " ^ (string_of_int res))); debug_print (lazy ("actual: branching" ^ (string_of_int diff))); - (* one goal is closed by the application *) - if og_no - old_og_no >= res then + (* some flexibility *) + if og_no - old_og_no > res then (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " ^ (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 +1063,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,13 +1084,22 @@ 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 maxd = ((depth + 1) = flags.maxdepth) in +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 let _, raw_gty = term_of_cic_term status gty context in + let is_prod, is_eq = + let status, t = term_of_cic_term status gty context in + let t = NCicReduction.whd status subst context t in + match t with + | NCic.Prod _ -> true, false + | _ -> false, NCicParamod.is_equation status metasenv subst context t + in debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty)); + let is_eq = + NCicParamod.is_equation status metasenv subst context raw_gty + in let raw_weak_gty, weak_gty = if smart then match raw_gty with @@ -1048,31 +1109,29 @@ 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 in + (* we now compute global candidates *) let global_cands, smart_global_cands = - match flags.candidates with - | Some l when (not maxd) -> l,[] - | Some _ - | None -> - let mapf s = - let to_ast = function - | 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 - universe) - NDiscriminationTree.TermSet.diff - NDiscriminationTree.TermSet.empty - raw_gty raw_weak_gty in - mapf g, mapf l in + let mapf s = + let to_ast = function + | 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 universe) + NDiscriminationTree.TermSet.diff + NDiscriminationTree.TermSet.empty + raw_gty raw_weak_gty in + mapf g, mapf l in + (* we now compute local candidates *) let local_cands,smart_local_cands = let mapf s = let to_ast t = @@ -1084,92 +1143,50 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = (fun ty -> search_in_th ty cache) Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in mapf g, mapf l in - sort_candidates status context (global_cands@local_cands), - sort_candidates status context (smart_global_cands@smart_local_cands) -;; - -(* old version -let get_candidates ?(smart=true) status cache signature gty = - let universe = status#auto_cache in - let _,_,metasenv,subst,_ = status#obj in - let context = ctx_of gty in - let t_ast t = - let _status, t = term_of_cic_term status t context - in Ast.NCic t in - 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 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 = - List.map c_ast - (List.filter (only signature context) - (NDiscriminationTree.TermSet.elements global)) @ - List.map t_ast (Ncic_termSet.elements local) in - let candidates = together cands local_cands in - let candidates = sort_candidates status context candidates in - let smart_candidates = - if smart then - match raw_gty with - | NCic.Appl _ - | NCic.Const _ - | NCic.Rel _ -> - let weak_gty = perforate_small status subst metasenv context raw_gty in - (* - NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0))) - (List.length tl)) in *) - let more_cands = - NDiscriminationTree.DiscriminationTree.retrieve_unifiables - universe weak_gty - in - let smart_cands = - NDiscriminationTree.TermSet.diff more_cands cands in - let cic_weak_gty = mk_cic_term context weak_gty in - let more_local_cands = search_in_th cic_weak_gty cache in - let smart_local_cands = - Ncic_termSet.diff more_local_cands local_cands in - together smart_cands smart_local_cands - (* together more_cands more_local_cands *) - | _ -> [] - else [] + (* we now splits candidates in facts or not facts *) + let test = is_a_fact_ast status subst metasenv context in + let by,given_candidates = + match flags.candidates with + | Some l -> true, l + | None -> false, [] in +(* we compute candidates to be applied in normal mode, splitted in + facts and not facts *) + 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 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 && (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 + else if by then given_candidates@ll2 + else gl2@ll2 + in l1,l2 in - let smart_candidates = sort_candidates status context smart_candidates in - (* if smart then smart_candidates, [] - else candidates, [] *) - candidates, smart_candidates -;; - -let get_candidates ?(smart=true) flags status cache signature gty = - match flags.candidates with - | None -> get_candidates ~smart status cache signature gty - | Some l -> l,[] -;; *) - - + (* we now compute candidates to be applied in smart mode, splitted in + facts and not facts *) + let smart_candidates_facts, smart_candidates_other = + if is_prod || not(smart) then [],[] + else + let sgl1,sgl2 = List.partition test smart_global_cands in + let sll1,sll2 = List.partition test smart_local_cands in + let l1 = if is_eq then [] else sgl1@sll1 in + let l2 = + if by && smart then given_candidates@sll2 + else if by then sll2 + else sgl2@sll2 + in l1,l2 + in + candidates_facts, + smart_candidates_facts, + sort_candidates status context (candidates_other), + 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 @@ -1183,25 +1200,13 @@ let applicative_case depth signature status flags gty cache = in debug_print ~depth (lazy (string_of_bool is_eq)); (* new *) - let candidates, smart_candidates = - get_candidates ~smart:true depth - flags status tcache signature gty in - let test = is_a_fact_ast status subst metasenv context in - let candidates_facts,candidates_other = - (* 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 l1,l2 = List.partition test candidates in - if is_eq then [Ast.Ident("refl",None)],l2 else l1,l2 - in - let smart_candidates_facts, smart_candidates_other = - if is_prod then [],[] - else - let l1,l2 = List.partition test smart_candidates in - if is_eq then [],l2 else l1,l2 + let candidates_facts, smart_candidates_facts, + candidates_other, smart_candidates_other = + get_candidates ~smart:true ~pfailed depth + flags status tcache signature gty in let sm = if is_eq || is_prod then 0 else 2 in - let sm1 = if flags.last then 2 else 0 in + let sm1 = if flags.last then 2 else 0 in let maxd = (depth + 1 = flags.maxdepth) in let try_candidates only_one sm acc candidates = List.fold_left @@ -1231,7 +1236,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 ( @@ -1402,7 +1406,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)); @@ -1425,7 +1429,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 @@ -1550,6 +1554,12 @@ match status#stack with List.for_all (fun i -> IntSet.mem i others) (HExtlib.filter_map is_open g) +let top_cache ~depth top status cache = + if top then + let unit_eq = index_local_equations status#eq_cache status in + {cache with unit_eq = unit_eq} + else cache + let rec auto_clusters ?(top=false) flags signature cache depth status : unit = debug_print ~depth (lazy ("entering auto clusters at depth " ^ @@ -1571,6 +1581,7 @@ let rec auto_clusters ?(top=false) in auto_clusters flags signature cache (depth-1) status else if List.length goals < 2 then + let cache = top_cache ~depth top status cache in auto_main flags signature cache depth status else let all_goals = open_goals (depth+1) status in @@ -1591,6 +1602,7 @@ let rec auto_clusters ?(top=false) let flags = {flags with last = (List.length all_goals = 1)} in (* no need to cluster *) + let cache = top_cache ~depth top status cache in auto_main flags signature cache depth status else let classes = if top then List.rev classes else classes in @@ -1611,6 +1623,7 @@ let rec auto_clusters ?(top=false) debug_print ~depth (lazy ("stack length = " ^ (string_of_int lold))); let fstatus = deep_focus_tac (depth+1) gl status in + let cache = top_cache ~depth top fstatus cache in try debug_print ~depth (lazy ("focusing on" ^ String.concat "," (List.map string_of_int gl))); @@ -1781,8 +1794,8 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = let status = (status:> NTacStatus.tac_status) in let goals = head_goals status#stack in let status, facts = mk_th_cache status goals in - let unit_eq = index_local_equations status#eq_cache status in - let cache = init_cache ~facts ~unit_eq () in +(* let unit_eq = index_local_equations status#eq_cache status in *) + let cache = init_cache ~facts () in (* pp_th status facts; *) (* NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> @@ -1798,7 +1811,8 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = | None -> None | Some l -> let to_Ast t = - let status, res = disambiguate status [] t None in +(* FG: `XTSort here? *) + let status, res = disambiguate status [] t `XTNone in let _,res = term_of_cic_term status res (ctx_of res) in Ast.NCic res in Some (List.map to_Ast l)