X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=eaa146ed1d9cd71178fbc29c087a043529e17a9a;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=ddeab3e6e685892cda6ada1eab64db1cfdc0473a;hpb=cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0;p=helm.git diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index ddeab3e6e..eaa146ed1 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -48,7 +48,7 @@ let sqlpat_of_shellglob = let nonvar uri = not (UriManager.uri_is_var uri) -let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = +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 "^^ @@ -56,12 +56,12 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = (MetadataTypes.name_tbl ()) sql_pat MetadataTypes.library_name_tbl sql_pat in - let result = Mysql.exec dbd query in + let result = HMysql.exec dbd query in List.filter nonvar - (Mysql.map result + (HMysql.map result (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)) -let match_term ~(dbd:Mysql.dbd) ty = +let match_term ~(dbd:HMysql.dbd) ty = (* debug_print (lazy (CicPp.ppterm ty)); *) let metadata = MetadataExtractor.compute ~body:None ~ty in let constants_no = @@ -236,7 +236,7 @@ let cmatch' = fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature *) let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose let cmatch' = Constr.cmatch' -let signature_of_goal ~(dbd:Mysql.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,28 +254,53 @@ let signature_of_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) = let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in uris -let equations_for_goal ~(dbd:Mysql.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:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = + ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = let (_, metasenv, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let (uris, (main, sig_constants)) = @@ -357,7 +382,7 @@ let experimental_hint (aux uris) let new_experimental_hint - ~(dbd:Mysql.dbd) ?(facts=false) ?signature ~universe + ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe ((proof, goal) as status) = let (_, metasenv, _, _) = proof in @@ -583,10 +608,10 @@ let fwd_simpl ~dbd t = let from = "genLemma" in let where = Printf.sprintf "h_outer = \"%s\"" - (Mysql.escape (UriManager.string_of_uri outer)) in + (HMysql.escape (UriManager.string_of_uri outer)) in let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in - let result = Mysql.exec dbd query in - let lemmas = Mysql.map ~f:(map inners) result 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 @@ -604,5 +629,5 @@ let decomposables ~dbd = in let select, from = "source", "decomposables" in let query = Printf.sprintf "SELECT %s FROM %s" select from in - let decomposables = Mysql.map ~f:map (Mysql.exec dbd query) in + let decomposables = HMysql.map ~f:map (HMysql.exec dbd query) in map_filter (fun _ x -> x) 0 decomposables