X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=d371409d2ecac8587947476abcba11087074d43d;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=23ad46494dbc1f92b6b03a781174f00af168eb34;hpb=cef076c6fbd4ceec7c460414cf4421611457188d;p=helm.git diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 23ad46494..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 @@ -26,9 +26,9 @@ let app_counter = ref 0 module RHT = struct type t = NReference.reference - let equal = (==) - let compare = Pervasives.compare - let hash = Hashtbl.hash + let equal = NReference.eq + let compare = NReference.compare + let hash = NReference.hash end;; module RefHash = Hashtbl.Make(RHT);; @@ -54,7 +54,7 @@ let incr_uses tbl item = let toref f tbl t = match t with | Ast.NRef n -> - f tbl n + f tbl n | Ast.NCic _ (* local candidate *) | _ -> () @@ -66,19 +66,23 @@ 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) = 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 lazy ("\n\nSTATISTICS:\n" ^ - String.concat "\n" (List.map vstring l)) + String.concat "\n" (List.map vstring l)) (* ======================= utility functions ========================= *) module IntSet = Set.Make(struct type t = int let compare = compare end) @@ -139,9 +143,9 @@ let is_a_fact_obj s uri = | _ -> false let is_a_fact_ast status subst metasenv ctx cand = - debug_print ~depth:0 - (lazy ("------- checking " ^ NotationPp.pp_term status cand)); - let status, t = disambiguate status ctx ("",0,cand) None in + noprint ~depth:0 + (lazy ("checking facts " ^ NotationPp.pp_term status cand)); + let status, t = disambiguate status ctx ("",0,cand) `XTNone in let status,t = term_of_cic_term status t ctx in let ty = NCicTypeChecker.typeof status subst metasenv ctx t in is_a_fact status (mk_cic_term ctx ty) @@ -231,10 +235,10 @@ let solve f status eq_cache goal = let gty = NCicUntrusted.apply_subst status subst ctx gty in let build_status (pt, _, metasenv, subst) = try - noprint (lazy ("refining: "^(status#ppterm ctx subst metasenv pt))); + debug_print (lazy ("refining: "^(status#ppterm ctx subst metasenv pt))); let stamp = Unix.gettimeofday () in let metasenv, subst, pt, pty = - (* NCicRefiner.typeof status + (* NCicRefiner.typeof status (* (status#set_coerc_db NCicCoercion.empty_db) *) metasenv subst ctx pt None in debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt))); @@ -243,7 +247,7 @@ let solve f status eq_cache goal = NCicUnification.unify status metasenv subst ctx gty pty *) NCicRefiner.typeof (status#set_coerc_db NCicCoercion.empty_db) - metasenv subst ctx pt (Some gty) + metasenv subst ctx pt (`XTSome gty) in noprint (lazy (Printf.sprintf "Refined in %fs" (Unix.gettimeofday() -. stamp))); @@ -254,15 +258,16 @@ let solve f status eq_cache goal = with NCicRefiner.RefineFailure msg | NCicRefiner.Uncertain msg -> - debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^ - snd (Lazy.force msg) ^ - "\n in the environment\n" ^ - status#ppmetasenv subst metasenv)); None + debug_print (lazy ("WARNING U: refining in fast_eq_check failed\n" ^ + snd (Lazy.force msg) ^ + "\n in the environment\n" ^ + status#ppmetasenv subst metasenv)); None | NCicRefiner.AssertFailure msg -> - debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^ + debug_print (lazy ("WARNING F: refining in fast_eq_check failed" ^ Lazy.force msg ^ - "\n in the environment\n" ^ - status#ppmetasenv subst metasenv)); None + "\n in the environment\n" ^ + status#ppmetasenv subst metasenv)); None + | Sys.Break as e -> raise e | _ -> None in HExtlib.filter_map build_status @@ -287,11 +292,15 @@ let auto_eq_check eq_cache status = | Error _ -> debug_print (lazy ("no paramod proof found"));[] ;; -let index_local_equations eq_cache status = +let index_local_equations eq_cache ?(flag=false) status = + if flag then + NCicParamod.empty_state + else begin noprint (lazy "indexing equations"); 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,20 +308,59 @@ 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 eq_cache t ty) + (debug_print(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 _ | NCicTypeChecker.AssertFailure _ -> eq_cache) eq_cache ctx + end +;; + +let index_local_equations2 eq_cache status open_goal lemmas ?flag:(_=false) nohyps = + noprint (lazy "indexing equations"); + let eq_cache,lemmas = + match lemmas with + None -> eq_cache,[] + | Some l -> NCicParamod.empty_state,l + 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 status,lemmas = + List.fold_left + (fun (status,lemmas) l -> + let status,l = NTacStatus.disambiguate status ctx l `XTNone in + let status,l = NTacStatus.term_of_cic_term status l ctx in + status,l::lemmas) + (status,[]) lemmas in + let local_equations = + if nohyps then [] else + List.map (fun i -> NCic.Rel (i + 1)) + (HExtlib.list_seq 1 (List.length ctx)) in + let lemmas = lemmas @ local_equations in + List.fold_left + (fun eq_cache t -> + try + let ty = NCicTypeChecker.typeof status subst metasenv ctx t in + if is_a_fact status (mk_cic_term ctx ty) then + (debug_print(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 subst metasenv ty))); + eq_cache) + with + | NCicTypeChecker.TypeCheckerFailure _ + | NCicTypeChecker.AssertFailure _ -> eq_cache) + eq_cache lemmas ;; -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 ;; @@ -323,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 ;; @@ -335,8 +383,11 @@ let demod eq_cache status goal = ;; let demod_tac ~params s = - let unit_eq = index_local_equations s#eq_cache s in - NTactics.distribute_tac (demod unit_eq) s + let unit_eq s i = + index_local_equations2 s#eq_cache s i (fst params) + (List.mem_assoc "nohyps" (snd params)) + in + NTactics.distribute_tac (fun s i -> demod (unit_eq s i) s i) s ;; (* @@ -369,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 = @@ -377,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 @@ -397,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 @@ -413,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; @@ -431,7 +482,9 @@ let close_metasenv status metasenv subst = (* prerr_endline (status#ppterm ctx [] [] iterm); *) let s_entry = i, ([], ctx, iterm, ty) in s_entry::subst,okind::objs - with _ -> assert false) + with + Sys.Break as e -> raise e + | _ -> assert false) (subst,[]) metasenv ;; @@ -468,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 -> @@ -483,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 @@ -526,22 +579,22 @@ let saturate_to_ref status metasenv subst ctx nref ty = NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in match ty with | NCic.Const(NReference.Ref (_,NReference.Def _) as nre) - when nre<>nref -> - let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in - aux metasenv bo (args@moreargs) + when nre<>nref -> + let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in + aux metasenv bo (args@moreargs) | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl) - when nre<>nref -> - let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in - aux metasenv (NCic.Appl(bo::tl)) (args@moreargs) + when nre<>nref -> + let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in + aux metasenv (NCic.Appl(bo::tl)) (args@moreargs) | _ -> ty,metasenv,(args@moreargs) in 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 None in + let status, t = disambiguate status ctx t `XTNone in let status,t = term_of_cic_term status t ctx in let _,_,metasenv,subst,_ = status#obj in let ty = NCicTypeChecker.typeof status subst metasenv ctx t in @@ -549,9 +602,9 @@ let smart_apply t unit_eq status g = match gty with | NCic.Const(nref) | NCic.Appl(NCic.Const(nref)::_) -> - saturate_to_ref status metasenv subst ctx nref ty + saturate_to_ref status metasenv subst ctx nref ty | _ -> - NCicMetaSubst.saturate status metasenv subst ctx ty 0 in + NCicMetaSubst.saturate status metasenv subst ctx ty 0 in let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in let status = status#set_obj (n,h,metasenv,subst,o) in let pterm = if args=[] then t else @@ -575,19 +628,55 @@ let smart_apply t unit_eq status g = let _,_,metasenv,subst,_ = status#obj in let _,ctx,jty = List.assoc j metasenv in let jty = NCicUntrusted.apply_subst status subst ctx jty in - noprint(lazy("goal " ^ (status#ppterm ctx [] [] jty))); - fast_eq_check unit_eq status j + debug_print(lazy("goal " ^ (status#ppterm ctx [] [] jty))); + let res = fast_eq_check unit_eq status j in + 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 *) + | NCicTypeChecker.TypeCheckerFailure _ -> + debug_print (lazy "TypeCheckerFailure"); + raise (Error (lazy "no proof found",None)) +;; + +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 knoweledge of the symmetry of equality; + hence it is in trouble in proving (a = b) = (b = a) *) +let try_sym tac status g = + let sym_eq = Ast.Appl [Ast.Ident("sym_eq",None); 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 **************) @@ -807,10 +896,10 @@ type flags = { do_types : bool; (* solve goals in Type *) last : bool; (* last goal: take first solution only *) candidates: Ast.term list option; + local_candidates: bool; maxwidth : int; maxsize : int; maxdepth : int; - timeout : float; } type cache = @@ -824,20 +913,20 @@ 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)); - {cache with trace = t::cache.trace} + debug_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 let pptrace status tr = (lazy ("Proof Trace: " ^ (String.concat ";" - (List.map (NotationPp.pp_term status) tr)))) + (List.map (NotationPp.pp_term status) tr)))) (* not used let remove_from_trace cache t = match t with | Ast.NRef _ -> - (match cache.trace with - | _::tl -> {cache with trace = tl} + (match cache.trace with + | _::tl -> {cache with trace = tl} | _ -> assert false) | Ast.NCic _ (* local candidate *) | _ -> (*not an application *) cache *) @@ -868,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 = @@ -893,12 +982,12 @@ let openg_no status = List.length (head_goals status#stack) let sort_candidates status ctx candidates = let _,_,metasenv,subst,_ = status#obj in let branch cand = - let status,ct = disambiguate status ctx ("",0,cand) None in + let status,ct = disambiguate status ctx ("",0,cand) `XTNone in let status,t = term_of_cic_term status ct ctx in let ty = NCicTypeChecker.typeof status subst metasenv ctx t in let res = branch status (mk_cic_term ctx ty) in noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = " - ^ (string_of_int res))); + ^ (string_of_int res))); res in let candidates = List.map (fun t -> branch t,t) candidates in @@ -906,43 +995,66 @@ let sort_candidates status ctx candidates = List.sort (fun (a,_) (b,_) -> a - b) candidates in let candidates = List.map snd candidates in noprint (lazy ("candidates =\n" ^ (String.concat "\n" - (List.map (NotationPp.pp_term status) candidates)))); + (List.map (NotationPp.pp_term status) candidates)))); candidates let sort_new_elems l = List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l -let try_candidate ?(smart=0) flags depth status eq_cache ctx t = - try - debug_print ~depth (lazy ("try " ^ (NotationPp.pp_term status) t)); - let status = - if smart= 0 then NTactics.apply_tac ("",0,t) status - else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status - else (* smart = 2: both *) - try NTactics.apply_tac ("",0,t) status - with Error _ -> +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 " ^ (string_of_int smart) ^ " : " + ^ (NotationPp.pp_term status) t)); + let status = + if smart = 0 then NTactics.apply_tac ("",0,t) status + else if smart = 1 then 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)) - with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None + else (* smart = 2: both *) + try NTactics.apply_tac ("",0,t) status + with Error _ -> + smart_apply_auto ("",0,t) eq_cache status + in +(* FG: this optimization rules out some applications of + * lift_bind (from contribs/lambda_delta/Basic_2/substitution/lift.ma) + * + (* 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 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) + else +*) (incr candidate_no; Some ((!candidate_no,t),status)) + with Error _ -> debug_print ~depth (lazy "failed"); None ;; let sort_of status subst metasenv ctx t = @@ -958,14 +1070,14 @@ let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ") let perforate_small status subst metasenv context t = let rec aux = function | NCic.Appl (hd::tl) -> - let map t = - let s = sort_of status subst metasenv context t in - match s with - | NCic.Sort(NCic.Type [`Type,u]) - when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0)) - | _ -> aux t - in - NCic.Appl (hd::List.map map tl) + let map t = + let s = sort_of status subst metasenv context t in + match s with + | NCic.Sort(NCic.Type [`Type,u]) + when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0)) + | _ -> aux t + in + NCic.Appl (hd::List.map map tl) | t -> t in aux t @@ -980,142 +1092,133 @@ let get_cands retrieve_for diff empty gty weak_gty = cands, diff more_cands cands ;; -let get_candidates ?(smart=true) depth flags status cache signature gty = - let maxd = ((depth + 1) = flags.maxdepth) in +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 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 - | NCic.Appl _ - | NCic.Const _ - | NCic.Rel _ -> + | 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)); + noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak)); Some raw_weak, Some (weak) - | _ -> None,None + | _ -> 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 + 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 = 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 _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) -;; - -(* 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 [] + (fun ty -> search_in_th ty cache) + Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in + mapf g, mapf l 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,[] -;; *) + 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 = + 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 and paramodulation did not fail + we avoid to apply unit equalities; refl is an + exception since it prompts for convertibility *) + let l1 = if is_eq && (not pfailed) + then [Ast.Ident("refl",None)] 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 + (* 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 = +let applicative_case ~pfailed depth signature status flags gty cache = app_counter:= !app_counter+1; let _,_,metasenv,subst,_ = status#obj in let context = ctx_of gty in @@ -1124,89 +1227,47 @@ let applicative_case depth signature status flags gty cache = 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 + | NCic.Prod _ -> true, false + | _ -> 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 = - 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",None) ::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 *) + let candidates_facts, smart_candidates_facts, + candidates_other, smart_candidates_other = + get_candidates ~smart:true ~pfailed depth + 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 = if cache=[] then false else ( @@ -1262,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 = @@ -1303,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 @@ -1326,11 +1387,11 @@ let rec intros_facts ~depth status facts = | _ -> status, facts ;; -let intros ~depth status cache = +let intros ~depth status ?(use_given_only=false) cache = match is_prod status with | `Inductive _ | `Some _ -> - let trace = cache.trace in + let trace = cache.trace in let status,facts = intros_facts ~depth status cache.facts in @@ -1339,7 +1400,7 @@ let intros ~depth status cache = [(0,Ast.Ident("__intros",None)),status], cache else (* we reindex the equation from scratch *) - let unit_eq = index_local_equations status#eq_cache status in + let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in let status = NTactics.merge_tac status in [(0,Ast.Ident("__intros",None)),status], init_cache ~facts ~unit_eq () ~trace @@ -1368,8 +1429,23 @@ let reduce ~whd ~depth status g = [(!candidate_no,Ast.Ident("__whd",None)),status]) ;; -let do_something signature flags status g depth gty cache = - let l0, cache = intros ~depth status cache in +let is_meta status gty = + let _, ty = term_of_cic_term status gty (ctx_of gty) in + match ty with + | NCic.Meta _ -> true + | _ -> false +;; + +let do_something signature flags status g depth gty ?(use_given_only=false) cache = + (* if the goal is meta we close it with I:True. This should work + thanks to the toplogical sorting of goals. *) + if is_meta status gty then + let t = Ast.Ident("I",None) in + debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t)); + let s = NTactics.apply_tac ("",0,t) status in + [(0,t),s], cache + else + let l0, cache = intros ~depth status cache ~use_given_only in if l0 <> [] then l0, cache else (* whd *) @@ -1385,7 +1461,7 @@ let do_something signature flags status g depth gty cache = in let l2 = if ((l1 <> []) && flags.last) then [] else - applicative_case depth signature status flags gty cache + applicative_case ~pfailed:(l1=[]) depth signature status flags gty cache in (* statistics *) List.iter @@ -1393,8 +1469,8 @@ let do_something signature flags status g depth gty cache = (* states in l1 have have an empty set of subgoals: no point to sort them *) debug_print ~depth (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2))))); - (* l1 @ (sort_new_elems (l @ l2)), cache *) - l1 @ (List.rev l2) @ l, cache + (* we order alternatives w.r.t the number of subgoals they open *) + l1 @ (sort_new_elems l2) @ l, cache ;; let pp_goal = function @@ -1425,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 @@ -1440,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 ;; @@ -1449,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 ;; @@ -1485,12 +1561,12 @@ let deep_focus_tac level focus status = let rec slice level gs = if level = 0 then [],[],gs else match gs with - | [] -> assert false - | (g, t, k, tag) :: s -> + | [] -> assert false + | (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 @@ -1498,37 +1574,27 @@ 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 - | (g,_,_,_)::tl -> + | (g,_,_,_,_)::tl -> let is_open = function | (_,Continuationals.Stack.Open i) -> Some i | (_,Continuationals.Stack.Closed _) -> None in let others = menv_closure status (stack_goals (level-1) tl) in List.for_all (fun i -> IntSet.mem i others) - (HExtlib.filter_map is_open g) + (HExtlib.filter_map is_open g) + +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} + else cache -let rec auto_clusters ?(top=false) - flags signature cache depth status : unit = +let rec auto_clusters ?(top=false) flags signature cache depth ?(use_given_only=false) status : unit = debug_print ~depth (lazy ("entering auto clusters at depth " ^ - (string_of_int depth))); + (string_of_int depth))); debug_print ~depth (pptrace status cache.trace); (* ignore(Unix.select [] [] [] 0.01); *) let status = clean_up_tac status in @@ -1539,14 +1605,15 @@ let rec auto_clusters ?(top=false) 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} + 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 + auto_clusters flags signature cache (depth-1) status ~use_given_only else if List.length goals < 2 then - auto_main flags signature cache depth status + let cache = top_cache ~depth top status cache ~use_given_only in + auto_main flags signature cache depth status ~use_given_only else let all_goals = open_goals (depth+1) status in debug_print ~depth (lazy ("goals = " ^ @@ -1557,16 +1624,17 @@ let rec auto_clusters ?(top=false) (fun gl -> if List.length gl > flags.maxwidth then begin - debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); - HLog.warn (sprintf "global width (%u) exceeded: %u" - flags.maxwidth (List.length gl)); - raise (Gaveup cache.failures) - end else ()) classes; + debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); + HLog.warn (sprintf "global width (%u) exceeded: %u" + flags.maxwidth (List.length gl)); + raise (Gaveup cache.failures) + end else ()) classes; if List.length classes = 1 then let flags = {flags with last = (List.length all_goals = 1)} in - (* no need to cluster *) - auto_main flags signature cache depth status + (* no need to cluster *) + let cache = top_cache ~depth top status cache ~use_given_only in + auto_main flags signature cache depth status ~use_given_only else let classes = if top then List.rev classes else classes in debug_print ~depth @@ -1583,20 +1651,21 @@ let rec auto_clusters ?(top=false) let flags = {flags with last = (List.length gl = 1)} in let lold = List.length status#stack in - debug_print ~depth (lazy ("stack length = " ^ - (string_of_int lold))); + 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 ~use_given_only in try debug_print ~depth (lazy ("focusing on" ^ String.concat "," (List.map string_of_int gl))); - auto_main flags signature cache depth fstatus; assert false + auto_main flags signature cache depth fstatus ~use_given_only; assert false with | Proved(status,trace) -> - let status = NTactics.merge_tac status in - let cache = {cache with trace = trace} in - let lnew = List.length status#stack in - assert (lold = lnew); - (status,cache,true) + let status = NTactics.merge_tac status in + let cache = {cache with trace = trace} in + let lnew = List.length status#stack in + assert (lold = lnew); + (status,cache,true) | Gaveup failures when top -> let cache = {cache with failures = failures} in (status,cache,b) @@ -1604,18 +1673,18 @@ let rec auto_clusters ?(top=false) (status,cache,false) classes in let rec final_merge n s = - if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s) + if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s) in let status = final_merge depth status in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures) and (* BRAND NEW VERSION *) -auto_main flags signature cache depth status: 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 = " ^ - (string_of_int (List.length status#stack)))); + (string_of_int (List.length status#stack)))); (* ignore(Unix.select [] [] [] 0.01); *) let status = sort_tac (clean_up_tac status) in let goals = head_goals status#stack in @@ -1630,8 +1699,8 @@ auto_main flags signature cache depth status: unit = | 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 - | orig::_ -> + 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 @@ -1642,17 +1711,17 @@ auto_main flags signature cache depth status: unit = | 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 + 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 debug_print ~depth (lazy "FAIL LOCAL WIDTH"); - HLog.warn (sprintf "local width (%u) exceeded: %u" - flags.maxwidth ng); - raise (Gaveup cache.failures) + HLog.warn (sprintf "local width (%u) exceeded: %u" + flags.maxwidth ng); + raise (Gaveup cache.failures) end else if depth = flags.maxdepth then - raise (Gaveup cache.failures) + raise (Gaveup cache.failures) else let status = NTactics.branch_tac ~force:true status in let g,gctx, gty = current_goal status in @@ -1668,11 +1737,11 @@ auto_main flags signature cache depth status: unit = NCicParamod.is_equation status metasenv subst ctx ty in (* if the goal is an equality we artificially raise its depth up to flags.maxdepth - 1 *) - if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then + if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then (* for efficiency reasons, in this case we severely cripple the search depth *) (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1))); - auto_main flags signature cache (depth+1) status) + auto_main flags signature cache (depth+1) status ~use_given_only) (* check for loops *) else if is_subsumed depth false status closegty (snd cache.under_inspection) then (debug_print ~depth (lazy "SUBSUMED"); @@ -1682,40 +1751,40 @@ auto_main flags signature cache depth status: unit = (debug_print ~depth (lazy "ALREADY MET"); raise (Gaveup cache.failures)) else - let new_sig = height_of_goal g status in + let new_sig = height_of_goal g status in if new_sig < signature then - (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig))); - debug_print ~depth (lazy ("olds = " ^ (string_of_int signature)))); + (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig))); + debug_print ~depth (lazy ("olds = " ^ (string_of_int signature)))); let alternatives, cache = - do_something signature flags status g depth gty cache in + do_something signature flags status g depth gty cache ~use_given_only in let loop_cache = if flags.last then - let l,tree = cache.under_inspection in - let l,tree = closegty::l, add_to_th closegty tree closegty in + let l,tree = cache.under_inspection in + let l,tree = closegty::l, add_to_th closegty tree closegty in {cache with under_inspection = l,tree} else cache in let failures = List.fold_left (fun allfailures ((_,t),status) -> debug_print ~depth - (lazy ("(re)considering goal " ^ - (string_of_int g) ^" : "^ppterm status gty)); + (lazy ("(re)considering goal " ^ + (string_of_int g) ^" : "^ppterm status gty)); debug_print (~depth:depth) (lazy ("Case: " ^ NotationPp.pp_term status t)); let depth,cache = - if t=Ast.Ident("__whd",None) || + if t=Ast.Ident("__whd",None) || t=Ast.Ident("__intros",None) then depth, cache - else depth+1,loop_cache in - let cache = add_to_trace status ~depth cache t in + else depth+1,loop_cache in + let cache = add_to_trace status ~depth cache t in let cache = {cache with failures = allfailures} in - try - auto_clusters flags signature cache depth status; + try + auto_clusters flags signature cache depth status ~use_given_only; assert false; - with Gaveup fail -> - debug_print ~depth (lazy "Failed"); - fail) - cache.failures alternatives in + with Gaveup fail -> + debug_print ~depth (lazy "Failed"); + fail) + cache.failures alternatives in let failures = if flags.last then let newfail = @@ -1726,7 +1795,7 @@ auto_main flags signature cache depth status: unit = add_to_th newfail failures closegty else failures in debug_print ~depth (lazy "no more candidates"); - raise (Gaveup failures) + raise (Gaveup failures) ;; let int name l def = @@ -1746,18 +1815,40 @@ let cleanup_trace s trace = (* filtering facts *) in List.filter (fun t -> - match t with - | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u) - | _ -> false) trace + match t with + | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u) + | _ -> false) trace ;; -let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = +(*CSC: TODO + +- auto_params e' una high tactic che prende in input i parametri e poi li + processa nel contesto vuoto calcolando i candidate + +- astrarla su una auto_params' che prende in input gia' i candidate e un + nuovo parametro per evitare il calcolo dei candidate locali che invece + diventano vuoti (ovvero: non usare automaticamente tutte le ipotesi, bensi' + nessuna) + +- reimplementi la auto_params chiamando la auto_params' con il flag a + false e il vecchio codice per andare da parametri a candiddati + OVVERO: usa tutti le ipotesi locali + candidati globali + +- crei un nuovo entry point lowtac che calcola i candidati usando il contesto + corrente e poi fa exec della auto_params' con i candidati e il flag a true + OVVERO: usa solo candidati globali che comprendono ipotesi locali +*) + +type auto_params = NTacStatus.tactic_term list option * (string * string) list + +(*let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =*) +let auto_tac' candidates ~local_candidates ?(use_given_only=false) flags ?(trace_ref=ref []) status = let oldstatus = status in 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 -> @@ -1768,16 +1859,6 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = (NDiscriminationTree.TermSet.elements t)) ))); *) - let candidates = - match univ with - | None -> 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 depth = int "depth" flags 3 in let size = int "size" flags 10 in let width = int "width" flags 4 (* (3+List.length goals)*) in @@ -1787,10 +1868,10 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = let flags = { last = true; candidates = candidates; + local_candidates = local_candidates; maxwidth = width; maxsize = size; maxdepth = depth; - timeout = Unix.gettimeofday() +. 3000.; do_types = false; } in let initial_time = Unix.gettimeofday() in @@ -1806,7 +1887,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in let flags = { flags with maxdepth = x } in - try auto_clusters (~top:true) flags signature cache 0 status;assert false + try auto_clusters (~top:true) flags signature cache 0 status ~use_given_only;assert false (* try auto_main flags signature cache 0 status;assert false *) @@ -1814,12 +1895,12 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = | Gaveup _ -> up_to (x+1) y | Proved (s,trace) -> debug_print (lazy ("proved at depth " ^ string_of_int x)); - List.iter (toref incr_uses statistics) trace; + List.iter (toref incr_uses statistics) trace; let trace = cleanup_trace s trace in - let _ = debug_print (pptrace status trace) in + 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 @@ -1835,6 +1916,34 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = s ;; +let candidates_from_ctx univ ctx status = + match univ with + | None -> None + | Some l -> + let to_Ast t = + (* FG: `XTSort here? *) + 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) +(* 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 + let ctx = ctx_of gty in + let candidates = candidates_from_ctx univ ctx status in + auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref []) + +let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = + let candidates = candidates_from_ctx univ [] status in + auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref status + let auto_tac ~params:(_,flags as params) ?trace_ref = if List.mem_assoc "demod" flags then demod_tac ~params @@ -1844,23 +1953,3 @@ let auto_tac ~params:(_,flags as params) ?trace_ref = fast_eq_check_tac ~params else auto_tac ~params ?trace_ref ;; - - - - - - - - - - - - - - - - - - - -