From fa0b30be968340ec83c8821169218e7bdcbc8426 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 9 Dec 2009 16:02:48 +0000 Subject: [PATCH] Attached fast_eq_check to auto --- helm/software/components/ng_tactics/nnAuto.ml | 359 ++++++++++-------- 1 file changed, 210 insertions(+), 149 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 827c1dc46..0251a84c9 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -11,7 +11,7 @@ open Printf -let debug = ref false +let debug = ref true let debug_print ?(depth=0) s = if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else () (* let print= debug_print *) @@ -25,7 +25,66 @@ open NTacStatus module Ast = CicNotationPt let app_counter = ref 0 -(* =================================== paramod =========================== *) +(* ======================= utility functions ========================= *) +module IntSet = Set.Make(struct type t = int let compare = compare end) + +let get_sgoalty status g = + let _,_,metasenv,subst,_ = status#obj in + try + let _, ctx, ty = NCicUtils.lookup_meta g metasenv in + let ty = NCicUntrusted.apply_subst subst ctx ty in + let ctx = NCicUntrusted.apply_subst_context + ~fix_projections:true subst ctx + in + NTacStatus.mk_cic_term ctx ty + with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty") +;; + +let deps status g = + let gty = get_sgoalty status g in + metas_of_term status gty +;; + +let menv_closure status gl = + let rec closure acc = function + | [] -> acc + | x::l when IntSet.mem x acc -> closure acc l + | x::l -> closure (IntSet.add x acc) (deps status x @ l) + in closure IntSet.empty gl +;; + +(* we call a "fact" an object whose hypothesis occurs 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 g_metas = metas_of_term status ty in + let clos = menv_closure status g_metas in + let _,_,metasenv,_,_ = status#obj in + let menv = + List.fold_left + (fun acc (i,_) -> IntSet.add i acc) + IntSet.empty metasenv + in IntSet.equal clos menv;; + +let is_a_fact_obj s uri = + let obj = NCicEnvironment.get_checked_obj uri in + match obj with + | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) -> + is_a_fact s (mk_cic_term [] ty) +(* aggiungere i costruttori *) + | _ -> false + +let current_goal status = + let open_goals = head_goals status#stack in + assert (List.length open_goals = 1); + let open_goal = List.hd open_goals in + let gty = get_goalty status open_goal in + let ctx = ctx_of gty in + open_goal, ctx, gty + + + +(* =============================== paramod =========================== *) let auto_paramod ~params:(l,_) status goal = let gty = get_goalty status goal in let n,h,metasenv,subst,o = status#obj in @@ -53,53 +112,53 @@ let auto_paramod_tac ~params status = NTactics.distribute_tac (auto_paramod ~params) status ;; -let fast_eq_check ~params status goal = +let fast_eq_check_all status eq_cache goal = let gty = get_goalty status goal in + let ctx = ctx_of gty in let n,h,metasenv,subst,o = status#obj in - let eq_cache = status#eq_cache in - let status,t = term_of_cic_term status gty (ctx_of gty) in - match - NCicParamod.fast_eq_check status metasenv subst (ctx_of gty) - eq_cache (NCic.Rel ~-1,t) - 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 status,t = term_of_cic_term status gty ctx in + let build_status (pt, metasenv, subst) = + let status = status#set_obj (n,h,metasenv,subst,o) in + let gty = get_goalty status goal in + instantiate status goal (mk_cic_term ctx pt) + in + List.map build_status + (NCicParamod.fast_eq_check status metasenv subst ctx + eq_cache (NCic.Rel ~-1,t)) ;; -let fast_eq_check_tac ~params = - NTactics.distribute_tac (fast_eq_check ~params) +let fast_eq_check eq_cache status goal = + match fast_eq_check_all status eq_cache goal with + | [] -> raise (Error (lazy "no proof found",None)) + | s::_ -> s ;; -(*************** subsumption ****************) -module IntSet = Set.Make(struct type t = int let compare = compare end) -(* exceptions *) - -let get_sgoalty status g = - let _,_,metasenv,subst,_ = status#obj in - try - let _, ctx, ty = NCicUtils.lookup_meta g metasenv in - let ty = NCicUntrusted.apply_subst subst ctx ty in - let ctx = NCicUntrusted.apply_subst_context - ~fix_projections:true subst ctx - in - NTacStatus.mk_cic_term ctx ty - with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty") +let fast_eq_check_tac ~params s = + NTactics.distribute_tac (fast_eq_check s#eq_cache) s ;; -let deps status g = - let gty = get_sgoalty status g in - metas_of_term status gty +let auto_eq_check eq_cache status = + try + let s = + NTactics.distribute_tac (fast_eq_check eq_cache) status in + [s] + with + | Error _ -> [] ;; -let menv_closure status gl = - let rec closure acc = function - | [] -> acc - | x::l when IntSet.mem x acc -> closure acc l - | x::l -> closure (IntSet.add x acc) (deps status x @ l) - in closure IntSet.empty gl +(* +let fast_eq_check_tac_all ~params eq_cache status = + let g,_,_ = current_goal status in + let allstates = fast_eq_check_all status eq_cache g in + let pseudo_low_tac s _ _ = s in + let pseudo_low_tactics = + List.map pseudo_low_tac allstates + in + List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics ;; +*) + +(*************** subsumption ****************) let close_wrt_context = List.fold_left @@ -1121,6 +1180,8 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa *) (****************** types **************) + + type th_cache = (NCic.context * InvRelDiscriminationTree.t) list let keys_of_term status t = @@ -1223,6 +1284,12 @@ type flags = { timeout : float; } +type cache = + {facts : th_cache; (* positive results *) + under_inspection : th_cache; (* to prune looping *) + unit_eq : NCicParamod.state + } + type sort = T | P type goal = int * sort (* goal, depth, sort *) type fail = goal * cic_term @@ -1238,28 +1305,34 @@ exception Proved of #NTacStatus.tac_status (* let put_in_subst s _ _ _ = s;; *) (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *) (* let cache_add_underinspection c _ _ = c;; *) -let equational_case _ _ _ _ _ _ = [];; + +let init_cache ?(facts=[]) ?(under_inspection=[]) + ?(unit_eq=NCicParamod.empty_state) _ = + {facts = facts; + under_inspection = under_inspection; + unit_eq = unit_eq + } + let only _ _ _ = true;; let candidate_no = ref 0;; -let sort_new_elems l = - List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l -;; +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 t = try debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t)); let status = NTactics.apply_tac ("",0,t) status in - let open_goals = head_goals status#stack in - debug_print ~depth - (lazy ("success: "^String.concat " "(List.map string_of_int open_goals))); - if List.length open_goals > flags.maxwidth || - (depth = flags.maxdepth && open_goals <> []) then + 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) else (incr candidate_no; - Some ((!candidate_no,t),status,open_goals)) + Some ((!candidate_no,t),status)) with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None ;; @@ -1281,8 +1354,8 @@ let get_candidates status cache signature gty = List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands ;; -let applicative_case depth signature status flags gty cache = - let tcache,_ = cache in +let applicative_case depth signature status flags gty (cache:cache) = + let tcache = cache.facts in app_counter:= !app_counter+1; let candidates = get_candidates status tcache signature gty in debug_print ~depth @@ -1302,7 +1375,7 @@ exception Found ;; (* gty is supposed to be meta-closed *) -let is_subsumed depth status gty (_,cache) = +let is_subsumed depth status gty cache = if cache=[] then false else ( debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty))); let n,h,metasenv,subst,obj = status#obj in @@ -1343,58 +1416,21 @@ let is_subsumed depth status gty (_,cache) = with Found -> debug_print ~depth (lazy "success");true) ;; - -let equational_and_applicative_case - signature flags status g depth gty cache -= - let elems = - if false (*is_equational_case gty flags*) then - let elems = - equational_case - signature status flags g gty cache - in - let more_elems = - applicative_case depth - signature status flags gty cache - in - elems@more_elems - else - let elems = - (*match LibraryObjects.eq_URI () with - | Some _ -> - smart_applicative_case dbd tables depth s fake_proof goalno - gty m context signature universe cache flags - | None -> *) - applicative_case depth - signature status flags gty cache - in - elems - in - let elems = - List.map (fun c,s,gl -> - c,1,1,s,List.map (fun i -> - let sort = - let gty = get_goalty s i in - let _, sort = typeof s (ctx_of gty) gty in - match term_of_cic_term s sort (ctx_of sort) with - | _, NCic.Sort NCic.Prop -> P - | _ -> T - in - i,sort) gl) elems - in - (* let elems = sort_new_elems elems in *) - elems, cache -;; - (* warning: ctx is supposed to be already instantiated w.r.t subst *) -let index_local_equations eq_cache ctx = +let index_local_equations eq_cache status = + let open_goals = head_goals status#stack in + assert (List.length open_goals = 1); + let open_goal = List.hd open_goals in + let ngty = get_goalty status open_goal in + let ctx = ctx_of ngty in let c = ref 0 in List.fold_left - (fun cache _ -> + (fun eq_cache _ -> c:= !c+1; - let t = NCic.Rel 1 in + let t = NCic.Rel !c in try let ty = NCicTypeChecker.typeof [] [] ctx t in + prerr_endline ("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)); NCicParamod.forward_infer_step eq_cache t ty with | NCicTypeChecker.TypeCheckerFailure _ @@ -1408,33 +1444,46 @@ let rec guess_name name ctx = guess_name (name^"'") ctx ;; -let intro ~depth status (tcache,fcache) name = +let is_prod status = + let _, ctx, gty = current_goal status in + let _, raw_gty = term_of_cic_term status gty ctx in + match raw_gty with + | NCic.Prod (name,_,_) -> Some (guess_name name ctx) + | _ -> None + +let intro ~depth status facts name = let status = NTactics.intro_tac name status in - let open_goals = head_goals status#stack in - assert (List.length open_goals = 1); - let open_goal = List.hd open_goals in - let ngty = get_goalty status open_goal in - let ctx = ctx_of ngty 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 tcache = List.fold_left (add_to_th t) tcache keys in - debug_print ~depth (lazy ("intro: "^ string_of_int open_goal)); + let facts = List.fold_left (add_to_th t) facts keys in + debug_print ~depth (lazy ("intro: "^ name)); (* unprovability is not stable w.r.t introduction *) - status, (tcache,[]) + status, facts ;; -let rec intros ~depth status cache = - let open_goals = head_goals status#stack in - assert (List.length open_goals = 1); - let open_goal = List.hd open_goals in - let gty = get_goalty status open_goal in - let _, raw_gty = term_of_cic_term status gty (ctx_of gty) in - match raw_gty with - | NCic.Prod (name,_,_) -> - let status,cache = - intro ~depth status cache (guess_name name (ctx_of gty)) - in intros ~depth status cache - | _ -> status, cache, open_goal +let rec intros_facts ~depth status facts = + match is_prod status with + | Some(name) -> + let status,facts = + intro ~depth status facts name + in intros_facts ~depth status facts + | _ -> status, facts +;; + +let rec intros ~depth status (cache:cache) = + match is_prod status with + | Some _ -> + prerr_endline "is prod"; + let status,facts = + intros_facts ~depth status cache.facts + in + (* we reindex the equation from scratch *) + let unit_eq = + index_local_equations status#eq_cache status in + (* under_inspection must be set to empty *) + status, init_cache ~facts ~unit_eq () + | _ -> status, cache ;; let reduce ~depth status g = @@ -1451,16 +1500,24 @@ let reduce ~depth status g = in let status = status#set_obj (n,h,metasenv,subst,o) in incr candidate_no; - [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[g,P]]) + [(!candidate_no,Ast.Ident("__whd",None)),status]) ;; let do_something signature flags status g depth gty cache = + (* whd *) let l = reduce ~depth status g in - let l1,cache = - (equational_and_applicative_case - signature flags status g depth gty cache) + (* backward aplications *) + let l1 = applicative_case depth signature status flags gty cache in + (* fast paramodulation *) + let l2 = + List.map + (fun s -> + incr candidate_no; + ((!candidate_no,Ast.Ident("__paramod",None)),s)) + (auto_eq_check cache.unit_eq status) + (* states in l2 have have an set of subgoals: no point to sort them *) in - sort_new_elems (l@l1), cache + l2 @ (sort_new_elems (l@l1)), cache ;; let pp_goal = function @@ -1580,41 +1637,43 @@ and (* let rec auto_main flags signature cache status k depth = *) -auto_main flags signature cache depth status: unit = +auto_main flags signature (cache:cache) depth status: unit = debug_print ~depth (lazy "entering auto main"); (* ignore(Unix.select [] [] [] 0.01); *) let status = sort_tac (clean_up_tac status) in let goals = head_goals status#stack in match goals with | [] -> raise (Proved status) - | g::tlg -> + | _ -> + let branch = List.length(goals)>1 in if depth = flags.maxdepth then raise (Gaveup IntSet.empty) else let status = - if tlg=[] then status - else NTactics.branch_tac status in - let status, cache, g = intros ~depth status cache in - let gty = get_goalty status g in + if branch then NTactics.branch_tac status + else status in + let status, cache = intros ~depth status cache in + let g,gctx, gty = current_goal status in let ctx,ty = close status g in let closegty = mk_cic_term ctx ty in - let status, gty = apply_subst status (ctx_of gty) gty in + let status, gty = apply_subst status gctx gty in debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); - if is_subsumed depth status closegty cache then + if is_subsumed depth status closegty cache.under_inspection then (debug_print (lazy "SUBSUMED"); raise (Gaveup IntSet.add g IntSet.empty)) else let alternatives, cache = do_something signature flags status g depth gty cache in - let loop_cache = - let tcache,fcache = cache in - tcache,add_to_th closegty fcache closegty in + let loop_cache = + let under_inspection = + add_to_th closegty cache.under_inspection closegty in + {cache with under_inspection = under_inspection} in let unsat = List.fold_left (* the underscore information does not need to be returned by do_something *) - (fun unsat ((_,t),_,_,status,_) -> + (fun unsat ((_,t),status) -> let depth',looping_cache = - if t=(Ast.Implicit `JustOne) then depth,cache + if t=Ast.Ident("__whd",None) then depth,cache else depth+1, loop_cache in debug_print (~depth:depth') (lazy ("Case: " ^ CicNotationPp.pp_term t)); @@ -1623,20 +1682,20 @@ auto_main flags signature cache depth status: unit = with | Proved status -> debug_print (~depth:depth') (lazy "proved"); - if tlg=[] then raise (Proved status) - else + if branch then let status = NTactics.merge_tac status - in - ( (* old cache, here *) - try auto_clusters flags signature cache - depth status; assert false - with Gaveup f -> - debug_print ~depth - (lazy ("Unsat1 at depth " ^ (string_of_int depth) + in + (* old cache, here *) + try auto_clusters flags signature cache + depth status; assert false + with Gaveup f -> + debug_print ~depth + (lazy ("Unsat1 at depth " ^ (string_of_int depth) ^ ": " ^ (pp_goals status (IntSet.elements f)))); (* TODO: cache failures *) - IntSet.union f unsat) + IntSet.union f unsat + else raise (Proved status) | Gaveup f -> debug_print (~depth:depth') (lazy ("Unsat2 at depth " ^ (string_of_int depth') @@ -1656,8 +1715,10 @@ let int name l def = let auto_tac ~params:(_univ,flags) status = let goals = head_goals status#stack in - let status, cache = mk_th_cache status goals in -(* pp_th status cache; *) + 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 +(* pp_th status facts; *) (* NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> debug_print (lazy( @@ -1693,7 +1754,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;status + try auto_clusters flags signature cache 0 status;assert false with | Gaveup _ -> up_to (x+1) y | Proved s -> -- 2.39.2