From dd103db6b51f6b3d763ff6e05892dbcfa85c0a9d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 12 Mar 2010 07:40:38 +0000 Subject: [PATCH] Subst was missing in perforate small (apparently, gty is not meta-closed). --- helm/software/components/ng_tactics/nnAuto.ml | 160 ++++++++++++------ 1 file changed, 110 insertions(+), 50 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index bee8b69cc..ede2e856a 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -11,13 +11,10 @@ open Printf -let debug = ref false let print ?(depth=0) s = prerr_endline (String.make depth '\t'^Lazy.force s) -let debug_print ?(depth=0) s = - if !debug then print ~depth s else () - -let debug_do f = if !debug then f () else () +let noprint ?(depth=0) _ = () +let debug_print = noprint open Continuationals.Stack open NTacStatus @@ -54,9 +51,9 @@ 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 branch status ty = let status, ty, metas = saturate ~delta:0 status ty in - debug_print (lazy ("saturated ty :" ^ (ppterm status ty))); + noprint (lazy ("saturated ty :" ^ (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 *) @@ -68,7 +65,11 @@ let is_a_fact status ty = | NCic.Meta(i,_) -> IntSet.add i acc | _ -> assert false) IntSet.empty metas - in IntSet.subset menv clos;; + in + (* IntSet.subset menv clos *) + IntSet.cardinal(IntSet.diff menv clos) + +let is_a_fact status ty = branch status ty = 0 let is_a_fact_obj s uri = let obj = NCicEnvironment.get_checked_obj uri in @@ -655,7 +656,8 @@ let init_cache ?(facts=[]) ?(under_inspection=[],[]) unit_eq = unit_eq } -let only signature _context candidate = +let only signature _context candidate = true +(* (* TASSI: nel trie ci mettiamo solo il body, non il ty *) let candidate_ty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate @@ -669,17 +671,36 @@ let only signature _context candidate = debug_print (lazy ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[] ~metasenv:[] candidate ^ ": " ^ string_of_int height)); - rc + rc *) ;; let candidate_no = ref 0;; 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,t = term_of_cic_term status ct ctx in + let ty = NCicTypeChecker.typeof subst metasenv ctx t in + let res = branch status (mk_cic_term ctx ty) in + debug_print (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = " + ^ (string_of_int res))); + res + in + let candidates = List.map (fun t -> branch t,t) candidates in + let candidates = + List.sort (fun (a,_) (b,_) -> a - b) candidates in + let candidates = List.map snd candidates in + debug_print (lazy ("candidates =\n" ^ (String.concat "\n" + (List.map CicNotationPp.pp_term candidates)))); + candidates + let sort_new_elems l = List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l -let try_candidate ?(smart=0) flags depth status eq_cache t = +let try_candidate ?(smart=0) flags depth status eq_cache ctx t = try debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t)); let status = @@ -687,31 +708,44 @@ let try_candidate ?(smart=0) flags depth status eq_cache t = 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 + with Error _ as exc -> + smart_apply_auto ("",0,t) eq_cache status + in +(* let og_no = openg_no status in if (* og_no > flags.maxwidth || *) ((depth + 1) = flags.maxdepth && og_no <> 0) then (debug_print ~depth (lazy "pruned immediately"); None) - else - (incr candidate_no; - Some ((!candidate_no,t),status)) + else *) + (* useless + let status, cict = disambiguate status ctx ("",0,t) None in + let status,ct = term_of_cic_term status cict ctx in + let _,_,metasenv,subst,_ = status#obj in + let ty = NCicTypeChecker.typeof subst metasenv ctx ct in + let res = branch status (mk_cic_term ctx ty) in + if smart=1 && og_no > res then + (print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " + ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no))); + print ~depth (lazy "strange application"); None) + else *) + (incr candidate_no; + Some ((!candidate_no,t),status)) with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None ;; -let sort_of metasenv ctx t = - let ty = NCicTypeChecker.typeof [] metasenv ctx t in - NCicTypeChecker.typeof [] metasenv ctx ty +let sort_of subst metasenv ctx t = + let ty = NCicTypeChecker.typeof subst metasenv ctx t in + NCicTypeChecker.typeof subst metasenv ctx ty ;; let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ") ;; -let perforate_small metasenv context t = +let perforate_small subst metasenv context t = let rec aux = function | NCic.Appl (hd::tl) -> let map t = - let s = sort_of metasenv context t in + let s = sort_of subst metasenv context t in match s with | NCic.Sort(NCic.Type [`Type,u]) when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0)) @@ -733,23 +767,25 @@ let get_candidates ?(smart=true) status cache signature gty = 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 raw_gty = NCicUntrusted.apply_subst subst context raw_gty in *) let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables - universe raw_gty in + universe raw_gty in let local_cands = search_in_th gty cache in debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty)); debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands))))); - let together global local = + 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 candidates = together cands local_cands in + let candidates = sort_candidates status context candidates in let smart_candidates = if smart then match raw_gty with - | NCic.Appl _ -> - let weak_gty = perforate_small metasenv context raw_gty in + | NCic.Appl _ + | NCic.Const _ + | NCic.Rel _ -> + let weak_gty = perforate_small subst metasenv context raw_gty in (* NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0))) (List.length tl)) in *) @@ -762,11 +798,15 @@ let get_candidates ?(smart=true) status cache signature gty = 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 + together smart_cands smart_local_cands + (* together more_cands more_local_cands *) | _ -> [] else [] in - candidates, smart_candidates + let smart_candidates = sort_candidates status context smart_candidates in + (* if smart then smart_candidates, [] + else candidates, [] *) + candidates, smart_candidates ;; let applicative_case depth signature status flags gty (cache:cache) = @@ -807,7 +847,7 @@ let applicative_case depth signature status flags gty (cache:cache) = then (debug_print (lazy "pruned: not a fact"); elems) else match try_candidate (~smart:sm) - flags depth status cache.unit_eq cand with + flags depth status cache.unit_eq context cand with | None -> elems | Some x -> x::elems) [] candidates @@ -824,7 +864,7 @@ let applicative_case depth signature status flags gty (cache:cache) = then (debug_print (lazy "pruned: not a fact"); elems) else match try_candidate (~smart:1) - flags depth status cache.unit_eq cand with + flags depth status cache.unit_eq context cand with | None -> elems | Some x -> x::elems) [] smart_candidates @@ -963,7 +1003,8 @@ let do_something signature flags status g depth gty cache = (* states in l1 have have an empty set of subgoals: no point to sort them *) debug_print ~depth (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2))))); - l1 @ (sort_new_elems (l @ l2)), cache + (* l1 @ (sort_new_elems (l @ l2)), cache *) + l1 @ (List.rev l2) @ l, cache ;; let pp_goal = function @@ -1067,21 +1108,33 @@ let deep_focus_tac level focus status = status#set_stack gstatus ;; -let open_goals level status = - let rec aux level gs = - if level = 0 then [] - else match gs with - | [] -> assert false - | (g, _, _, _) :: s -> - let is_open = function - | (_,Continuationals.Stack.Open i) -> Some i - | (_,Continuationals.Stack.Closed _) -> None - in - HExtlib.filter_map is_open g @ aux (level-1) s - in - aux level status#stack +let rec stack_goals level gs = + if level = 0 then [] + else match gs with + | [] -> assert false + | (g,_,_,_)::s -> + let is_open = function + | (_,Continuationals.Stack.Open i) -> Some i + | (_,Continuationals.Stack.Closed _) -> None + in + HExtlib.filter_map is_open g @ stack_goals (level-1) s +;; + +let open_goals level status = stack_goals level status#stack ;; +let move_to_side level status = +match status#stack with + | [] -> assert false + | (g,_,_,_)::tl -> + let is_open = function + | (_,Continuationals.Stack.Open i) -> Some i + | (_,Continuationals.Stack.Closed _) -> None + in + let others = menv_closure status (stack_goals (level-1) tl) in + List.for_all (fun i -> IntSet.mem i others) + (HExtlib.filter_map is_open g) + let rec auto_clusters ?(top=false) flags signature cache depth status : unit = debug_print ~depth (lazy ("entering auto clusters at depth " ^ @@ -1104,7 +1157,7 @@ let rec auto_clusters ?(top=false) List.iter (fun gl -> if List.length gl > flags.maxwidth then - (debug_print (lazy "FAIL GLOBAL WIDTH"); + (debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); raise (Gaveup IntSet.empty)) else ()) classes; if List.length classes = 1 then @@ -1170,13 +1223,20 @@ auto_main flags signature (cache:cache) depth status: unit = | a::tl -> let tree = rm_from_th a tree a in {cache with under_inspection = tl,tree} in - auto_clusters flags signature (cache:cache) (depth-1) status + auto_clusters flags signature cache (depth-1) status | orig::_ -> + if depth > 0 && move_to_side depth status + then + let _ = print (lazy "merged") in + let status = NTactics.merge_tac status in + auto_clusters flags signature cache (depth-1) status + else let ng = List.length goals in (* moved inside auto_clusters *) if ng > flags.maxwidth then - (debug_print (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty)) - else if depth = flags.maxdepth then raise (Gaveup IntSet.empty) + (print ~depth (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty)) + else if depth = flags.maxdepth then + raise (Gaveup IntSet.empty) else let status = NTactics.branch_tac ~force:true status in let status, cache = intros ~depth status cache in @@ -1214,7 +1274,7 @@ auto_main flags signature (cache:cache) depth status: unit = with Gaveup _ -> debug_print ~depth (lazy "Failed");()) alternatives; - raise (Gaveup IntSet.empty) + raise (debug_print(lazy "no more candidates"); Gaveup IntSet.empty) ;; let int name l def = -- 2.39.2