X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fauto.ml;h=2db8cc0014ec1d468b60df2872caff898fba9c57;hb=1b1a0b78ea59c7f0fe2bf7ffda4a5cda260add35;hp=e377b63683049ae55d0fd30ea6a355d90fe0a01c;hpb=61acdea2419b3889096fd1e41275062b78253af0;p=helm.git diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index e377b6368..2db8cc001 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -24,8 +24,164 @@ *) open AutoTypes;; +open AutoCache;; -let debug_print s = ();;(*prerr_endline s;;*) +let debug_print s = () (* prerr_endline s;; *) + +(* {{{ *********** local given_clause wrapper ***********) + +let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status = + let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout = + match tables with + | None -> + (* first time, do a huge saturation *) + let bag, equalities, cache, maxmeta = + Saturation.find_equalities dbd status ?auto smart_flag cache + in + let passive = Saturation.make_passive equalities in + let active = Saturation.make_active [] in + let goal_steps, saturation_steps, timeout = + if flags.use_only_paramod then max_int,max_int,flags.timeout + else 82, 82, infinity + in + let maxm = max maxm maxmeta in + active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout + | Some (active,passive,bag,oldcache) -> + (* saturate a bit more if cache cahnged *) + let bag, equalities, cache, maxm = + if cache_size oldcache <> cache_size cache then + Saturation.saturate_more + bag active maxm status smart_flag ?auto cache + else + bag, [], cache, maxm + in + let minsteps = List.length equalities in + let passive = Saturation.add_to_passive equalities passive in + let goal_steps, saturation_steps, timeout = + if flags.use_only_paramod then max_int,max_int,flags.timeout + else max 80 minsteps, minsteps, infinity + in + active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout + in + let res,actives,passives,maxmeta = + Saturation.given_clause bag maxmeta status active passive + goal_steps saturation_steps timeout + in + res,actives,passives,bag,cache,maxmeta +;; + +(* }}} ****************************************************************) + +(* {{{ **************** applyS *******************) + +let new_metasenv_and_unify_and_t + dbd proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity += + let (consthead,newmetasenv,arguments,_) = + ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in + let term'' = + match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) + in + let proof',oldmetasenv = + let (puri,metasenv,pbo,pty) = proof in + (puri,newmetasenv,pbo,pty),metasenv + in + let goal_for_paramod = + match LibraryObjects.eq_URI () with + | Some uri -> + Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty] + | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined")) + in + let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in + let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in + let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + let proof''',goals = + ProofEngineTypes.apply_tactic + (EqualityTactics.rewrite_tac ~direction:`RightToLeft + ~pattern:(ProofEngineTypes.conclusion_pattern None) + (Cic.Meta(newmeta,irl))) + (proof'',goal) + in + let goal = match goals with [g] -> g | _ -> assert false in + let subst, (proof'''', _), _ = + PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal) + in + match + let cache, flags = cache_empty, default_flags() in + let flags = + {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} + in + given_clause dbd ?tables 0 cache [] flags true (proof'''',newmeta) + with + | None, active, passive, bag,_,_ -> + raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) + | Some (_,proof''''',_), active, passive,bag,_,_ -> + subst,proof''''', + ProofEngineHelpers.compare_metasenvs ~oldmetasenv + ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive +;; + +let rec count_prods context ty = + match CicReduction.whd context ty with + Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t + | _ -> 0 + +let apply_smart ~dbd ~term ~subst ?tables (proof, goal) = + let module T = CicTypeChecker in + let module R = CicReduction in + let module C = Cic in + let (_,metasenv,_,_) = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let newmeta = CicMkImplicit.new_meta metasenv subst in + let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = + match term with + C.Var (uri,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.Var (uri,exp_named_subst') + | C.Const (uri,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.MutInd (uri,tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.MutConstruct (uri,tyno,consno,exp_named_subst') + | _ -> [],newmeta,[],term + in + let metasenv' = metasenv@newmetasenvfragment in + let termty,_ = + CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph + in + let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in + let goal_arity = count_prods context ty in + let subst, proof, gl, active, passive = + new_metasenv_and_unify_and_t dbd proof goal ?tables + newmeta' metasenv' context term' ty termty goal_arity + in + subst, proof, gl, active, passive +;; + +(* }}} **************** applyS **************) + +(* {{{ ***************** AUTO ********************) let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;; let ugraph = CicUniv.empty_ugraph;; @@ -43,9 +199,13 @@ let assert_proof_is_valid proof metasenv context goalty = let b,_ = CicReduction.are_convertible context ty goalty u in if not b then begin - prerr_endline (CicPp.ppterm proof); - prerr_endline (CicPp.ppterm ty); - prerr_endline (CicPp.ppterm goalty); + let names = + List.map (function None -> None | Some (x,_) -> Some x) context + in + prerr_endline ("PROOF:" ^ CicPp.pp proof names); + prerr_endline ("PROOFTY:" ^ CicPp.pp ty names); + prerr_endline ("GOAL:" ^ CicPp.pp goalty names); + prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv); end; assert b ;; @@ -103,21 +263,73 @@ let order_new_goals metasenv subst open_goals ppterm = open_goals ;; -let try_candidate subst fake_proof goalno depth context cand = +let is_an_equational_goal = function + | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true + | _ -> false +;; + +let equational_case + dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context + flags += + let ppterm = ppterm context in + prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty ); + prerr_endline ""; + prerr_endline (cache_print context cache); + prerr_endline ""; + match + given_clause dbd ?tables maxm ?auto cache subst flags false (fake_proof,goalno) + with + | None, active,passive, bag, cache, maxmeta -> + let tables = Some (active,passive,bag,cache) in + None, tables, cache, maxmeta + | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,bag,cache,maxmeta -> + let tables = Some (active,passive,bag,cache) in + assert_subst_are_disjoint subst subst'; + let subst = subst@subst' in + let open_goals = order_new_goals metasenv subst open_goals ppterm in + let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in + Some [metasenv,subst,open_goals], tables, cache, maxmeta +;; + +let try_candidate + goalty dbd tables maxm subst fake_proof goalno depth context cand += let ppterm = ppterm context in try - debug_print (" PROVO: " ^ ppterm cand); - let subst', ((_,metasenv,_,_), open_goals) = - PrimitiveTactics.apply_with_subst ~term:cand ~subst (fake_proof,goalno) + let subst', ((_,metasenv,_,_), open_goals), maxmeta = + PrimitiveTactics.apply_with_subst + ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno) in debug_print (" OK: " ^ ppterm cand); + assert (maxmeta >= maxm); (*FIXME:sicuro che posso @?*) assert_subst_are_disjoint subst subst'; let subst = subst@subst' in let open_goals = order_new_goals metasenv subst open_goals ppterm in let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in - Some (metasenv,subst,open_goals) - with ProofEngineTypes.Fail s -> (*debug_print(" KO: "^Lazy.force s);*)None + Some (metasenv,subst,open_goals), tables , maxmeta + with ProofEngineTypes.Fail s -> + (*debug_print(" KO: "^Lazy.force s);*)None,tables, maxm +;; + +let applicative_case + dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache += + let candidates = get_candidates cache goalty in + let tables, elems, maxm = + List.fold_left + (fun (tables,elems,maxm) cand -> + match + try_candidate goalty + dbd tables maxm subst fake_proof goalno depth context cand + with + | None, tables,maxm -> tables,elems, maxm + | Some x, tables, maxm -> tables,x::elems, maxm) + (tables,[],maxm) candidates + in + let elems = sort_new_elems elems in + elems, tables, cache, maxm ;; (* Works if there is no dependency over proofs *) @@ -125,40 +337,86 @@ let is_a_green_cut goalty = CicUtil.is_meta_closed goalty ;; let prop = function (_,_,P) -> true | _ -> false;; - -let auto_main context flags elems cache universe = - let timeout = +let calculate_timeout flags = if flags.timeout = 0. then - infinity + (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity}) else - Unix.gettimeofday () +. flags.timeout + flags +;; +let is_equational_case goalty flags = + let ensure_equational t = + if is_an_equational_goal t then true + else false + (* + let msg="Not an equational goal.\nYou cant use the paramodulation flag"in + raise (ProofEngineTypes.Fail (lazy msg)) + *) in + (flags.use_paramod && is_an_equational_goal goalty) || + (flags.use_only_paramod && ensure_equational goalty) +;; +let cache_add_success sort cache k v = + if sort = P then cache_add_success cache k v else cache +;; + +let rec auto_main dbd tables maxm context flags elems cache = + let callback_for_paramod maxm flags proof commonctx cache l = + let flags = {flags with use_paramod = false;dont_cache_failures=true} in + let _,metasenv,_,_ = proof in + let oldmetasenv = metasenv in + match + auto_all_solutions + dbd tables maxm cache commonctx metasenv l flags + with + | [],cache,maxm -> [],cache,maxm + | solutions,cache,maxm -> + let solutions = + HExtlib.filter_map + (fun (subst,newmetasenv) -> + let opened = + ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv + in + if opened = [] then Some subst else None) + solutions + in + solutions,cache,maxm + in + let flags = calculate_timeout flags in let ppterm = ppterm context in let irl = mk_irl context in - let rec aux cache = function (* elems in OR *) - | [] -> Fail "no more steps can be done", cache (* COMPLETE FAILURE *) + let rec aux tables maxm cache = function (* elems in OR *) + | [] -> Fail "no more steps can be done", tables, cache, maxm + (*COMPLETE FAILURE*) | (metasenv,subst,[])::tl -> - Success (metasenv,subst,tl), cache (* solution::cont *) + Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *) | (metasenv,subst,goals)::tl when List.length (List.filter prop goals) > flags.maxwidth -> debug_print (" FAILURE(width): " ^ string_of_int (List.length goals)); - aux cache tl (* FAILURE (width) *) + aux tables maxm cache tl (* FAILURE (width) *) | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl -> - if Unix.gettimeofday() > timeout then Fail "timeout",cache + if Unix.gettimeofday() > flags.timeout then + Fail "timeout",tables,cache,maxm else try let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty); - if sort = T then + if sort = T && tl <> [] then (* FIXME!!!! *) (debug_print (" FAILURE(not in prop)"); - aux cache tl (* FAILURE (not in prop) *)) + aux tables maxm cache tl (* FAILURE (not in prop) *)) else - match aux_single cache metasenv subst elem goalty cc with - | Fail _, cache -> - debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty); - let cache = cache_add_failure cache goalty depth in - aux cache tl - | Success (metasenv,subst,others), cache -> + match aux_single tables maxm cache metasenv subst elem goalty cc with + | Fail s, tables, cache, maxm' -> + assert(maxm' >= maxm);let maxm = maxm' in + debug_print + (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty); + let cache = + if flags.dont_cache_failures then + cache_remove_underinspection cache goalty + else cache_add_failure cache goalty depth + in + aux tables maxm cache tl + | Success (metasenv,subst,others), tables, cache, maxm' -> + assert(maxm' >= maxm);let maxm = maxm' in (* others are alternatives in OR *) try let goal = Cic.Meta(goalno,irl) in @@ -166,14 +424,14 @@ let auto_main context flags elems cache universe = debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof); if is_a_green_cut goalty then (assert_proof_is_valid proof metasenv context goalty; - let cache = cache_add_success cache goalty proof in - aux cache ((metasenv,subst,gl)::tl)) + let cache = cache_add_success sort cache goalty proof in + aux tables maxm cache ((metasenv,subst,gl)::tl)) else (let goalty = CicMetaSubst.apply_subst subst goalty in assert_proof_is_valid proof metasenv context goalty; let cache = if is_a_green_cut goalty then - cache_add_success cache goalty proof + cache_add_success sort cache goalty proof else cache in @@ -182,18 +440,21 @@ let auto_main context flags elems cache universe = (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl)) others in - aux cache ((metasenv,subst,gl)::others@tl)) + aux tables maxm cache ((metasenv,subst,gl)::others@tl)) with CicUtil.Meta_not_found i when i = goalno -> assert false with CicUtil.Meta_not_found i when i = goalno -> (* goalno was closed by sideeffect *) - aux cache ((metasenv,subst,gl)::tl) - and aux_single cache metasenv subst (goalno, depth, _) goalty cc = + debug_print ("Goal "^string_of_int goalno^" closed by sideeffect"); + aux tables maxm cache ((metasenv,subst,gl)::tl) + and aux_single tables maxm cache metasenv subst (goalno, depth, _) goalty cc = let goalty = CicMetaSubst.apply_subst subst goalty in (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *) (* FAILURE (euristic cut) *) match cache_examine cache goalty with - | Failed_in d when d >= depth -> Fail "depth",cache(*FAILURE(depth)*) + | Failed_in d when d >= depth -> + Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth), + tables,cache,maxm(*FAILURE(depth)*) | Succeded t -> assert(List.for_all (fun (i,_) -> i <> goalno) subst); let entry = goalno, (cc, t,goalty) in @@ -201,49 +462,82 @@ let auto_main context flags elems cache universe = let subst = entry :: subst in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in debug_print (" CACHE HIT!"); - Success (metasenv, subst, []),cache - | UnderInspection -> Fail "looping",cache + Success (metasenv, subst, []), tables, cache, maxm + | UnderInspection -> Fail "looping",tables,cache, maxm | Notfound | Failed_in _ when depth > 0 -> (* we have more depth now *) let cache = cache_add_underinspection cache goalty depth in - let candidates = get_candidates universe goalty in let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in - let elems = - HExtlib.filter_map - (try_candidate subst fake_proof goalno depth context) - candidates + let elems, tables, cache, maxm = + if is_equational_case goalty flags then + match + equational_case dbd tables maxm + ~auto:callback_for_paramod cache + depth fake_proof goalno goalty subst context flags + with + | Some elems, tables, cache, maxm -> + elems, tables, cache, maxm (* manca cache *) + | None, tables,cache,maxm -> + applicative_case dbd tables maxm depth subst fake_proof goalno + goalty metasenv context cache + else + applicative_case dbd tables maxm depth subst fake_proof goalno + goalty metasenv context cache in - let elems = sort_new_elems elems in - aux cache elems - | _ -> Fail "??",cache + aux tables maxm cache elems + | _ -> Fail "??",tables,cache,maxm in - aux cache elems -;; - -let auto universe cache context metasenv gl flags = + aux tables maxm cache elems + +and + auto_all_solutions dbd tables maxm cache context metasenv gl flags += let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in let elems = [metasenv,[],goals] in - match auto_main context flags elems cache universe with - | Fail s,cache -> prerr_endline s;None,cache - | Success (metasenv,subst,_), cache -> Some (subst,metasenv), cache + let rec aux tables maxm solutions cache elems flags = + match auto_main dbd tables maxm context flags elems cache with + | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm + | Success (metasenv,subst,others),tables,cache,maxm -> + if Unix.gettimeofday () > flags.timeout then + ((subst,metasenv)::solutions), cache, maxm + else + aux tables maxm ((subst,metasenv)::solutions) cache others flags + in + let rc = aux tables maxm [] cache elems flags in + prerr_endline "fine auto all solutions"; + rc ;; -let auto_all_solutions universe cache context metasenv gl flags = +(* }}} ****************** AUTO ***************) + +let auto_all_solutions dbd cache context metasenv gl flags = + let solutions, cache, _ = + auto_all_solutions dbd None 0 cache context metasenv gl flags + in + solutions, cache +;; + +let auto dbd cache context metasenv gl flags = + let initial_time = Unix.gettimeofday() in let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in let elems = [metasenv,[],goals] in - let bigbang = Unix.gettimeofday () in - let rec aux solutions cache elems flags = - match auto_main context flags elems cache universe with - | Fail s,cache ->prerr_endline s; solutions,cache - | Success (metasenv,subst,others), cache -> - let elapsed = Unix.gettimeofday () -. bigbang in - if elapsed > flags.timeout then - ((subst,metasenv)::solutions), cache - else - aux ((subst,metasenv)::solutions) cache others - {flags with timeout = flags.timeout -. elapsed} - in - aux [] cache elems flags + match auto_main dbd None 0 context flags elems cache with + | Success (metasenv,subst,_), tables,cache,_ -> + prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)); + Some (subst,metasenv), cache + | Fail s,tables,cache,maxm -> None,cache ;; + +let applyS_tac ~dbd ~term = + ProofEngineTypes.mk_tactic + (fun status -> + try + let _, proof, gl,_,_ = apply_smart ~dbd ~term ~subst:[] status in + proof, gl + with + | CicUnification.UnificationFailure msg + | CicTypeChecker.TypeCheckerFailure msg -> + raise (ProofEngineTypes.Fail msg)) +