From: Enrico Tassi Date: Wed, 27 Sep 2006 16:20:40 +0000 (+0000) Subject: auto snapshot X-Git-Tag: make_still_working~6842 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=041ad23b567b9844ec187ad436595868441802f4;p=helm.git auto snapshot --- diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml index 33ecea7ce..9d6914847 100644 --- a/helm/software/components/cic/discrimination_tree.ml +++ b/helm/software/components/cic/discrimination_tree.ml @@ -242,6 +242,10 @@ let remove_index tree equality = | term -> term ;; + let rec skip_prods = function + | Cic.Prod (_,_,t) -> skip_prods t + | term -> term + ;; let rec subterm_at_pos pos term = match pos with @@ -287,6 +291,7 @@ let remove_index tree equality = ;; let retrieve_generalizations (tree,arity) term = + let term = skip_prods term in let rec retrieve tree term pos = match tree with | DiscriminationTree.Node (Some s, _) when pos = [] -> s @@ -347,6 +352,7 @@ let remove_index tree equality = let retrieve_unifiables (tree,arities) term = + let term = skip_prods term in let rec retrieve tree term pos = match tree with | DiscriminationTree.Node (Some s, _) when pos = [] -> s diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 380c50f51..04154280b 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -8,15 +8,15 @@ metadataQuery.cmi: proofEngineTypes.cmi autoTypes.cmi: proofEngineTypes.cmi paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi -paramodulation/inference.cmi: paramodulation/utils.cmi \ - paramodulation/subst.cmi proofEngineTypes.cmi paramodulation/equality.cmi \ - autoTypes.cmi +paramodulation/inference.cmi: paramodulation/subst.cmi proofEngineTypes.cmi \ + paramodulation/equality.cmi autoTypes.cmi paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/indexing.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/equality_indexing.cmi \ paramodulation/equality.cmi -paramodulation/saturation.cmi: proofEngineTypes.cmi autoTypes.cmi +paramodulation/saturation.cmi: proofEngineTypes.cmi \ + paramodulation/inference.cmi paramodulation/equality.cmi autoTypes.cmi variousTactics.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi @@ -63,8 +63,8 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ hashtbl_equiv.cmi metadataQuery.cmi metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi -autoTypes.cmo: metadataQuery.cmi paramodulation/equality.cmi autoTypes.cmi -autoTypes.cmx: metadataQuery.cmx paramodulation/equality.cmx autoTypes.cmi +autoTypes.cmo: metadataQuery.cmi autoTypes.cmi +autoTypes.cmx: metadataQuery.cmx autoTypes.cmi paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi paramodulation/subst.cmo: paramodulation/subst.cmi @@ -98,12 +98,12 @@ paramodulation/indexing.cmx: paramodulation/utils.cmx \ paramodulation/saturation.cmo: paramodulation/utils.cmi \ paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/inference.cmi \ - paramodulation/indexing.cmi paramodulation/equality.cmi \ + paramodulation/indexing.cmi paramodulation/equality.cmi autoTypes.cmi \ paramodulation/saturation.cmi paramodulation/saturation.cmx: paramodulation/utils.cmx \ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/inference.cmx \ - paramodulation/indexing.cmx paramodulation/equality.cmx \ + paramodulation/indexing.cmx paramodulation/equality.cmx autoTypes.cmx \ paramodulation/saturation.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ @@ -133,22 +133,26 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineReduction.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ equalityTactics.cmi -auto.cmo: proofEngineTypes.cmi primitiveTactics.cmi autoTypes.cmi auto.cmi -auto.cmx: proofEngineTypes.cmx primitiveTactics.cmx autoTypes.cmx auto.cmi -autoTactic.cmo: tacticals.cmi paramodulation/saturation.cmi \ - proofEngineTypes.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ - metadataQuery.cmi equalityTactics.cmi paramodulation/equality.cmi \ - autoTypes.cmi auto.cmi autoTactic.cmi -autoTactic.cmx: tacticals.cmx paramodulation/saturation.cmx \ - proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ - metadataQuery.cmx equalityTactics.cmx paramodulation/equality.cmx \ - autoTypes.cmx auto.cmx autoTactic.cmi +auto.cmo: tacticals.cmi paramodulation/saturation.cmi proofEngineTypes.cmi \ + proofEngineHelpers.cmi primitiveTactics.cmi equalityTactics.cmi \ + autoTypes.cmi auto.cmi +auto.cmx: tacticals.cmx paramodulation/saturation.cmx proofEngineTypes.cmx \ + proofEngineHelpers.cmx primitiveTactics.cmx equalityTactics.cmx \ + autoTypes.cmx auto.cmi +autoTactic.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \ + proofEngineHelpers.cmi primitiveTactics.cmi metadataQuery.cmi \ + paramodulation/equality.cmi autoTypes.cmi auto.cmi autoTactic.cmi +autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \ + proofEngineHelpers.cmx primitiveTactics.cmx metadataQuery.cmx \ + paramodulation/equality.cmx autoTypes.cmx auto.cmx autoTactic.cmi discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ - proofEngineTypes.cmi primitiveTactics.cmi introductionTactics.cmi \ - equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi + proofEngineTypes.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \ + introductionTactics.cmi equalityTactics.cmi eliminationTactics.cmi \ + discriminationTactics.cmi discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \ - proofEngineTypes.cmx primitiveTactics.cmx introductionTactics.cmx \ - equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi + proofEngineTypes.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \ + introductionTactics.cmx equalityTactics.cmx eliminationTactics.cmx \ + discriminationTactics.cmi inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ equalityTactics.cmi inversion.cmi @@ -192,13 +196,13 @@ tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi \ proofEngineStructuralRules.cmi primitiveTactics.cmi negationTactics.cmi \ inversion.cmi introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ - autoTactic.cmi tactics.cmi + autoTactic.cmi auto.cmi tactics.cmi tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx \ paramodulation/saturation.cmx ring.cmx reductionTactics.cmx \ proofEngineStructuralRules.cmx primitiveTactics.cmx negationTactics.cmx \ inversion.cmx introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ - autoTactic.cmx tactics.cmi + autoTactic.cmx auto.cmx tactics.cmi declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \ diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index e377b6368..6b1bf82ab 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -25,7 +25,156 @@ open AutoTypes;; -let debug_print s = ();;(*prerr_endline s;;*) +let debug_print s = () (* prerr_endline s;; *) + +let given_clause dbd ?tables maxm ?auto cache subst flags status = + prerr_endline ("given_clause " ^ string_of_int maxm); + let active, passive, bag, cache, maxmeta, goal_steps, saturation_steps, timeout = + match tables with + | None -> + let bag, equalities, cache, maxmeta = + Saturation.find_equalities dbd status ?auto true 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) -> + let bag, equalities, cache, maxm = + if cache_size oldcache <> cache_size cache then + Saturation.saturate_more bag active maxm status true ?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 30 minsteps, minsteps, infinity + in + active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout + in + let res,a,p, maxmeta = + Saturation.given_clause bag maxmeta status active passive + goal_steps saturation_steps timeout + in + res,a,p,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 = AutoTypes.cache_empty, AutoTypes.default_flags() in + let flags = + {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} + in + given_clause dbd ?tables 0 cache [] flags (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 +192,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 +256,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 (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 universe += + let candidates = get_candidates universe 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, maxm ;; (* Works if there is no dependency over proofs *) @@ -125,40 +330,79 @@ 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 + 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 universe = + let callback_for_paramod maxm flags proof commonctx cache l = + let flags = {flags with use_paramod = false} in + let _,metasenv,_,_ = proof in + let oldmetasenv = metasenv in + match + auto_all_solutions + dbd tables maxm universe 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 -> + match aux_single tables maxm cache metasenv subst elem goalty cc with + | Fail _, tables, cache, maxm' -> + assert(maxm' >= maxm);let maxm = maxm' in 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 -> + 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 +410,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 +426,20 @@ 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",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 +447,88 @@ 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 -> + let elems, tables, maxm = + applicative_case dbd tables maxm depth subst fake_proof goalno + goalty metasenv context universe + in elems, tables, cache, maxm + else + let elems, tables, maxm = + applicative_case dbd tables maxm depth subst fake_proof goalno + goalty metasenv context universe + in elems, tables, cache, maxm 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 universe 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 universe 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 universe cache context metasenv gl flags = + let solutions, cache, _ = + auto_all_solutions dbd None 0 universe cache context metasenv gl flags + in + solutions, cache +;; + +let auto dbd universe 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 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 universe with + | Success (metasenv,subst,_), tables,cache,_ -> Some (subst,metasenv), cache + | Fail s,tables,cache,maxm -> + let cache = cache_clean cache in + match auto_main dbd tables maxm context flags elems cache universe with + | Success (metasenv,subst,_), tables,cache,_ -> + Some (subst,metasenv), cache + | Fail s,tables,cache,maxm -> prerr_endline s;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)) + diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli index 7150a1246..68057fa9c 100644 --- a/helm/software/components/tactics/auto.mli +++ b/helm/software/components/tactics/auto.mli @@ -25,6 +25,7 @@ (* stops at the first solution *) val auto: + HMysql.dbd -> AutoTypes.universe -> AutoTypes.cache -> Cic.context -> @@ -34,6 +35,7 @@ val auto: (Cic.substitution * Cic.metasenv) option * AutoTypes.cache val auto_all_solutions: + HMysql.dbd -> AutoTypes.universe -> AutoTypes.cache -> Cic.context -> @@ -41,3 +43,6 @@ val auto_all_solutions: ProofEngineTypes.goal list -> AutoTypes.flags -> (Cic.substitution * Cic.metasenv) list * AutoTypes.cache + +val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic + diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml index 61d078c22..03fdf9555 100644 --- a/helm/software/components/tactics/autoTactic.ml +++ b/helm/software/components/tactics/autoTactic.ml @@ -266,123 +266,46 @@ and auto_new_aux dbd width already_seen_goals universe = function | _ -> assert false ;; -let default_depth = 5 -let default_width = 3 - -(* -let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) - () -= - let auto_tac dbd (proof,goal) = - let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in - Hashtbl.clear inspected_goals; - debug_print (lazy "Entro in Auto"); - let id t = t in - let t1 = Unix.gettimeofday () in - match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with - [] -> debug_print (lazy "Auto failed"); - raise (ProofEngineTypes.Fail "No Applicable theorem") - | (_,(proof,[],_))::_ -> - let t2 = Unix.gettimeofday () in - debug_print (lazy "AUTO_TAC HA FINITO"); - let _,_,p,_ = proof in - debug_print (lazy (CicPp.ppterm p)); - Printf.printf "tempo: %.9f\n" (t2 -. t1); - (proof,[]) - | _ -> assert false - in - ProofEngineTypes.mk_tactic (auto_tac dbd) -;; -*) - -(* -let paramodulation_tactic = ref - (fun dbd ?full ?depth ?width status -> - raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));; - -let term_is_equality = ref - (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);; -*) - -let bool name params = - try let _ = List.assoc name params in true with - | Not_found -> false +let bool params name default = + try + let s = List.assoc name params in + if s = "" || s = "1" || s = "true" || s = "yes" then true + else if s = "0" || s = "false" || s = "no" then false + else + let msg = "Unrecognized value for parameter "^name^"\n" in + let msg = msg ^ "Accepted values are 1,true,yes and 0,false,no" in + raise (ProofEngineTypes.Fail (lazy msg)) + with Not_found -> default ;; -let string name params = +let string params name default = try List.assoc name params with - | Not_found -> "" + | Not_found -> default ;; -let int name default params = +let int params name default = try int_of_string (List.assoc name params) with | Not_found -> default | Failure _ -> raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) ;; -(* -let callback_for_paramodulation dbd width depth t l = - let _,y,x,xx = t in - let universe = MetadataQuery.universe_of_goals ~dbd t l in - let todo = List.map (fun g -> (g, depth)) l in - prerr_endline ("AUTO: " ^ CicPp.ppterm x ^ " : " ^ CicPp.ppterm xx); - prerr_endline ("MENV: " ^ CicMetaSubst.ppmetasenv [] y); - match auto_new dbd width [] universe [(fun x -> x), (t, todo, None)] with - | (_,(proof,[],_))::_ -> proof - | _ -> raise (Failure "xxx") -;; -*) - -let callback_for_paramodulation dbd flags proof commonctx ?universe cache l = - let _,metasenv,_,_ = proof in - let oldmetasenv = metasenv in - let universe = - match universe with - | Some u -> u - | None -> - let universe = - AutoTypes.universe_of_goals dbd proof l AutoTypes.empty_universe - in - AutoTypes.universe_of_context commonctx metasenv universe - in - match - Auto.auto_all_solutions universe cache commonctx metasenv l flags - with - | [],cache -> [],cache,universe - | solutions,cache -> - let solutions = - HExtlib.filter_map - (fun (subst,metasenv) -> - let opened = - ProofEngineHelpers.compare_metasenvs - ~oldmetasenv ~newmetasenv:metasenv - in - if opened = [] then - Some subst - else - None) - solutions - in - solutions,cache,universe -;; - let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = (* argument parsing *) - let depth = int "depth" AutoTypes.default_flags.AutoTypes.maxdepth params in - let width = int "width" AutoTypes.default_flags.AutoTypes.maxwidth params in - let timeout = string "timeout" params in - let paramodulation = bool "paramodulation" params in - let full = bool "full" params in - let superposition = bool "superposition" params in - let target = string "target" params in - let table = string "table" params in - let subterms_only = bool "subterms_only" params in - let caso_strano = bool "caso_strano" params in - let demod_table = string "demod_table" params in - let timeout = - try Some (float_of_string timeout) with Failure _ -> None - in + let int = int params + and string = string params + and bool = bool params in + let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in + let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in + let timeout = int "timeout" 0 in + let use_paramod = bool "use_paramod" true in + let use_only_paramod = bool "paramodulation" false in + (* hacks to debug paramod *) + let superposition = bool "superposition" false in + let target = string "target" "" in + let table = string "table" "" in + let subterms_only = bool "subterms_only" false in + let demod_table = string "demod_table" "" in match superposition with | true -> (* this is the ugly hack to debug paramod *) @@ -392,166 +315,38 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = (* this is the real auto *) let _, metasenv, _, _ = proof in let _, context, goalty = CicUtil.lookup_meta goal metasenv in - let use_paramodulation = - paramodulation && Equality.term_is_equality goalty + let universe = + AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe + in + let universe = AutoTypes.universe_of_context context metasenv universe in + let oldmetasenv = metasenv in + let flags = { + AutoTypes.maxdepth = depth; + AutoTypes.maxwidth = width; + AutoTypes.timeout = + if timeout = 0 then float_of_int timeout + else Unix.gettimeofday() +. (float_of_int timeout); + AutoTypes.use_paramod = use_paramod; + AutoTypes.use_only_paramod = use_only_paramod} in - if use_paramodulation then - try - let rc = - Saturation.saturate - ~auto:(callback_for_paramodulation dbd) - caso_strano dbd ~depth ~width ~full - ?timeout (proof, goal) + let cache = AutoTypes.cache_empty in + match Auto.auto dbd universe cache context metasenv [goal] flags with + | None,cache -> + raise (ProofEngineTypes.Fail (lazy "Auto gave up")) + | Some (subst,metasenv),cache -> + let proof,metasenv = + ProofEngineHelpers.subst_meta_and_metasenv_in_proof + proof goal (CicMetaSubst.apply_subst subst) metasenv in - prerr_endline (Saturation.get_stats ());rc - with exn -> - prerr_endline (Saturation.get_stats ());raise exn - else - let universe = - AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe - in - let universe = (* we should get back a menv too XXX *) - AutoTypes.universe_of_context context metasenv universe - in - let oldmetasenv = metasenv in - match - Auto.auto universe AutoTypes.cache_empty context metasenv [goal] - {AutoTypes.default_flags with - AutoTypes.maxdepth = depth; - AutoTypes.maxwidth = width; -(* AutoTypes.timeout = 0; *) - } - with - | None,cache -> - raise (ProofEngineTypes.Fail (lazy "Auto gave up")) - | Some (subst,metasenv),cache -> - 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 + let opened = + ProofEngineHelpers.compare_metasenvs ~oldmetasenv + ~newmetasenv:metasenv + in + proof,opened ;; let auto_tac ~params ~dbd = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd) ;; -(* {{{ **************** applyS *******************) - -let new_metasenv_and_unify_and_t dbd proof goal 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',metasenv = - let (puri,metasenv,pbo,pty) = proof in - (puri,newmetasenv,pbo,pty),metasenv - in - let proof'',goals = - match LibraryObjects.eq_URI () with - | Some uri -> - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*)) - ~continuation: - (PrimitiveTactics.cut_tac - (CicSubstitution.lift 1 - (Cic.Appl - [Cic.MutInd (uri,0,[]); - Cic.Sort Cic.Prop; - consthead; - ty])))) (proof',goal) - | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined")) - in - match goals with - [g1;g2] -> - let proof'',goals = - ProofEngineTypes.apply_tactic - (auto_tac ~params:["caso_strano","on";"paramodulation","on"] ~dbd) (proof'',g2) - in - let proof'',goals = - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft - ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1)) - ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) - ) (proof'',g1) - in - proof'', - (*CSC: Brrrr.... *) - ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv - ~newmetasenv:(let _,m,_,_ = proof'' in m) - | _ -> assert false - -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 applyS_tac ~dbd ~term (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 = ProofEngineHelpers.new_meta_of_proof ~proof 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 res = - new_metasenv_and_unify_and_t dbd proof goal - newmeta' metasenv' context term' ty termty goal_arity - in - res - -let applyS_tac ~dbd ~term = - ProofEngineTypes.mk_tactic - (fun status -> - try applyS_tac ~dbd ~term status - with - | CicUnification.UnificationFailure msg - | CicTypeChecker.TypeCheckerFailure msg -> - raise (ProofEngineTypes.Fail msg)) - -(* }}} ********************************) - let pp_proofterm = Equality.pp_proofterm;; diff --git a/helm/software/components/tactics/autoTactic.mli b/helm/software/components/tactics/autoTactic.mli index 354b1b738..fadb603eb 100644 --- a/helm/software/components/tactics/autoTactic.mli +++ b/helm/software/components/tactics/autoTactic.mli @@ -29,6 +29,4 @@ val auto_tac: dbd:HMysql.dbd -> ProofEngineTypes.tactic -val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic - val pp_proofterm: Cic.term -> string diff --git a/helm/software/components/tactics/autoTypes.ml b/helm/software/components/tactics/autoTypes.ml index f9d6a0216..60643d870 100644 --- a/helm/software/components/tactics/autoTypes.ml +++ b/helm/software/components/tactics/autoTypes.ml @@ -84,6 +84,9 @@ let universe_of_context ctx metasenv universe = in rc ;; +let add_to_universe key proof universe = + index universe key proof +;; (* (proof,ty) list *) type cache_key = Cic.term @@ -126,18 +129,33 @@ let cache_add_underinspection cache cache_key depth = | Succeded _ -> assert false (* it must be a new goal *) ;; let cache_empty = [] +let cache_print context cache = + let names = List.map (function None -> None | Some (x,_) -> Some x) context in + String.concat "\n" + (HExtlib.filter_map + (function + | (k,Succeded _) -> Some (CicPp.pp k names) + | _ -> None) + cache) +;; +let cache_size cache = + List.length (List.filter (function (_,Succeded _) -> true | _ -> false) cache) +;; +let cache_clean cache = + List.filter (function (_,Succeded _) -> true | _ -> false) cache +;; type flags = { maxwidth: int; maxdepth: int; timeout: float; + use_paramod: bool; + use_only_paramod : bool; } -let default_flags = { - maxwidth = 3; - maxdepth = 5; - timeout = 0.; -} +let default_flags _ = + {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +. 3.0;use_paramod=true;use_only_paramod=false} +;; (* (metasenv, subst, (metano,depth)list *) type sort = P | T;; diff --git a/helm/software/components/tactics/autoTypes.mli b/helm/software/components/tactics/autoTypes.mli index c580bff39..1cf966ca0 100644 --- a/helm/software/components/tactics/autoTypes.mli +++ b/helm/software/components/tactics/autoTypes.mli @@ -30,6 +30,7 @@ val universe_of_goals: HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list -> universe -> universe val universe_of_context: Cic.context -> Cic.metasenv -> universe -> universe +val add_to_universe: Cic.term -> Cic.term -> universe -> universe type cache type cache_key = Cic.term @@ -43,14 +44,19 @@ val cache_add_failure: cache -> cache_key -> int -> cache val cache_add_success: cache -> cache_key -> Cic.term -> cache val cache_add_underinspection: cache -> cache_key -> int -> cache val cache_empty: cache +val cache_print: Cic.context -> cache -> string +val cache_size: cache -> int +val cache_clean: cache -> cache type flags = { maxwidth: int; maxdepth: int; timeout: float; + use_paramod: bool; + use_only_paramod : bool; } -val default_flags : flags +val default_flags : unit -> flags (* (metasenv, subst, (metano,depth)list *) type sort = P | T;; diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml index 0dc19582a..cd14f3f5e 100644 --- a/helm/software/components/tactics/metadataQuery.ml +++ b/helm/software/components/tactics/metadataQuery.ml @@ -207,6 +207,14 @@ let is_predicate u = check_last_pi ty ;; +let only constants uri = + prerr_endline (UriManager.string_of_uri uri); + let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *) + let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + let consts = Constr.constants_of ty in + Constr.UriManagerSet.subset consts constants +;; + let universe_of_goals ~(dbd:HMysql.dbd) proof goals = let (_, metasenv, _, _) = proof in let add_uris_for acc goal = @@ -245,6 +253,7 @@ let universe_of_goals ~(dbd:HMysql.dbd) proof goals = *) let uris = List.filter nonvar (List.map snd uris) in let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in + let uris = List.filter (only all_constants_closed) uris in uris ;; diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 2c287d563..cfef9452f 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -29,6 +29,7 @@ type rule = SuperpositionRight | SuperpositionLeft | Demodulation type uncomparable = int -> int + type equality = uncomparable * (* trick to break structural equality *) int * (* weight *) @@ -45,29 +46,29 @@ and proof = (* subst, (rule,eq1, eq2,predicate) *) and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list ;; +type equality_bag = (int,equality) Hashtbl.t * int ref type goal = goal_proof * Cic.metasenv * Cic.term (* globals *) -let maxid = ref 0;; -let id_to_eq = Hashtbl.create 1024;; +let mk_equality_bag () = + Hashtbl.create 1024, ref 0 +;; -let freshid () = - incr maxid; !maxid +let freshid (_,i) = + incr i; !i ;; -let reset () = - maxid := 0; - Hashtbl.clear id_to_eq +let add_to_bag (id_to_eq,_) id eq = + Hashtbl.add id_to_eq id eq ;; let uncomparable = fun _ -> 0 -let mk_equality (weight,p,(ty,l,r,o),m) = - let id = freshid () in +let mk_equality bag (weight,p,(ty,l,r,o),m) = + let id = freshid bag in let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in - Hashtbl.add id_to_eq id eq; - + add_to_bag bag id eq; eq ;; @@ -111,7 +112,7 @@ let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) = Pervasives.compare s1 s2 ;; -let rec max_weight_in_proof current = +let rec max_weight_in_proof ((id_to_eq,_) as bag) current = function | Exact _ -> current | Step (_, (_,id1,(_,id2),_)) -> @@ -120,23 +121,23 @@ let rec max_weight_in_proof current = let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in let current = max current w1 in - let current = max_weight_in_proof current p1 in + let current = max_weight_in_proof bag current p1 in let current = max current w2 in - max_weight_in_proof current p2 + max_weight_in_proof bag current p2 -let max_weight_in_goal_proof = +let max_weight_in_goal_proof ((id_to_eq,_) as bag) = List.fold_left (fun current (_,_,id,_,_) -> let eq = Hashtbl.find id_to_eq id in let (w,p,(_,_,_,_),_,_) = open_equality eq in let current = max current w in - max_weight_in_proof current p) + max_weight_in_proof bag current p) -let max_weight goal_proof proof = - let current = max_weight_in_proof 0 proof in - max_weight_in_goal_proof current goal_proof +let max_weight bag goal_proof proof = + let current = max_weight_in_proof bag 0 proof in + max_weight_in_goal_proof bag current goal_proof -let proof_of_id id = +let proof_of_id (id_to_eq,_) id = try let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in p,l,r @@ -144,7 +145,7 @@ let proof_of_id id = Not_found -> assert false -let string_of_proof ?(names=[]) p gp = +let string_of_proof ?(names=[]) bag p gp = let str_of_pos = function | Utils.Left -> "left" | Utils.Right -> "right" @@ -159,8 +160,8 @@ let string_of_proof ?(names=[]) p gp = Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n" prefix (string_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) (CicPp.pp pred names)^ - aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ - aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) + aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id bag eq1)) ^ + aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id bag eq2)) in aux 0 "" p ^ String.concat "\n" @@ -169,11 +170,11 @@ let string_of_proof ?(names=[]) p gp = (Printf.sprintf "GOAL: %s %s %d %s %s\n" (string_of_rule r) (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^ - aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i))) + aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id bag i))) gp) ;; -let rec depend eq id seen = +let rec depend ((id_to_eq,_) as bag) eq id seen = let (_,p,(_,_,_,_),_,ideq) = open_equality eq in if List.mem ideq seen then false,seen @@ -187,11 +188,11 @@ let rec depend eq id seen = let seen = ideq::seen in let eq1 = Hashtbl.find id_to_eq id1 in let eq2 = Hashtbl.find id_to_eq id2 in - let b1,seen = depend eq1 id seen in - if b1 then b1,seen else depend eq2 id seen + let b1,seen = depend bag eq1 id seen in + if b1 then b1,seen else depend bag eq2 id seen ;; -let depend eq id = fst (depend eq id []);; +let depend bag eq id = fst (depend bag eq id []);; let ppsubst = Subst.ppsubst ~names:[];; @@ -612,9 +613,9 @@ let parametrize_proof p l r ty = proof, instance ;; -let wfo goalproof proof id = +let wfo bag goalproof proof id = let rec aux acc id = - let p,_,_ = proof_of_id id in + let p,_,_ = proof_of_id bag id in match p with | Exact _ -> if (List.mem id acc) then acc else id :: acc | Step (_,(_,id1, (_,id2), _)) -> @@ -630,7 +631,7 @@ let wfo goalproof proof id = List.fold_left (fun acc (_,_,id,_,_) -> aux acc id) acc goalproof ;; -let string_of_id names id = +let string_of_id (id_to_eq,_) names id = if id = 0 then "" else try let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in @@ -649,8 +650,8 @@ let string_of_id names id = with Not_found -> assert false -let pp_proof names goalproof proof subst id initial_goal = - String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof id)) ^ +let pp_proof bag names goalproof proof subst id initial_goal = + String.concat "\n" (List.map (string_of_id bag names) (wfo bag goalproof proof id)) ^ "\ngoal:\n " ^ (String.concat "\n " (fst (List.fold_right @@ -675,24 +676,24 @@ module OT = module M = Map.Make(OT) -let rec find_deps m i = +let rec find_deps bag m i = if M.mem i m then m else - let p,_,_ = proof_of_id i in + let p,_,_ = proof_of_id bag i in match p with | Exact _ -> M.add i [] m | Step (_,(_,id1,(_,id2),_)) -> - let m = find_deps m id1 in - let m = find_deps m id2 in + let m = find_deps bag m id1 in + let m = find_deps bag m id2 in (* without the uniq there is a stack overflow doing concatenation *) let xxx = [id1;id2] @ M.find id1 m @ M.find id2 m in let xxx = HExtlib.list_uniq (List.sort Pervasives.compare xxx) in M.add i xxx m ;; -let topological_sort l = +let topological_sort bag l = (* build the partial order relation *) - let m = List.fold_left (fun m i -> find_deps m i) M.empty l in + let m = List.fold_left (fun m i -> find_deps bag m i) M.empty l in let m = (* keep only deps inside l *) List.fold_left (fun m' i -> @@ -724,14 +725,14 @@ let topological_sort l = (* returns the list of ids that should be factorized *) -let get_duplicate_step_in_wfo l p = +let get_duplicate_step_in_wfo bag l p = let ol = List.rev l in let h = Hashtbl.create 13 in (* NOTE: here the n parameter is an approximation of the dependency between equations. To do things seriously we should maintain a dependency graph. This approximation is not perfect. *) let add i = - let p,_,_ = proof_of_id i in + let p,_,_ = proof_of_id bag i in match p with | Exact _ -> true | _ -> @@ -746,23 +747,23 @@ let get_duplicate_step_in_wfo l p = | Step (_,(_,i1,(_,i2),_)) -> let go_on_1 = add i1 in let go_on_2 = add i2 in - if go_on_1 then aux (let p,_,_ = proof_of_id i1 in p); - if go_on_2 then aux (let p,_,_ = proof_of_id i2 in p) + if go_on_1 then aux (let p,_,_ = proof_of_id bag i1 in p); + if go_on_2 then aux (let p,_,_ = proof_of_id bag i2 in p) in aux p; List.iter - (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id id in p)) + (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id bag id in p)) ol; (* now h is complete *) let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in let proofs = List.filter (fun (_,c) -> c > 1) proofs in - let res = topological_sort (List.map (fun (i,_) -> i) proofs) in + let res = topological_sort bag (List.map (fun (i,_) -> i) proofs) in res ;; -let build_proof_term eq h lift proof = +let build_proof_term bag eq h lift proof = let proof_of_id aux id = - let p,l,r = proof_of_id id in + let p,l,r = proof_of_id bag id in try List.assoc id h,l,r with Not_found -> aux p, l, r in let rec aux = function @@ -792,17 +793,17 @@ let build_proof_term eq h lift proof = aux proof ;; -let build_goal_proof eq l initial ty se context menv = +let build_goal_proof bag eq l initial ty se context menv = let se = List.map (fun i -> Cic.Meta (i,[])) se in - let lets = get_duplicate_step_in_wfo l initial in + let lets = get_duplicate_step_in_wfo bag l initial in let letsno = List.length lets in let _,mty,_,_ = open_eq ty in let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in let lets,_,h = List.fold_left (fun (acc,n,h) id -> - let p,l,r = proof_of_id id in - let cic = build_proof_term eq h n p in + let p,l,r = proof_of_id bag id in + let cic = build_proof_term bag eq h n p in let real_cic,instance = parametrize_proof cic l r (CicSubstitution.lift n mty) in @@ -814,8 +815,8 @@ let build_goal_proof eq l initial ty se context menv = let rec aux se current_proof = function | [] -> current_proof,se | (rule,pos,id,subst,pred)::tl -> - let p,l,r = proof_of_id id in - let p = build_proof_term eq h letsno p in + let p,l,r = proof_of_id bag id in + let p = build_proof_term bag eq h letsno p in let pos = if pos = Utils.Left then Utils.Right else Utils.Left in let varname = match rule with @@ -833,9 +834,9 @@ let build_goal_proof eq l initial ty se context menv = in let proof,se = aux se proof tl in Subst.apply_subst_lift letsno subst proof, - List.map (fun x -> Subst.apply_subst_lift letsno subst x) se + List.map (fun x -> Subst.apply_subst(*_lift letsno*) subst x) se in - aux se (build_proof_term eq h letsno initial) l + aux se (build_proof_term bag eq h letsno initial) l in let n,proof = let initial = proof in @@ -857,7 +858,7 @@ let refl_proof eq_uri ty term = Cic.Appl [Cic.MutConstruct (eq_uri, 0, 1, []); ty; term] ;; -let metas_of_proof p = +let metas_of_proof bag p = let eq = match LibraryObjects.eq_URI () with | Some u -> u @@ -866,7 +867,7 @@ let metas_of_proof p = (ProofEngineTypes.Fail (lazy "No default equality defined when calling metas_of_proof")) in - let p = build_proof_term eq [] 0 p in + let p = build_proof_term bag eq [] 0 p in Utils.metas_of_term p ;; @@ -908,7 +909,7 @@ let fix_metas_goal newmeta goal = newmeta+1,(proof, menv, ty) ;; -let fix_metas newmeta eq = +let fix_metas bag newmeta eq = let w, p, (ty, left, right, o), menv,_ = open_equality eq in let to_be_relocated = (* List.map (fun i ,_,_ -> i) menv *) @@ -926,7 +927,7 @@ let fix_metas newmeta eq = Step (Subst.concat s subst,(r,id1,(pos,id2), pred)) in let p = fix_proof p in - let eq' = mk_equality (w, p, (ty, left, right, o), metasenv) in + let eq' = mk_equality bag (w, p, (ty, left, right, o), metasenv) in newmeta+1, eq' exception NotMetaConvertible;; @@ -1066,14 +1067,14 @@ let term_is_equality term = | _ -> false ;; -let equality_of_term proof term = +let equality_of_term bag proof term = match term with | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when LibraryObjects.is_eq_URI uri -> let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = Utils.compute_equality_weight stat in - let e = mk_equality (w, Exact proof, stat,[]) in + let e = mk_equality bag (w, Exact proof, stat,[]) in e | _ -> raise TermIsNotAnEquality @@ -1114,7 +1115,7 @@ let term_of_equality eq_uri equality = menv (argsno, t)) ;; -let symmetric eq_ty l id uri m = +let symmetric bag eq_ty l id uri m = let eq = Cic.MutInd(uri,0,[]) in let pred = Cic.Lambda (Cic.Name "Sym",eq_ty, @@ -1127,7 +1128,7 @@ let symmetric eq_ty l id uri m = [Cic.MutConstruct(uri,0,1,[]);eq_ty;l]) in let id1 = - let eq = mk_equality (0,prefl,(eq_ty,l,l,Utils.Eq),m) in + let eq = mk_equality bag (0,prefl,(eq_ty,l,l,Utils.Eq),m) in let (_,_,_,_,id) = open_equality eq in id in @@ -1144,10 +1145,10 @@ module IntSet = Set.Make(IntOT);; let n_purged = ref 0;; -let collect alive1 alive2 alive3 = +let collect ((id_to_eq,_) as bag) alive1 alive2 alive3 = (* let _ = <:start> in *) let deps_of id = - let p,_,_ = proof_of_id id in + let p,_,_ = proof_of_id bag id in match p with | Exact _ -> IntSet.empty | Step (_,(_,id1,(_,id2),_)) -> diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli index 1a909dfc4..bd3d4c2ac 100644 --- a/helm/software/components/tactics/paramodulation/equality.mli +++ b/helm/software/components/tactics/paramodulation/equality.mli @@ -25,6 +25,10 @@ type rule = SuperpositionRight | SuperpositionLeft | Demodulation +type equality_bag + +val mk_equality_bag: unit -> equality_bag + type equality and proof = @@ -36,21 +40,20 @@ and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list type goal = goal_proof * Cic.metasenv * Cic.term val pp_proof: + equality_bag -> (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int -> Cic.term -> string val pp_proofterm: Cic.term -> string -val reset : unit -> unit - val mk_equality : - int * proof * + equality_bag -> int * proof * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> equality val mk_tmp_equality : - int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> + int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> equality val open_equality : @@ -58,28 +61,31 @@ val open_equality : int * proof * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv * int -val depend : equality -> int -> bool +val depend : equality_bag -> equality -> int -> bool val compare : equality -> equality -> int -val max_weight_in_proof : int-> proof -> int -val max_weight : goal_proof -> proof -> int -val string_of_equality : ?env:Utils.environment -> equality -> string +val max_weight_in_proof : equality_bag -> int -> proof -> int +val max_weight : equality_bag -> goal_proof -> proof -> int +val string_of_equality : + ?env:Utils.environment -> equality -> string val string_of_proof : - ?names:(Cic.name option)list -> proof -> goal_proof -> string + ?names:(Cic.name option)list -> equality_bag -> proof -> goal_proof -> string (* given a proof and a list of meta indexes we are interested in the * instantiation gives back the cic proof and the list of instantiations *) (* build_goal_proof [eq_URI] [goal_proof] [initial_proof] [ty] * [ty] is the type of the goal *) val build_goal_proof: + equality_bag -> UriManager.uri -> goal_proof -> proof -> Cic.term-> int list -> Cic.context -> Cic.metasenv -> Cic.term * Cic.term list -val build_proof_term : +val build_proof_term : + equality_bag -> UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term (** ensures that metavariables in equality are unique *) val fix_metas_goal: int -> goal -> int * goal -val fix_metas: int -> equality -> int * equality -val metas_of_proof: proof -> int list +val fix_metas: equality_bag -> int -> equality -> int * equality +val metas_of_proof: equality_bag -> proof -> int list (* this should be used _only_ to apply (efficiently) this subst on the * initial proof passed to build_goal_proof *) @@ -90,7 +96,7 @@ exception TermIsNotAnEquality;; raises TermIsNotAnEquality if term is not an equation. The first Cic.term is a proof of the equation *) -val equality_of_term: Cic.term -> Cic.term -> equality +val equality_of_term: equality_bag -> Cic.term -> Cic.term -> equality (** Re-builds the term corresponding to this equality @@ -117,13 +123,13 @@ val is_identity: Utils.environment -> equality -> bool * [eq_ty] the ty of the equality sides *) val symmetric: - Cic.term -> Cic.term -> int -> UriManager.uri -> + equality_bag -> Cic.term -> Cic.term -> int -> UriManager.uri -> Cic.metasenv -> proof (* takes 3 lists of alive ids (they are threated the same way, the type is * funny just to not oblige you to concatenate them) and drops all the dead * equalities *) -val collect: int list -> int list -> int list -> unit +val collect: equality_bag -> int list -> int list -> int list -> unit (* given an equality, returns the numerical id *) val id_of: equality -> int diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index f3af1b482..0b3ec04a8 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -127,14 +127,14 @@ let check_res res msg = | None -> () ;; -let check_target context target msg = +let check_target bag context target msg = let w, proof, (eq_ty, left, right, order), metas,_ = Equality.open_equality target in (* check that metas does not contains duplicates *) let eqs = Equality.string_of_equality target in let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right) - @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in + @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof) in let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in let _ = if menv <> metas then begin @@ -210,7 +210,7 @@ let get_candidates ?env mode tree term = the build_newtarget functions] )) *) -let rec find_matches metasenv context ugraph lift_amount term termty = +let rec find_matches bag metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in let module S = CicSubstitution in @@ -226,7 +226,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = Equality.open_equality equality in if Utils.debug_metas then - ignore(check_target context (snd candidate) "find_matches"); + ignore(check_target bag context (snd candidate) "find_matches"); if Utils.debug_res then begin let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in @@ -242,7 +242,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = end; if check && not (fst (CicReduction.are_convertible ~metasenv context termty ty ugraph)) then ( - find_matches metasenv context ugraph lift_amount term termty tl + find_matches bag metasenv context ugraph lift_amount term termty tl ) else let do_match c = let subst', metasenv', ugraph' = @@ -260,7 +260,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = try do_match c with Inference.MatchingFailure -> - find_matches metasenv context ugraph lift_amount term termty tl + find_matches bag metasenv context ugraph lift_amount term termty tl in if Utils.debug_res then ignore (check_res res "find1"); res @@ -280,10 +280,10 @@ let rec find_matches metasenv context ugraph lift_amount term termty = if order = U.Gt then res else - find_matches + find_matches bag metasenv context ugraph lift_amount term termty tl | None -> - find_matches metasenv context ugraph lift_amount term termty tl + find_matches bag metasenv context ugraph lift_amount term termty tl ;; let find_matches metasenv context ugraph lift_amount term termty = @@ -370,7 +370,7 @@ let print_res l = let subsumption_aux use_unification env table target = let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in - let metasenv, context, ugraph = env in + let _, context, ugraph = env in let metasenv = tmetas in let predicate, unif_fun = if use_unification then @@ -426,7 +426,7 @@ let unification x y z = subsumption_aux true x y z ;; -let rec demodulation_aux ?from ?(typecheck=false) +let rec demodulation_aux bag ?from ?(typecheck=false) metasenv context ugraph table lift_amount term = (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*) let module C = Cic in @@ -448,7 +448,7 @@ let rec demodulation_aux ?from ?(typecheck=false) C.Implicit None, ugraph in let res = - find_matches metasenv context ugraph lift_amount term termty candidates + find_matches bag metasenv context ugraph lift_amount term termty candidates in if Utils.debug_res then ignore(check_res res "demod1"); if res <> None then @@ -463,7 +463,7 @@ let rec demodulation_aux ?from ?(typecheck=false) (res, tl @ [S.lift 1 t]) else let r = - demodulation_aux ~from:"1" metasenv context ugraph table + demodulation_aux bag ~from:"1" metasenv context ugraph table lift_amount t in match r with @@ -478,12 +478,12 @@ let rec demodulation_aux ?from ?(typecheck=false) ) | C.Prod (nn, s, t) -> let r1 = - demodulation_aux ~from:"2" + demodulation_aux bag ~from:"2" metasenv context ugraph table lift_amount s in ( match r1 with | None -> let r2 = - demodulation_aux metasenv + demodulation_aux bag metasenv ((Some (nn, C.Decl s))::context) ugraph table (lift_amount+1) t in ( @@ -499,12 +499,12 @@ let rec demodulation_aux ?from ?(typecheck=false) ) | C.Lambda (nn, s, t) -> let r1 = - demodulation_aux + demodulation_aux bag metasenv context ugraph table lift_amount s in ( match r1 with | None -> let r2 = - demodulation_aux metasenv + demodulation_aux bag metasenv ((Some (nn, C.Decl s))::context) ugraph table (lift_amount+1) t in ( @@ -528,7 +528,7 @@ let rec demodulation_aux ?from ?(typecheck=false) exception Foo (** demodulation, when target is an equality *) -let rec demodulation_equality ?from eq_uri newmeta env table target = +let rec demodulation_equality bag ?from eq_uri newmeta env table target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -546,7 +546,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table target = (* let w = Utils.compute_equality_weight stat in*) (* let target = Equality.mk_equality (w, proof, stat, metas) in *) if Utils.debug_metas then - ignore(check_target context target "demod equalities input"); + ignore(check_target bag context target "demod equalities input"); let metasenv' = (* metasenv @ *) metas in let maxmeta = ref newmeta in @@ -557,7 +557,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table target = ignore(check_for_duplicates menv "input1"); ignore(check_disjoint_invariant subst menv "input2"); let substs = Subst.ppsubst subst in - ignore(check_target context (snd eq_found) ("input3" ^ substs)) + ignore(check_target bag context (snd eq_found) ("input3" ^ substs)) end; let pos, equality = eq_found in let (_, proof', @@ -585,14 +585,14 @@ let rec demodulation_equality ?from eq_uri newmeta env table target = let stat = (eq_ty, left, right, ordering) in let res = let w = Utils.compute_equality_weight stat in - (Equality.mk_equality (w, newproof, stat,newmenv)) + (Equality.mk_equality bag (w, newproof, stat,newmenv)) in if Utils.debug_metas then - ignore(check_target context res "buildnew_target output"); + ignore(check_target bag context res "buildnew_target output"); !maxmeta, res in - let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in + let res = demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left in if Utils.debug_res then check_res res "demod result"; let newmeta, newtarget = match res with @@ -603,9 +603,9 @@ let rec demodulation_equality ?from eq_uri newmeta env table target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality ?from eq_uri newmeta env table newtarget + demodulation_equality bag ?from eq_uri newmeta env table newtarget | None -> - let res = demodulation_aux metasenv' context ugraph table 0 right in + let res = demodulation_aux bag metasenv' context ugraph table 0 right in if Utils.debug_res then check_res res "demod result 1"; match res with | Some t -> @@ -614,7 +614,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality ?from eq_uri newmeta env table newtarget + demodulation_equality bag ?from eq_uri newmeta env table newtarget | None -> newmeta, target in @@ -760,7 +760,7 @@ let rec betaexpand_term the first free meta index, i.e. the first number above the highest meta index: its updated value is also returned *) -let superposition_right +let superposition_right bag ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target= let module C = Cic in let module S = CicSubstitution in @@ -772,7 +772,7 @@ let superposition_right Equality.open_equality target in if Utils.debug_metas then - ignore (check_target context target "superpositionright"); + ignore (check_target bag context target "superpositionright"); let metasenv' = newmetas in let maxmeta = ref newmeta in let res1, res2 = @@ -794,7 +794,7 @@ let superposition_right in let build_new ordering (bo, s, m, ug, eq_found) = if Utils.debug_metas then - ignore (check_target context (snd eq_found) "buildnew1" ); + ignore (check_target bag context (snd eq_found) "buildnew1" ); let pos, equality = eq_found in let (_, proof', (ty, what, other, _), menv',id') = @@ -826,17 +826,17 @@ let superposition_right let stat = (eq_ty, left, right, neworder) in let eq' = let w = Utils.compute_equality_weight stat in - Equality.mk_equality (w, newproof, stat, newmenv) in + Equality.mk_equality bag (w, newproof, stat, newmenv) in if Utils.debug_metas then - ignore (check_target context eq' "buildnew3"); - let newm, eq' = Equality.fix_metas !maxmeta eq' in + ignore (check_target bag context eq' "buildnew3"); + let newm, eq' = Equality.fix_metas bag !maxmeta eq' in if Utils.debug_metas then - ignore (check_target context eq' "buildnew4"); + ignore (check_target bag context eq' "buildnew4"); newm, eq' in maxmeta := newmeta; if Utils.debug_metas then - ignore(check_target context newequality "buildnew2"); + ignore(check_target bag context newequality "buildnew2"); newequality in let new1 = List.map (build_new U.Gt) res1 @@ -847,7 +847,7 @@ let superposition_right ;; (** demodulation, when the target is a theorem *) -let rec demodulation_theorem newmeta env table theorem = +let rec demodulation_theorem bag newmeta env table theorem = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -879,7 +879,7 @@ let rec demodulation_theorem newmeta env table theorem = !maxmeta, (newterm, newty, menv) in let res = - demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty + demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty in match res with | Some t -> @@ -888,7 +888,7 @@ let rec demodulation_theorem newmeta env table theorem = if Equality.meta_convertibility termty newty then newmeta, newthm else - demodulation_theorem newmeta env table newthm + demodulation_theorem bag newmeta env table newthm | None -> newmeta, theorem ;; @@ -934,7 +934,7 @@ let fix_expansion goal posu (t, subst, menv, ug, eq_f) = (* ginve the old [goal], the side that has not changed [posu] and the * expansion builds a new goal *) -let build_newgoal context goal posu rule expansion = +let build_newgoal bag context goal posu rule expansion = let goalproof,_,_,_,_,_ = open_goal goal in let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in let pos, equality = eq_found in @@ -960,7 +960,7 @@ let build_newgoal context goal posu rule expansion = returns a list of new clauses inferred with a left superposition step the negative equation "target" and one of the positive equations in "table" *) -let superposition_left (metasenv, context, ugraph) table goal maxmeta = +let superposition_left bag (metasenv, context, ugraph) table goal maxmeta = let names = Utils.names_of_context context in let proof,menv,eq,ty,l,r = open_goal goal in let c = !Utils.compare_terms l r in @@ -973,9 +973,9 @@ let superposition_left (metasenv, context, ugraph) table goal maxmeta = prerr_endline (string_of_int (List.length expansionsl)); prerr_endline (string_of_int (List.length expansionsr)); *) - List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl + List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl @ - List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr + List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr end else match c with @@ -983,13 +983,13 @@ let superposition_left (metasenv, context, ugraph) table goal maxmeta = let big,small,possmall = l,r,Utils.Right in let expansions, _ = betaexpand_term menv context ugraph table 0 big in List.map - (build_newgoal context goal possmall Equality.SuperpositionLeft) + (build_newgoal bag context goal possmall Equality.SuperpositionLeft) expansions | Utils.Lt -> (* prerr_endline "LT"; *) let big,small,possmall = r,l,Utils.Left in let expansions, _ = betaexpand_term menv context ugraph table 0 big in List.map - (build_newgoal context goal possmall Equality.SuperpositionLeft) + (build_newgoal bag context goal possmall Equality.SuperpositionLeft) expansions | Utils.Eq -> [] | _ -> @@ -1005,31 +1005,31 @@ let superposition_left (metasenv, context, ugraph) table goal maxmeta = ;; (** demodulation, when the target is a goal *) -let rec demodulation_goal env table goal = +let rec demodulation_goal bag env table goal = let goalproof,menv,_,_,left,right = open_goal goal in let _, context, ugraph = env in (* let term = Utils.guarded_simpl (~debug:true) context term in*) let do_right () = - let resright = demodulation_aux menv context ugraph table 0 right in + let resright = demodulation_aux bag menv context ugraph table 0 right in match resright with | Some t -> let newg = - build_newgoal context goal Utils.Left Equality.Demodulation t + build_newgoal bag context goal Utils.Left Equality.Demodulation t in if goal_metaconvertibility_eq goal newg then false, goal else - true, snd (demodulation_goal env table newg) + true, snd (demodulation_goal bag env table newg) | None -> false, goal in - let resleft = demodulation_aux menv context ugraph table 0 left in + let resleft = demodulation_aux bag menv context ugraph table 0 left in match resleft with | Some t -> - let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in + let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in if goal_metaconvertibility_eq goal newg then do_right () else - true, snd (demodulation_goal env table newg) + true, snd (demodulation_goal bag env table newg) | None -> do_right () ;; diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index ef068151e..e180511a6 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -50,11 +50,13 @@ val subsumption : (Subst.substitution * Equality.equality * bool) option val superposition_left : + Equality.equality_bag -> Cic.conjecture list * Cic.context * CicUniv.universe_graph -> Index.t -> Equality.goal -> int -> int * Equality.goal list val superposition_right : + Equality.equality_bag -> ?subterms_only:bool -> UriManager.uri -> int -> @@ -64,6 +66,7 @@ val superposition_right : int * Equality.equality list val demodulation_equality : + Equality.equality_bag -> ?from:string -> UriManager.uri -> int -> @@ -71,17 +74,20 @@ val demodulation_equality : Index.t -> Equality.equality -> int * Equality.equality val demodulation_goal : + Equality.equality_bag -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> Equality.goal -> bool * Equality.goal val demodulation_theorem : + Equality.equality_bag -> 'a -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> Cic.term * Cic.term * Cic.metasenv -> 'a * (Cic.term * Cic.term * Cic.metasenv) val check_target: + Equality.equality_bag -> Cic.context -> Equality.equality -> string -> unit diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml index e7f3d8d21..9ada69943 100644 --- a/helm/software/components/tactics/paramodulation/inference.ml +++ b/helm/software/components/tactics/paramodulation/inference.ml @@ -31,12 +31,13 @@ open Utils;; open Printf;; type auto_type = + int -> AutoTypes.flags -> ProofEngineTypes.proof -> Cic.context -> - ?universe:AutoTypes.universe -> AutoTypes.cache -> + AutoTypes.cache -> ProofEngineTypes.goal list -> - Cic.substitution list * AutoTypes.cache * AutoTypes.universe + Cic.substitution list * AutoTypes.cache * int let debug_print s = prerr_endline (Lazy.force s);; @@ -220,8 +221,8 @@ let check_eq context msg eq = else () ;; -let default_auto _ _ _ ?(universe:AutoTypes.universe option) _ _ = - [],AutoTypes.cache_empty,AutoTypes.empty_universe +let default_auto maxm _ _ _ _ _ = + [],AutoTypes.cache_empty,maxm ;; (* far sta roba e' un casino perche' bisogna pulire il contesto lasciando solo @@ -256,9 +257,9 @@ let ty_of_eq = function | _ -> assert false ;; -exception UnableToSaturate of AutoTypes.universe option * AutoTypes.cache +exception UnableToSaturate of AutoTypes.cache * int -let saturate_term context metasenv oldnewmeta term ?universe cache auto fast = +let saturate_term context metasenv oldnewmeta term cache auto fast = let head, metasenv, args, newmeta = ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 in @@ -280,23 +281,27 @@ let saturate_term context metasenv oldnewmeta term ?universe cache auto fast = | _ -> assert false) args in - let results,universe,cache = + let results,cache,newmeta = if args_for_auto = [] then let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in - [args,metasenv,newmetas,head,newmeta],universe,cache + [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.timeout = 1.0;maxwidth = 2;maxdepth = 2} + {AutoTypes.timeout = Unix.gettimeofday() +. 1.0; + maxwidth = 2;maxdepth = 2; + use_paramod=true;use_only_paramod=false} else - {AutoTypes.timeout = 1.0;maxwidth = 3;maxdepth = 3} + {AutoTypes.timeout = Unix.gettimeofday() +. 1.0; + maxwidth = 3;maxdepth = 3; + use_paramod=true;use_only_paramod=false} in - match auto flags proof context ?universe cache args_for_auto with - | [],cache,universe -> raise (UnableToSaturate (Some universe,cache)) - | substs,cache,universe -> + match auto newmeta flags proof context cache args_for_auto with + | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta)) + | substs,cache,newmeta -> List.map (fun subst -> let metasenv = @@ -307,11 +312,11 @@ let saturate_term context metasenv oldnewmeta term ?universe cache auto fast = List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv in let args = List.map (CicMetaSubst.apply_subst subst) args in - args,metasenv,newmetas,head,newmeta) - substs, - Some universe,cache + let newm = CicMkImplicit.new_meta metasenv subst in + args,metasenv,newmetas,head,max newm newmeta) + substs, cache, newmeta in - results,universe,cache + results,cache,newmeta ;; let rec is_an_equality = function @@ -321,7 +326,7 @@ let rec is_an_equality = function | _ -> false ;; -let build_equality_of_hypothesis index head args newmetas = +let build_equality_of_hypothesis bag index head args newmetas maxmeta = match head with | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] -> let p = @@ -335,27 +340,31 @@ let build_equality_of_hypothesis index head args newmetas = (* let w = compute_equality_weight stat in *) let w = 0 in let proof = Equality.Exact p in - Equality.mk_equality (w, proof, stat, newmetas) + 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 build_equality ty t1 t2 proof menv = +let build_equality bag ty t1 t2 proof menv maxmeta = let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in let proof = Equality.Exact proof in - Equality.mk_equality (w, proof, stat, menv) + let e = Equality.mk_equality bag (w, proof, stat, menv) in + (* to clean the local context of metas *) + Equality.fix_metas bag maxmeta e ;; -let find_equalities ?(auto = default_auto) context proof ?universe cache = +let find_equalities maxmeta bag ?(auto = default_auto) 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 = ProofEngineHelpers.new_meta_of_proof ~proof in - let rec aux universe cache index newmeta = function - | [] -> [], newmeta,universe,cache + let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in + let rec aux cache index newmeta = function + | [] -> [], newmeta,cache | (Some (_, C.Decl (term)))::tl -> debug_print (lazy @@ -365,47 +374,50 @@ let find_equalities ?(auto = default_auto) context proof ?universe cache = | C.Prod (name, s, t) when is_an_equality t -> (try let term = S.lift index term in - let saturated ,universe,cache = + let saturated,cache,newmeta = saturate_term context metasenv newmeta term - ?universe cache auto false + cache auto false in let eqs,newmeta = List.fold_left (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') -> - let equality = - build_equality_of_hypothesis index head args newmetas + let newmeta, equality = + build_equality_of_hypothesis + bag index head args newmetas (max newmeta newmeta') in - equality::acc,(max newmeta newmeta' + 1)) - ([],0) saturated + equality::acc, newmeta + 1) + ([],newmeta) saturated in - eqs, newmeta, universe, cache - with UnableToSaturate (universe,cache) -> - [],newmeta,universe,cache) + eqs, newmeta, cache + with UnableToSaturate (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 e = build_equality_of_hypothesis index term [] [] in - [e], (newmeta+1),universe,cache - | _ -> [], newmeta, universe, cache + let newmeta, e = + build_equality_of_hypothesis bag index term [] [] newmeta + in + [e], (newmeta+1),cache + | _ -> [], newmeta, cache in - let eqs, newmeta, universe, cache = do_find context term in + let eqs, newmeta, cache = do_find context term in if eqs = [] then debug_print (lazy "skipped") else debug_print (lazy "ok"); - let rest, newmeta,universe,cache = - aux universe cache (index+1) newmeta tl + let rest, newmeta,cache = + aux cache (index+1) newmeta tl in - List.map (fun x -> index,x) eqs @ rest, newmeta, universe, cache + List.map (fun x -> index,x) eqs @ rest, newmeta, cache | _::tl -> - aux universe cache (index+1) newmeta tl + aux cache (index+1) newmeta tl in - let il, maxm, universe, cache = - aux universe cache 1 newmeta context + let il, maxm, cache = + aux cache 1 newmeta context in let indexes, equalities = List.split il in (* ignore (List.iter (check_eq context "find") equalities); *) - indexes, equalities, maxm, universe, cache + indexes, equalities, maxm, cache ;; @@ -458,8 +470,8 @@ let utty_of_u u = u, t, ty ;; -let find_library_equalities - ?(auto = default_auto) caso_strano dbd context status maxmeta ?universe cache +let find_library_equalities bag + ?(auto = default_auto) caso_strano dbd context status maxmeta cache = prerr_endline "find_library_equalities"; let module C = Cic in @@ -519,20 +531,20 @@ let find_library_equalities let candidates = List.map utty_of_u eqs in let candidates = List.filter is_monomorphic_eq candidates in let candidates = List.filter is_var_free candidates in - let rec aux universe cache newmeta = function - | [] -> [], newmeta, universe, cache + let rec aux cache newmeta = function + | [] -> [], newmeta, cache | (uri, term, termty)::tl -> debug_print (lazy (Printf.sprintf "Examining: %s (%s)" (CicPp.ppterm term) (CicPp.ppterm termty))); - let res, newmeta, universe, cache = + let res, newmeta, cache = match termty with | C.Prod (name, s, t) -> (try - let saturated, universe,cache = + let saturated,cache,newmeta = saturate_term context metasenv newmeta termty - ?universe cache auto true + cache auto true in let eqs,newmeta = List.fold_left @@ -542,27 +554,28 @@ let find_library_equalities when LibraryObjects.is_eq_URI uri -> let proof = C.Appl (term::args) in prerr_endline ("PROVA: " ^ CicPp.ppterm proof); - let equality = - build_equality ty t1 t2 proof newmetas + let maxmeta, equality = + build_equality bag ty t1 t2 proof newmetas + (max newmeta newmeta') in - equality::acc,(max newmeta newmeta' + 1) + equality::acc,maxmeta + 1 | _ -> assert false) - ([],0) saturated + ([],newmeta) saturated in - eqs, newmeta , universe, cache - with UnableToSaturate (universe,cache) -> - [], newmeta , universe, cache) + eqs, newmeta , cache + with UnableToSaturate (cache,newmeta) -> + [], newmeta , cache) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> - let e = build_equality ty t1 t2 term [] in - [e], (newmeta+1), universe, cache + let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in + [e], newmeta+1, cache | _ -> assert false in let res = List.map (fun e -> uri, e) res in - let tl, newmeta, universe, cache = aux universe cache newmeta tl in - res @ tl, newmeta, universe, cache + let tl, newmeta, cache = aux cache newmeta tl in + res @ tl, newmeta, cache in - let found, maxm, universe, cache = - aux universe cache maxmeta candidates + let found, maxm, cache = + aux cache maxmeta candidates in let uriset, eqlist = let mceq = Equality.meta_convertibility_eq in @@ -577,7 +590,7 @@ let find_library_equalities ) else (UriManager.UriSet.add u s, (u, e)::l)) (UriManager.UriSet.empty, []) found) in - uriset, eqlist, maxm, universe, cache + uriset, eqlist, maxm, cache ;; let get_stats () = "" (*<:show>*) ;; diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli index 47626fcf0..97c868985 100644 --- a/helm/software/components/tactics/paramodulation/inference.mli +++ b/helm/software/components/tactics/paramodulation/inference.mli @@ -42,13 +42,14 @@ val unification: CicUniv.universe_graph -> Subst.substitution * Cic.metasenv * CicUniv.universe_graph -type auto_type = +type auto_type = (* the universe must be hardocded *) + int -> (* maxmeta *) AutoTypes.flags -> ProofEngineTypes.proof -> Cic.context -> - ?universe:AutoTypes.universe -> AutoTypes.cache -> + AutoTypes.cache -> ProofEngineTypes.goal list -> - Cic.substitution list * AutoTypes.cache * AutoTypes.universe + Cic.substitution list * AutoTypes.cache * int (** scans the context to find all Declarations "left = right"; returns a @@ -57,20 +58,22 @@ type auto_type = fresh metas... *) val find_equalities: + int -> + Equality.equality_bag -> ?auto:auto_type -> Cic.context -> ProofEngineTypes.proof -> - ?universe:AutoTypes.universe -> AutoTypes.cache -> - int list * Equality.equality list * int * - AutoTypes.universe option * AutoTypes.cache + AutoTypes.cache -> + int list * Equality.equality list * int * AutoTypes.cache (** searches the library for equalities that can be applied to the current goal *) val find_library_equalities: + Equality.equality_bag -> ?auto:auto_type -> bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> - ?universe:AutoTypes.universe -> AutoTypes.cache -> + AutoTypes.cache -> UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int * - AutoTypes.universe option * AutoTypes.cache + AutoTypes.cache val get_stats: unit -> string diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index cf093473c..11966ef8d 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -70,15 +70,6 @@ let maxmeta = ref 0;; let maxdepth = ref 3;; let maxwidth = ref 3;; -type new_proof = - Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv -type result = - | ParamodulationFailure of string - | ParamodulationSuccess of new_proof -;; - -(* type goal = Equality.goal_proof * Cic.metasenv * Cic.term;; *) - type theorem = Cic.term * Cic.term * Cic.metasenv;; let symbols_of_equality equality = @@ -117,22 +108,25 @@ end module EqualitySet = Set.Make(OrderedEquality);; -exception Empty_list;; - -type passives = Equality.equality list * EqualitySet.t;; -type actives = Equality.equality list * Indexing.Index.t;; - -(* initializes the passive set of equalities - * XXX I think EqualitySet.elements should be ok (to eliminate duplicates) - *) -let make_passive pos = +type passive_table = Equality.equality list * EqualitySet.t +type active_table = Equality.equality list * Indexing.Index.t +type new_proof = + Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv +type result = + | ParamodulationFailure of string * active_table * passive_table + | ParamodulationSuccess of new_proof * active_table * passive_table +;; +let make_passive eq_list = let set = - List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty pos + List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list in - (*EqualitySet.elements*) pos, set + (*EqualitySet.elements set*) eq_list, set +;; +let make_empty_active () = [], Indexing.empty ;; +let make_active eq_list = + eq_list, List.fold_left Indexing.index Indexing.empty eq_list ;; -let make_active () = [], Indexing.empty ;; let size_of_passive (passive_list, _) = List.length passive_list;; let size_of_active (active_list, _) = List.length active_list;; let passive_is_empty = function @@ -256,12 +250,12 @@ let rec select env g passive = ;; -let filter_dependent passive id = +let filter_dependent bag passive id = let pos_list, pos_set = passive in let passive,no_pruned = List.fold_right (fun eq ((list,set),no) -> - if Equality.depend eq id then + if Equality.depend bag eq id then (list, EqualitySet.remove eq set), no + 1 else (eq::list, set), no) @@ -288,7 +282,6 @@ let add_to_passive passive new_pos preferred = (fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred) pos in - assert(pos_head = []); pos_head @ pos_list @ pos_tail, add pos_set pos ;; @@ -350,30 +343,30 @@ let prune_passive howmany (active, _) passive = (** inference of new equalities between current and some in active *) -let infer eq_uri env current (active_list, active_table) = +let infer bag eq_uri env current (active_list, active_table) = let (_,c,_) = env in if Utils.debug_metas then - (ignore(Indexing.check_target c current "infer1"); - ignore(List.map (function current -> Indexing.check_target c current "infer2") active_list)); + (ignore(Indexing.check_target bag c current "infer1"); + ignore(List.map (function current -> Indexing.check_target bag c current "infer2") active_list)); let new_pos = - let maxm, copy_of_current = Equality.fix_metas !maxmeta current in + let maxm, copy_of_current = Equality.fix_metas bag !maxmeta current in maxmeta := maxm; let active_table = Indexing.index active_table copy_of_current in (* let _ = <:start> in *) let maxm, res = - Indexing.superposition_right eq_uri !maxmeta env active_table current + Indexing.superposition_right bag eq_uri !maxmeta env active_table current in (* let _ = <:stop> in *) if Utils.debug_metas then ignore(List.map (function current -> - Indexing.check_target c current "sup0") res); + Indexing.check_target bag c current "sup0") res); maxmeta := maxm; let rec infer_positive table = function | [] -> [] | equality::tl -> let maxm, res = - Indexing.superposition_right + Indexing.superposition_right bag ~subterms_only:true eq_uri !maxmeta env table equality in maxmeta := maxm; @@ -381,7 +374,7 @@ let infer eq_uri env current (active_list, active_table) = ignore (List.map (function current -> - Indexing.check_target c current "sup2") res); + Indexing.check_target bag c current "sup2") res); let pos = infer_positive table tl in res @ pos in @@ -396,7 +389,7 @@ let infer eq_uri env current (active_list, active_table) = if Utils.debug_metas then ignore(List.map (function current -> - Indexing.check_target c current "sup3") pos); + Indexing.check_target bag c current "sup3") pos); res @ pos in derived_clauses := !derived_clauses + (List.length new_pos); @@ -444,22 +437,22 @@ let check_for_deep_subsumption env active_table eq = ;; (** simplifies current using active and passive *) -let forward_simplify eq_uri env current (active_list, active_table) = +let forward_simplify bag eq_uri env current (active_list, active_table) = let _, context, _ = env in let demodulate table current = let newmeta, newcurrent = - Indexing.demodulation_equality eq_uri !maxmeta env table current + Indexing.demodulation_equality bag eq_uri !maxmeta env table current in maxmeta := newmeta; if Equality.is_identity env newcurrent then None else Some newcurrent in let rec demod current = if Utils.debug_metas then - ignore (Indexing.check_target context current "demod0"); + ignore (Indexing.check_target bag context current "demod0"); let res = demodulate active_table current in if Utils.debug_metas then ignore ((function None -> () | Some x -> - ignore (Indexing.check_target context x "demod1");()) res); + ignore (Indexing.check_target bag context x "demod1");()) res); res in let res = demod current in @@ -475,18 +468,18 @@ let forward_simplify eq_uri env current (active_list, active_table) = ;; (** simplifies new using active and passive *) -let forward_simplify_new eq_uri env new_pos active = +let forward_simplify_new bag eq_uri env new_pos active = if Utils.debug_metas then begin let m,c,u = env in ignore(List.map - (fun current -> Indexing.check_target c current "forward new pos") + (fun current -> Indexing.check_target bag c current "forward new pos") new_pos;) end; let active_list, active_table = active in let demodulate table target = let newmeta, newtarget = - Indexing.demodulation_equality eq_uri !maxmeta env table target + Indexing.demodulation_equality bag eq_uri !maxmeta env table target in maxmeta := newmeta; newtarget @@ -510,27 +503,29 @@ let forward_simplify_new eq_uri env new_pos active = (** simplifies a goal with equalities in active and passive *) -let rec simplify_goal env goal (active_list, active_table) = - let demodulate table goal = Indexing.demodulation_goal env table goal in +let rec simplify_goal bag env goal (active_list, active_table) = + let demodulate table goal = Indexing.demodulation_goal bag env table goal in let changed, goal = demodulate active_table goal in changed, if not changed then goal else - snd (simplify_goal env goal (active_list, active_table)) + snd (simplify_goal bag env goal (active_list, active_table)) ;; -let simplify_goals env goals active = +let simplify_goals bag env goals active = let a_goals, p_goals = goals in - let p_goals = List.map (fun g -> snd (simplify_goal env g active)) p_goals in - let a_goals = List.map (fun g -> snd (simplify_goal env g active)) a_goals in + let p_goals = List.map (fun g -> snd (simplify_goal bag env g active)) p_goals in + let a_goals = List.map (fun g -> snd (simplify_goal bag env g active)) a_goals in a_goals, p_goals ;; (** simplifies active usign new *) -let backward_simplify_active eq_uri env new_pos new_table min_weight active = +let backward_simplify_active + bag eq_uri env new_pos new_table min_weight active += let active_list, active_table = active in let active_list, newa, pruned = List.fold_right @@ -540,7 +535,7 @@ let backward_simplify_active eq_uri env new_pos new_table min_weight active = equality::res, newn,pruned else match - forward_simplify eq_uri env equality (new_pos, new_table) + forward_simplify bag eq_uri env equality (new_pos, new_table) with | None -> res, newn, id::pruned | Some e -> @@ -580,7 +575,9 @@ let backward_simplify_active eq_uri env new_pos new_table min_weight active = (** simplifies passive using new *) -let backward_simplify_passive eq_uri env new_pos new_table min_weight passive = +let backward_simplify_passive + bag eq_uri env new_pos new_table min_weight passive += let (pl, ps), passive_table = passive in let f equality (resl, ress, newn) = let ew, _, _, _ , _ = Equality.open_equality equality in @@ -588,7 +585,7 @@ let backward_simplify_passive eq_uri env new_pos new_table min_weight passive = equality::resl, ress, newn else match - forward_simplify eq_uri env equality (new_pos, new_table) + forward_simplify bag eq_uri env equality (new_pos, new_table) with | None -> resl, EqualitySet.remove equality ress, newn | Some e -> @@ -617,15 +614,15 @@ let build_table equations = ;; -let backward_simplify eq_uri env new' active = +let backward_simplify bag eq_uri env new' active = let new_pos, new_table, min_weight = build_table new' in let active, newa, pruned = - backward_simplify_active eq_uri env new_pos new_table min_weight active + backward_simplify_active bag eq_uri env new_pos new_table min_weight active in - active, newa, None, pruned + active, newa, pruned ;; -let close eq_uri env new' given = +let close bag eq_uri env new' given = let new_pos, new_table, min_weight = List.fold_left (fun (l, t, w) e -> @@ -635,7 +632,7 @@ let close eq_uri env new' given = in List.fold_left (fun p c -> - let pos = infer eq_uri env c (new_pos,new_table) in + let pos = infer bag eq_uri env c (new_pos,new_table) in pos@p) [] given ;; @@ -651,7 +648,7 @@ let is_commutative_law eq = | _ -> false ;; -let prova eq_uri env new' active = +let prova bag eq_uri env new' active = let given = List.filter is_commutative_law (fst active) in let _ = Utils.debug_print @@ -661,7 +658,7 @@ let prova eq_uri env new' active = (List.map (fun e -> Equality.string_of_equality ~env e) given)))) in - close eq_uri env new' given + close bag eq_uri env new' given ;; (* returns an estimation of how many equalities in passive can be activated @@ -710,7 +707,7 @@ let activate_theorem (active, passive) = -let simplify_theorems env theorems ?passive (active_list, active_table) = +let simplify_theorems bag env theorems ?passive (active_list, active_table) = let pl, passive_table = match passive with | None -> [], None @@ -719,7 +716,7 @@ let simplify_theorems env theorems ?passive (active_list, active_table) = let a_theorems, p_theorems = theorems in let demodulate table theorem = let newmeta, newthm = - Indexing.demodulation_theorem !maxmeta env table theorem in + Indexing.demodulation_theorem bag !maxmeta env table theorem in maxmeta := newmeta; theorem != newthm, newthm in @@ -741,20 +738,20 @@ let simplify_theorems env theorems ?passive (active_list, active_table) = ;; -let rec simpl eq_uri env e others others_simpl = +let rec simpl bag eq_uri env e others others_simpl = let active = others @ others_simpl in let tbl = List.fold_left (fun t e -> - if Equality.is_weak_identity e then t else Indexing.index t e) + if Equality.is_weak_identity e then t else Indexing.index t e) Indexing.empty active in - let res = forward_simplify eq_uri env e (active, tbl) in + let res = forward_simplify bag eq_uri env e (active, tbl) in match others with | hd::tl -> ( match res with - | None -> simpl eq_uri env hd tl others_simpl - | Some e -> simpl eq_uri env hd tl (e::others_simpl) + | None -> simpl bag eq_uri env hd tl others_simpl + | Some e -> simpl bag eq_uri env hd tl (e::others_simpl) ) | [] -> ( match res with @@ -763,7 +760,7 @@ let rec simpl eq_uri env e others others_simpl = ) ;; -let simplify_equalities eq_uri env equalities = +let simplify_equalities bag eq_uri env equalities = Utils.debug_print (lazy (Printf.sprintf "equalities:\n%s\n" @@ -774,7 +771,7 @@ let simplify_equalities eq_uri env equalities = | [] -> [] | hd::tl -> let res = - List.rev (simpl eq_uri env hd tl []) + List.rev (simpl bag eq_uri env hd tl []) in Utils.debug_print (lazy @@ -807,13 +804,13 @@ let pp_goal_set msg goals names = passive_goals))) ;; -let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = +let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = (* let names = Utils.names_of_context ctx in *) match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] when LibraryObjects.is_eq_URI uri -> (let goal_equation = - Equality.mk_equality + Equality.mk_equality bag (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) in (* match Indexing.subsumption env table goal_equation with*) @@ -830,7 +827,7 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in let p = if swapped then - Equality.symmetric eq_ty l id uri m + Equality.symmetric bag eq_ty l id uri m else p in @@ -866,7 +863,7 @@ let rec check goal = function | (Some p) as ok -> ok ;; -let simplify_goal_set env goals active = +let simplify_goal_set bag env goals active = let active_goals, passive_goals = goals in let find (_,_,g) where = List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where @@ -877,7 +874,7 @@ let simplify_goal_set env goals active = in *) List.fold_left (fun (acc_a,acc_p) goal -> - match simplify_goal env goal active with + match simplify_goal bag env goal active with | changed, g -> if changed then if find g acc_p then acc_a,acc_p else acc_a,g::acc_p @@ -886,7 +883,7 @@ let simplify_goal_set env goals active = ([],passive_goals) active_goals ;; -let check_if_goals_set_is_solved env active goals = +let check_if_goals_set_is_solved bag env active goals = let active_goals, passive_goals = goals in List.fold_left (fun proof goal -> @@ -895,17 +892,17 @@ let check_if_goals_set_is_solved env active goals = | None -> check goal [ check_if_goal_is_identity env; - check_if_goal_is_subsumed env (snd active)]) + check_if_goal_is_subsumed bag env (snd active)]) (* provare active and passive?*) None active_goals ;; -let infer_goal_set env active goals = +let infer_goal_set bag env active goals = let active_goals, passive_goals = goals in let rec aux = function | [] -> active_goals, [] | hd::tl -> - let changed,selected = simplify_goal env hd active in + let changed,selected = simplify_goal bag env hd active in (* if changed then prerr_endline ("--------------- goal semplificato"); @@ -923,7 +920,7 @@ let infer_goal_set env active goals = if Utils.metas_of_term t1 = [] then passive_goals else let newmaxmeta,new' = - Indexing.superposition_left env (snd active) selected + Indexing.superposition_left bag env (snd active) selected !maxmeta in maxmeta := newmaxmeta; @@ -934,15 +931,13 @@ let infer_goal_set env active goals = aux passive_goals ;; -let infer_goal_set_with_current env current goals active = - let active_goals, passive_goals = - simplify_goal_set env goals active - in +let infer_goal_set_with_current bag env current goals active = + let active_goals, passive_goals = simplify_goal_set bag env goals active in let l,table,_ = build_table [current] in active_goals, List.fold_left (fun acc g -> - let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in + let newmaxmeta, new' = Indexing.superposition_left bag env table g !maxmeta in maxmeta := newmaxmeta; acc @ new') passive_goals active_goals @@ -986,7 +981,8 @@ let print_status iterno goals active passive = (** given-clause algorithm with full reduction strategy: NEW implementation *) (* here goals is a set of goals in OR *) let given_clause - eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time + bag eq_uri ((_,context,_) as env) goals passive active + goal_steps saturation_steps max_time = let initial_time = Unix.gettimeofday () in let iterations_left iterno = @@ -999,19 +995,19 @@ let given_clause let iterations_left = time_left /. iteration_medium_cost in int_of_float iterations_left in - let rec step goals theorems passive active iterno = - if iterno > max_iterations then - (ParamodulationFailure "No more iterations to spend") + let rec step goals passive active g_iterno s_iterno = + if g_iterno > goal_steps && s_iterno > saturation_steps then + (ParamodulationFailure ("No more iterations to spend",active,passive)) else if Unix.gettimeofday () > max_time then - (ParamodulationFailure "No more time to spend") + (ParamodulationFailure ("No more time to spend",active,passive)) else let _ = -(* print_status iterno goals active passive *) - Printf.eprintf ".%!"; + print_status (max g_iterno s_iterno) goals active passive +(* Printf.eprintf ".%!"; *) in (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) let passive = - let selection_estimate = iterations_left iterno in + let selection_estimate = iterations_left (max g_iterno s_iterno) in let kept = size_of_passive passive in if kept > selection_estimate then begin @@ -1022,49 +1018,55 @@ let given_clause passive in kept_clauses := (size_of_passive passive) + (size_of_active active); - let goals = infer_goal_set env active goals + let goals = + if g_iterno < goal_steps then + infer_goal_set bag env active goals + else + goals in - match check_if_goals_set_is_solved env active goals with + match check_if_goals_set_is_solved bag env active goals with | Some p -> prerr_endline (Printf.sprintf "\nFound a proof in: %f\n" (Unix.gettimeofday() -. initial_time)); - ParamodulationSuccess p + ParamodulationSuccess (p,active,passive) | None -> (* SELECTION *) if passive_is_empty passive then if no_more_passive_goals goals then - ParamodulationFailure "No more passive equations/goals" + ParamodulationFailure + ("No more passive equations/goals",active,passive) (*maybe this is a success! *) else - step goals theorems passive active (iterno+1) + step goals passive active (g_iterno+1) (s_iterno+1) else begin (* COLLECTION OF GARBAGED EQUALITIES *) - if iterno mod 40 = 0 then + if max g_iterno s_iterno mod 40 = 0 then begin - print_status iterno goals active passive; + print_status (max g_iterno s_iterno) goals active passive; let active = List.map Equality.id_of (fst active) in let passive = List.map Equality.id_of (fst passive) in let goal = ids_of_goal_set goals in - Equality.collect active passive goal + Equality.collect bag active passive goal end; - let current, passive = select env goals passive in - (* SIMPLIFICATION OF CURRENT *) -(* - prerr_endline - ("Selected : " ^ - Equality.string_of_equality ~env current); -*) - let res = - forward_simplify eq_uri env current active + let res, passive = + if s_iterno < saturation_steps then + let current, passive = select env goals passive in + (* SIMPLIFICATION OF CURRENT *) + prerr_endline + ("Selected : " ^ + Equality.string_of_equality ~env current); + forward_simplify bag eq_uri env current active, passive + else + None, passive in match res with - | None -> step goals theorems passive active (iterno+1) + | None -> step goals passive active (g_iterno+1) (s_iterno+1) | Some current -> (* GENERATION OF NEW EQUATIONS *) (* prerr_endline "infer"; *) - let new' = infer eq_uri env current active in + let new' = infer bag eq_uri env current active in (* prerr_endline "infer goal"; *) (* match check_if_goals_set_is_solved env active goals with @@ -1080,59 +1082,56 @@ let given_clause al @ [current], Indexing.index tbl current in let goals = - infer_goal_set_with_current env current goals active + infer_goal_set_with_current bag env current goals active in (* FORWARD AND BACKWARD SIMPLIFICATION *) (* prerr_endline "fwd/back simpl"; *) - let rec simplify new' active passive head = + let rec simplify new' active passive = let new' = - forward_simplify_new eq_uri env new' active + forward_simplify_new bag eq_uri env new' active in - let active, newa, retained, pruned = - backward_simplify eq_uri env new' active + let active, newa, pruned = + backward_simplify bag eq_uri env new' active in let passive = - List.fold_left filter_dependent passive pruned + List.fold_left (filter_dependent bag) passive pruned in - match newa, retained with - | None, None -> active, passive, new', head - | Some p, None - | None, Some p -> simplify (new' @ p) active passive head - | Some p, Some rp -> - simplify (new' @ p @ rp) active passive (head @ p) + match newa with + | None -> active, passive, new' + | Some p -> simplify (new' @ p) active passive in - let active, passive, new', head = - simplify new' active passive [] + let active, passive, new' = + simplify new' active passive in (* prerr_endline "simpl goal with new"; *) let goals = let a,b,_ = build_table new' in (* let _ = <:start> in *) - let rc = simplify_goal_set env goals (a,b) in + let rc = simplify_goal_set bag env goals (a,b) in (* let _ = <:stop> in *) rc in - let passive = add_to_passive passive new' head in - step goals theorems passive active (iterno+1) + let passive = add_to_passive passive new' [] in + step goals passive active (g_iterno+1) (s_iterno+1) end in - step goals theorems passive active 1 + step goals passive active 1 1 ;; -let rec saturate_equations eq_uri env goal accept_fun passive active = +let rec saturate_equations bag eq_uri env goal accept_fun passive active = elapsed_time := Unix.gettimeofday () -. !start_time; if !elapsed_time > !time_limit then (active, passive) else let current, passive = select env ([goal],[]) passive in - let res = forward_simplify eq_uri env current active in + let res = forward_simplify bag eq_uri env current active in match res with | None -> - saturate_equations eq_uri env goal accept_fun passive active + saturate_equations bag eq_uri env goal accept_fun passive active | Some current -> Utils.debug_print (lazy (Printf.sprintf "selected: %s" (Equality.string_of_equality ~env current))); - let new' = infer eq_uri env current active in + let new' = infer bag eq_uri env current active in let active = if Equality.is_identity env current then active else @@ -1142,16 +1141,14 @@ let rec saturate_equations eq_uri env goal accept_fun passive active = (* alla fine new' contiene anche le attive semplificate! * quindi le aggiungo alle passive insieme alle new *) let rec simplify new' active passive = - let new' = forward_simplify_new eq_uri env new' active in - let active, newa, retained, pruned = - backward_simplify eq_uri env new' active in + let new' = forward_simplify_new bag eq_uri env new' active in + let active, newa, pruned = + backward_simplify bag eq_uri env new' active in let passive = - List.fold_left filter_dependent passive pruned in - match newa, retained with - | None, None -> active, passive, new' - | Some p, None - | None, Some p -> simplify (new' @ p) active passive - | Some p, Some rp -> simplify (new' @ p @ rp) active passive + List.fold_left (filter_dependent bag) passive pruned in + match newa with + | None -> active, passive, new' + | Some p -> simplify (new' @ p) active passive in let active, passive, new' = simplify new' active passive in let _ = @@ -1174,7 +1171,7 @@ let rec saturate_equations eq_uri env goal accept_fun passive active = in let new' = List.filter accept_fun new' in let passive = add_to_passive passive new' [] in - saturate_equations eq_uri env goal accept_fun passive active + saturate_equations bag eq_uri env goal accept_fun passive active ;; let default_depth = !maxdepth @@ -1195,7 +1192,6 @@ let reset_refs () = passive_maintainance_time := 0.; derived_clauses := 0; kept_clauses := 0; - Equality.reset (); ;; let eq_of_goal = function @@ -1210,102 +1206,26 @@ let eq_and_ty_of_goal = function | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) ;; -let saturate - caso_strano - dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) - ?(timeout=600.) ?auto status = - let module C = Cic in - reset_refs (); - Indexing.init_index (); - maxdepth := depth; - maxwidth := width; -(* CicUnification.unif_ty := false;*) +(* status: input proof status + * goalproof: forward steps on goal + * newproof: backward steps + * subsumption_id: the equation used if goal is closed by subsumption + * (0 if not closed by subsumption) (DEBUGGING: can be safely removed) + * subsumption_subst: subst to make newproof and goalproof match + * proof_menv: final metasenv + *) +let build_proof + bag status + goalproof newproof subsumption_id subsumption_subst proof_menv += 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 cleaned_goal = Utils.remove_local_context type_of_goal in - Utils.set_goal_symbols cleaned_goal; - let names = Utils.names_of_context context in - let eq_indexes, equalities, maxm, universe, cache = - Inference.find_equalities ?auto context proof AutoTypes.cache_empty - in - prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>"; - List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities; - prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; - 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 res, time = - let t1 = Unix.gettimeofday () in - let lib_eq_uris, library_equalities, maxm, universe, cache = - Inference.find_library_equalities - ?auto caso_strano dbd context (proof, goalno) (maxm+2) - ?universe cache - in - prerr_endline ">>>>>>>>>> gained from the library >>>>>>>>>>>>"; - List.iter - (fun (_,e) -> prerr_endline (Equality.string_of_equality e)) - library_equalities; - prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; - let library_equalities = List.map snd library_equalities in - let t2 = Unix.gettimeofday () in - maxmeta := maxm+2; - let equalities = - simplify_equalities eq_uri env (equalities@library_equalities) - in - Utils.debug_print - (lazy - (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))); - 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_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 - eq_uri env goals theorems passive active 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) -> + let names = Utils.names_of_context context in prerr_endline "Proof:"; prerr_endline - (Equality.pp_proof names goalproof newproof subsumption_subst + (Equality.pp_proof bag names goalproof newproof subsumption_subst subsumption_id type_of_goal); (* prerr_endline "ENDOFPROOFS"; *) (* @@ -1320,7 +1240,7 @@ let saturate in let goal_proof, side_effects_t = let initial = Equality.add_subst subsumption_subst newproof in - Equality.build_goal_proof + Equality.build_goal_proof bag eq_uri goalproof initial type_of_goal side_effects context proof_menv in @@ -1341,7 +1261,8 @@ let saturate (fun (acc1,acc2,acc3,uniq) (i,_,ty) -> match uniq with | Some m -> - acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq +(* acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq *) + (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl))::acc3, uniq | None -> [i,context,ty], (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) @@ -1381,6 +1302,12 @@ let saturate let free_metas_menv = List.map (fun i -> CicUtil.lookup_meta i goal_proof_menv) free_metas in +(* + prerr_endline ("XX type_of_goal " ^ CicPp.ppterm type_of_goal); + prerr_endline ("XX replaced_goal " ^ CicPp.ppterm replaced_goal); + prerr_endline ("XX metasenv " ^ + CicMetaSubst.ppmetasenv [] (metasenv @ free_metas_menv)); +*) try CicUnification.fo_unif_subst [] context (metasenv @ free_metas_menv) replaced_goal type_of_goal CicUniv.empty_ugraph @@ -1422,192 +1349,192 @@ let saturate (CicMetaSubst.ppmetasenv [] metasenv) (CicMetaSubst.ppmetasenv [] real_metasenv); *) - prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time); - proof, open_goals + final_subst, proof, open_goals ;; -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 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 eq_indexes, equalities, maxm,universe,cache = - Inference.find_equalities context proof AutoTypes.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, unvierse, cache = - Inference.find_library_equalities - false dbd context (proof, goal') (maxm+2) ?universe 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 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 - ) + let env = (metasenv, context, CicUniv.empty_ugraph) in + let bag = Equality.mk_equality_bag () in + let eq_indexes, equalities, maxm, cache = + Inference.find_equalities 0 bag ?auto context proof cache 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))) + 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 = + Inference.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 + 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 saturate_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 = + Inference.find_equalities maxmeta bag ?auto context proof cache + in + let equalities = +(* + HExtlib.filter_map + (fun e -> forward_simplify bag eq_uri env e active) +*) + equalities + in + bag, equalities, cache, maxm -let main_demod_equalities dbd term metasenv ugraph = +let saturate + smart_flag + dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) + ?(timeout=600.) ?auto status = 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 eq_indexes, equalities, maxm, universe, cache = - Inference.find_equalities context proof AutoTypes.cache_empty in - let lib_eq_uris, library_equalities, maxm,universe,cache = - Inference.find_library_equalities - false dbd context (proof, goal') (maxm+2) ?universe 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 + reset_refs (); + maxdepth := depth; + maxwidth := width; +(* CicUnification.unif_ty := false;*) + 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 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 AutoTypes.cache_empty in - let env = (metasenv, context, ugraph) in - (*try*) - let goal = [], [], goal + 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 equalities = - simplify_equalities eq_uri env (equalities@library_equalities) + 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_active () 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 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 + 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 addfun s e = - if not (EqualitySet.mem e initial) then EqualitySet.add e s else s + 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 ******************** *) - 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) +(* exported version of given_clause *) +let given_clause + bag maxm status active passive goal_steps 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 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 cleaned_goal = Utils.remove_local_context type_of_goal in + Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *) + let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in + let env = metasenv,context,CicUniv.empty_ugraph in + let goals = make_goal_set goal in + match + given_clause bag eq_uri env goals passive active + goal_steps saturation_steps max_time + with + | ParamodulationFailure (_,a,p) -> + None, a, p, !maxmeta + | ParamodulationSuccess + ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p) -> + let subst, proof, gl = + build_proof bag + status goalproof newproof subsumption_id subsumption_subst proof_menv 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))) -*) + 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 eq_uri = eq_of_goal ty in - let eq_indexes, equalities, maxm, universe, cache = - Inference.find_equalities context proof AutoTypes.cache_empty + let eq_uri = eq_of_goal ty in + let bag = Equality.mk_equality_bag () in + let eq_indexes, equalities, maxm, cache = + Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in - let lib_eq_uris, library_equalities, maxm, universe, cache = - Inference.find_library_equalities - false dbd context (proof, goal) (maxm+2) ?universe cache + let lib_eq_uris, library_equalities, maxm, cache = + Inference.find_library_equalities bag + false dbd context (proof, goal) (maxm+2) cache in if library_equalities = [] then prerr_endline "VUOTA!!!"; let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in @@ -1615,7 +1542,7 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = let initgoal = [], [], ty in let env = (metasenv, context, CicUniv.empty_ugraph) in let equalities = - simplify_equalities eq_uri env (equalities@library_equalities) + simplify_equalities bag eq_uri env (equalities@library_equalities) in let table = List.fold_left @@ -1623,14 +1550,14 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = Indexing.empty equalities in let changed,(newproof,newmetasenv, newty) = - Indexing.demodulation_goal + 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 + Equality.build_goal_proof bag eq_uri newproof opengoal ty [] context metasenv in let extended_metasenv = (maxm,context,newty)::metasenv in @@ -1676,15 +1603,15 @@ let rec position_of i x = function let superposition_tac ~target ~table ~subterms_only ~demod_table status = reset_refs(); - Indexing.init_index (); 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 eq_index, equalities, maxm,universe,cache = - Inference.find_equalities context proof AutoTypes.cache_empty + let bag = Equality.mk_equality_bag () in + let eq_index, equalities, maxm,cache = + Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in let eq_what = let what = find_in_ctx 1 target context in @@ -1705,7 +1632,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = 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 + Indexing.superposition_right bag ~subterms_only eq_uri maxm env index eq_what in prerr_endline ("Superposition right:"); @@ -1725,7 +1652,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = 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 eq_uri [] 0 p) names)) eql; + CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql; if demod_table <> "" then begin let eql = @@ -1745,7 +1672,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = List.fold_left (fun (maxm,acc) e -> let maxm,eq = - Indexing.demodulation_equality eq_uri maxm env table e + Indexing.demodulation_equality bag eq_uri maxm env table e in maxm,eq::acc) (maxm,[]) eql @@ -1771,3 +1698,186 @@ let 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 = + Inference.find_equalities 0 bag context proof AutoTypes.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 = + Inference.find_library_equalities bag + 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 = + Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in + let lib_eq_uris, library_equalities, maxm,cache = + Inference.find_library_equalities bag + 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/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli index abf8808ca..3bd04454c 100644 --- a/helm/software/components/tactics/paramodulation/saturation.mli +++ b/helm/software/components/tactics/paramodulation/saturation.mli @@ -25,21 +25,63 @@ (* $Id$ *) - -val saturate : +val saturate : (* FIXME: should be exported a a tactic *) bool -> HMysql.dbd -> ?full:bool -> ?depth:int -> ?width:int -> ?timeout:float -> - ?auto:(AutoTypes.flags -> ProofEngineTypes.proof -> Cic.context -> - ?universe:AutoTypes.universe -> - AutoTypes.cache -> ProofEngineTypes.goal list -> - Cic.substitution list * AutoTypes.cache * AutoTypes.universe) -> - ProofEngineTypes.proof * ProofEngineTypes.goal -> + ?auto:Inference.auto_type -> + ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list +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 find_equalities: + HMysql.dbd -> + ProofEngineTypes.status -> + bool -> (* smart_flag *) + ?auto:Inference.auto_type -> + AutoTypes.cache -> + Equality.equality_bag * + Equality.equality list * AutoTypes.cache * int +val saturate_more: + Equality.equality_bag -> + active_table -> + int -> (* maxmeta *) + ProofEngineTypes.status -> + bool -> (* smart flag *) + ?auto:Inference.auto_type -> + AutoTypes.cache -> + Equality.equality_bag * Equality.equality list * AutoTypes.cache * int + +val given_clause: + Equality.equality_bag -> + int -> (* maxmeta *) + ProofEngineTypes.status -> + active_table -> + passive_table -> + int -> int -> float -> + (Cic.substitution * + ProofEngineTypes.proof * + 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 @@ -48,16 +90,10 @@ 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 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 -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 +(* eof *) diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml index eabf24353..6ac2132aa 100644 --- a/helm/software/components/tactics/paramodulation/utils.ml +++ b/helm/software/components/tactics/paramodulation/utils.ml @@ -356,7 +356,7 @@ let compute_equality_weight e = d ); *) - w + d + w + d ;; (* old diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 139842435..16cff94d7 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -246,14 +246,14 @@ let rec count_prods context ty = Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t | _ -> 0 -let apply_with_subst ~term ~subst (proof, goal) = +let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = (* Assumption: The term "term" must be closed in the current context *) 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 newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with C.Var (uri,exp_named_subst) -> @@ -321,16 +321,17 @@ let apply_with_subst ~term ~subst (proof, goal) = ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv'' in - (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *) - (newproof, - List.map (function (i,_,_) -> i) new_uninstantiatedmetas)) + let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in + subst, + (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas), + max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst) (* ALB *) -let apply_with_subst ~term ?(subst=[]) status = +let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status = try (* apply_tac_verbose ~term status *) - apply_with_subst ~term ~subst status + apply_with_subst ~term ~subst ~maxmeta status (* TODO cacciare anche altre eccezioni? *) with | CicUnification.UnificationFailure msg @@ -339,7 +340,7 @@ let apply_with_subst ~term ?(subst=[]) status = (* ALB *) let apply_tac_verbose ~term status = - let subst, status = apply_with_subst ~term status in + let subst, status, _ = apply_with_subst ~term status in (CicMetaSubst.apply_subst subst), status let apply_tac ~term status = snd (apply_tac_verbose ~term status) diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli index c30952cae..6e0c821cc 100644 --- a/helm/software/components/tactics/primitiveTactics.mli +++ b/helm/software/components/tactics/primitiveTactics.mli @@ -44,8 +44,8 @@ val classify_metas : (* ALB, needed by the new paramodulation... *) val apply_with_subst: - term:Cic.term -> ?subst:Cic.substitution -> ProofEngineTypes.proof * int -> - Cic.substitution * (ProofEngineTypes.proof * int list) + term:Cic.term -> ?subst:Cic.substitution -> ?maxmeta:int -> ProofEngineTypes.proof * int -> + Cic.substitution * (ProofEngineTypes.proof * int list) * int (* not a real tactic *) val apply_tac_verbose : diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index dfca1c908..f146d45e6 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/components/tactics/tactics.ml @@ -27,7 +27,7 @@ let absurd = NegationTactics.absurd_tac let apply = PrimitiveTactics.apply_tac -let applyS = AutoTactic.applyS_tac +let applyS = Auto.applyS_tac let assumption = VariousTactics.assumption_tac let auto = AutoTactic.auto_tac let change = ReductionTactics.change_tac diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index a5d6f0086..9060afdd6 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Sep 25 18:28:48 CEST 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Sep 27 17:37:14 CEST 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic