From: Andrea Asperti Date: Fri, 8 Jan 2010 08:09:39 +0000 (+0000) Subject: Support for the new // tactics. X-Git-Tag: make_still_working~3144 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3b44e3ec72da65e9eee560fb6ec3a8d29b41bd52;p=helm.git Support for the new // tactics. --- diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index e00bb2ade..e2ddda033 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -116,28 +116,33 @@ let fast_eq_check_all status eq_cache goal = let gname, ctx, gty = List.assoc goal metasenv in let gty = NCicUntrusted.apply_subst subst ctx gty in let build_status (pt, _, metasenv, subst) = - let stamp = Unix.gettimeofday () in - let metasenv, subst, pt, pty = - NCicRefiner.typeof - (status#set_coerc_db NCicCoercion.empty_db) - metasenv subst ctx pt None in - let metasenv, subst = - NCicUnification.unify status metasenv subst ctx gty pty -(* the previous code is much less expensive than directly refining - pt with expected type pty - in - NCicRefiner.typeof - (status#set_coerc_db NCicCoercion.empty_db) - metasenv subst ctx pt (Some gty) *) - in - print (lazy (Printf.sprintf "Refined in %fs" + try + print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt))); + let stamp = Unix.gettimeofday () in + let metasenv, subst, pt, pty = + NCicRefiner.typeof + (status#set_coerc_db NCicCoercion.empty_db) + metasenv subst ctx pt None in + print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty))); + let metasenv, subst = + NCicUnification.unify status metasenv subst ctx gty pty + (* the previous code is much less expensive than directly refining + pt with expected type pty + in + prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty)); + NCicRefiner.typeof + (status#set_coerc_db NCicCoercion.empty_db) + metasenv subst ctx pt (Some gty) *) + in + print (lazy (Printf.sprintf "Refined in %fs" (Unix.gettimeofday() -. stamp))); - let status = status#set_obj (n,h,metasenv,subst,o) in - let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in - let subst = (goal,(gname,ctx,pt,pty)) :: subst in - status#set_obj (n,h,metasenv,subst,o) + let status = status#set_obj (n,h,metasenv,subst,o) in + let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in + let subst = (goal,(gname,ctx,pt,pty)) :: subst in + Some (status#set_obj (n,h,metasenv,subst,o)) + with _ -> prerr_endline "WARNING: refining in fast_eq_check failed"; None in - List.map build_status + HExtlib.filter_map build_status (NCicParamod.fast_eq_check status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty)) ;; @@ -1344,7 +1349,7 @@ let pp_th status = let search_in_th gty th = let c = ctx_of gty in let rec aux acc = function - | [] -> Ncic_termSet.elements acc + | [] -> (* Ncic_termSet.elements *) acc | (_::tl) as k -> try let idx = List.assq k th in @@ -1403,55 +1408,96 @@ let openg_no status = List.length (head_goals status#stack) let sort_new_elems l = List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l -let try_candidate flags depth status eq_cache t = +let try_candidate ?(smart=0) flags depth status eq_cache t = try - debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t)); + print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t)); let status = - smart_apply_auto ("",0,t) eq_cache status in - (* let status = NTactics.apply_tac ("",0,t) status in *) - let og_no = openg_no status in - if og_no > flags.maxwidth || + 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 _ -> + smart_apply_auto ("",0,t) eq_cache status in + let og_no = openg_no status in + if og_no > flags.maxwidth || (depth = flags.maxdepth && og_no <> 0) then - (debug_print ~depth (lazy "pruned immediately"); None) + (debug_print ~depth (lazy "pruned immediately"); None) else (incr candidate_no; Some ((!candidate_no,t),status)) with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None ;; -let get_candidates status cache signature gty = +let get_candidates ?(smart=true) status cache signature gty = let universe = status#auto_cache 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 cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables - universe raw_gty - in - let cands = - List.filter (only signature context) - (NDiscriminationTree.TermSet.elements cands) + universe raw_gty in + let local_cands = search_in_th gty cache in + 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 smart_candidates = + if smart then + match raw_gty with + | NCic.Appl (hd::tl) -> + let weak_gty = + 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 + | _ -> [] + else [] in - List.map (fun t -> - let _status, t = term_of_cic_term status t context in Ast.NCic t) - (search_in_th gty cache) - @ - List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands + candidates, smart_candidates ;; let applicative_case depth signature status flags gty (cache:cache) = + app_counter:= !app_counter+1; let tcache = cache.facts in - app_counter:= !app_counter+1; - let candidates = get_candidates status tcache signature gty in - debug_print ~depth + let candidates, smart_candidates = + get_candidates status tcache signature gty in + print ~depth (lazy ("candidates: " ^ string_of_int (List.length candidates))); + print ~depth + (lazy ("smart candidates: " ^ + string_of_int (List.length smart_candidates))); let elems = List.fold_left (fun elems cand -> - match try_candidate flags depth status cache.unit_eq cand with + match try_candidate (~smart:2) + flags depth status cache.unit_eq cand with | None -> elems | Some x -> x::elems) [] candidates in - elems + let more_elems = + List.fold_left + (fun elems cand -> + match try_candidate (~smart:1) + flags depth status cache.unit_eq cand with + | None -> elems + | Some x -> x::elems) + [] smart_candidates + in + elems@more_elems ;; exception Found @@ -1660,7 +1706,7 @@ let focus_tac focus status = status#set_stack gstatus ;; -let rec auto_clusters +let rec auto_clusters ?(top=false) flags signature cache depth status : unit = debug_print ~depth (lazy "entering auto clusters"); (* ignore(Unix.select [] [] [] 0.01); *) @@ -1674,6 +1720,7 @@ let rec auto_clusters debug_print ~depth (lazy ("goals = " ^ String.concat "," (List.map string_of_int goals))); let classes = HExtlib.clusters (deps status) goals in + let classes = if top then List.rev classes else classes in debug_print ~depth (lazy (String.concat "\n" @@ -1681,17 +1728,20 @@ let rec auto_clusters (fun l -> ("cluster:" ^ String.concat "," (List.map string_of_int l))) classes))); - let status = + let status,b = List.fold_left - (fun status gl -> + (fun (status,b) gl -> let status = focus_tac gl status in try debug_print ~depth (lazy ("focusing on" ^ String.concat "," (List.map string_of_int gl))); - auto_main flags signature cache depth status; status - with Proved(status) -> NTactics.merge_tac status) - status classes - in raise (Proved status) + auto_main flags signature cache depth status; assert false + with + | Proved(status) -> (NTactics.merge_tac status,true) + | Gaveup _ when top -> (NTactics.merge_tac status,b) + ) + (status,false) classes + in if b then raise (Proved status) else raise (Gaveup IntSet.empty) and @@ -1817,7 +1867,7 @@ let auto_tac ~params:(_univ,flags) status = let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in let flags = { flags with maxdepth = x } in - try auto_clusters flags signature cache 0 status;assert false + try auto_clusters (~top:true) flags signature cache 0 status;assert false with | Gaveup _ -> up_to (x+1) y | Proved s ->