X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=d371409d2ecac8587947476abcba11087074d43d;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=21f1e42e81e6e056c67e824780db4d03bfd7afa9;hpb=3fab56d1663ba3d5aeb9207612279e0bb0edbb8c;p=helm.git diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 21f1e42e8..d371409d2 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -13,7 +13,7 @@ open Printf let print ?(depth=0) s = prerr_endline (String.make (2*depth) ' '^Lazy.force s) -let noprint ?(depth=0) _ = () +let noprint ?depth:(_=0) _ = () let debug_print = noprint open Continuationals.Stack @@ -66,7 +66,7 @@ let is_relevant tbl item = else true with Not_found -> true -let print_stat status tbl = +let print_stat _status tbl = let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in let relevance v = float !(v.uses) /. float !(v.nominations) in let vcompare (_,v1) (_,v2) = @@ -322,10 +322,7 @@ let index_local_equations eq_cache ?(flag=false) status = end ;; -let index_local_equations2 eq_cache status open_goal lemmas ?(flag=false) nohyps = - if flag then - NCicParamod.empty_state - else begin +let index_local_equations2 eq_cache status open_goal lemmas ?flag:(_=false) nohyps = noprint (lazy "indexing equations"); let eq_cache,lemmas = match lemmas with @@ -361,10 +358,9 @@ let index_local_equations2 eq_cache status open_goal lemmas ?(flag=false) nohyps | NCicTypeChecker.TypeCheckerFailure _ | NCicTypeChecker.AssertFailure _ -> eq_cache) eq_cache lemmas - end ;; -let fast_eq_check_tac ~params s = +let fast_eq_check_tac ~params:_ s = let unit_eq = index_local_equations s#eq_cache s in dist_fast_eq_check unit_eq s ;; @@ -375,7 +371,7 @@ let paramod eq_cache status goal = | s::_ -> s ;; -let paramod_tac ~params s = +let paramod_tac ~params:_ s = let unit_eq = index_local_equations s#eq_cache s in NTactics.distribute_tac (paramod unit_eq) s ;; @@ -424,7 +420,7 @@ let close_wrt_context status = (fun ty ctx_entry -> match ctx_entry with | name, NCic.Decl t -> NCic.Prod(name,t,ty) - | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty) + | _name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty) ;; let args_for_context ?(k=1) ctx = @@ -432,8 +428,8 @@ let args_for_context ?(k=1) ctx = List.fold_left (fun (n,l) ctx_entry -> match ctx_entry with - | name, NCic.Decl t -> n+1,NCic.Rel(n)::l - | name, NCic.Def(bo, _) -> n+1,l) + | _name, NCic.Decl _t -> n+1,NCic.Rel(n)::l + | _name, NCic.Def(_bo, _) -> n+1,l) (k,[]) ctx in args @@ -452,7 +448,7 @@ let refresh metasenv = List.fold_left (fun (metasenv,subst) (i,(iattr,ctx,ty)) -> let ikind = NCicUntrusted.kind_of_meta iattr in - let metasenv,j,instance,ty = + let metasenv,_j,instance,ty = NCicMetaSubst.mk_meta ~attrs:iattr metasenv ctx ~with_type:ty ikind in let s_entry = i,(iattr, ctx, instance, ty) in @@ -468,12 +464,12 @@ let close_metasenv status metasenv subst = *) let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in List.fold_left - (fun (subst,objs) (i,(iattr,ctx,ty)) -> + (fun (subst,objs) (i,(_iattr,ctx,ty)) -> let ty = NCicUntrusted.apply_subst status subst ctx ty in let ctx = NCicUntrusted.apply_subst_context status ~fix_projections:true subst ctx in - let (uri,_,_,_,obj) as okind = + let (uri,_,_,_,_obj) as okind = constant_for_meta status ctx ty i in try NCicEnvironment.check_and_add_obj status okind; @@ -525,7 +521,7 @@ let replace_meta status i args target = | _ -> let args = List.map (NCicSubstitution.subst_meta status lc) args in NCic.Appl(NCic.Rel k::args)) - | NCic.Meta (j,lc) as m -> + | NCic.Meta (_j,lc) as m -> (match lc with _,NCic.Irl _ -> m | n,NCic.Ctx l -> @@ -540,7 +536,7 @@ let replace_meta status i args target = let close_wrt_metasenv status subst = List.fold_left - (fun ty (i,(iattr,ctx,mty)) -> + (fun ty (i,(_iattr,ctx,mty)) -> let mty = NCicUntrusted.apply_subst status subst ctx mty in let ctx = NCicUntrusted.apply_subst_context status ~fix_projections:true @@ -595,8 +591,8 @@ let saturate_to_ref status metasenv subst ctx nref ty = aux metasenv ty [] let smart_apply t unit_eq status g = - let n,h,metasenv,subst,o = status#obj in - let gname, ctx, gty = List.assoc g metasenv in + let n,h,metasenv,_subst,o = status#obj in + let _gname, ctx, gty = List.assoc g metasenv in (* let ggty = mk_cic_term context gty in *) let status, t = disambiguate status ctx t `XTNone in let status,t = term_of_cic_term status t ctx in @@ -637,7 +633,7 @@ let smart_apply t unit_eq status g = debug_print(lazy("ritorno da fast_eq_check")); res with - | NCicEnvironment.ObjectNotFound s as e -> + | NCicEnvironment.ObjectNotFound _s as e -> raise (Error (lazy "eq_coerc non yet defined",Some e)) | Error _ as e -> debug_print (lazy "error"); raise e (* FG: for now we catch TypeCheckerFailure; to be understood *) @@ -961,7 +957,7 @@ let init_cache ?(facts=[]) ?(under_inspection=[],[]) unit_eq = unit_eq; trace = trace} -let only signature _context candidate = true +let only _signature _context _candidate = true (* (* TASSI: nel trie ci mettiamo solo il body, non il ty *) let candidate_ty = @@ -1009,7 +1005,7 @@ let rec stack_goals level gs = if level = 0 then [] else match gs with | [] -> assert false - | (g,_,_,_)::s -> + | (g,_,_,_,_)::s -> let is_open = function | (_,Continuationals.Stack.Open i) -> Some i | (_,Continuationals.Stack.Closed _) -> None @@ -1020,9 +1016,9 @@ let rec stack_goals level gs = let open_goals level status = stack_goals level status#stack ;; -let try_candidate ?(smart=0) flags depth status eq_cache ctx t = +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 + (*let old_og_no = List.length (open_goals (depth+1) status) in*) debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : " ^ (NotationPp.pp_term status) t)); let status = @@ -1058,7 +1054,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = 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 + with Error _ -> debug_print ~depth (lazy "failed"); None ;; let sort_of status subst metasenv ctx t = @@ -1096,12 +1092,20 @@ let get_cands retrieve_for diff empty gty weak_gty = cands, diff more_cands cands ;; -let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty = +let is_a_needed_uri s = + s = "cic:/matita/basics/logic/eq.ind" || + s = "cic:/matita/basics/logic/sym_eq.con" || + s = "cic:/matita/basics/logic/trans_eq.con" || + s = "cic:/matita/basics/logic/eq_f3.con" || + s = "cic:/matita/basics/logic/eq_f2.con" || + s = "cic:/matita/basics/logic/eq_f.con" + +let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gty = 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 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 @@ -1128,26 +1132,31 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty in (* we now compute global candidates *) let global_cands, smart_global_cands = - if flags.local_candidates then - 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 - else [],[] 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 + let global_cands,smart_global_cands = + if flags.local_candidates then global_cands,smart_global_cands + else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri + (NUri.string_of_uri + uri) | _ -> false) + in filter global_cands,filter smart_global_cands + in (* we now compute local candidates *) let local_cands,smart_local_cands = - if flags.local_candidates then let mapf s = let to_ast t = let _status, t = term_of_cic_term status t context @@ -1158,7 +1167,14 @@ let get_candidates ?(smart=true) ~pfailed 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 - else [],[] in + in + let local_cands,smart_local_cands = + if flags.local_candidates then local_cands,smart_local_cands + else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri + (NUri.string_of_uri + uri) | _ -> false) + in filter local_cands,filter smart_local_cands + in (* we now splits candidates in facts or not facts *) let test = is_a_fact_ast status subst metasenv context in let by,given_candidates = @@ -1222,7 +1238,7 @@ let applicative_case ~pfailed depth signature status flags gty cache = 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 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 @@ -1307,7 +1323,7 @@ let is_subsumed depth filter_depth status gty cache = NCicMetaSubst.mk_meta metasenv ctx ~with_type:implication `IsType in let status = status#set_obj (n,h,metasenv,subst,obj) in - let status = status#set_stack [([1,Open j],[],[],`NoTag)] in + let status = status#set_stack [([1,Open j],[],[],`NoTag,[])] in try let status = NTactics.intro_tac "foo" status in let status = @@ -1348,7 +1364,7 @@ let is_prod status = let intro ~depth status facts name = let status = NTactics.intro_tac name status in - let _, ctx, ngty = current_goal status in + let _, ctx, _ngty = current_goal status in let t = mk_cic_term ctx (NCic.Rel 1) in let status, keys = keys_of_term status t in let facts = List.fold_left (add_to_th t) facts keys in @@ -1485,7 +1501,7 @@ let sort_tac status = let gstatus = match status#stack with | [] -> assert false - | (goals, t, k, tag) :: s -> + | (goals, t, k, tag, p) :: s -> let g = head_goals status#stack in let sortedg = (List.rev (MS.topological_sort g (deps status))) in @@ -1500,7 +1516,7 @@ let sort_tac status = let sorted_goals = List.map (fun i -> List.find (is_it i) goals) sortedg in - (sorted_goals, t, k, tag) :: s + (sorted_goals, t, k, tag, p) :: s in status#set_stack gstatus ;; @@ -1509,13 +1525,13 @@ let clean_up_tac status = let gstatus = match status#stack with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> let is_open = function | (_,Continuationals.Stack.Open _) -> true | (_,Continuationals.Stack.Closed _) -> false in let g' = List.filter is_open g in - (g', t, k, tag) :: s + (g', t, k, tag, p) :: s in status#set_stack gstatus ;; @@ -1546,11 +1562,11 @@ let deep_focus_tac level focus status = if level = 0 then [],[],gs else match gs with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag,p) :: s -> let f,o,gs = slice (level-1) s in let f1,o1 = List.partition in_focus g in - (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs + (f1,[],[],`BranchTag, [])::f, (o1, t, k, tag, p)::o, gs in let gstatus = let f,o,s = slice level status#stack in f@o@s @@ -1561,7 +1577,7 @@ let deep_focus_tac level focus status = let move_to_side level status = match status#stack with | [] -> assert false - | (g,_,_,_)::tl -> + | (g,_,_,_,_)::tl -> let is_open = function | (_,Continuationals.Stack.Open i) -> Some i | (_,Continuationals.Stack.Closed _) -> None @@ -1570,7 +1586,7 @@ 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 ?(use_given_only=false) cache = +let top_cache ~depth:_ top status ?(use_given_only=false) cache = if top then let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in {cache with unit_eq = unit_eq} @@ -1664,7 +1680,7 @@ let rec auto_clusters ?(top=false) flags signature cache depth ?(use_given_only= and (* BRAND NEW VERSION *) -auto_main flags signature cache depth status ?(use_given_only=false): unit= +auto_main flags signature cache depth ?(use_given_only=false) status: unit= debug_print ~depth (lazy "entering auto main"); debug_print ~depth (pptrace status cache.trace); debug_print ~depth (lazy ("stack length = " ^ @@ -1675,28 +1691,28 @@ auto_main flags signature cache depth status ?(use_given_only=false): unit= match goals with | [] when depth = 0 -> raise (Proved (status,cache.trace)) | [] -> - let status = NTactics.merge_tac status in - let cache = - let l,tree = cache.under_inspection in - match l with - | [] -> cache (* possible because of intros that cleans the cache *) - | a::tl -> let tree = rm_from_th a tree a in - {cache with under_inspection = tl,tree} - in - auto_clusters flags signature cache (depth-1) status ~use_given_only - | orig::_ -> - if depth > 0 && move_to_side depth status - then - let status = NTactics.merge_tac status in - let cache = - let l,tree = cache.under_inspection in - match l with - | [] -> cache (* possible because of intros that cleans the cache*) - | a::tl -> let tree = rm_from_th a tree a in - {cache with under_inspection = tl,tree} - in - auto_clusters flags signature cache (depth-1) status ~use_given_only - else + let status = NTactics.merge_tac status in + let cache = + let l,tree = cache.under_inspection in + match l with + | [] -> cache (* possible because of intros that cleans the cache *) + | a::tl -> let tree = rm_from_th a tree a in + {cache with under_inspection = tl,tree} + in + auto_clusters flags signature cache (depth-1) status ~use_given_only + | _orig::_ -> + if depth > 0 && move_to_side depth status + then + let status = NTactics.merge_tac status in + let cache = + let l,tree = cache.under_inspection in + match l with + | [] -> cache (* possible because of intros that cleans the cache*) + | a::tl -> let tree = rm_from_th a tree a in + {cache with under_inspection = tl,tree} + in + auto_clusters flags signature cache (depth-1) status ~use_given_only + else let ng = List.length goals in (* moved inside auto_clusters *) if ng > flags.maxwidth then begin @@ -1884,7 +1900,7 @@ let auto_tac' candidates ~local_candidates ?(use_given_only=false) flags ?(trace let _ = debug_print (pptrace status trace) in let stack = match s#stack with - | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest + | (g,t,k,f,p) :: rest -> (filter_open g,t,k,f,p):: rest | _ -> assert false in let s = s#set_stack stack in @@ -1909,7 +1925,14 @@ let candidates_from_ctx univ ctx status = let status, res = disambiguate status ctx t `XTNone in let _,res = term_of_cic_term status res (ctx_of res) in Ast.NCic res - in Some (List.map to_Ast l) + in Some (List.map to_Ast l) +(* FG: adding these lemmas to (List.map to_Ast l) slows auto very much in some cases + @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None); + Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None); + Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None); + Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None) + ] +*) let auto_lowtac ~params:(univ,flags) status goal = let gty = get_goalty status goal in