From: Stefano Zacchiroli Date: Thu, 21 Oct 2004 08:14:13 +0000 (+0000) Subject: implemented in place old Filter_auto filtering X-Git-Tag: V_0_0_10~60 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=536faacc0486948d23c5fd02a693f0def64fb666;p=helm.git implemented in place old Filter_auto filtering --- diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 18ea81381..13a73b561 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -36,10 +36,13 @@ let locate ~(dbh:Dbi.connection) name = List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ()) let match_term ~(dbh:Dbi.connection) ty = - let metadata = MetadataExtractor.compute ~body:None ~ty in - Constr.at_least ~dbh metadata + let constraints = + List.map MetadataTypes.constr_of_metadata + (MetadataExtractor.compute ~body:None ~ty) + in + Constr.at_least ~dbh constraints -let nonvar (_, s) = +let nonvar s = let len = String.length s in let suffix = String.sub s (len-4) 4 in not (suffix = ".var") @@ -56,6 +59,28 @@ let signature_of_hypothesis context = Constr.StringSet.union set (Constr.constants_of t)) Constr.StringSet.empty context +let intersect l1 l2 = + let set1 = List.fold_right Constr.StringSet.add l1 Constr.StringSet.empty in + let set2 = List.fold_right Constr.StringSet.add l2 Constr.StringSet.empty in + Constr.StringSet.elements (Constr.StringSet.inter set1 set2) + +let filter_uris_forward ~dbh (main, constants) uris = + let main_uris = + match main with + | None -> [] + | Some (main, types) -> main :: types + in + let full_signature = + List.fold_right Constr.StringSet.add main_uris constants + in + List.filter (Constr.at_most ~dbh full_signature) uris + +let filter_uris_backward ~dbh signature uris = + let siguris = + List.map snd (MetadataConstraints.sigmatch ~dbh ~where:`Statement signature) + in + intersect uris siguris + let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) = let (_, metasenv, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in @@ -64,15 +89,7 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) = | Some signature -> (Constr.sigmatch ~dbh signature, signature) | None -> (Constr.cmatch' ~dbh ty, Constr.signature_of ty) in - let uris = List.filter nonvar uris in -(* - let concl_constants = - match main with - | None -> sig_constants - | Some (main, types) -> - List.fold_right Constr.StringSet.add sig_constants (main :: types) - in -*) + let uris = List.filter nonvar (List.map snd uris) in let types_constants = match main with | None -> Constr.StringSet.empty @@ -87,12 +104,10 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) = let uris = if (List.length uris < 2 ** (Constr.StringSet.cardinal other_constants)) then begin - prerr_endline - "MetadataQuery: large signature, falling back to old method"; - List.filter (Filter_auto.filter_new_constants ~dbh all_constants main) - uris + prerr_endline "MetadataQuery: large sig, falling back to old method"; + filter_uris_forward ~dbh (main, other_constants) uris end else - Filter_auto.filter_uris ~dbh all_constants uris main + filter_uris_backward ~dbh (main, other_constants) uris in List.map (fun uri -> @@ -100,4 +115,5 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) = ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri)) status)) + uris