X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=67c7fb62d88ff289537c3653c64628953cdc3111;hb=706fcc9a5598a85d3d63ad0c9dd4245c8e0233f6;hp=73a96d23b50c76f7a4f65b51cd9a627b943af209;hpb=91332d82ed5c852a36eb2da15f977bb43aa78c72;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 73a96d23b..67c7fb62d 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -368,16 +368,12 @@ let init_cache_and_tables = let _, metasenv, subst, _, _, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let is_prop m s c t = - let ty,_ = - CicTypeChecker.type_of_aux' m ~subst:s c t CicUniv.oblivion_ugraph - in - let sort,_ = - CicTypeChecker.type_of_aux' m ~subst:s c ty CicUniv.oblivion_ugraph - in - match CicReduction.whd ~subst c sort with - | Cic.Sort Cic.Prop | Cic.Sort (Cic.CProp _) -> true - | _ -> false + let add_list_to_tables metasenv subst automation_cache ct = + List.fold_left + (fun automation_cache (t,_) -> + AutomationCache.add_term_to_active automation_cache + metasenv subst context t None) + automation_cache ct in if restricted_univ = [] then let ct = @@ -390,112 +386,47 @@ let init_cache_and_tables in let cache = AutoCache.cache_empty in let cache = cache_add_list cache context (ct@lt) in - let automation_cache, _ = - List.fold_left - (fun (c,maxmeta) (t,ty) -> - let head, metasenv, args, maxmeta = - TermUtil.saturate_term maxmeta metasenv context ty 0 - in - if List.exists (is_prop metasenv subst context) args then - c,maxmeta - else - let st = if args = [] then t else Cic.Appl (t::args) in - AutomationCache.add_term_to_active - c metasenv [] context st (Some head), maxmeta) - (automation_cache,CicMkImplicit.new_meta metasenv subst) ct + let automation_cache = + add_list_to_tables metasenv subst automation_cache ct in - (* AutomationCache.pp_cache automation_cache; *) +(* AutomationCache.pp_cache automation_cache; *) automation_cache.AutomationCache.univ, automation_cache.AutomationCache.tables, cache else - let metasenv, t_ty, s_t_ty, _ = - List.fold_left - (fun (metasenv as orig,acc, sacc, maxmeta) t -> - let ty, _ = - CicTypeChecker.type_of_aux' - metasenv ~subst:[] context t CicUniv.oblivion_ugraph - in - let head, metasenv, args, maxmeta = - TermUtil.saturate_term maxmeta metasenv context ty 0 - in - if List.exists (is_prop metasenv subst context) args then - orig, (t,ty)::acc, sacc, maxmeta - else - let st = if args = [] then t else Cic.Appl (t::args) in - metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta) - (metasenv, [],[], CicMkImplicit.new_meta metasenv subst) restricted_univ + let t_ty = + List.map + (fun t -> + let ty, _ = CicTypeChecker.type_of_aux' + metasenv ~subst:[] context t CicUniv.oblivion_ugraph + in + t, ty) + restricted_univ in - let automation_cache = AutomationCache.empty () in + (* let automation_cache = AutomationCache.empty () in *) let automation_cache = - let universe = automation_cache.AutomationCache.univ in + let universe = Universe.empty in let universe = Universe.index_list universe context t_ty in { automation_cache with AutomationCache.univ = universe } in + let ct = + if use_context then find_context_theorems context metasenv else t_ty + in let automation_cache = - List.fold_left - (fun c (t,ty) -> - AutomationCache.add_term_to_active c metasenv [] context t (Some ty)) - automation_cache s_t_ty + add_list_to_tables metasenv subst automation_cache ct in (* AutomationCache.pp_cache automation_cache; *) automation_cache.AutomationCache.univ, automation_cache.AutomationCache.tables, - cache_add_list cache_empty context t_ty + cache_empty ;; - (* -(* let signature = MetadataQuery.signature_of metasenv goal in *) -(* let newmeta = CicMkImplicit.new_meta metasenv [] in *) - let equations = - retrieve_equations dont_filter (* true *) signature universe cache context metasenv - in - debug_print - (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations)))); - let eqs_and_types = - HExtlib.filter_map - (fun t -> - let ty,_ = - CicTypeChecker.type_of_aux' - metasenv context t CicUniv.oblivion_ugraph - in - (* retrieve_equations could also return flexible terms *) - if is_an_equality ty then Some(t,ty) - else - try - let ty' = unfold context ty in - if is_an_equality ty' then Some(t,ty') else None - with ProofEngineTypes.Fail _ -> None) - equations - in - let bag = Equality.mk_equality_bag () in - let units, other_equalities, newmeta = - partition_unit_equalities context metasenv newmeta bag eqs_and_types - in - (* SIMPLIFICATION STEP - let equalities = - let env = (metasenv, context, CicUniv.oblivion_ugraph) in - let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in - Saturation.simplify_equalities bag eq_uri env units - in - *) - let passive = Saturation.make_passive units in - let no = List.length units in - let active = Saturation.make_active [] in - let active,passive,newmeta = - if paramod then active,passive,newmeta - else - Saturation.pump_actives - context bag newmeta active passive (no+1) infinity - in - (active,passive,bag),cache,newmeta -*) -let fill_hypothesis context metasenv term tables (universe:Universe.universe) cache auto fast = +let fill_hypothesis context metasenv subst term tables (universe:Universe.universe) cache auto fast = let actives, passives, bag = tables in let bag, head, metasenv, args = - Equality.saturate_term bag metasenv context term + Equality.saturate_term bag metasenv subst context term in let tables = actives, passives, bag in let propositional_args = @@ -557,14 +488,14 @@ let fill_hypothesis context metasenv term tables (universe:Universe.universe) ca results,cache,tables ;; -let build_equalities auto context metasenv tables universe cache equations = +let build_equalities auto context metasenv subst tables universe cache equations = List.fold_left (fun (tables,facts,cache) (t,ty) -> (* in any case we add the equation to the cache *) let cache = AutoCache.cache_add_list cache context [(t,ty)] in try let saturated, cache, tables = - fill_hypothesis context metasenv ty tables universe cache auto true + fill_hypothesis context metasenv subst ty tables universe cache auto true in let eqs, tables = List.fold_left @@ -585,10 +516,9 @@ let build_equalities auto context metasenv 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 _, metasenv,subst,_,_, _ = proof in let equations = retrieve_equations false signature universe cache context metasenv in @@ -602,7 +532,7 @@ let close_more tables context status auto universe cache = if is_an_equality ty then Some(t,ty) else None) equations in let tables, units, cache = - build_equalities auto context metasenv tables universe cache eqs_and_types + build_equalities auto context metasenv subst tables universe cache eqs_and_types in let active,passive,bag = tables in let passive = Saturation.add_to_passive units passive in @@ -618,7 +548,7 @@ let find_context_equalities dbd tables context proof (universe:Universe.universe let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in - let _,metasenv,_subst,_,_, _ = proof in + let _,metasenv,subst,_,_, _ = proof in (* if use_auto is true, we try to close the hypothesis of equational statements using auto; a naif, and probably wrong approach *) let rec aux tables cache index = function @@ -633,7 +563,7 @@ let find_context_equalities dbd tables context proof (universe:Universe.universe (try let term = S.lift index term in let saturated, cache, tables = - fill_hypothesis context metasenv term + fill_hypothesis context metasenv subst term tables universe cache default_auto false in let actives, passives, bag = tables in @@ -1104,8 +1034,8 @@ let apply_smart_aux automation_cache univ (proof'''',newmeta) in match - Saturation.given_clause bag (proof'''',newmeta) active passive - 1 0 infinity + Saturation.solve_narrowing bag (proof'''',newmeta) active passive + 1 (*0 infinity*) with | None, active, passive, bag -> raise (ProofEngineTypes.Fail (lazy ("paramod fails"))) @@ -1608,8 +1538,7 @@ let equational_case 1,0,flags.timeout in match - Saturation.given_clause bag status active passive - goal_steps saturation_steps timeout + Saturation.solve_narrowing bag status active passive goal_steps with | None, active, passive, bag -> [], (active,passive,bag), cache, flags @@ -1701,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 @@ -1760,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) -> @@ -1779,7 +1707,12 @@ let smart_applicative_case dbd let smart_candidates = List.filter (fun x -> not(List.mem x candidates)) smart_candidates - in + in + let debug_msg = + (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 @@ -1823,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 @@ -1846,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 @@ -1946,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; @@ -2058,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 *) @@ -2107,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 @@ -2114,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) -> @@ -2141,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))); @@ -2167,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)));