From 8e15fc948d1c5dafb982701790fb085f34a7dd10 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 18 Jan 2010 10:04:51 +0000 Subject: [PATCH] New paramod tac. --- helm/software/components/ng_tactics/nnAuto.ml | 108 ++++++++++-------- 1 file changed, 62 insertions(+), 46 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index e2ddda033..6044f3a34 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -56,7 +56,8 @@ let menv_closure status gl = (* we call a "fact" an object whose hypothesis occur in the goal or in types of goal-variables *) let is_a_fact status ty = - let status, ty, _ = saturate ~delta:max_int status ty in + let status, ty, _ = saturate ~delta:0 status ty in + debug_print (lazy (ppterm status ty)); let g_metas = metas_of_term status ty in let clos = menv_closure status g_metas in let _,_,metasenv,_,_ = status#obj in @@ -84,34 +85,10 @@ let current_goal status = (* =============================== paramod =========================== *) -let auto_paramod ~params:(l,_) status goal = - let gty = get_goalty status goal in - let n,h,metasenv,subst,o = status#obj in - let status,t = term_of_cic_term status gty (ctx_of gty) in - let status, l = - List.fold_left - (fun (status, l) t -> - let status, t = disambiguate status (ctx_of gty) t None in - let status, ty = typeof status (ctx_of t) t in - let status, t = term_of_cic_term status t (ctx_of gty) in - let status, ty = term_of_cic_term status ty (ctx_of ty) in - (status, (t,ty) :: l)) - (status,[]) l - in - match - NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l - with - | [] -> raise (Error (lazy "no proof found",None)) - | (pt, _, metasenv, subst)::_ -> - let status = status#set_obj (n,h,metasenv,subst,o) in - instantiate status goal (mk_cic_term (ctx_of gty) pt) -;; - -let auto_paramod_tac ~params status = - NTactics.distribute_tac (auto_paramod ~params) status -;; - -let fast_eq_check_all status eq_cache goal = +let solve fast status eq_cache goal = + let f = + if fast then NCicParamod.fast_eq_check + else NCicParamod.paramod in let n,h,metasenv,subst,o = status#obj in let gname, ctx, gty = List.assoc goal metasenv in let gty = NCicUntrusted.apply_subst subst ctx gty in @@ -120,8 +97,8 @@ let fast_eq_check_all status eq_cache goal = 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) + NCicRefiner.typeof status + (* (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 = @@ -140,15 +117,22 @@ let fast_eq_check_all status eq_cache goal = 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 + with + NCicRefiner.RefineFailure msg + | NCicRefiner.Uncertain msg -> + debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^ + snd (Lazy.force msg))); None + | NCicRefiner.AssertFailure msg -> + debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^ + Lazy.force msg)); None + | _ -> None in HExtlib.filter_map build_status - (NCicParamod.fast_eq_check status metasenv subst ctx - eq_cache (NCic.Rel ~-1,gty)) + (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty)) ;; let fast_eq_check eq_cache status goal = - match fast_eq_check_all status eq_cache goal with + match solve true status eq_cache goal with | [] -> raise (Error (lazy "no proof found",None)) | s::_ -> s ;; @@ -191,6 +175,17 @@ let fast_eq_check_tac ~params s = dist_fast_eq_check unit_eq s ;; +let paramod eq_cache status goal = + match solve false status eq_cache goal with + | [] -> raise (Error (lazy "no proof found",None)) + | s::_ -> s +;; + +let paramod_tac ~params s = + let unit_eq = index_local_equations s#eq_cache s in + NTactics.distribute_tac (paramod unit_eq) s +;; + (* let fast_eq_check_tac_all ~params eq_cache status = let g,_,_ = current_goal status in @@ -203,6 +198,17 @@ let fast_eq_check_tac_all ~params eq_cache status = ;; *) +(* +let demod status eq_cache goal = + let n,h,metasenv,subst,o = status#obj in + let gname, ctx, gty = List.assoc goal metasenv in + let gty = NCicUntrusted.apply_subst subst ctx gty in + +let demod_tac ~params s = + let unit_eq = index_local_equations s#eq_cache s in + dist_fast_eq_check unit_eq s +*) + (*************** subsumption ****************) let close_wrt_context = @@ -1470,19 +1476,27 @@ let get_candidates ?(smart=true) status cache signature gty = ;; let applicative_case depth signature status flags gty (cache:cache) = - app_counter:= !app_counter+1; + app_counter:= !app_counter+1; + let _,_,metasenv,subst,_ = status#obj in + let context = ctx_of gty in let tcache = cache.facts in + let is_eq = + let status, t = term_of_cic_term status gty context in + NCicParamod.is_equation metasenv subst context t + in + debug_print(lazy (string_of_bool is_eq)); let candidates, smart_candidates = - get_candidates status tcache signature gty in - print ~depth + get_candidates ~smart:(not is_eq) status tcache signature gty in + debug_print ~depth (lazy ("candidates: " ^ string_of_int (List.length candidates))); - print ~depth + debug_print ~depth (lazy ("smart candidates: " ^ string_of_int (List.length smart_candidates))); + let sm = if is_eq then 0 else 2 in let elems = List.fold_left (fun elems cand -> - match try_candidate (~smart:2) + match try_candidate (~smart:sm) flags depth status cache.unit_eq cand with | None -> elems | Some x -> x::elems) @@ -1613,17 +1627,19 @@ let do_something signature flags status g depth gty cache = (* whd *) let l = reduce ~depth status g in (* backward aplications *) - let l1 = applicative_case depth signature status flags gty cache in - (* fast paramodulation *) - let l2 = + let l1 = List.map (fun s -> incr candidate_no; ((!candidate_no,Ast.Ident("__paramod",None)),s)) - (auto_eq_check cache.unit_eq status) + (auto_eq_check cache.unit_eq status) in + let l2 = + if (l1 <> []) then [] + else applicative_case depth signature status flags gty cache + (* fast paramodulation *) in - (* states in l2 have have an set of subgoals: no point to sort them *) - l2 @ (sort_new_elems (l@l1)), cache + (* states in l1 have have an empty set of subgoals: no point to sort them *) + l1 @ (sort_new_elems (l@l2)), cache ;; let pp_goal = function -- 2.39.2