From d78fbf3cface8f01d11f385757cbf47ae1866326 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Sep 2006 16:00:31 +0000 Subject: [PATCH] snapshot of queries for auto+paramod --- .../metadata/metadataConstraints.ml | 8 +- .../components/tactics/metadataQuery.ml | 76 ++++++++++++------- .../components/tactics/metadataQuery.mli | 5 +- 3 files changed, 59 insertions(+), 30 deletions(-) diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml index cb8460147..785f73fe4 100644 --- a/helm/software/components/metadata/metadataConstraints.ml +++ b/helm/software/components/metadata/metadataConstraints.ml @@ -29,7 +29,7 @@ open Printf open MetadataTypes let critical_value = 7 -let just_factor = 3 +let just_factor = 1 module UriManagerSet = UriManager.UriSet module SetSet = Set.Make (UriManagerSet) @@ -546,7 +546,10 @@ let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) maximal_prefixes) in (* Printf.fprintf stderr "all: %d\n" (List.length all);flush_all (); *) - List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in + List.filter (function (_,uri) -> + prerr_endline ("W" ^UriManager.string_of_uri uri); + at_most ~dbd ~where constants uri) all + in let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in greater_than @ equal_to @@ -624,6 +627,7 @@ let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) let types_no = List.length types in List.map (function (n,l) -> (n+types_no,types@l)) subsets in + prerr_endline ("critical_value exceded..." ^ string_of_int constants_no); let all_constants = let all = match main with None -> types | Some m -> m::types in List.fold_right UriManagerSet.add all constants diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml index a5c387971..0dc19582a 100644 --- a/helm/software/components/tactics/metadataQuery.ml +++ b/helm/software/components/tactics/metadataQuery.ml @@ -57,6 +57,7 @@ let signature_of_hypothesis context metasenv = CicTypeChecker.type_of_aux' metasenv current_ctx ty CicUniv.empty_ugraph in + let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in match sort with | Cic.Sort Cic.Prop -> set, hyp::current_ctx | _ -> Constr.UriManagerSet.union set (Constr.constants_of t), @@ -191,31 +192,11 @@ let cmatch' = *) let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose let cmatch' = Constr.cmatch' - -let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = - let (_, metasenv, _, _) = proof in - let (_, context, ty) = CicUtil.lookup_meta goal metasenv in - let main, sig_constants = Constr.signature_of ty in - let set = signature_of_hypothesis context metasenv in - let set = - match main with - None -> set - | Some (main,l) -> - List.fold_right Constr.UriManagerSet.add (main::l) set in - let set = Constr.UriManagerSet.union set sig_constants in - let all_constants_closed = close_with_types set metasenv context in - let uris = - sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in - let uris = List.filter nonvar (List.map snd uris) in - let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in - uris -;; - -let filter_predicate set ctx menv = - let is_predicate t = + +let is_predicate u = let ty, _ = try CicTypeChecker.type_of_aux' [] [] - (CicUtil.term_of_uri t) CicUniv.empty_ugraph + (CicUtil.term_of_uri u) CicUniv.empty_ugraph with CicTypeChecker.TypeCheckerFailure _ -> assert false in let rec check_last_pi = function @@ -223,9 +204,52 @@ let filter_predicate set ctx menv = | Cic.Sort Cic.Prop -> true | _ -> false in - not (check_last_pi ty) + check_last_pi ty +;; + +let universe_of_goals ~(dbd:HMysql.dbd) proof goals = + let (_, metasenv, _, _) = proof in + let add_uris_for acc goal = + let (_, context, ty) = CicUtil.lookup_meta goal metasenv in + let main, sig_constants = Constr.signature_of ty in + let set = signature_of_hypothesis context metasenv in + let set = + match main with + None -> set + | Some (main,l) -> + List.fold_right Constr.UriManagerSet.add (main::l) set in + let set = Constr.UriManagerSet.union set sig_constants in + let all_constants_closed = close_with_types set metasenv context in + Constr.UriManagerSet.union all_constants_closed acc + in + let all_constants_closed = + List.fold_left add_uris_for Constr.UriManagerSet.empty goals in + (* we split predicates from the rest *) + let predicates, rest = + Constr.UriManagerSet.partition is_predicate all_constants_closed + in + let uris = + Constr.UriManagerSet.fold + (fun u acc -> + let uris = + sigmatch ~dbd ~facts:false ~where:`Statement + (Some (u,[]),all_constants_closed) + in + acc @ uris) + predicates [] + in +(* + let uris = + sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in - Constr.UriManagerSet.filter is_predicate set +*) + let uris = List.filter nonvar (List.map snd uris) in + let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in + uris +;; + +let filter_out_predicate set ctx menv = + Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set ;; let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) = @@ -268,7 +292,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) = let set = signature_of_hypothesis context metasenv in (* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *) let set = Constr.UriManagerSet.union set sig_constants in - let set = filter_predicate set context metasenv in + let set = filter_out_predicate set context metasenv in let set = close_with_types set metasenv context in (* Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *) let set = close_with_constructors set metasenv context in diff --git a/helm/software/components/tactics/metadataQuery.mli b/helm/software/components/tactics/metadataQuery.mli index 0fa4a01df..c260d5e99 100644 --- a/helm/software/components/tactics/metadataQuery.mli +++ b/helm/software/components/tactics/metadataQuery.mli @@ -28,8 +28,9 @@ * @param pat shell like pattern matching over object names, a string where "*" * is interpreted as 0 or more characters and "?" as exactly one character *) -val signature_of_goal: - dbd:HMysql.dbd -> ProofEngineTypes.status -> UriManager.uri list +val universe_of_goals: + dbd:HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list -> + UriManager.uri list val equations_for_goal: dbd:HMysql.dbd -> -- 2.39.2