From: Andrea Asperti Date: Tue, 3 Oct 2006 12:56:38 +0000 (+0000) Subject: Changed auto from implicit to option and renamed a few functions. X-Git-Tag: make_still_working~6799 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b05fae519ae04a4a5dc79108f3d4ebe1bd4e112d;p=helm.git Changed auto from implicit to option and renamed a few functions. --- diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index c65826a4f..1e99c9b64 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -30,13 +30,13 @@ let debug_print s = () (*prerr_endline s;;*) (* {{{ *********** local given_clause wrapper ***********) -let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status = +let given_clause dbd ?tables maxm auto cache subst flags smart_flag status = let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout = match tables with | None -> (* first time, do a huge saturation *) let bag, equalities, cache, maxmeta = - Saturation.find_equalities dbd status ?auto smart_flag cache + Saturation.find_equalities dbd status smart_flag auto cache in let passive = Saturation.make_passive equalities in let active = Saturation.make_active [] in @@ -50,8 +50,8 @@ let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status = (* saturate a bit more if cache cahnged *) let bag, equalities, cache, maxm = if cache_size oldcache <> cache_size cache then - Saturation.saturate_more - bag active maxm status smart_flag ?auto cache + Saturation.close_more + bag active maxm status smart_flag auto cache else bag, [], cache, maxm in @@ -112,7 +112,7 @@ let new_metasenv_and_unify_and_t let flags = {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} in - given_clause dbd ?tables 0 cache [] flags true (proof'''',newmeta) + given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta) with | None, active, passive, bag,_,_ -> raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) @@ -269,7 +269,7 @@ let is_an_equational_goal = function ;; let equational_case - dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context + dbd tables maxm auto cache depth fake_proof goalno goalty subst context flags = let ppterm = ppterm context in @@ -280,7 +280,7 @@ let equational_case prerr_endline ""; *) match - given_clause dbd ?tables maxm ?auto cache subst flags false (fake_proof,goalno) + given_clause dbd ?tables maxm auto cache subst flags false (fake_proof,goalno) with | None, active,passive, bag, cache, maxmeta -> let tables = Some (active,passive,bag,cache) in @@ -475,7 +475,7 @@ let rec auto_main dbd tables maxm context flags elems cache = if is_equational_case goalty flags then match equational_case dbd tables maxm - ~auto:callback_for_paramod cache + (Some callback_for_paramod) cache depth fake_proof goalno goalty subst context flags with | Some elems, tables, cache, maxm -> diff --git a/helm/software/components/tactics/paramodulation/equality_retrieval.ml b/helm/software/components/tactics/paramodulation/equality_retrieval.ml index 4637a1a43..886cc7ffe 100644 --- a/helm/software/components/tactics/paramodulation/equality_retrieval.ml +++ b/helm/software/components/tactics/paramodulation/equality_retrieval.ml @@ -133,12 +133,12 @@ let equations_blacklist = *) let equations_blacklist = UriManager.UriSet.empty;; -(* {{{ ****************** SATURATION STUFF ***************************) -exception UnableToSaturate of AutoCache.cache * int +(*****************************************************************) +exception AutoFailure of AutoCache.cache * int -let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;; +let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;; -let saturate_term context metasenv oldnewmeta term cache auto fast = +let close_hypothesis_of_term context metasenv oldnewmeta term cache auto fast = let head, metasenv, args, newmeta = ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 in @@ -181,7 +181,7 @@ let saturate_term context metasenv oldnewmeta term cache auto fast = use_paramod=true;use_only_paramod=false} in match auto newmeta flags proof context cache args_for_auto with - | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta)) + | [],cache,newmeta -> raise (AutoFailure (cache,newmeta)) | substs,cache,newmeta -> List.map (fun subst -> @@ -202,7 +202,7 @@ let saturate_term context metasenv oldnewmeta term cache auto fast = (* }}} ***************************************************************) let find_context_equalities - maxmeta bag ?(auto = default_auto) context proof cache + maxmeta bag auto context proof cache = prerr_endline "find_equalities"; let module C = Cic in @@ -210,6 +210,12 @@ let find_context_equalities let module T = CicTypeChecker in let _,metasenv,_,_ = proof in let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in + let use_auto, auto = + match auto with + | None -> false, default_auto + | Some auto -> true, auto in + (* if use_auto is true, we try to close the hypothesis of equational + statements using auto; a naif, and probably wrong approach *) let rec aux cache index newmeta = function | [] -> [], newmeta,cache | (Some (_, C.Decl (term)))::tl -> @@ -218,11 +224,11 @@ let find_context_equalities (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term))); let do_find context term = match term with - | C.Prod (name, s, t) when is_an_equality t -> + | C.Prod (name, s, t) when (is_an_equality t && use_auto) -> (try let term = S.lift index term in let saturated,cache,newmeta = - saturate_term context metasenv newmeta term + close_hypothesis_of_term context metasenv newmeta term cache auto false in let eqs,newmeta = @@ -236,7 +242,7 @@ let find_context_equalities ([],newmeta) saturated in eqs, newmeta, cache - with UnableToSaturate (cache,newmeta) -> + with AutoFailure (cache,newmeta) -> [],newmeta,cache) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when LibraryObjects.is_eq_URI uri -> @@ -261,7 +267,7 @@ let find_context_equalities ;; let find_library_equalities bag - ?(auto = default_auto) caso_strano dbd context status maxmeta cache + auto caso_strano dbd context status maxmeta cache = let module C = Cic in let module S = CicSubstitution in @@ -296,6 +302,12 @@ let find_library_equalities bag 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 use_auto, auto = + match auto with + | None -> false, default_auto + | Some auto -> true, auto in + (* if use_auto is true, we try to close the hypothesis of equational + statements using auto; a naif, and probably wrong approach *) let rec aux cache newmeta = function | [] -> [], newmeta, cache | (uri, term, termty)::tl -> @@ -305,10 +317,10 @@ let find_library_equalities bag (CicPp.ppterm term) (CicPp.ppterm termty))); let res, newmeta, cache = match termty with - | C.Prod (name, s, t) -> + | C.Prod (name, s, t) when use_auto -> (try let saturated,cache,newmeta = - saturate_term context metasenv newmeta termty + close_hypothesis_of_term context metasenv newmeta termty cache auto true in let eqs,newmeta = @@ -327,8 +339,9 @@ let find_library_equalities bag ([],newmeta) saturated in eqs, newmeta , cache - with UnableToSaturate (cache,newmeta) -> + with AutoFailure (cache,newmeta) -> [], newmeta , cache) + | C.Prod _ -> [], newmeta, cache | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in [e], newmeta+1, cache diff --git a/helm/software/components/tactics/paramodulation/equality_retrieval.mli b/helm/software/components/tactics/paramodulation/equality_retrieval.mli index e9506580d..7a24e3a55 100644 --- a/helm/software/components/tactics/paramodulation/equality_retrieval.mli +++ b/helm/software/components/tactics/paramodulation/equality_retrieval.mli @@ -43,7 +43,7 @@ type auto_type = val find_context_equalities: int -> (* maxmeta *) Equality.equality_bag -> - ?auto:auto_type -> + auto_type option -> Cic.context -> ProofEngineTypes.proof -> (* FIXME:Why bot context and proof?*) AutoCache.cache -> int list * Equality.equality list * int * AutoCache.cache @@ -53,7 +53,7 @@ val find_context_equalities: *) val find_library_equalities: Equality.equality_bag -> - ?auto:auto_type -> + auto_type option-> bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> AutoCache.cache -> UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int * diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index b5026d320..dc1f1273f 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -1367,7 +1367,7 @@ let build_proof final_subst, proof, open_goals ;; -let find_equalities dbd status smart_flag ?auto cache = +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 @@ -1375,14 +1375,14 @@ let find_equalities dbd status smart_flag ?auto cache = let env = (metasenv, context, CicUniv.empty_ugraph) in let bag = Equality.mk_equality_bag () in let eq_indexes, equalities, maxm, cache = - Equality_retrieval.find_context_equalities 0 bag ?auto context proof cache + Equality_retrieval.find_context_equalities 0 bag auto context proof cache in prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>"; List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities; prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; let lib_eq_uris, library_equalities, maxm, cache = Equality_retrieval.find_library_equalities bag - ?auto smart_flag dbd context (proof, goalno) (maxm+2) + auto smart_flag dbd context (proof, goalno) (maxm+2) cache in prerr_endline (">>>>>>>>>> gained from the library >>>>>>>>>>>>" ^ @@ -1402,14 +1402,14 @@ let find_equalities dbd status smart_flag ?auto cache = bag, equalities, cache, maxm ;; -let saturate_more bag active maxmeta status smart_flag ?auto cache = +let close_more bag active maxmeta status smart_flag auto cache = let proof, goalno = status in let _, metasenv,_,_ = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in let env = (metasenv, context, CicUniv.empty_ugraph) in let eq_indexes, equalities, maxm, cache = - Equality_retrieval.find_context_equalities maxmeta bag ?auto context proof cache + Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache in prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^ string_of_int maxm); @@ -1431,7 +1431,7 @@ let saturate_more bag active maxmeta status smart_flag ?auto cache = let saturate smart_flag dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) - ?(timeout=600.) ?auto status = + ?(timeout=600.) auto status = let module C = Cic in reset_refs (); maxdepth := depth; @@ -1447,7 +1447,7 @@ let saturate let env = (metasenv, context, ugraph) in let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in let bag, equalities, cache, maxm = - find_equalities dbd status smart_flag ?auto AutoCache.cache_empty + find_equalities dbd status smart_flag auto AutoCache.cache_empty in let res, time = maxmeta := maxm+2; @@ -1557,10 +1557,10 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = let eq_uri = eq_of_goal ty in let bag = Equality.mk_equality_bag () in let eq_indexes, equalities, maxm, cache = - Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty + Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in let lib_eq_uris, library_equalities, maxm, cache = - Equality_retrieval.find_library_equalities bag + Equality_retrieval.find_library_equalities bag None false dbd context (proof, goal) (maxm+2) cache in if library_equalities = [] then prerr_endline "VUOTA!!!"; @@ -1638,7 +1638,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = let names = Utils.names_of_context context in let bag = Equality.mk_equality_bag () in let eq_index, equalities, maxm,cache = - Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty + Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in let eq_what = let what = find_in_ctx 1 target context in @@ -1743,12 +1743,12 @@ let retrieve_and_print dbd term metasenv ugraph = let eq_uri = eq_of_goal type_of_goal in let bag = Equality.mk_equality_bag () in let eq_indexes, equalities, maxm,cache = - Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in + Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm, cache = - Equality_retrieval.find_library_equalities bag + Equality_retrieval.find_library_equalities bag None false dbd context (proof, goal') (maxm+2) cache in let t2 = Unix.gettimeofday () in @@ -1827,9 +1827,9 @@ let main_demod_equalities dbd term metasenv ugraph = let eq_uri = eq_of_goal goal in let bag = Equality.mk_equality_bag () in let eq_indexes, equalities, maxm, cache = - Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in + Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in let lib_eq_uris, library_equalities, maxm,cache = - Equality_retrieval.find_library_equalities bag + Equality_retrieval.find_library_equalities bag None false dbd context (proof, goal') (maxm+2) cache in let library_equalities = List.map snd library_equalities in diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli index d16c9e28a..aa8f24ec3 100644 --- a/helm/software/components/tactics/paramodulation/saturation.mli +++ b/helm/software/components/tactics/paramodulation/saturation.mli @@ -32,7 +32,7 @@ val saturate : (* FIXME: should be exported a a tactic *) ?depth:int -> ?width:int -> ?timeout:float -> - ?auto:Equality_retrieval.auto_type -> + Equality_retrieval.auto_type option -> ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list @@ -46,17 +46,18 @@ val find_equalities: HMysql.dbd -> ProofEngineTypes.status -> bool -> (* smart_flag *) - ?auto:Equality_retrieval.auto_type -> - AutoCache.cache -> + Equality_retrieval.auto_type option -> + AutoCache.cache -> Equality.equality_bag * Equality.equality list * AutoCache.cache * int -val saturate_more: + +val close_more: Equality.equality_bag -> active_table -> int -> (* maxmeta *) ProofEngineTypes.status -> bool -> (* smart flag *) - ?auto:Equality_retrieval.auto_type -> + Equality_retrieval.auto_type option -> AutoCache.cache -> Equality.equality_bag * Equality.equality list * AutoCache.cache * int