X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=b9c0536538e4295726347b7ad82071e1c89ed160;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=c266502cb16fa50378252228c2f3c7af2e9dea7c;hpb=259a4a2080cc5af5b20da1cd9133eb32f28c5d8f;p=helm.git diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index c266502cb..b9c053653 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -23,87 +23,19 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf +let nonvar uri = not (UriManager.uri_is_var uri) + module Constr = MetadataConstraints -module PET = ProofEngineTypes exception Goal_is_not_an_equation let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) - (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for - * the "like" operator (which uses '%' and '_'). Does not support escaping. *) -let sqlpat_of_shellglob = - let star_RE, qmark_RE, percent_RE, uscore_RE = - Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_" - in - fun shellglob -> - Pcre.replace ~rex:star_RE ~templ:"%" - (Pcre.replace ~rex:qmark_RE ~templ:"_" - (Pcre.replace ~rex:percent_RE ~templ:"\\%" - (Pcre.replace ~rex:uscore_RE ~templ:"\\_" - shellglob))) - -let nonvar uri = not (UriManager.uri_is_var uri) - -let locate ~(dbd:HMysql.dbd) ?(vars = false) pat = - let sql_pat = sqlpat_of_shellglob pat in - let query = - sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^ - "SELECT source FROM %s WHERE value LIKE \"%s\"") - (MetadataTypes.name_tbl ()) sql_pat - MetadataTypes.library_name_tbl sql_pat - in - let result = HMysql.exec dbd query in - List.filter nonvar - (HMysql.map result - (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)) - -let match_term ~(dbd:HMysql.dbd) ty = -(* debug_print (lazy (CicPp.ppterm ty)); *) - let metadata = MetadataExtractor.compute ~body:None ~ty in - let constants_no = - MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty) - in - let full_card, diff = - if CicUtil.is_meta_closed ty then - Some (MetadataConstraints.Eq constants_no), None - else - let diff_no = - let (hyp_constants, concl_constants) = - (* collect different constants in hypotheses and conclusions *) - List.fold_left - (fun ((hyp, concl) as acc) metadata -> - match (metadata: MetadataTypes.metadata) with - | `Sort _ | `Rel _ -> acc - | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _) - when not (List.mem uri concl) -> (hyp, uri :: concl) - | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _) - when not (List.mem uri hyp) -> (uri :: hyp, concl) - | `Obj _ -> acc) - ([], []) - metadata - in - List.length hyp_constants - List.length concl_constants - in - let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in - let diff = - if MetadataExtractor.IntSet.equal concl_metas hyp_metas then - Some (MetadataConstraints.Eq diff_no) - else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then - Some (MetadataConstraints.Gt (diff_no - 1)) - else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then - Some (MetadataConstraints.Lt (diff_no + 1)) - else - None - in - None, diff - in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - Constr.at_least ~dbd ?full_card ?diff constraints - let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y)) let signature_of_hypothesis context = @@ -133,7 +65,9 @@ let sigmatch = let profiler = CicUtil.profile "sigmatch" in fun ~dbd ~facts ~where signature -> profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature -*) let at_most = Constr.at_most let sigmatch = MetadataConstraints.sigmatch +*) +let at_most = Constr.at_most +let sigmatch = MetadataConstraints.sigmatch let filter_uris_forward ~dbd (main, constants) uris = let main_uris = @@ -234,9 +168,11 @@ let sigmatch = let cmatch' = let profiler = CicUtil.profile "cmatch'" in fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature -*) let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose let cmatch' = Constr.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 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 @@ -254,25 +190,50 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) = let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in uris -let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) = +let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = +(* let to_string set = + "{ " ^ + (String.concat ", " + (Constr.UriManagerSet.fold + (fun u l -> (UriManager.string_of_uri u)::l) set [])) + ^ " }" + in *) let (_, metasenv, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let main, sig_constants = Constr.signature_of ty in - match main with - None -> raise Goal_is_not_an_equation - | Some (m,l) -> - if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then - let set = signature_of_hypothesis context in - let set = Constr.UriManagerSet.union set sig_constants in - let set = close_with_types set metasenv context in - let set = close_with_constructors set metasenv context in - let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in - let uris = - sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in - let uris = List.filter nonvar (List.map snd uris) in - let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in - uris - else raise Goal_is_not_an_equation +(* Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *) +(* match main with *) +(* None -> raise Goal_is_not_an_equation *) +(* | Some (m,l) -> *) + let m, l = + let eq_URI = + let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + UriManager.uri_of_string (us ^ "#xpointer(1/1)") + in + match main with + | None -> eq_URI, [] + | Some (m, l) when UriManager.eq m eq_URI -> m, l + | Some (m, l) -> eq_URI, [] + in + Printf.printf "\nSome (m, l): %s, [%s]\n\n" + (UriManager.string_of_uri m) + (String.concat "; " (List.map UriManager.string_of_uri l)); + (* if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *) + let set = signature_of_hypothesis context in + (* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *) + let set = Constr.UriManagerSet.union set sig_constants 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 + (* Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *) + let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in + let uris = + sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in + let uris = List.filter nonvar (List.map snd uris) in + let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in + uris + (* ) *) + (* else raise Goal_is_not_an_equation *) let experimental_hint ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = @@ -404,205 +365,3 @@ let new_experimental_hint Pervasives.compare (List.length goals1) (List.length goals2)) (aux uris) -let elim ~dbd uri = - let constraints = - [`Rel [`MainConclusion None]; - `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]); - `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]); - `Obj (uri,[`InHypothesis]); - ] - in - MetadataConstraints.at_least ~rating:`Hits ~dbd constraints - - -let fill_with_dummy_constants t = - let rec aux i types = - function - Cic.Lambda (n,s,t) -> - let dummy_uri = - UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in - (aux (i+1) (s::types) - (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t)) - | t -> t,types - in - let t,types = aux 0 [] t in - t, List.rev types - -let instance ~dbd t = - let t',types = fill_with_dummy_constants t in - let metadata = MetadataExtractor.compute ~body:None ~ty:t' in -(* List.iter - (fun x -> - debug_print - (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x)))) - metadata; *) - let no_concl = MetadataDb.count_distinct `Conclusion metadata in - let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in - let no_full = MetadataDb.count_distinct `Statement metadata in - let is_dummy = function - | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy" - | _ -> true - in - let rec look_for_dummy_main = function - | [] -> None - | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_ - when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") -> - let s = UriManager.string_of_uri s in - let len = String.length s in - let dummy_index = int_of_string (String.sub s 11 (len-15)) in - let dummy_type = List.nth types dummy_index in - Some (d,dummy_type) - | _::l -> look_for_dummy_main l - in - match (look_for_dummy_main metadata) with - | None-> -(* debug_print (lazy "Caso None"); *) - (* no dummy in main position *) - let metadata = List.filter is_dummy metadata in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - let concl_card = Some (MetadataConstraints.Eq no_concl) in - let full_card = Some (MetadataConstraints.Eq no_full) in - let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in - Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints - | Some (depth, dummy_type) -> -(* debug_print - (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *) - (* a dummy in main position *) - let metadata_for_dummy_type = - MetadataExtractor.compute ~body:None ~ty:dummy_type in - (* Let us skip this for the moment - let main_of_dummy_type = - look_for_dummy_main metadata_for_dummy_type in *) - let metadata = List.filter is_dummy metadata in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - let metadata_for_dummy_type = - List.filter is_dummy metadata_for_dummy_type in - let metadata_for_dummy_type, depth' = - (* depth' = the depth of the A -> A -> Prop *) - List.fold_left (fun (acc,dep) c -> - match c with - | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> - (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i - | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> - (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i - | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) -> - (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i - | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type - in - let constraints_for_dummy_type = - List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in - (* start with the dummy constant in main conlusion *) - let from = ["refObj as table0"] in - let where = - [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos; - sprintf "table0.h_depth >= %d" depth] in - let (n,from,where) = - List.fold_left - (MetadataConstraints.add_constraint ~start:2) - (2,from,where) constraints in - let concl_card = Some (MetadataConstraints.Eq no_concl) in - let full_card = Some (MetadataConstraints.Eq no_full) in - let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in - let (n,from,where) = - MetadataConstraints.add_all_constr - (n,from,where) concl_card full_card diff in - (* join with the constraints over the type of the constant *) - let where = - (sprintf "table0.h_occurrence = table%d.source" n)::where in - let where = - sprintf "table0.h_depth - table%d.h_depth = %d" - n (depth - depth')::where - in - let (m,from,where) = - List.fold_left - (MetadataConstraints.add_constraint ~start:n) - (n,from,where) constraints_for_dummy_type in - Constr.exec ~dbd (m,from,where) - -(* fwd_simpl ****************************************************************) - -let rec map_filter f n = function - | [] -> [] - | hd :: tl -> - match f n hd with - | None -> map_filter f (succ n) tl - | Some hd -> hd :: map_filter f (succ n) tl - -let get_uri t = - let aux = function - | Cic.Appl (hd :: tl) -> Some (CicUtil.uri_of_term hd, tl) - | hd -> Some (CicUtil.uri_of_term hd, []) - in - try aux t with - | Invalid_argument "uri_of_term" -> None - -let get_metadata t = - let f n t = - match get_uri t with - | None -> None - | Some (uri, _) -> Some (n, uri) - in - match get_uri t with - | None -> None - | Some (uri, args) -> Some (uri, map_filter f 1 args) - -let debug_metadata = function - | None -> () - | Some (outer, inners) -> - let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n (UriManager.string_of_uri uri) in - Printf.eprintf "\n%s: %s\n" "fwd" (UriManager.string_of_uri outer); - List.iter f inners; prerr_newline () - -let fwd_simpl ~dbd t = - let map inners row = - match row.(0), row.(1), row.(2) with - | Some source, Some inner, Some index -> - source, - List.mem - (int_of_string index, (UriManager.uri_of_string inner)) inners - | _ -> "", false - in - let rec rank ranks (source, ok) = - match ranks, ok with - | [], false -> [source, 0] - | [], true -> [source, 1] - | (uri, i) :: tl, false when uri = source -> (uri, 0) :: tl - | (uri, 0) :: tl, true when uri = source -> (uri, 0) :: tl - | (uri, i) :: tl, true when uri = source -> (uri, succ i) :: tl - | hd :: tl, _ -> hd :: rank tl (source, ok) - in - let compare (_, x) (_, y) = compare x y in - let filter n (uri, rank) = - if rank > 0 then Some (UriManager.uri_of_string uri) else None - in - let metadata = get_metadata t in debug_metadata metadata; - match metadata with - | None -> [] - | Some (outer, inners) -> - let select = "source, h_inner, h_index" in - let from = "genLemma" in - let where = - Printf.sprintf "h_outer = \"%s\"" - (HMysql.escape (UriManager.string_of_uri outer)) in - let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in - let result = HMysql.exec dbd query in - let lemmas = HMysql.map ~f:(map inners) result in - let ranked = List.fold_left rank [] lemmas in - let ordered = List.rev (List.fast_sort compare ranked) in - map_filter filter 0 ordered - -(* get_decomposables ********************************************************) - -let decomposables ~dbd = - let map row = match row.(0) with - | None -> None - | Some str -> - match CicUtil.term_of_uri (UriManager.uri_of_string str) with - | Cic.MutInd (uri, typeno, _) -> Some (uri, typeno) - | _ -> - raise (UriManager.IllFormedUri str) - in - let select, from = "source", "decomposables" in - let query = Printf.sprintf "SELECT %s FROM %s" select from in - let decomposables = HMysql.map ~f:map (HMysql.exec dbd query) in - map_filter (fun _ x -> x) 0 decomposables