X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=1937229af366726d641bd7bcc13a43d0a9085aa8;hb=69d929da2e17a9acc74edd49c2e726c72abf42ae;hp=b8a3dd44a0af3340efe48830192578eaf3060a32;hpb=4400d6a1bf09682b3c679edf0e1775117fe059c2;p=helm.git diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index b8a3dd44a..1937229af 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -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);; @@ -145,7 +145,7 @@ let is_a_fact_obj s uri = let is_a_fact_ast status subst metasenv ctx cand = noprint ~depth:0 (lazy ("checking facts " ^ NotationPp.pp_term status cand)); - let status, t = disambiguate status ctx ("",0,cand) None in + 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) @@ -247,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))); @@ -318,6 +318,44 @@ let index_local_equations eq_cache status = eq_cache ctx ;; +let index_local_equations2 eq_cache status open_goal lemmas 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 unit_eq = index_local_equations s#eq_cache s in dist_fast_eq_check unit_eq s @@ -341,8 +379,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 ;; (* @@ -549,7 +590,7 @@ 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 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 @@ -591,6 +632,10 @@ let smart_apply t unit_eq status g = | 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 = @@ -850,7 +895,6 @@ type flags = { maxwidth : int; maxsize : int; maxdepth : int; - timeout : float; } type cache = @@ -933,7 +977,7 @@ 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 @@ -1770,7 +1814,8 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = | None -> None | Some l -> let to_Ast t = - let status, res = disambiguate status [] t None in +(* FG: `XTSort here? *) + let status, res = disambiguate status [] 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) @@ -1787,7 +1832,6 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = maxwidth = width; maxsize = size; maxdepth = depth; - timeout = Unix.gettimeofday() +. 3000.; do_types = false; } in let initial_time = Unix.gettimeofday() in @@ -1841,23 +1885,3 @@ let auto_tac ~params:(_,flags as params) ?trace_ref = fast_eq_check_tac ~params else auto_tac ~params ?trace_ref ;; - - - - - - - - - - - - - - - - - - - -