From 711a06aebcd4f8e1127a56d82dd1fc4de22d5ea2 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 23 Nov 2009 10:42:34 +0000 Subject: [PATCH] Subsumption and reduction --- helm/software/components/ng_tactics/nnAuto.ml | 223 ++++++++++++------ 1 file changed, 154 insertions(+), 69 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 70e6ed24e..0ff4ddbe5 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -223,16 +223,16 @@ let close status g = let elems = IntSet.elements subset in let _, ctx, ty = NCicUtils.lookup_meta g metasenv in let ty = NCicUntrusted.apply_subst subst ctx ty in - print (lazy ("Elements for " ^ (NCicPp.ppterm ctx [] metasenv ty))); - print (lazy (String.concat ", " (List.map string_of_int elems))); + debug_print (lazy ("metas in " ^ (NCicPp.ppterm ctx [] metasenv ty))); + debug_print (lazy (String.concat ", " (List.map string_of_int elems))); let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in (* let submenv = metasenv in *) let ty = close_wrt_metasenv subst ty submenv in - print (lazy (NCicPp.ppterm ctx [] [] ty)); - ty + debug_print (lazy (NCicPp.ppterm ctx [] [] ty)); + ctx,ty ;; @@ -1180,7 +1180,6 @@ let pp_th status = pp_idx status idx) ;; - let search_in_th gty th = let c = ctx_of gty in let rec aux acc = function @@ -1214,14 +1213,14 @@ exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive atoms of the input goals *) exception Proved of #NTacStatus.tac_status -let close_failures _ c = c;; -let prunable _ _ _ = false;; -let cache_examine cache gty = `Notfound;; -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 close_failures _ c = c;; *) +(* let prunable _ _ _ = false;; *) +(* let cache_examine cache gty = `Notfound;; *) +(* 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 only _ _ _ = true;; +let only _ _ _ = true;; let candidate_no = ref 0;; @@ -1229,10 +1228,9 @@ let sort_new_elems l = List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l ;; -let try_candidate flags depth status t g = +let try_candidate flags depth status t = try debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t)); - (* let status = NTactics.focus_tac [g] status in *) let status = NTactics.apply_tac ("",0,t) status in let open_goals = head_goals status#stack in debug_print ~depth @@ -1246,12 +1244,12 @@ let try_candidate flags depth status t g = with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None ;; -let get_candidates status cache_th signature gty = +let get_candidates status cache signature gty = let universe = status#auto_cache in let context = ctx_of gty in let _, raw_gty = term_of_cic_term status gty context in - let cands = - NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty + let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables + universe raw_gty in let cands = List.filter (only signature context) @@ -1259,20 +1257,21 @@ let get_candidates status cache_th signature gty = in List.map (fun t -> let _status, t = term_of_cic_term status t context in Ast.NCic t) - (search_in_th gty cache_th) + (search_in_th gty cache) @ List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands ;; -let applicative_case depth signature status flags g gty cache = +let applicative_case depth signature status flags gty cache = + let tcache,_ = cache in app_counter:= !app_counter+1; - let candidates = get_candidates status cache signature gty in + let candidates = get_candidates status tcache signature gty in debug_print ~depth (lazy ("candidates: " ^ string_of_int (List.length candidates))); let elems = List.fold_left (fun elems cand -> - match try_candidate flags depth status cand g with + match try_candidate flags depth status cand with | None -> elems | Some x -> x::elems) [] candidates @@ -1280,6 +1279,52 @@ let applicative_case depth signature status flags g gty cache = elems ;; +exception Found +;; + +(* gty is supposed to be meta-closed *) +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 + let ctx = ctx_of gty in + let _ , target = term_of_cic_term status gty ctx in + let target = NCicSubstitution.lift 1 target in + (* candidates must only be searched w.r.t the given context *) + let candidates = + try + let idx = List.assq ctx cache in + Ncic_termSet.elements + (InvRelDiscriminationTree.retrieve_generalizations idx gty) + with Not_found -> [] + in + debug_print ~depth + (lazy ("failure candidates: " ^ string_of_int (List.length candidates))); + try + List.iter + (fun t -> + let _ , source = term_of_cic_term status t ctx in + let implication = + NCic.Prod("foo",source,target) in + let metasenv,j,_,_ = + 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 + try + let status = NTactics.intro_tac "foo" status in + let status = + NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status + in + if (head_goals status#stack = []) then raise Found + else () + with + | Error _ -> ()) + candidates;false + with Found -> debug_print ~depth (lazy "success");true) +;; + + let equational_and_applicative_case signature flags status g depth gty cache = @@ -1291,7 +1336,7 @@ let equational_and_applicative_case in let more_elems = applicative_case depth - signature status flags g gty cache + signature status flags gty cache in elems@more_elems else @@ -1302,7 +1347,7 @@ let equational_and_applicative_case gty m context signature universe cache flags | None -> *) applicative_case depth - signature status flags g gty cache + signature status flags gty cache in elems in @@ -1318,7 +1363,7 @@ let equational_and_applicative_case in i,sort) gl) elems in - let elems = sort_new_elems elems in + (* let elems = sort_new_elems elems in *) elems, cache ;; @@ -1328,22 +1373,59 @@ let rec guess_name name ctx = guess_name (name^"'") ctx ;; -let intro_case status gno gty depth cache name = - (* let status = NTactics.focus_tac [gno] status in *) - let status = NTactics.intro_tac (guess_name name (ctx_of gty)) 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 t = mk_cic_term ctx (NCic.Rel 1) in - let status, keys = keys_of_term status t in - let cache = List.fold_left (add_to_th t) cache keys in - debug_print ~depth (lazy ("intro: "^ string_of_int open_goal)); - incr candidate_no; - (* XXX compute the sort *) - [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[open_goal,P]], - cache +let intro ~depth status (tcache,fcache) 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 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)); + (* unprovability is not stable w.r.t introduction *) + status, (tcache,[]) +;; + +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 reduce ~depth status g = + let n,h,metasenv,subst,o = status#obj in + let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in + let ty = NCicUntrusted.apply_subst subst ctx ty in + let ty' = NCicReduction.whd ~subst ctx ty in + if ty = ty' then [] + else + (debug_print ~depth + (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty')); + let metasenv = + (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv) + 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]]) +;; + +let do_something signature flags status g depth gty cache = + let l = reduce ~depth status g in + let l1,cache = + (equational_and_applicative_case + signature flags status g depth gty cache) + in + sort_new_elems (l@l1), cache ;; let pp_goal = function @@ -1360,14 +1442,6 @@ let pp_goals status l = l) ;; -let do_something signature flags s gno depth gty cache = - let _s, raw_gty = term_of_cic_term s gty (ctx_of gty) in - match raw_gty with - | NCic.Prod (name,_,_) -> intro_case s gno gty depth cache name - | _ -> - equational_and_applicative_case signature flags s gno depth gty cache -;; - module M = struct type t = int @@ -1469,9 +1543,6 @@ let rec auto_clusters and -(* The pair solved,init_status is used for chaching purposes. - solved is the list of goals in init_status already proved. - Initially, init_status=status and k is set to [] *) (* let rec auto_main flags signature cache status k depth = *) auto_main flags signature cache depth status: unit = @@ -1482,29 +1553,37 @@ auto_main flags signature cache depth status: unit = match goals with | [] -> raise (Proved status) | g::tlg -> - if depth = flags.maxdepth then raise (Gaveup IntSet.empty) - else - let status = + 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 + 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 - debug_print ~depth (lazy("Depth = " ^ (string_of_int depth))); - debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); - close status g; - (* let closed = metas_of_term status gty = [] in *) + debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); + if is_subsumed depth status closegty cache 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 unsat = List.fold_left (* the underscore information does not need to be returned by do_something *) (fun unsat ((_,t),_,_,status,_) -> - let depth' = - if t=(Ast.Implicit `JustOne) then depth else depth+1 in + let depth',looping_cache = + if t=(Ast.Implicit `JustOne) then depth,cache + else depth+1, loop_cache in debug_print (~depth:depth') - (lazy ("Case: " ^ CicNotationPp.pp_term t)); - try auto_clusters flags signature cache + (lazy ("Case: " ^ CicNotationPp.pp_term t)); + try auto_clusters flags signature loop_cache depth' status; unsat with | Proved status -> @@ -1513,8 +1592,9 @@ auto_main flags signature cache depth status: unit = else let status = NTactics.merge_tac status in - (try auto_clusters flags signature cache - depth status; unsat + ( (* 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) @@ -1568,16 +1648,21 @@ let auto_tac ~params:(_univ,flags) status = let initial_time = Unix.gettimeofday() in app_counter:= 0; let rec up_to x y = - if x > y then raise (Error (lazy "auto gave up", None)) + if x > y then + (print(lazy + ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); + print(lazy + ("Applicative nodes:"^string_of_int !app_counter)); + raise (Error (lazy "auto gave up", None))) else 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;status with | Gaveup _ -> up_to (x+1) y | Proved s -> - HLog.debug ("proved at depth " ^ string_of_int x); + print (lazy ("proved at depth " ^ string_of_int x)); let stack = match s#stack with | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest @@ -1586,9 +1671,9 @@ let auto_tac ~params:(_univ,flags) status = s#set_stack stack in let s = up_to depth depth in - debug_print(lazy + print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); - debug_print(lazy + print(lazy ("Applicative nodes:"^string_of_int !app_counter)); s ;; -- 2.39.2