X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=a7af3bbe5be2703e3831a2085eb2b09bddd755fd;hb=7b29f50ea116524e4bc91b762b81fd5ae927c4ea;hp=d24c244a75f4f24e26530dd5319229affd2fa0be;hpb=2b80cfd9b2f739a28ea9938c4b1fbb7629839d32;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index d24c244a7..a7af3bbe5 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -66,11 +66,11 @@ let naif_closure ?(prefix_name="xxx_") t metasenv context = let lambda_close ?prefix_name t menv ctx = let t = naif_closure ?prefix_name t menv ctx in List.fold_left - (fun t -> function - | None -> CicSubstitution.subst (Cic.Implicit None) t (* delift *) - | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t) - | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t)) - t ctx + (fun (t,i) -> function + | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *) + | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1 + | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t),i+1) + (t,List.length menv) ctx ;; (* functions for retrieving theorems *) @@ -147,7 +147,9 @@ let is_unit_equation context metasenv oldnewmeta term = args in if propositional_args = [] then - let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in + let newmetas = + List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv + in Some (args,metasenv,newmetas,head,newmeta) else None ;; @@ -163,19 +165,21 @@ let get_candidates universe cache t = candidates ;; -let only signature context t = +let only signature context metasenv t = try - let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph + in let consts = MetadataConstraints.constants_of ty in let b = MetadataConstraints.UriManagerSet.subset consts signature in if b then b else - try - let ty' = unfold context ty in - let consts' = MetadataConstraints.constants_of ty' in - MetadataConstraints.UriManagerSet.subset consts' signature - with _-> false - with _ -> false + let ty' = unfold context ty in + let consts' = MetadataConstraints.constants_of ty' in + MetadataConstraints.UriManagerSet.subset consts' signature + with + | CicTypeChecker.TypeCheckerFailure _ -> assert false + | ProofEngineTypes.Fail _ -> false (* unfold may fail *) ;; let not_default_eq_term t = @@ -184,7 +188,7 @@ let not_default_eq_term t = not (LibraryObjects.in_eq_URIs uri) with Invalid_argument _ -> true -let retrieve_equations signature universe cache context= +let retrieve_equations dont_filter signature universe cache context metasenv = match LibraryObjects.eq_URI() with | None -> [] | Some eq_uri -> @@ -192,11 +196,10 @@ let retrieve_equations signature universe cache context= let fake= Cic.Meta(-1,[]) in let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in let candidates = get_candidates universe cache fake_eq in - (* defaults eq uris are built-in in auto *) - let candidates = List.filter not_default_eq_term candidates in - let candidates = List.filter (only signature context) candidates in - List.iter (fun t -> debug_print (lazy (CicPp.ppterm t))) candidates; - candidates + if dont_filter then candidates + else + let candidates = List.filter not_default_eq_term candidates in + List.filter (only signature context metasenv) candidates let build_equality bag head args proof newmetas maxmeta = match head with @@ -218,6 +221,14 @@ let build_equality bag head args proof newmetas maxmeta = let partition_unit_equalities context metasenv newmeta bag equations = List.fold_left (fun (units,other,maxmeta)(t,ty) -> + if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then + let _ = + HLog.warn + ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context + ^ " since it is not meta closed") + in + units,(t,ty)::other,maxmeta + else match is_unit_equation context metasenv maxmeta ty with | Some (args,metasenv,newmetas,head,newmeta') -> let maxmeta,equality = @@ -232,50 +243,58 @@ let empty_tables = Saturation.make_passive [], Equality.mk_equality_bag) -let init_cache_and_tables dbd use_library paramod universe (proof, goal) = +let init_cache_and_tables + ?dbd use_library paramod use_context dont_filter universe (proof, goal) += (* the local cache in initially empty *) let cache = AutoCache.cache_empty in let _, metasenv, _subst,_, _, _ = proof in let signature = MetadataQuery.signature_of metasenv goal in let newmeta = CicMkImplicit.new_meta metasenv [] in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let ct = find_context_theorems context metasenv in + let ct = if use_context then find_context_theorems context metasenv else [] in debug_print (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct)))); let lt = - if use_library then - find_library_theorems dbd metasenv goal - else [] in + match use_library, dbd with + | true, Some dbd -> find_library_theorems dbd metasenv goal + | _ -> [] + in debug_print (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt)))); let cache = cache_add_list cache context (ct@lt) in let equations = - retrieve_equations signature universe cache context in + retrieve_equations dont_filter 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.empty_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 _ -> None) (* catturare l'eccezione giusta di unfold *) - equations in + CicTypeChecker.type_of_aux' + metasenv context t CicUniv.empty_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 _ -> None) (* catturare l'eccezione giusta di unfold *) + 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 - (* let env = (metasenv, context, CicUniv.empty_ugraph) in - let equalities = - let eq_uri = - match LibraryObjects.eq_URI() with - | None ->assert false - | Some eq_uri -> eq_uri in - Saturation.simplify_equalities bag eq_uri env units in *) + partition_unit_equalities context metasenv newmeta bag eqs_and_types + in + (* SIMPLIFICATION STEP + let equalities = + let env = (metasenv, context, CicUniv.empty_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 @@ -380,7 +399,9 @@ let close_more tables maxmeta context status auto universe cache = let proof, goalno = status in let _, metasenv,_subst,_,_, _ = proof in let signature = MetadataQuery.signature_of metasenv goalno in - let equations = retrieve_equations signature universe cache context in + let equations = + retrieve_equations false signature universe cache context metasenv + in let eqs_and_types = HExtlib.filter_map (fun t -> @@ -509,7 +530,7 @@ let new_metasenv_and_unify_and_t in match let (active, passive,bag), cache, maxmeta = - init_cache_and_tables dbd flags.use_library true universe + init_cache_and_tables ~dbd flags.use_library true true false universe (proof'''',newmeta) in Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive @@ -831,9 +852,13 @@ let pause b = in_pause := b;; let cond = Condition.create ();; let mutex = Mutex.create ();; let hint = ref None;; +let prune_hint = ref [];; let step _ = Condition.signal cond;; let give_hint n = hint := Some n;; +let give_prune_hint hint = + prune_hint := hint :: !prune_hint +;; let check_pause _ = if !in_pause then @@ -1081,7 +1106,7 @@ let equational_case assert (maxmeta >= maxm); let res' = List.map - (fun subst',(_,metasenv,_subst,proof,_, _),open_goals -> + (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) -> assert_subst_are_disjoint subst subst'; let subst = subst@subst' in let open_goals = @@ -1119,8 +1144,8 @@ let try_candidate ;; let sort_new_elems = - List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2) -(* List.sort (fun (_,_,_,l2) (_,_,_,l1) -> List.length l1 - List.length l2) *) + List.sort (fun (_,_,_,l1) (_,_,_,l2) -> + List.length (prop_only l1) - List.length (prop_only l2)) ;; let applicative_case @@ -1240,7 +1265,18 @@ let prunable menv subst ty todo = aux todo ;; - +let condition_for_prune_hint prune (m, s, size, don, todo, fl) = + let s = + HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo + in + List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s +;; +let filter_prune_hint l = + let prune = !prune_hint in + prune_hint := []; (* possible race... *) + if prune = [] then l + else List.filter (condition_for_prune_hint prune) l +;; let auto_main tables maxm context flags universe cache elems = auto_context := context; let rec aux tables maxm flags cache (elems : status) = @@ -1249,8 +1285,9 @@ let auto_main tables maxm context flags universe cache elems = auto_status := elems; check_pause (); *) + let elems = filter_prune_hint elems in match elems with - | (m, s, size, don, todo, fl)::orlist as status when !hint <> None -> + | (m, s, size, don, todo, fl)::orlist when !hint <> None -> (match !hint with | Some i when condition_for_hint i todo -> aux tables maxm flags cache orlist @@ -1663,8 +1700,8 @@ let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) = (* just for testing *) let use_library = flags.use_library in let tables,cache,newmeta = - init_cache_and_tables dbd use_library flags.use_only_paramod - universe (proof, goal) in + init_cache_and_tables ~dbd use_library flags.use_only_paramod true + false universe (proof, goal) in let tables,cache,newmeta = if flags.close_more then close_more @@ -1706,15 +1743,57 @@ let eq_of_goal = function | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) ;; +(* performs steps of rewrite with the universe, obtaining if possible + * a trivial goal *) +let solve_rewrite_tac ~universe ?(steps=1) (proof,goal as status)= + let _,metasenv,_subst,_,_,_ = proof in + let _,context,ty = CicUtil.lookup_meta goal metasenv in + let eq_uri = eq_of_goal ty in + let (active,passive,bag), cache, maxm = + (* we take the whole universe (no signature filtering) *) + init_cache_and_tables false true false true universe (proof,goal) + in + let initgoal = [], metasenv, ty in + let table = + let equalities = (Saturation.list_of_passive passive) in + (* we demodulate using both actives passives *) + List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities + in + let env = metasenv,context,CicUniv.empty_ugraph in + match Indexing.solve_demodulating bag env table initgoal steps with + | Some (proof, metasenv, newty) -> + let refl = + match newty with + | Cic.Appl[Cic.MutInd _;eq_ty;left;_] -> + Equality.Exact (Equality.refl_proof eq_uri eq_ty left) + | _ -> assert false + in + let proofterm,_ = + Equality.build_goal_proof + bag eq_uri proof refl newty [] context metasenv + in + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) status + | None -> + raise + (ProofEngineTypes.Fail (lazy + ("Unable to solve with " ^ string_of_int steps ^ " demodulations"))) +;; +let solve_rewrite_tac ~universe ?steps () = + ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ?steps) +;; + (* DEMODULATE *) let demodulate_tac ~dbd ~universe (proof,goal)= let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let initgoal = [], [], ty in + let initgoal = [], metasenv, ty in let eq_uri = eq_of_goal ty in let (active,passive,bag), cache, maxm = - init_cache_and_tables dbd false true universe (proof,goal) in + init_cache_and_tables + ~dbd false true true false universe (proof,goal) + in let equalities = (Saturation.list_of_passive passive) in (* we demodulate using both actives passives *) let table = @@ -1755,3 +1834,4 @@ let demodulate_tac ~dbd ~universe = let pp_proofterm = Equality.pp_proofterm;; let revision = "$Revision$";; +let size_and_depth context metasenv t = 100, 100