X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=1fa530e782054d30ca02a7da400ed7ef9b0123b3;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=b841f87e76f34eba283b68b9cdd5f6479eb85ecd;hpb=98f3202363b4baf3bf8e13af10f086ca1cf848be;p=helm.git diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index b841f87e7..1fa530e78 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -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 @@ -146,9 +150,11 @@ let is_a_fact_ast status subst metasenv ctx cand = let ty = NCicTypeChecker.typeof status subst metasenv ctx t in is_a_fact status (mk_cic_term ctx ty) -let current_goal status = +let current_goal ?(single_goal=true) status = let open_goals = head_goals status#stack in - assert (List.length open_goals = 1); + if single_goal + then assert (List.length open_goals = 1) + else assert (List.length open_goals >= 1); let open_goal = List.hd open_goals in let gty = get_goalty status open_goal in let ctx = ctx_of gty in @@ -292,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 @@ -299,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 _ @@ -582,12 +589,42 @@ let smart_apply t unit_eq status g = raise (Error (lazy "eq_coerc non yet defined",Some e)) | Error _ as e -> debug_print (lazy "error"); raise e +let compare_statuses ~past ~present = + let _,_,past,_,_ = past#obj in + let _,_,present,_,_ = present#obj in + List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present), + List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past) +;; + +(* 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 *) + let sym_eq = Ast.Appl [Ast.Ident("sym_eq",`Ambiguous); Ast.Implicit `Vector] in + let _,_,metasenv,subst,_ = status#obj in + let _, context, gty = List.assoc g metasenv in + let is_eq = + NCicParamod.is_equation status metasenv subst context gty + in + if is_eq then + try tac status g + with Error _ -> + let new_status = instantiate_with_ast status g ("",0,sym_eq) in + let go, _ = compare_statuses ~past:status ~present:new_status in + assert (List.length go = 1); + let ng = List.hd go in + tac new_status ng + else tac status g +;; + let smart_apply_tac t s = let unit_eq = index_local_equations s#eq_cache s in - NTactics.distribute_tac (smart_apply t unit_eq) s + NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s + (* NTactics.distribute_tac (smart_apply t unit_eq) s *) let smart_apply_auto t eq_cache = - NTactics.distribute_tac (smart_apply t eq_cache) + NTactics.distribute_tac (try_sym (smart_apply t eq_cache)) + (* NTactics.distribute_tac (smart_apply t eq_cache) *) (****************** types **************) @@ -824,7 +861,7 @@ type cache = let add_to_trace status ~depth cache t = match t with | Ast.NRef _ -> - debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t)); + print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t)); {cache with trace = t::cache.trace} | Ast.NCic _ (* local candidate *) | _ -> (*not an application *) cache @@ -912,8 +949,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 @@ -923,25 +976,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) ^ " = " - ^ (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)) + (* 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))); + (* 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 diff))); + 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 ;; @@ -981,12 +1036,21 @@ let get_cands retrieve_for diff empty gty weak_gty = ;; let get_candidates ?(smart=true) depth flags status cache signature gty = - let maxd = ((depth + 1) = flags.maxdepth) in 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 @@ -1001,26 +1065,24 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = | _ -> 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 = @@ -1032,88 +1094,47 @@ 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 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 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 = app_counter:= !app_counter+1; @@ -1128,84 +1149,42 @@ let applicative_case depth signature status flags gty cache = | _ -> false, NCicParamod.is_equation status metasenv subst context t in debug_print ~depth (lazy (string_of_bool is_eq)); - (* old - let candidates, smart_candidates = - get_candidates ~smart:(not is_eq) depth - flags status tcache signature gty 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 candidates = - let test x = not (is_a_fact_ast status subst metasenv context x) in - if is_eq then - Ast.Ident("refl",None) ::List.filter test candidates - else candidates in *) (* new *) - let candidates, smart_candidates = + let candidates_facts, smart_candidates_facts, + candidates_other, smart_candidates_other = get_candidates ~smart:true depth - flags status tcache signature gty 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 candidates,smart_candidates = - let test x = not (is_a_fact_ast status subst metasenv context x) in - if is_eq then - Ast.Ident("refl",`Ambiguous) ::List.filter test candidates, - List.filter test smart_candidates - else candidates,smart_candidates in - debug_print ~depth - (lazy ("candidates: " ^ string_of_int (List.length candidates))); - debug_print ~depth - (lazy ("smart candidates: " ^ - string_of_int (List.length smart_candidates))); - (* - let sm = 0 in - let smart_candidates = [] in *) - let sm = if is_eq then 0 else 2 in - (* wrong: we constraint maxdepth for equality goals to three *) - (* let maxdepth = if is_eq then min flags.maxdepth 6 else flags.maxdepth in *) + 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 maxd = (depth + 1 = flags.maxdepth) in - let only_one = flags.last && maxd in - debug_print ~depth (lazy ("only_one: " ^ (string_of_bool only_one))); - debug_print ~depth (lazy ("maxd: " ^ (string_of_bool maxd))); - let elems = + let try_candidates only_one sm acc candidates = List.fold_left (fun elems cand -> if (only_one && (elems <> [])) then elems - else - if (maxd && not(is_prod) & - not(is_a_fact_ast status subst metasenv context cand)) - then (debug_print ~depth (lazy "pruned: not a fact"); elems) else match try_candidate (~smart:sm) flags depth status cache.unit_eq context cand with | None -> elems | Some x -> x::elems) - [] candidates - in - let more_elems = - if only_one && elems <> [] then elems - else - List.fold_left - (fun elems cand -> - if (only_one && (elems <> [])) then elems - else - if (maxd && not(is_prod) && - not(is_a_fact_ast status subst metasenv context cand)) - then (debug_print ~depth (lazy "pruned: not a fact"); elems) - else - match try_candidate (~smart:2) (* was smart:1 *) - flags depth status cache.unit_eq context cand with - | None -> elems - | Some x -> x::elems) - [] smart_candidates - in - elems@more_elems + acc candidates + in + (* if the goal is the last one we stop at the first fact *) + let elems = try_candidates flags.last sm [] candidates_facts in + (* now we add smart_facts *) + let elems = try_candidates flags.last sm elems smart_candidates_facts in + (* if we are at maxdepth and the goal is not a product we are done + similarly, if the goal is the last one and we already found a + solution *) + if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems + else + let elems = try_candidates false 2 elems candidates_other in + debug_print ~depth (lazy ("not facts: try smart application")); + try_candidates false 2 elems smart_candidates_other ;; exception Found -;; - +;; (* gty is supposed to be meta-closed *) let is_subsumed depth filter_depth status gty cache = @@ -1498,21 +1477,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 +1489,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 +1516,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 +1537,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 +1558,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,28 +1729,35 @@ 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 -> - debug_print (lazy( + (*debug_*)print (lazy( NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^ String.concat "\n " (List.map ( status#ppterm ~metasenv:[] ~context:[] ~subst:[]) (NDiscriminationTree.TermSet.elements t)) ))); *) - let candidates = + (* To allow using Rels in the user-specified candidates, we need a context + * but in the case where multiple goals are open, there is no single context + * to type the Rels. At this time, we require that Rels be typed in the + * context of the first selected goal *) + let _,ctx,_ = current_goal ~single_goal:false status in + let status, candidates = match univ with - | None -> None + | None -> status, None | Some l -> - let to_Ast t = - let status, res = disambiguate status [] t None in - let _,res = term_of_cic_term status res (ctx_of res) - in Ast.NCic res - in Some (List.map to_Ast l) - in + let to_Ast (st,l) t = + let st, res = disambiguate st ctx t None in + let st, res = term_of_cic_term st res (ctx_of res) + in (st, Ast.NCic res::l) + in + let status, l' = List.fold_left to_Ast (status,[]) l in + status, Some l' + in let depth = int "depth" flags 3 in let size = int "size" flags 10 in let width = int "width" flags 4 (* (3+List.length goals)*) in @@ -1815,6 +1795,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = | Proved (s,trace) -> debug_print (lazy ("proved at depth " ^ string_of_int x)); List.iter (toref incr_uses statistics) trace; + let _ = debug_print (pptrace status trace) in let trace = cleanup_trace s trace in let _ = debug_print (pptrace status trace) in let stack = @@ -1824,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