X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=1fa530e782054d30ca02a7da400ed7ef9b0123b3;hb=513c4a61f11ce03888a8a0f9d8e513de6e3a7c8b;hp=38e19486b36ead0682dff766b3563c8d2405547d;hpb=0aa993bb1d23567612aa5d63fab74ef6fb918c0d;p=helm.git diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index 38e19486b..1fa530e78 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 @@ -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 @@ -294,6 +298,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 @@ -301,12 +306,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 status [] [] ctx eq_cache t ty) + (noprint(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 _ @@ -591,7 +596,7 @@ let compare_statuses ~past ~present = List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past) ;; -(* paramodulation has only an implicit knoweledge of the symmetry of equality; +(* paramodulation has only an implicit knowledge of the symmetry of equality; hence it is in trouble in proving (a = b) = (b = a) *) let try_sym tac status g = (* put the right uri *) @@ -985,10 +990,10 @@ 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 diff > res && res > 0 (* facts are never pruned *) then (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " - ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no))); + ^ (string_of_int res) ^ " vs. " ^ (string_of_int diff))); debug_print ~depth (lazy "strange application"); None) else (incr candidate_no; Some ((!candidate_no,t),status)) @@ -1098,18 +1103,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 +1121,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, @@ -1727,7 +1734,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = (* pp_th status facts; *) (* NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> - debug_print (lazy( + (*debug_*)print (lazy( NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^ String.concat "\n " (List.map ( status#ppterm ~metasenv:[] ~context:[] ~subst:[]) @@ -1798,10 +1805,10 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = in let s = s#set_stack stack in trace_ref := trace; - oldstatus#set_status s + oldstatus#set_status s in let s = up_to depth depth in - debug_print (print_stat status statistics); + debug_print (print_stat status statistics); debug_print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); debug_print(lazy