X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fmetadata%2FmetadataConstraints.ml;h=c2dee6f5edb40cdc839ea5df43f1d8f56e96f800;hb=66929b8edb58d468a134b648466f3e9c45ba5c0e;hp=d7192bd7e75e12c65f1c0d12922ec6e5e3f31673;hpb=2907089ebbbe440dacf8f64d4599d881b2c03fcf;p=helm.git diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml index d7192bd7e..c2dee6f5e 100644 --- a/helm/software/components/metadata/metadataConstraints.ml +++ b/helm/software/components/metadata/metadataConstraints.ml @@ -153,7 +153,7 @@ let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata = in ((n+2), from, where) -let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) = +let exec ~(dbd:HSql.dbd) ?rating (n,from,where) = let from = String.concat ", " from in let where = String.concat " and " where in let query = @@ -166,12 +166,12 @@ let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) = from where in (* prerr_endline query; *) - let result = HMysql.exec dbd query in - HMysql.map result + let result = HSql.exec dbd query in + HSql.map result (fun row -> match row.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false) -let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables +let at_least ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables (metadata: MetadataTypes.constr list) = let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables in @@ -191,7 +191,7 @@ let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables ;; let at_least - ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating + ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating (metadata: MetadataTypes.constr list) = if are_tables_ownerized () then @@ -438,7 +438,7 @@ let must_of_prefix ?(where = `Conclusion) m s = let escape = Str.global_replace (Str.regexp_string "\'") "\\'" -let get_constants (dbd:HMysql.dbd) ~where uri = +let get_constants (dbd:HSql.dbd) ~where uri = let uri = escape (UriManager.string_of_uri uri) in let positions = match where with @@ -458,16 +458,16 @@ let get_constants (dbd:HMysql.dbd) ~where uri = MetadataTypes.library_obj_tbl uri pos_predicate in - let result = HMysql.exec dbd query in + let result = HSql.exec dbd query in let set = ref UriManagerSet.empty in - HMysql.iter result + HSql.iter result (fun col -> match col.(0) with | Some uri -> set := UriManagerSet.add (UriManager.uri_of_string uri) !set | _ -> assert false); !set -let at_most ~(dbd:HMysql.dbd) ?(where = `Conclusion) only u = +let at_most ~(dbd:HSql.dbd) ?(where = `Conclusion) only u = let inconcl = get_constants dbd ~where u in UriManagerSet.subset inconcl only @@ -485,7 +485,7 @@ let myspeciallist = 0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal3.con"] -let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes = +let compute_exactly ~(dbd:HSql.dbd) ?(facts=false) ~where main prefixes = List.concat (List.map (fun (m,s) -> @@ -516,7 +516,7 @@ let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes = (* critical value reached, fallback to "only" constraints *) -let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) +let compute_with_only ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion) main prefixes constants = let max_prefix_length = @@ -557,7 +557,7 @@ let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) (* real match query implementation *) -let cmatch ~(dbd:HMysql.dbd) ?(facts=false) t = +let cmatch ~(dbd:HSql.dbd) ?(facts=false) t = let (main, constants) = signature_of t in match main with | None -> [] @@ -611,7 +611,7 @@ let power consts = type where = [ `Conclusion | `Statement ] -let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) +let sigmatch ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion) (main, constants) = let main,types =