From bb8f6e4e6d605e2ee354e19a86bf634e9a6b81a7 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 15 Nov 2011 08:25:59 +0000 Subject: [PATCH] non-facts local candidates must be applied too in presence of a trace --- matitaB/components/ng_tactics/nnAuto.ml | 32 +++++++++++++------------ 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index 38e19486b..697355db2 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -14,7 +14,7 @@ open Printf let print ?(depth=0) s = prerr_endline (String.make (2*depth) ' '^Lazy.force s) let noprint ?(depth=0) _ = () -let debug_print = print +let debug_print = noprint open Continuationals.Stack open NTacStatus @@ -985,8 +985,8 @@ 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) @@ -1098,18 +1098,17 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = (* we compute candidates to be applied in normal mode, splitted in facts and not facts *) let candidates_facts,candidates_other = - (* warning : the order between global_cands and local_cand is - relevant. In this way we process first local cands *) - let l1,l2 = List.partition test (global_cands@local_cands) in + 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 exception since it prompts for convertibility *) - let l1 = if is_eq then [Ast.Ident("refl",`Ambiguous)] else l1 in + let l1 = if is_eq then [Ast.Ident("refl",`Ambiguous)] else gl1@ll1 in let l2 = (* if smart given candidates are applied in smart mode *) - if by && smart then [] - else if by then given_candidates - else l2 + if by && smart then ll2 + else if by then given_candidates@ll2 + else gl2@ll2 in l1,l2 in (* we now compute candidates to be applied in smart mode, splitted in @@ -1117,11 +1116,14 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = let smart_candidates_facts, smart_candidates_other = if is_prod || not(smart) then [],[] else - let l1,l2 = List.partition test (smart_local_cands@smart_global_cands) in - let l1 = if is_eq then [] else l1 in - let l2 = if by then given_candidates else l2 - in - l1,l2 + 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, -- 2.39.2