X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=fc8c83938689a9be03f9452275eae10a18d49474;hb=d6f1365a9f1cb48af8a7b32cf074373466779e7e;hp=af30fcf9373166de3a267ad7b22ecb788ab526a6;hpb=0c7ccf8fc6a32cb187b5464ff36e1ff0502ae054;p=helm.git diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index af30fcf93..fc8c83938 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -942,8 +942,24 @@ let sort_candidates status ctx candidates = let sort_new_elems l = List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l +let rec stack_goals level gs = + if level = 0 then [] + else match gs with + | [] -> assert false + | (g,_,_,_)::s -> + let is_open = function + | (_,Continuationals.Stack.Open i) -> Some i + | (_,Continuationals.Stack.Closed _) -> None + in + HExtlib.filter_map is_open g @ stack_goals (level-1) s +;; + +let open_goals level status = stack_goals level status#stack +;; + let try_candidate ?(smart=0) flags depth status eq_cache ctx t = try + let old_og_no = List.length (open_goals (depth+1) status) in debug_print ~depth (lazy ("try " ^ (NotationPp.pp_term status) t)); let status = if smart= 0 then NTactics.apply_tac ("",0,t) status @@ -953,25 +969,27 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = with Error _ -> smart_apply_auto ("",0,t) eq_cache status in -(* - let og_no = openg_no status in - if (* og_no > flags.maxwidth || *) - ((depth + 1) = flags.maxdepth && og_no <> 0) then - (debug_print ~depth (lazy "pruned immediately"); None) - else *) - (* useless - let status, cict = disambiguate status ctx ("",0,t) None in - let status,ct = term_of_cic_term status cict ctx in - let _,_,metasenv,subst,_ = status#obj in - let ty = NCicTypeChecker.typeof subst metasenv ctx ct in - let res = branch status (mk_cic_term ctx ty) in - if smart=1 && og_no > res then - (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " + (* 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, + such as the application of eq_f that always succeeds. + There is some gain but less than expected *) + let og_no = List.length (open_goals (depth+1) status) in + let status, cict = disambiguate status ctx ("",0,t) None in + let status,ct = term_of_cic_term status cict ctx in + let _,_,metasenv,subst,_ = status#obj in + let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in + let res = branch status (mk_cic_term ctx ty) in + 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 + (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)) + debug_print ~depth (lazy "strange application"); None) + else + (incr candidate_no; Some ((!candidate_no,t),status)) with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None ;; @@ -1498,21 +1516,6 @@ let deep_focus_tac level focus status = status#set_stack gstatus ;; -let rec stack_goals level gs = - if level = 0 then [] - else match gs with - | [] -> assert false - | (g,_,_,_)::s -> - let is_open = function - | (_,Continuationals.Stack.Open i) -> Some i - | (_,Continuationals.Stack.Closed _) -> None - in - HExtlib.filter_map is_open g @ stack_goals (level-1) s -;; - -let open_goals level status = stack_goals level status#stack -;; - let move_to_side level status = match status#stack with | [] -> assert false @@ -1525,6 +1528,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 " ^ @@ -1546,6 +1555,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 @@ -1566,6 +1576,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 @@ -1586,6 +1597,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))); @@ -1756,8 +1768,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 ->