X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=67c7fb62d88ff289537c3653c64628953cdc3111;hb=c78edd42f3ebc7c82bb319b876908bf17288ab04;hp=53120a44d80940decbd54ad7d6b5932f6f7bd8cc;hpb=25564c06c570e5ab9be455904c0b381842f8d4c4;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 53120a44d..67c7fb62d 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,6 +1712,7 @@ 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 *) let candidates = List.filter (only signature context metasenv) candidates in let smart_candidates = List.filter (only signature context metasenv) smart_candidates @@ -1757,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 @@ -1780,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 @@ -1880,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; @@ -1992,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 *) @@ -2041,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 @@ -2048,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) -> @@ -2075,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))); @@ -2101,19 +2118,32 @@ 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 signature = + List.fold_left + (fun set t -> + let ty, _ = + CicTypeChecker.type_of_aux' metasenv context t + CicUniv.oblivion_ugraph + in + MetadataConstraints.UriManagerSet.union set + (MetadataConstraints.constants_of ty) + ) + signature univ + 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)));