X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=a89bbd4a164b9e1c673b9ea9a7a0e2620788904d;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=15b2d848bf7cab4facc1ace9784900fa2100f8ac;hpb=af8005720dd5a6e90f052202a7c5f108f54e652b;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 15b2d848b..a89bbd4a1 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -38,12 +38,14 @@ let ppterm ctx t = let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in CicPp.pp t names ;; + let is_propositional context sort = match CicReduction.whd context sort with | Cic.Sort Cic.Prop | Cic.Sort (Cic.CProp _) -> true | _-> false ;; + let is_in_prop context subst metasenv ty = let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in is_propositional context sort @@ -139,7 +141,7 @@ let is_an_equational_goal = function | _ -> false ;; -type auto_params = Cic.term list * (string * string) list +type auto_params = Cic.term list option * (string * string) list let elems = ref [] ;; @@ -368,145 +370,66 @@ 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 - in let add_list_to_tables metasenv subst automation_cache ct = - let _,_,bag = automation_cache.AutomationCache.tables in - let maxmeta = Equality.maxmeta bag in - 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,maxmeta) 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 = - if use_context then find_context_theorems context metasenv else [] - in - let lt = - match use_library, dbd with - | true, Some dbd -> find_library_theorems dbd metasenv goal - | _ -> [] - in - let cache = AutoCache.cache_empty in - let cache = cache_add_list cache context (ct@lt) in - let automation_cache, _ = add_list_to_tables metasenv subst automation_cache ct - in - (* 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 - in - (* let automation_cache = AutomationCache.empty () in *) - let automation_cache = - 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 [] - in - let automation_cache, _ = add_list_to_tables metasenv subst automation_cache ct - in - (* proviamo a tenere tutte le equazioni - 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 - in *) + match restricted_univ with + | None -> + let ct = + if use_context then find_context_theorems context metasenv else [] + in + let lt = + match use_library, dbd with + | true, Some dbd -> find_library_theorems dbd metasenv goal + | _ -> [] + in + let cache = AutoCache.cache_empty in + let cache = cache_add_list cache context (ct@lt) in + let automation_cache = + add_list_to_tables metasenv subst automation_cache ct + in +(* AutomationCache.pp_cache automation_cache; *) + automation_cache.AutomationCache.univ, + automation_cache.AutomationCache.tables, + cache + | Some 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 = + 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 = + 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 -*) + automation_cache.AutomationCache.univ, + automation_cache.AutomationCache.tables, + cache_empty +;; -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 = @@ -568,14 +491,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 @@ -596,10 +519,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 @@ -613,7 +535,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 @@ -629,7 +551,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 @@ -644,7 +566,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 @@ -1035,7 +957,7 @@ let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache = (***************** applyS *******************) let apply_smart_aux - dbd automation_cache params proof goal newmeta' metasenv' subst + dbd automation_cache (params:auto_params) proof goal newmeta' metasenv' subst context term' ty termty goal_arity = let consthead,newmetasenv,arguments,_ = @@ -1115,8 +1037,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 + 2 (*0 infinity*) with | None, active, passive, bag -> raise (ProofEngineTypes.Fail (lazy ("paramod fails"))) @@ -1619,8 +1541,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 @@ -1712,18 +1633,27 @@ 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 + signature universe cache flags = - let goalty_aux = + (* let goalty_aux = match goalty with | Cic.Appl (hd::tl) -> Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl)) | _ -> goalty - in + in *) + let goalty_aux = goalty in let candidates = get_candidates flags.skip_trie_filtering universe cache goalty_aux in + (* if the goal is an equality we skip the congruence theorems + let candidates = + if is_equational_case goalty flags + then List.filter not_default_eq_term candidates + else candidates + in *) + let candidates = List.filter (only signature context metasenv) candidates + in let tables, elems = List.fold_left (fun (tables,elems) cand -> @@ -1744,7 +1674,7 @@ let try_smart_candidate dbd = let ppterm = ppterm context in try - let params = ([],[]) in + let params = (None,[]) in let automation_cache = { AutomationCache.tables = tables ; AutomationCache.univ = Universe.empty; } @@ -1771,10 +1701,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) -> @@ -1838,7 +1767,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 @@ -1853,7 +1782,7 @@ let equational_and_applicative_case dbd else applicative_case dbd tables depth s fake_proof goalno - gty m context universe cache flags + gty m context signature universe cache flags in elems@more_elems, tables, cache, flags else @@ -1861,10 +1790,10 @@ 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 + gty m context signature universe cache flags in elems, tables, cache, flags ;; @@ -1961,7 +1890,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; @@ -2073,7 +2003,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 *) @@ -2122,6 +2052,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 @@ -2129,7 +2067,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) -> @@ -2156,12 +2094,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))); @@ -2182,19 +2129,35 @@ 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 = + match univ with + | None -> signature + | Some l -> + 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 l + 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)));