X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=38e19486b36ead0682dff766b3563c8d2405547d;hb=d6578d33463c053073c6dab75728ca318717e1de;hp=201f522d05420ba5ad8e01152ce65abb940d24e8;hpb=365bd84918e8e2fe0c6f3714b94e81b443a8f244;p=helm.git diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index 201f522d0..38e19486b 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 = noprint +let debug_print = print open Continuationals.Stack open NTacStatus @@ -146,9 +146,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 @@ -854,7 +856,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 @@ -1174,130 +1176,9 @@ let applicative_case depth signature status flags gty cache = try_candidates false 2 elems smart_candidates_other ;; - -(* -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 - debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty)); - let raw_weak_gty, weak_gty = - if smart then - match raw_gty with - | NCic.Appl _ - | NCic.Const _ - | NCic.Rel _ -> - 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)); - Some raw_weak, Some (weak) - | _ -> None,None - else None,None - in - 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 local_cands,smart_local_cands = - let mapf s = - let to_ast t = - let _status, t = term_of_cic_term status t context - in Ast.NCic t in - List.map to_ast (Ncic_termSet.elements s) in - let g,l = - get_cands - (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) -;; - -let applicative_case depth signature status flags gty cache = - app_counter:= !app_counter+1; - let _,_,metasenv,subst,_ = status#obj in - let context = ctx_of gty in - let tcache = cache.facts 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 (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 - (* put the right uri *) - if is_eq then [Ast.Ident("refl",`Ambiguous)],l2 else l1,l2 - in - let smart_candidates_facts, smart_candidates_other = - match flags.candidates with - | Some l -> [],l - | None -> - let l1,l2 = List.partition test smart_candidates in - if is_eq then [],l2 else l1,l2 - in - let sm = if is_eq then 0 else 2 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 - (fun elems cand -> - if (only_one && (elems <> [])) then elems - else - match try_candidate (~smart:sm) - flags depth status cache.unit_eq context cand with - | None -> elems - | Some x -> x::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 = if cache=[] then false else ( @@ -1853,15 +1734,22 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = (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) + 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 @@ -1900,6 +1788,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 =