From: Andrea Asperti Date: Fri, 20 Oct 2006 15:43:02 +0000 (+0000) Subject: Major changes to auto, documented on the helm mailing list. X-Git-Tag: 0.4.95@7852~865 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9ab7d3460c70ee067f75bf6523d06b67d6e7750a;p=helm.git Major changes to auto, documented on the helm mailing list. --- diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index b904d52cb..06aa8b303 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -26,53 +26,371 @@ open AutoTypes;; open AutoCache;; -let debug_print s = () (* prerr_endline s;; *) +let debug_print s = prerr_endline (Lazy.force s);; -(* {{{ *********** local given_clause wrapper ***********) +(* functions for retrieving theorems *) -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 smart_flag auto 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.close_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 50 minsteps, minsteps, infinity - in - active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout +exception FillingFailure of AutoCache.cache * int + + + +let find_library_theorems dbd proof gl = + let univ = MetadataQuery.universe_of_goals ~dbd proof gl in + let terms = List.map CicUtil.term_of_uri univ in + List.map + (fun t -> + (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph))) + terms + +let find_context_theorems context metasenv = + let l,_ = + List.fold_left + (fun (res,i) ctxentry -> + match ctxentry with + | Some (_,Cic.Decl t) -> + (Cic.Rel i, CicSubstitution.lift i t)::res,i+1 + | Some (_,Cic.Def (_,Some t)) -> + (Cic.Rel i, CicSubstitution.lift i t)::res,i+1 + | Some (_,Cic.Def (_,None)) -> + let t = Cic.Rel i in + let ty,_ = + CicTypeChecker.type_of_aux' + metasenv context t CicUniv.empty_ugraph + in + (t,ty)::res,i+1 + | _ -> res,i+1) + ([],1) context + in l + +let rec is_an_equality = function + | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] + when (LibraryObjects.is_eq_URI uri) -> true + | Cic.Prod (_, _, t) -> is_an_equality t + | _ -> false +;; + +let partition_equalities = + List.partition (fun (_,ty) -> is_an_equality ty) + + +let default_auto maxm _ cache _ _ _ _ = [],cache,maxm ;; + + +let is_unit_equation context metasenv oldnewmeta term = + let head, metasenv, args, newmeta = + ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 in - let res,actives,passives,maxmeta = - Saturation.given_clause bag maxmeta status active passive - goal_steps saturation_steps timeout + let propositional_args = + HExtlib.filter_map + (function + | Cic.Meta(i,_) -> + let _,_,mt = CicUtil.lookup_meta i metasenv in + let sort,u = + CicTypeChecker.type_of_aux' metasenv context mt + CicUniv.empty_ugraph + in + let b, _ = + CicReduction.are_convertible ~metasenv context + sort (Cic.Sort Cic.Prop) u + in + if b then Some i else None + | _ -> assert false) + args + in + if propositional_args = [] then + let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in + Some (args,metasenv,newmetas,head,newmeta) + else None + +let retrieve_equations cache = + let eq_uri = + match LibraryObjects.eq_URI() with + | None ->assert false + | Some eq_uri -> eq_uri in + let fake= Cic.Meta(-1,[]) in + let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);Cic.Meta(-1,[]); + Cic.Meta(-2,[]); Cic.Meta(-3,[])] in + let candidates = get_candidates cache fake_eq in + let debug_msg = + (lazy ("candidates for " ^ (CicPp.ppterm fake_eq) ^ " = " ^ + (String.concat "\n" (List.map CicPp.ppterm candidates)))) in + debug_print debug_msg; + candidates + +(* + let proof, goalno = status in + let _, metasenv,_,_ = proof in + let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in + let eq_uri = eq_of_goal type_of_goal in + let env = (metasenv, context, CicUniv.empty_ugraph) in + let eq_indexes, equalities, maxm, cache = + Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache in - res,actives,passives,bag,cache,maxmeta + prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^ + string_of_int maxm); + List.iter + (fun e -> prerr_endline (Equality.string_of_equality ~env e)) + equalities; + prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; + let equalities = + HExtlib.filter_map + (fun e -> forward_simplify bag eq_uri env e active) + equalities + in + prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>"; + List.iter + (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities; + prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm); + bag, equalities, cache, maxm +*) + +let build_equality bag head args proof newmetas maxmeta = + match head with + | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] -> + let p = + if args = [] then proof else Cic.Appl (proof::args) + in + let o = !Utils.compare_terms t1 t2 in + let stat = (ty,t1,t2,o) in + (* let w = compute_equality_weight stat in *) + let w = 0 in + let proof = Equality.Exact p in + let e = Equality.mk_equality bag (w, proof, stat, newmetas) in + (* to clean the local context of metas *) + Equality.fix_metas bag maxmeta e + | _ -> assert false ;; -(* }}} ****************************************************************) +let partition_unit_equalities context metasenv newmeta bag equations = + List.fold_left + (fun (units,other,maxmeta)(t,ty) -> + match is_unit_equation context metasenv maxmeta ty with + | Some (args,metasenv,newmetas,head,newmeta') -> + let maxmeta,equality = + build_equality bag head args t newmetas newmeta' in + equality::units,other,maxmeta + | None -> + units,(t,ty)::other,maxmeta) + ([],[],newmeta) equations -(* {{{ **************** applyS *******************) +let empty_tables = + (Saturation.make_active [], + Saturation.make_passive [], + Equality.mk_equality_bag) + +let init_cache_and_tables dbd use_library (proof, goal) = + let _, metasenv, _, _ = proof in + let newmeta = CicMkImplicit.new_meta metasenv [] in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let eq_uri = + match LibraryObjects.eq_URI() with + | None ->assert false + | Some eq_uri -> eq_uri in + let ct = find_context_theorems context metasenv in + let lt = + if use_library then + find_library_theorems dbd metasenv [goal] + else [] in + (* all equations are added to the cache *) + prerr_endline ("ho trovato " ^ (string_of_int (List.length lt))); + let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in + let equations,others = partition_equalities (ct@lt) in + let bag = Equality.mk_equality_bag () in + let units, other_equalities, newmeta = + partition_unit_equalities context metasenv newmeta bag equations in + (* other equations are added to the cache; note that untis equalities + are not)*) + let env = (metasenv, context, CicUniv.empty_ugraph) in + (* let equalities = + Saturation.simplify_equalities bag eq_uri env units in *) + let passive = Saturation.make_passive units in + let no = List.length units in + prerr_endline ("No = " ^ (string_of_int no)); + let active = Saturation.make_active [] in + let active,passive,newmeta = + Saturation.pump_actives context bag newmeta active passive (no+1) infinity + in + (active,passive,bag),cache,newmeta + +let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast = + let head, metasenv, args, newmeta = + ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 + in + let propositional_args = + HExtlib.filter_map + (function + | Cic.Meta(i,_) -> + let _,_,mt = CicUtil.lookup_meta i metasenv in + let sort,u = + CicTypeChecker.type_of_aux' metasenv context mt + CicUniv.empty_ugraph + in + let b, _ = + CicReduction.are_convertible ~metasenv context + sort (Cic.Sort Cic.Prop) u + in + if b then Some i else None + | _ -> assert false) + args + in + let results,cache,newmeta = + if propositional_args = [] then + let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in + [args,metasenv,newmetas,head,newmeta],cache,newmeta + else + let proof = + None,metasenv,term,term (* term non e' significativo *) + in + let flags = + if fast then + {AutoTypes.default_flags() with + AutoTypes.timeout = Unix.gettimeofday() +. 1.0; + maxwidth = 2;maxdepth = 2; + use_paramod=true;use_only_paramod=false} + else + {AutoTypes.default_flags() with + AutoTypes.timeout = Unix.gettimeofday() +. 1.0; + maxwidth = 2;maxdepth = 4; + use_paramod=true;use_only_paramod=false} + in + match auto newmeta tables cache context metasenv propositional_args flags with + | [],cache,newmeta -> raise (FillingFailure (cache,newmeta)) + | substs,cache,newmeta -> + List.map + (fun subst -> + let metasenv = + CicMetaSubst.apply_subst_metasenv subst metasenv + in + let head = CicMetaSubst.apply_subst subst head in + let newmetas = + List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv + in + let args = List.map (CicMetaSubst.apply_subst subst) args in + let newm = CicMkImplicit.new_meta metasenv subst in + args,metasenv,newmetas,head,max newm newmeta) + substs, cache, newmeta + in + results,cache,newmeta + +let build_equalities auto context metasenv tables cache newmeta equations = + List.fold_left + (fun (facts,cache,newmeta) (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,newmeta = + fill_hypothesis context metasenv newmeta ty tables cache auto true + in + let (active,passive,bag) = tables in + let eqs,bag,newmeta = + List.fold_left + (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') -> + let maxmeta,equality = + build_equality bag head args t newmetas newmeta' + in + equality::acc,bag,maxmeta) + ([],bag,newmeta) saturated + in + (eqs@facts, cache, newmeta) + with FillingFailure (cache,newmeta) -> + (* if filling hypothesis fails we add the equation to + the cache *) + (facts,cache,newmeta) + ) + ([],cache,newmeta) equations + +let close_more tables maxmeta context status auto cache = + let (active,passive,bag) = tables in + let proof, goalno = status in + let _, metasenv,_,_ = proof in + let equations = retrieve_equations cache in + 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 None) + equations in + let units, cache, maxm = + build_equalities auto context metasenv tables cache maxmeta eqs_and_types in + prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^ + string_of_int maxm); + List.iter + (fun e -> prerr_endline (Equality.string_of_equality e)) + units; + prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; + let passive = Saturation.add_to_passive units passive in + let no = List.length units in + prerr_endline ("No = " ^ (string_of_int no)); + let active,passive,newmeta = + Saturation.pump_actives context bag maxm active passive (no+1) infinity + in + (active,passive,bag),cache,newmeta + +let find_context_equalities + maxmeta bag context proof cache += + prerr_endline "find_equalities"; + let module C = Cic in + let module S = CicSubstitution in + let module T = CicTypeChecker in + let _,metasenv,_,_ = proof in + let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta 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 cache index newmeta = function + | [] -> [], newmeta,cache + | (Some (_, C.Decl (term)))::tl -> + debug_print + (lazy + (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term))); + let do_find context term = + match term with + | C.Prod (name, s, t) when is_an_equality t -> + (try + + let term = S.lift index term in + let saturated,cache,newmeta = + fill_hypothesis context metasenv newmeta term + empty_tables cache default_auto false + in + let eqs,newmeta = + List.fold_left + (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') -> + let newmeta, equality = + build_equality + bag head args (Cic.Rel index) newmetas (max newmeta newmeta') + in + equality::acc, newmeta + 1) + ([],newmeta) saturated + in + eqs, newmeta, cache + with FillingFailure (cache,newmeta) -> + [],newmeta,cache) + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when LibraryObjects.is_eq_URI uri -> + let term = S.lift index term in + let newmeta, e = + build_equality bag term [] (Cic.Rel index) [] newmeta + in + [e], (newmeta+1),cache + | _ -> [], newmeta, cache + in + let eqs, newmeta, cache = do_find context term in + let rest, newmeta,cache = aux cache (index+1) newmeta tl in + List.map (fun x -> index,x) eqs @ rest, newmeta, cache + | _::tl -> + aux cache (index+1) newmeta tl + in + let il, maxm, cache = + aux cache 1 newmeta context + in + let indexes, equalities = List.split il in + indexes, equalities, maxm, cache +;; + +(***************** applyS *******************) let new_metasenv_and_unify_and_t dbd flags proof goal ?tables newmeta' metasenv' context term' ty termty @@ -109,12 +427,15 @@ let new_metasenv_and_unify_and_t PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal) in match - let cache = cache_empty in - given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta) + let (active, passive,bag), cache, maxmeta = + init_cache_and_tables dbd true (proof'''',newmeta) + in + Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive + max_int max_int flags.timeout with - | None, active, passive, bag,_,_ -> + | None, _,_,_ -> raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) - | Some (_,proof''''',_), active, passive,bag,_,_ -> + | Some (_,proof''''',_), active,passive,_ -> subst,proof''''', ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive @@ -177,9 +498,7 @@ let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) = subst, proof, gl, active, passive ;; -(* }}} **************** applyS **************) - -(* {{{ ***************** AUTO ********************) +(****************** AUTO ********************) let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;; let ugraph = CicUniv.empty_ugraph;; @@ -190,7 +509,7 @@ let ppterm ctx t = ;; let is_in_prop context subst metasenv ty = let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in - fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u) + fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u) ;; let assert_proof_is_valid proof metasenv context goalty = let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in @@ -222,12 +541,16 @@ let split_goals_in_prop metasenv subst gl = let _,context,ty = CicUtil.lookup_meta g metasenv in try let sort,u = typeof ~subst metasenv context ty ugraph in - fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u) + let b,_ = + CicReduction.are_convertible + ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in + b with | CicTypeChecker.AssertFailure s | CicTypeChecker.TypeCheckerFailure s -> - debug_print (ppterm context (CicMetaSubst.apply_subst subst ty)); - debug_print (Lazy.force s); + debug_print + (lazy (ppterm context (CicMetaSubst.apply_subst subst ty))); + debug_print s; false) (* FIXME... they should type! *) gl @@ -252,12 +575,16 @@ let order_new_goals metasenv subst open_goals ppterm = in let tys = List.map - (fun (i,_) -> - let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals + (fun (i,sort) -> + let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals in - debug_print (" OPEN: "^ - String.concat " " - (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys)); + debug_print (lazy (" OPEN: "^ + String.concat "\n" + (List.map + (function + | (i,t,P) -> string_of_int i (* ":"^ppterm t^ "Prop" *) + | (i,t,T) -> string_of_int i ) (* ":"^ppterm t^ "Type")*) + tys))); open_goals ;; @@ -267,33 +594,69 @@ let is_an_equational_goal = function ;; let equational_case - dbd tables maxm auto cache depth fake_proof goalno goalty subst context + tables maxm cache depth fake_proof goalno goalty subst context flags = + let active,passive,bag = tables in let ppterm = ppterm context in - prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty ); + let status = (fake_proof,goalno) in + if flags.use_only_paramod then + begin + prerr_endline ("PARAMODULATION SU: " ^ + string_of_int goalno ^ " " ^ ppterm goalty ); + let goal_steps, saturation_steps, timeout = max_int,max_int,flags.timeout in + match + Saturation.given_clause bag maxm status active passive + goal_steps saturation_steps timeout + with + | None, active, passive, maxmeta -> + [], (active,passive,bag), cache, maxmeta, flags + | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta -> + 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,sort) open_goals in + [metasenv,subst,open_goals], (active,passive,bag), + cache, maxmeta, flags + end + else + begin + prerr_endline ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty ); + let res, maxmeta = Saturation.all_subsumed bag maxm status active passive in + assert (maxmeta >= maxm); + let res' = + List.map + (fun subst',(_,metasenv,proof,_),open_goals -> + 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,sort) open_goals in + metasenv,subst,open_goals) + res in + res', (active,passive,bag), cache, maxmeta, flags + end + (* - 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 + let active,passive,bag,cache,maxmeta,flags,goal_steps,saturation_steps,timeout = + given_clause_params + tables maxm auto cache subst flags context status in + match + Saturation.given_clause bag maxmeta status active passive + goal_steps saturation_steps timeout + with + | None, active, passive, maxmeta -> + None, (active,passive,bag), cache, maxmeta, flags + | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta -> 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 open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in + Some [metasenv,subst,open_goals], (active,passive,bag), cache, maxmeta, flags +*) ;; let try_candidate - goalty dbd tables maxm subst fake_proof goalno depth context cand + goalty tables maxm subst fake_proof goalno depth context cand = let ppterm = ppterm context in try @@ -301,7 +664,8 @@ let try_candidate PrimitiveTactics.apply_with_subst ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno) in - debug_print (" OK: " ^ ppterm cand); + debug_print (lazy (" OK: " ^ ppterm cand)); + let metasenv = CicRefine.pack_coercion_metasenv metasenv in assert (maxmeta >= maxm); (*FIXME:sicuro che posso @?*) assert_subst_are_disjoint subst subst'; @@ -314,28 +678,33 @@ let try_candidate ;; let applicative_case - dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache + tables maxm depth subst fake_proof goalno goalty metasenv context cache = let candidates = get_candidates cache goalty in + let debug_msg = + (lazy ("candidates for " ^ (CicPp.ppterm goalty) ^ " = " ^ + (String.concat "\n" (List.map CicPp.ppterm candidates)))) in + debug_print debug_msg; 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 + 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 + elems, tables, cache, maxm ;; (* Works if there is no dependency over proofs *) let is_a_green_cut goalty = CicUtil.is_meta_closed goalty ;; + let prop = function (_,_,P) -> true | _ -> false;; let calculate_timeout flags = if flags.timeout = 0. then @@ -360,73 +729,58 @@ let cache_add_success sort cache k v = cache k ;; -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 rec auto_main tables maxm context flags elems cache = let flags = calculate_timeout flags in let ppterm = ppterm context in let irl = mk_irl context in - let rec aux tables maxm cache = function (* elems in OR *) + let rec aux flags 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), 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 tables maxm cache tl (* FAILURE (width) *) + debug_print + (lazy (" FAILURE(width): " ^ string_of_int (List.length goals))); + aux flags tables maxm cache tl (* FAILURE (width) *) | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl -> 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); + debug_print + (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty)); + debug_print (lazy (AutoCache.cache_print context cache)); if sort = T && tl <> [] then (* FIXME!!!! *) - (debug_print (" FAILURE(not in prop)"); - aux tables maxm cache tl (* FAILURE (not in prop) *)) + (debug_print + (lazy (" FAILURE(not in prop)")); + aux flags tables maxm cache tl (* FAILURE (not in prop) *)) else - match aux_single tables maxm cache metasenv subst elem goalty cc with + match aux_single flags 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); + (lazy + (" 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 + aux flags 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 let proof = CicMetaSubst.apply_subst subst goal in - debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof); + debug_print + (lazy ("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 sort cache goalty proof in - aux tables maxm cache ((metasenv,subst,gl)::tl)) + aux flags tables maxm cache ((metasenv,subst,gl)::tl)) else (let goalty = CicMetaSubst.apply_subst subst goalty in assert_proof_is_valid proof metasenv context goalty; @@ -441,17 +795,20 @@ let rec auto_main dbd tables maxm context flags elems cache = (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl)) others in - aux tables maxm cache ((metasenv,subst,gl)::others@tl)) + aux flags 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 *) - 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 = + debug_print + (lazy ("Goal "^string_of_int goalno^" closed by sideeffect")); + aux flags tables maxm cache ((metasenv,subst,gl)::tl) + + and aux_single flags 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) *) + prerr_endline ("DEPTH = +++++++= "^ (string_of_int depth)); match cache_examine cache goalty with | Failed_in d when d >= depth -> Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth), @@ -462,42 +819,49 @@ let rec auto_main dbd tables maxm context flags elems cache = assert_subst_are_disjoint subst [entry]; let subst = entry :: subst in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in - debug_print (" CACHE HIT!"); + debug_print (lazy (" CACHE HIT!")); 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 fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in - let elems, tables, cache, maxm = + let elems, tables, cache, maxm, flags = if is_equational_case goalty flags then - match - equational_case dbd tables maxm - (Some callback_for_paramod) cache - depth fake_proof goalno goalty subst context flags - with - | Some elems, tables, cache, maxm -> - elems, tables, cache, maxm - | None, tables,cache,maxm -> - applicative_case dbd tables maxm depth subst fake_proof goalno - goalty metasenv context cache + let elems,tables,cache,maxm1, flags = + equational_case tables maxm cache + depth fake_proof goalno goalty subst context flags in + assert(maxm1 >= maxm); + let maxm = maxm1 in + let more_elems, tables, cache, maxm1 = + if flags.use_only_paramod then + [],tables, cache, maxm + else + applicative_case + tables maxm depth subst fake_proof goalno + goalty metasenv context cache in + assert(maxm1 >= maxm); + let maxm = maxm1 in + elems@more_elems, tables, cache, maxm, flags else - applicative_case dbd tables maxm depth subst fake_proof goalno - goalty metasenv context cache + let elems, tables, cache, maxm = + applicative_case tables maxm depth subst fake_proof goalno + goalty metasenv context cache in + elems, tables, cache, maxm, flags in - aux tables maxm cache elems + aux flags tables maxm cache elems | _ -> Fail "??",tables,cache,maxm in - aux tables maxm cache elems + aux flags tables maxm cache elems and - auto_all_solutions dbd tables maxm cache context metasenv gl flags + auto_all_solutions maxm tables 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 let rec aux tables maxm solutions cache elems flags = - match auto_main dbd tables maxm context flags elems cache with + match auto_main 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 @@ -506,25 +870,36 @@ and 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 + match rc with + | [],cache,maxm -> [],cache,maxm + | solutions,cache,maxm -> + let solutions = + HExtlib.filter_map + (fun (subst,newmetasenv) -> + let opened = + ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv + in + if opened = [] then Some subst else None) + solutions + in + solutions,cache,maxm ;; (* }}} ****************** AUTO ***************) -let auto_all_solutions dbd cache context metasenv gl flags = +let auto_all tables cache context metasenv gl flags = let solutions, cache, _ = - auto_all_solutions dbd None 0 cache context metasenv gl flags + auto_all_solutions 0 tables cache context metasenv gl flags in solutions, cache ;; -let auto dbd cache context metasenv gl flags = +let auto flags metasenv tables cache context metasenv gl = 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 - match auto_main dbd None 0 context flags elems cache with + match auto_main tables 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 @@ -576,7 +951,7 @@ let flags_of_params params ?(for_applyS=false) () = Unix.gettimeofday() +. (float_of_int timeout); AutoTypes.use_paramod = use_paramod; AutoTypes.use_only_paramod = use_only_paramod; - AutoTypes.dont_cache_failures = false + AutoTypes.dont_cache_failures = false; } let applyS_tac ~dbd ~term ~params = @@ -593,11 +968,132 @@ let applyS_tac ~dbd ~term ~params = | CicTypeChecker.TypeCheckerFailure msg -> raise (ProofEngineTypes.Fail msg)) +(* SUPERPOSITION *) + +(* Syntax: + * auto superposition target = NAME + * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only] + * + * - if table is omitted no superposition will be performed + * - if demod_table is omitted no demodulation will be prformed + * - subterms_only is passed to Indexing.superposition_right + * + * lists are coded using _ (example: H_H1_H2) + *) + +let eq_and_ty_of_goal = function + | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri -> + uri,t + | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) +;; + +let rec find_in_ctx i name = function + | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name))) + | Some (Cic.Name name', _)::tl when name = name' -> i + | _::tl -> find_in_ctx (i+1) name tl +;; + +let rec position_of i x = function + | [] -> assert false + | j::tl when j <> x -> position_of (i+1) x tl + | _ -> i +;; + +let superposition_tac ~target ~table ~subterms_only ~demod_table status = + Saturation.reset_refs(); + let proof,goalno = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goalno metasenv in + let eq_uri,tty = eq_and_ty_of_goal ty in + let env = (metasenv, context, CicUniv.empty_ugraph) in + let names = Utils.names_of_context context in + let bag = Equality.mk_equality_bag () in + let eq_index, equalities, maxm,cache = + find_context_equalities 0 bag context proof AutoCache.cache_empty + in + let eq_what = + let what = find_in_ctx 1 target context in + List.nth equalities (position_of 0 what eq_index) + in + let eq_other = + if table <> "" then + let other = + let others = Str.split (Str.regexp "_") table in + List.map (fun other -> find_in_ctx 1 other context) others + in + List.map + (fun other -> List.nth equalities (position_of 0 other eq_index)) + other + else + [] + in + let index = List.fold_left Indexing.index Indexing.empty eq_other in + let maxm, eql = + if table = "" then maxm,[eq_what] else + Indexing.superposition_right bag + ~subterms_only eq_uri maxm env index eq_what + in + prerr_endline ("Superposition right:"); + prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env); + prerr_endline ("\n table: "); + List.iter (fun e -> prerr_endline (" " ^ Equality.string_of_equality e ~env)) eq_other; + prerr_endline ("\n result: "); + List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; + prerr_endline ("\n result (cut&paste): "); + List.iter + (fun e -> + let t = Equality.term_of_equality eq_uri e in + prerr_endline (CicPp.pp t names)) + eql; + prerr_endline ("\n result proofs: "); + List.iter (fun e -> + prerr_endline (let _,p,_,_,_ = Equality.open_equality e in + let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in + Subst.ppsubst s ^ "\n" ^ + CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql; + if demod_table <> "" then + begin + let eql = + if eql = [] then [eq_what] else eql + in + let demod = + let demod = Str.split (Str.regexp "_") demod_table in + List.map (fun other -> find_in_ctx 1 other context) demod + in + let eq_demod = + List.map + (fun demod -> List.nth equalities (position_of 0 demod eq_index)) + demod + in + let table = List.fold_left Indexing.index Indexing.empty eq_demod in + let maxm,eql = + List.fold_left + (fun (maxm,acc) e -> + let maxm,eq = + Indexing.demodulation_equality bag eq_uri maxm env table e + in + maxm,eq::acc) + (maxm,[]) eql + in + let eql = List.rev eql in + prerr_endline ("\n result [demod]: "); + List.iter + (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; + prerr_endline ("\n result [demod] (cut&paste): "); + List.iter + (fun e -> + let t = Equality.term_of_equality eq_uri e in + prerr_endline (CicPp.pp t names)) + eql; + end; + proof,[goalno] +;; + + let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) = (* argument parsing *) let string = string params in let bool = bool params in - let use_only_paramod = bool "paramodulation" false in (* hacks to debug paramod *) let superposition = bool "superposition" false in let target = string "target" "" in @@ -607,36 +1103,90 @@ let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) = match superposition with | true -> (* this is the ugly hack to debug paramod *) - Saturation.superposition_tac + superposition_tac ~target ~table ~subterms_only ~demod_table (proof,goal) | false -> (* this is the real auto *) - let _, metasenv, _, _ = proof in - let _, context, goalty = CicUtil.lookup_meta goal metasenv in - let cache = - let cache = - AutoCache.cache_add_context context metasenv AutoCache.cache_empty - in - if use_only_paramod then (* only paramod *) - cache - else - AutoCache.cache_add_library dbd proof [goal] cache - in - let oldmetasenv = metasenv in + let _,metasenv,_,_ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let flags = flags_of_params params () in - match auto dbd cache context metasenv [goal] flags with - | None,cache -> - raise (ProofEngineTypes.Fail (lazy "Auto gave up")) - | Some (subst,metasenv),cache -> - let proof,metasenv = + (* just for testing *) + let use_library = not flags.use_only_paramod in + let tables,cache,newmeta = + init_cache_and_tables dbd use_library (proof, goal) in + let tables,cache,newmeta = + close_more tables newmeta context (proof, goal) auto_all_solutions cache in + let initial_time = Unix.gettimeofday() in + let (_,oldmetasenv,_,_) = proof in + let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in + match auto_main tables newmeta context flags [elem] cache with + | Success (metasenv,subst,_), tables,cache,_ -> + prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)); + let proof,metasenv = ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof goal (CicMetaSubst.apply_subst subst) metasenv - in - let opened = - ProofEngineHelpers.compare_metasenvs ~oldmetasenv - ~newmetasenv:metasenv - in - proof,opened + in + let opened = + ProofEngineHelpers.compare_metasenvs ~oldmetasenv + ~newmetasenv:metasenv + in + proof,opened + | Fail s,tables,cache,maxm -> + raise (ProofEngineTypes.Fail (lazy "Auto gave up")) ;; let auto_tac ~dbd ~params = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd);; + +let eq_of_goal = function + | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri -> + uri + | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) +;; + +(* DEMODULATE *) +let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = + let curi,metasenv,pbo,pty = 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 eq_uri = eq_of_goal ty in + let (active,passive,bag), cache, maxm = + init_cache_and_tables dbd true (proof,goal) in + let equalities = (Saturation.list_of_passive passive) in + (* we demodulate using both actives passives *) + let table = + List.fold_left + (fun tbl eq -> Indexing.index tbl eq) + (snd active) equalities + in + let changed,(newproof,newmetasenv, newty) = + Indexing.demodulation_goal bag + (metasenv,context,CicUniv.empty_ugraph) table initgoal + in + if changed then + begin + let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in + let proofterm,_ = + Equality.build_goal_proof bag + eq_uri newproof opengoal ty [] context metasenv + in + let extended_metasenv = (maxm,context,newty)::metasenv in + let extended_status = + (curi,extended_metasenv,pbo,pty),goal in + let (status,newgoals) = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) + extended_status in + (status,maxm::newgoals) + end + else (* if newty = ty then *) + raise (ProofEngineTypes.Fail (lazy "no progress")) + (*else ProofEngineTypes.apply_tactic + (ReductionTactics.simpl_tac + ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) +;; + +let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);; + + + diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli index 301aa4b45..6e64fb66e 100644 --- a/components/tactics/auto.mli +++ b/components/tactics/auto.mli @@ -30,3 +30,5 @@ val auto_tac: val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> params:(string * string) list -> ProofEngineTypes.tactic + +val demodulate_tac : dbd:HMysql.dbd -> ProofEngineTypes.tactic diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 12c8e9bd6..7bbc4d43c 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -404,7 +404,7 @@ let subsumption_aux use_unification env table target = | Founif.MatchingFailure | CicUnification.UnificationFailure _ -> ok what leftorright tl in - match ok right Utils.Left leftr with + match ok right Utils.Left leftr with | Some _ as res -> res | None -> let rightr = @@ -426,6 +426,61 @@ let unification x y z = subsumption_aux true x y z ;; +let subsumption_aux_all use_unification env table target = + let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in + let _, context, ugraph = env in + let metasenv = tmetas in + let predicate, unif_fun = + if use_unification then + Unification, Founif.unification + else + Matching, Founif.matching + in + let leftr = + match left with + | Cic.Meta _ when not use_unification -> [] + | _ -> + let leftc = get_candidates predicate table left in + find_all_matches ~unif_fun + metasenv context ugraph 0 left ty leftc + in + let rightr = + match right with + | Cic.Meta _ when not use_unification -> [] + | _ -> + let rightc = get_candidates predicate table right in + find_all_matches ~unif_fun + metasenv context ugraph 0 right ty rightc + in + let rec ok_all what leftorright = function + | [] -> [] + | (_, subst, menv, ug, (pos,equation))::tl -> + let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in + try + let other = if pos = Utils.Left then r else l in + let what' = Subst.apply_subst subst what in + let other' = Subst.apply_subst subst other in + let subst', menv', ug' = + unif_fun metasenv m context what' other' ugraph + in + (match Subst.merge_subst_if_possible subst subst' with + | None -> ok_all what leftorright tl + | Some s -> + (s, equation, leftorright <> pos )::(ok_all what leftorright tl)) + with + | Founif.MatchingFailure + | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl) + in + (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr ) +;; + +let subsumption_all x y z = + subsumption_aux_all false x y z +;; + +let unification_all x y z = + subsumption_aux_all true x y z +;; let rec demodulation_aux bag ?from ?(typecheck=false) metasenv context ugraph table lift_amount term = (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*) diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli index e180511a6..340a1eddb 100644 --- a/components/tactics/paramodulation/indexing.mli +++ b/components/tactics/paramodulation/indexing.mli @@ -48,7 +48,16 @@ val subsumption : Index.t -> Equality.equality -> (Subst.substitution * Equality.equality * bool) option - +val unification_all : + Cic.metasenv * Cic.context * CicUniv.universe_graph -> + Index.t -> + Equality.equality -> + (Subst.substitution * Equality.equality * bool) list +val subsumption_all : + Cic.metasenv * Cic.context * CicUniv.universe_graph -> + Index.t -> + Equality.equality -> + (Subst.substitution * Equality.equality * bool) list val superposition_left : Equality.equality_bag -> Cic.conjecture list * Cic.context * CicUniv.universe_graph -> diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index c23401e9c..40d07e414 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -116,6 +116,10 @@ type result = | ParamodulationFailure of string * active_table * passive_table | ParamodulationSuccess of new_proof * active_table * passive_table ;; + +let list_of_passive (l,s) = l +;; + let make_passive eq_list = let set = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list @@ -838,6 +842,29 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = | _ -> None ;; +let find_all_subsumed bag env table (goalproof,menv,ty) = + match ty with + | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] + when LibraryObjects.is_eq_URI uri -> + let goal_equation = + Equality.mk_equality bag + (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) + in + List.map + (fun (subst, equality, swapped ) -> + let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in + let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in + let p = + if swapped then + Equality.symmetric bag eq_ty l id uri m + else + p + in (goalproof, p, id, subst, cicmenv)) + (Indexing.unification_all env table goal_equation) + | _ -> assert false +;; + + let check_if_goal_is_identity env = function | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) when left = right && LibraryObjects.is_eq_URI uri -> @@ -1367,146 +1394,71 @@ let build_proof final_subst, proof, open_goals ;; -let find_equalities dbd status smart_flag auto cache = - let proof, goalno = status in - let _, metasenv,_,_ = proof in - let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in - let eq_uri = eq_of_goal type_of_goal in - let env = (metasenv, context, CicUniv.empty_ugraph) in - let bag = Equality.mk_equality_bag () in - let eq_indexes, equalities, maxm, cache = - Equality_retrieval.find_context_equalities 0 bag auto context proof cache - in - prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>"; - List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities; - prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; - let lib_eq_uris, library_equalities, maxm, cache = - Equality_retrieval.find_library_equalities bag - auto smart_flag dbd context (proof, goalno) (maxm+2) - cache - in - prerr_endline (">>>>>>>>>> gained from the library >>>>>>>>>>>>" ^ - string_of_int maxm); - List.iter - (fun (_,e) -> prerr_endline (Equality.string_of_equality e)) - library_equalities; - prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; - let equalities = List.map snd library_equalities @ equalities in - let equalities = - simplify_equalities bag eq_uri env equalities + +(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *) + +(* exported functions *) + +let pump_actives context bag maxm active passive saturation_steps max_time = + reset_refs(); + maxmeta := maxm; + let max_l l = + List.fold_left + (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in + List.fold_left (fun acc (i,_,_) -> max i acc) acc menv) + 0 l in + let active_l = fst active in + let passive_l = fst passive in + let ma = max_l active_l in + let mp = max_l passive_l in + assert (maxm > max ma mp); + let eq_uri = + match LibraryObjects.eq_URI () with + | None -> assert false + | Some uri -> uri in - prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>"; - List.iter - (fun e -> prerr_endline (Equality.string_of_equality e)) equalities; - prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm); - bag, equalities, cache, maxm + let env = [],context,CicUniv.empty_ugraph in + match + given_clause bag eq_uri env ([],[]) passive active 0 saturation_steps max_time + with + | ParamodulationFailure (_,a,p) -> + a, p, !maxmeta + | ParamodulationSuccess _ -> + assert false ;; -let close_more bag active maxmeta status smart_flag auto cache = - let proof, goalno = status in - let _, metasenv,_,_ = proof in - let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in - let eq_uri = eq_of_goal type_of_goal in - let env = (metasenv, context, CicUniv.empty_ugraph) in - let eq_indexes, equalities, maxm, cache = - Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache - in - prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^ - string_of_int maxm); - List.iter - (fun e -> prerr_endline (Equality.string_of_equality ~env e)) - equalities; - prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; - let equalities = - HExtlib.filter_map - (fun e -> forward_simplify bag eq_uri env e active) - equalities - in - prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>"; - List.iter - (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities; - prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm); - bag, equalities, cache, maxm - -let saturate - smart_flag - dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) - ?(timeout=600.) auto status = - let module C = Cic in - reset_refs (); - maxdepth := depth; - maxwidth := width; -(* CicUnification.unif_ty := false;*) +let all_subsumed bag maxm status active passive = + maxmeta := maxm; let proof, goalno = status in let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in - let eq_uri = eq_of_goal type_of_goal in + let env = metasenv,context,CicUniv.empty_ugraph in let cleaned_goal = Utils.remove_local_context type_of_goal in - Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *) - let ugraph = CicUniv.empty_ugraph in - let env = (metasenv, context, ugraph) in let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in - let bag, equalities, cache, maxm = - find_equalities dbd status smart_flag auto AutoCache.cache_empty - in - let res, time = - maxmeta := maxm+2; - let t1 = Unix.gettimeofday () in - let theorems = - let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in - let t = CicUtil.term_of_uri refl_equal in - let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - [(t, ty, [])], [] - in - let t2 = Unix.gettimeofday () in - let _ = - Utils.debug_print - (lazy - (Printf.sprintf - "Theorems:\n-------------------------------------\n%s\n" - (String.concat "\n" - (List.map - (fun (t, ty, _) -> - Printf.sprintf - "Term: %s, type: %s" - (CicPp.ppterm t) (CicPp.ppterm ty)) - (fst theorems))))); - Utils.debug_print - (lazy - (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); - in - let active = make_empty_active () in - let passive = make_passive equalities in - let start = Unix.gettimeofday () in - let res = -(* - let goals = make_goals goal in - given_clause_fullred dbd env goals theorems passive active -*) - let goals = make_goal_set goal in - let max_iterations = 10000 in - let max_time = Unix.gettimeofday () +. timeout (* minutes *) in - given_clause bag - eq_uri env goals passive active max_iterations max_iterations max_time - in - let finish = Unix.gettimeofday () in - (res, finish -. start) - in - match res with - | ParamodulationFailure (s,_,_) -> - raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s))) - | ParamodulationSuccess - ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),_,_) -> - prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time); - let _,p,gl = - build_proof bag - status goalproof newproof subsumption_id subsumption_subst proof_menv - in - p,gl -;; -(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *) + prerr_endline (string_of_int (List.length (fst active))); + (* we simplify using both actives passives *) + let table = + List.fold_left + (fun (l,tbl) eq -> eq::l,(Indexing.index tbl eq)) + active (list_of_passive passive) in + let _,goal = simplify_goal bag env goal table in + let (_,_,ty) = goal in + prerr_endline (CicPp.ppterm ty); + let subsumed = find_all_subsumed bag env (snd table) goal in + let subsumed_or_id = + match (check_if_goal_is_identity env goal) with + None -> subsumed + | Some id -> id::subsumed in + let res = + List.map + (fun + (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) -> + build_proof bag + status goalproof newproof subsumption_id subsumption_subst proof_menv) + subsumed_or_id in + res, !maxmeta + -(* exported version of given_clause *) let given_clause bag maxm status active passive goal_steps saturation_steps max_time = @@ -1537,6 +1489,7 @@ let given_clause prerr_endline ">>>>>>>>>>>>>>"; let goals = make_goal_set goal in match +(* given_caluse non prende in input maxm ????? *) given_clause bag eq_uri env goals passive active goal_steps saturation_steps max_time with @@ -1551,349 +1504,8 @@ let given_clause Some (subst, proof,gl),a,p, !maxmeta ;; -let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = - let curi,metasenv,pbo,pty = 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 eq_uri = eq_of_goal ty in - let bag, equalities, cache, maxm = - find_equalities dbd (proof,goal) false None AutoCache.cache_empty - in - let table = - List.fold_left - (fun tbl eq -> Indexing.index tbl eq) - Indexing.empty equalities - in - let changed,(newproof,newmetasenv, newty) = - Indexing.demodulation_goal bag - (metasenv,context,CicUniv.empty_ugraph) table initgoal - in - if changed then - begin - let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in - let proofterm,_ = - Equality.build_goal_proof bag - eq_uri newproof opengoal ty [] context metasenv - in - let extended_metasenv = (maxm,context,newty)::metasenv in - let extended_status = - (curi,extended_metasenv,pbo,pty),goal in - let (status,newgoals) = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) - extended_status in - (status,maxm::newgoals) - end - else (* if newty = ty then *) - raise (ProofEngineTypes.Fail (lazy "no progress")) - (*else ProofEngineTypes.apply_tactic - (ReductionTactics.simpl_tac - ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) -;; - -let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);; - -let rec find_in_ctx i name = function - | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name))) - | Some (Cic.Name name', _)::tl when name = name' -> i - | _::tl -> find_in_ctx (i+1) name tl -;; - -let rec position_of i x = function - | [] -> assert false - | j::tl when j <> x -> position_of (i+1) x tl - | _ -> i -;; - -(* Syntax: - * auto superposition target = NAME - * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only] - * - * - if table is omitted no superposition will be performed - * - if demod_table is omitted no demodulation will be prformed - * - subterms_only is passed to Indexing.superposition_right - * - * lists are coded using _ (example: H_H1_H2) - *) - -let superposition_tac ~target ~table ~subterms_only ~demod_table status = - reset_refs(); - let proof,goalno = status in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goalno metasenv in - let eq_uri,tty = eq_and_ty_of_goal ty in - let env = (metasenv, context, CicUniv.empty_ugraph) in - let names = Utils.names_of_context context in - let bag = Equality.mk_equality_bag () in - let eq_index, equalities, maxm,cache = - Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty - in - let eq_what = - let what = find_in_ctx 1 target context in - List.nth equalities (position_of 0 what eq_index) - in - let eq_other = - if table <> "" then - let other = - let others = Str.split (Str.regexp "_") table in - List.map (fun other -> find_in_ctx 1 other context) others - in - List.map - (fun other -> List.nth equalities (position_of 0 other eq_index)) - other - else - [] - in - let index = List.fold_left Indexing.index Indexing.empty eq_other in - let maxm, eql = - if table = "" then maxm,[eq_what] else - Indexing.superposition_right bag - ~subterms_only eq_uri maxm env index eq_what - in - prerr_endline ("Superposition right:"); - prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env); - prerr_endline ("\n table: "); - List.iter (fun e -> prerr_endline (" " ^ Equality.string_of_equality e ~env)) eq_other; - prerr_endline ("\n result: "); - List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; - prerr_endline ("\n result (cut&paste): "); - List.iter - (fun e -> - let t = Equality.term_of_equality eq_uri e in - prerr_endline (CicPp.pp t names)) - eql; - prerr_endline ("\n result proofs: "); - List.iter (fun e -> - prerr_endline (let _,p,_,_,_ = Equality.open_equality e in - let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in - Subst.ppsubst s ^ "\n" ^ - CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql; - if demod_table <> "" then - begin - let eql = - if eql = [] then [eq_what] else eql - in - let demod = - let demod = Str.split (Str.regexp "_") demod_table in - List.map (fun other -> find_in_ctx 1 other context) demod - in - let eq_demod = - List.map - (fun demod -> List.nth equalities (position_of 0 demod eq_index)) - demod - in - let table = List.fold_left Indexing.index Indexing.empty eq_demod in - let maxm,eql = - List.fold_left - (fun (maxm,acc) e -> - let maxm,eq = - Indexing.demodulation_equality bag eq_uri maxm env table e - in - maxm,eq::acc) - (maxm,[]) eql - in - let eql = List.rev eql in - prerr_endline ("\n result [demod]: "); - List.iter - (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; - prerr_endline ("\n result [demod] (cut&paste): "); - List.iter - (fun e -> - let t = Equality.term_of_equality eq_uri e in - prerr_endline (CicPp.pp t names)) - eql; - end; - proof,[goalno] -;; - -let get_stats () = "" -(* - <:show> ^ Indexing.get_stats () ^ Founif.get_stats () ^ - Equality.get_stats () -;; -*) - -(* THINGS USED ONLY BY saturate_main.ml *) - -let main _ _ _ _ _ = () ;; - -let retrieve_and_print dbd term metasenv ugraph = - let module C = Cic in - let module T = CicTypeChecker in - let module PET = ProofEngineTypes in - let module PP = CicPp in - let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in - let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in - let proof, goals = status in - let goal' = List.nth goals 0 in - let uri, metasenv, meta_proof, term_to_prove = proof in - let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in - let eq_uri = eq_of_goal type_of_goal in - let bag = Equality.mk_equality_bag () in - let eq_indexes, equalities, maxm,cache = - Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in - let ugraph = CicUniv.empty_ugraph in - let env = (metasenv, context, ugraph) in - let t1 = Unix.gettimeofday () in - let lib_eq_uris, library_equalities, maxm, cache = - Equality_retrieval.find_library_equalities bag None - false dbd context (proof, goal') (maxm+2) cache - in - let t2 = Unix.gettimeofday () in - maxmeta := maxm+2; - let equalities = (* equalities @ *) library_equalities in - Utils.debug_print - (lazy - (Printf.sprintf "\n\nequalities:\n%s\n" - (String.concat "\n" - (List.map - (fun (u, e) -> -(* Printf.sprintf "%s: %s" *) - (UriManager.string_of_uri u) -(* (string_of_equality e) *) - ) - equalities)))); - Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES..."); - let rec simpl e others others_simpl = - let (u, e) = e in - let active = (others @ others_simpl) in - let tbl = - List.fold_left - (fun t (_, e) -> Indexing.index t e) - Indexing.empty active - in - let res = forward_simplify bag eq_uri env e (active, tbl) in - match others with - | hd::tl -> ( - match res with - | None -> simpl hd tl others_simpl - | Some e -> simpl hd tl ((u, e)::others_simpl) - ) - | [] -> ( - match res with - | None -> others_simpl - | Some e -> (u, e)::others_simpl - ) - in - let _equalities = - match equalities with - | [] -> [] - | hd::tl -> - let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *) - let res = - List.rev (simpl (*(Positive,*) hd others []) - in - Utils.debug_print - (lazy - (Printf.sprintf "\nequalities AFTER:\n%s\n" - (String.concat "\n" - (List.map - (fun (u, e) -> - Printf.sprintf "%s: %s" - (UriManager.string_of_uri u) - (Equality.string_of_equality e) - ) - res)))); - res in - Utils.debug_print - (lazy - (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) -;; - - -let main_demod_equalities dbd term metasenv ugraph = - let module C = Cic in - let module T = CicTypeChecker in - let module PET = ProofEngineTypes in - let module PP = CicPp in - let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in - let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in - let proof, goals = status in - let goal' = List.nth goals 0 in - let _, metasenv, meta_proof, _ = proof in - let _, context, goal = CicUtil.lookup_meta goal' metasenv in - let eq_uri = eq_of_goal goal in - let bag = Equality.mk_equality_bag () in - let eq_indexes, equalities, maxm, cache = - Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in - let lib_eq_uris, library_equalities, maxm,cache = - Equality_retrieval.find_library_equalities bag None - false dbd context (proof, goal') (maxm+2) cache - in - let library_equalities = List.map snd library_equalities in - maxmeta := maxm+2; (* TODO ugly!! *) - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let new_meta_goal, metasenv, type_of_goal = - let _, context, ty = CicUtil.lookup_meta goal' metasenv in - Utils.debug_print - (lazy - (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n" - (CicPp.ppterm ty))); - Cic.Meta (maxm+1, irl), - (maxm+1, context, ty)::metasenv, - ty - in - let env = (metasenv, context, ugraph) in - (*try*) - let goal = [], [], goal - in - let equalities = - simplify_equalities bag eq_uri env (equalities@library_equalities) - in - let active = make_empty_active () in - let passive = make_passive equalities in - Printf.eprintf "\ncontext:\n%s\n" (PP.ppcontext context); - Printf.eprintf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv); - Printf.eprintf "\nequalities:\n%s\n" - (String.concat "\n" - (List.map - (Equality.string_of_equality ~env) equalities)); - prerr_endline "--------------------------------------------------"; - prerr_endline "GO!"; - start_time := Unix.gettimeofday (); - if !time_limit < 1. then time_limit := 60.; - let ra, rp = - saturate_equations bag eq_uri env goal (fun e -> true) passive active - in - - let initial = - List.fold_left (fun s e -> EqualitySet.add e s) - EqualitySet.empty equalities - in - let addfun s e = - if not (EqualitySet.mem e initial) then EqualitySet.add e s else s - in - - let passive = - match rp with - | p, _ -> - EqualitySet.elements (List.fold_left addfun EqualitySet.empty p) - in - let active = - let l = fst ra in - EqualitySet.elements (List.fold_left addfun EqualitySet.empty l) - in - Printf.eprintf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n" - (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) - (* (String.concat "\n" - (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *) -(* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *) - (String.concat "\n" - (List.map - (fun e -> CicPp.ppterm (Equality.term_of_equality eq_uri e)) - passive)); - print_newline (); -(* - with e -> - Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e))) -*) -;; -let saturate_equations eq_uri env goal accept_fun passive active = - let bag = Equality.mk_equality_bag () in - saturate_equations bag eq_uri env goal accept_fun passive active -;; - let add_to_passive eql passives = add_to_passive passives eql eql ;; + + diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli index aa8f24ec3..0c9a75e62 100644 --- a/components/tactics/paramodulation/saturation.mli +++ b/components/tactics/paramodulation/saturation.mli @@ -25,42 +25,40 @@ (* $Id$ *) -val saturate : (* FIXME: should be exported a a tactic *) - bool -> - HMysql.dbd -> - ?full:bool -> - ?depth:int -> - ?width:int -> - ?timeout:float -> - Equality_retrieval.auto_type option -> - ProofEngineTypes.status -> - ProofEngineTypes.proof * ProofEngineTypes.goal list +type passive_table +type active_table = Equality.equality list * Indexing.Index.t + +val reset_refs : unit -> unit -type active_table -type passive_table val make_active: Equality.equality list -> active_table val make_passive: Equality.equality list -> passive_table val add_to_passive: Equality.equality list -> passive_table -> passive_table +val list_of_passive: passive_table -> Equality.equality list -val find_equalities: - HMysql.dbd -> - ProofEngineTypes.status -> - bool -> (* smart_flag *) - Equality_retrieval.auto_type option -> - AutoCache.cache -> - Equality.equality_bag * - Equality.equality list * AutoCache.cache * int - -val close_more: +val simplify_equalities : Equality.equality_bag -> + UriManager.uri -> + Utils.environment -> + Equality.equality list -> + Equality.equality list +val pump_actives : + Cic.context -> + Equality.equality_bag -> + int -> active_table -> - int -> (* maxmeta *) + passive_table -> + int -> + float -> + active_table * passive_table * int +val all_subsumed : + Equality.equality_bag -> + int -> ProofEngineTypes.status -> - bool -> (* smart flag *) - Equality_retrieval.auto_type option -> - AutoCache.cache -> - Equality.equality_bag * Equality.equality list * AutoCache.cache * int - + active_table -> + passive_table -> + (Cic.substitution * + ProofEngineTypes.proof * + ProofEngineTypes.goal list) list * int val given_clause: Equality.equality_bag -> int -> (* maxmeta *) @@ -73,28 +71,4 @@ val given_clause: ProofEngineTypes.goal list) option * active_table * passive_table * int -val demodulate_tac: dbd:HMysql.dbd -> ProofEngineTypes.tactic - -val superposition_tac: - target:string -> table:string -> subterms_only:bool -> - demod_table:string -> ProofEngineTypes.proof * ProofEngineTypes.goal -> - ProofEngineTypes.proof * ProofEngineTypes.goal list -val get_stats: unit -> string - -(* this is used only in saturate_main: MUST BE REMOVED! *) -val weight_age_ratio : int ref -val weight_age_counter: int ref -val symbols_ratio: int ref -val symbols_counter: int ref -val use_fullred: bool ref -val time_limit: float ref -val maxwidth: int ref -val maxdepth: int ref -val retrieve_and_print: - HMysql.dbd -> Cic.term -> Cic.conjecture list -> 'a -> unit -val main_demod_equalities: HMysql.dbd -> - Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit -val main: HMysql.dbd -> - bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit -(* eof *)