From b308b5b8aa223ef214e5eb3f6fad2647e6e23d4c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 13 May 2009 09:27:34 +0000 Subject: [PATCH] Signature is computed on the initial goal, once and for all. Ripristined the filtering on candidates also for non-smart applications (was too slow on some examples, e.g. in Fsub * --- helm/software/components/tactics/auto.ml | 54 +++++++++++++++--------- 1 file changed, 35 insertions(+), 19 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 81d5c6f4c..dda3ee933 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -516,10 +516,9 @@ let build_equalities auto context metasenv subst tables universe cache equations ) (tables,[],cache) equations -let close_more tables context status auto universe cache = +let close_more tables context status auto signature universe cache = let proof, goalno = status in let _, metasenv,subst,_,_, _ = proof in - let signature = MetadataQuery.signature_of metasenv goalno in let equations = retrieve_equations false signature universe cache context metasenv in @@ -1631,8 +1630,8 @@ let try_candidate dbd ;; let applicative_case dbd - tables depth subst fake_proof goalno goalty metasenv context universe - cache flags + tables depth subst fake_proof goalno goalty metasenv context + universe cache flags = let goalty_aux = match goalty with @@ -1690,10 +1689,9 @@ let try_smart_candidate dbd ;; let smart_applicative_case dbd - tables depth subst fake_proof goalno goalty metasenv context universe - cache flags + tables depth subst fake_proof goalno goalty metasenv context signature + universe cache flags = - let signature = MetadataQuery.signature_of metasenv goalno in let goalty_aux = match goalty with | Cic.Appl (hd::tl) -> @@ -1714,9 +1712,8 @@ let smart_applicative_case dbd (lazy ("smart_candidates" ^ " = " ^ (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in debug_print debug_msg; -(* we only filter the smart candidates since they could be too many +(* we only filter the smart candidates since they could be too many *) let candidates = List.filter (only signature context metasenv) candidates in -*) let smart_candidates = List.filter (only signature context metasenv) smart_candidates in @@ -1759,7 +1756,7 @@ let smart_applicative_case dbd ;; let equational_and_applicative_case dbd - universe flags m s g gty tables cache context + signature universe flags m s g gty tables cache context = let goalno, depth, sort = g in let fake_proof = mk_fake_proof m s g gty context in @@ -1782,7 +1779,7 @@ let equational_and_applicative_case dbd match LibraryObjects.eq_URI () with | Some _ -> smart_applicative_case dbd tables depth s fake_proof goalno - gty m context universe cache flags + gty m context signature universe cache flags | None -> applicative_case dbd tables depth s fake_proof goalno gty m context universe cache flags @@ -1882,7 +1879,8 @@ let filter_prune_hint c l = cache_reset_underinspection c, List.filter (condition_for_prune_hint prune) l ;; -let auto_main dbd tables context flags universe cache elems = + +let auto_main dbd tables context flags signature universe cache elems = auto_context := context; let rec aux tables flags cache (elems : status) = pp_status context elems; @@ -1994,7 +1992,7 @@ let auto_main dbd tables context flags universe cache elems = (* elems are possible computations for proving gty *) let elems, tables, cache, flags = equational_and_applicative_case dbd - universe flags m s g gty tables cache context + signature universe flags m s g gty tables cache context in if elems = [] then (* this goal has failed *) @@ -2043,6 +2041,14 @@ let auto_main dbd tables context flags universe cache elems = let auto_all_solutions dbd tables universe cache context metasenv gl flags = + let signature = + List.fold_left + (fun set g -> + MetadataConstraints.UriManagerSet.union set + (MetadataQuery.signature_of metasenv g) + ) + MetadataConstraints.UriManagerSet.empty gl + in let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map @@ -2050,7 +2056,7 @@ let in let elems = [metasenv,[],1,[],goals,[]] in let rec aux tables solutions cache elems flags = - match auto_main dbd tables context flags universe cache elems with + match auto_main dbd tables context flags signature universe cache elems with | Gaveup (tables,cache) -> solutions,cache, tables | Proved (metasenv,subst,others,tables,cache) -> @@ -2077,12 +2083,21 @@ let (******************* AUTO ***************) + let auto dbd flags metasenv tables universe cache context metasenv gl = - let initial_time = Unix.gettimeofday() in + let initial_time = Unix.gettimeofday() in + let signature = + List.fold_left + (fun set g -> + MetadataConstraints.UriManagerSet.union set + (MetadataQuery.signature_of metasenv g) + ) + MetadataConstraints.UriManagerSet.empty gl + in let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in let elems = [metasenv,[],1,[],goals,[]] in - match auto_main dbd tables context flags universe cache elems with + match auto_main dbd tables context flags signature universe cache elems with | Proved (metasenv,subst,_, tables,cache) -> debug_print(lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); @@ -2103,19 +2118,20 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa in let _,metasenv,subst,_,_, _ = proof in let _,context,goalty = CicUtil.lookup_meta goal metasenv in + let signature = MetadataQuery.signature_of metasenv goal in let tables,cache = if flags.close_more then close_more tables context (proof, goal) - (auto_all_solutions dbd) universe cache + (auto_all_solutions dbd) signature universe cache else tables,cache in let initial_time = Unix.gettimeofday() in let (_,oldmetasenv,_,_,_, _) = proof in - hint := None; + hint := None; let elem = metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[] in - match auto_main dbd tables context flags universe cache [elem] with + match auto_main dbd tables context flags signature universe cache [elem] with | Proved (metasenv,subst,_, tables,cache) -> debug_print (lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); -- 2.39.2