From 4bc5e3edbedb79e13f16a09abe18ee38e9c78a20 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 12:40:58 +0000 Subject: [PATCH] - changed metadata type so that positions contains depth - introduced constraints (vs metadata) - positions no longer hard coded (so that both short and long names are supported) - added "where" parameter so that matching could be perfomed either on conclusion only or on the whole statement --- helm/ocaml/metadata/metadataConstraints.ml | 104 ++++++++++++-------- helm/ocaml/metadata/metadataConstraints.mli | 14 ++- helm/ocaml/metadata/metadataDb.ml | 14 +-- helm/ocaml/metadata/metadataPp.ml | 26 ++--- helm/ocaml/metadata/metadataTypes.ml | 9 ++ 5 files changed, 103 insertions(+), 64 deletions(-) diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 314ceba53..2e5250f62 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -69,18 +69,20 @@ let mk_positions positions cur_tbl = let add_card_constr tbl (n,from,where) = function | None -> (n,from,where) | Some (Eq card) -> + let cur_tbl = tbln n in (n+1, - (sprintf "%s as %s" tbl (tbln n) :: from), - (sprintf "no=%d" card :: + (sprintf "%s as %s" tbl cur_tbl :: from), + (sprintf "%s.no=%d" cur_tbl card :: (if n=0 then [] - else [sprintf "table0.source = %s.source" (tbln n)]) @ + else [sprintf "table0.source = %s.source" cur_tbl]) @ where)) | Some (Gt card) -> + let cur_tbl = tbln n in (n+1, - (sprintf "%s as %s" tbl (tbln n) :: from), - (sprintf "no>%d" card :: + (sprintf "%s as %s" tbl cur_tbl :: from), + (sprintf "%s.no>%d" cur_tbl card :: (if n=0 then [] - else [sprintf "table0.source = %s.source" (tbln n)]) @ + else [sprintf "table0.source = %s.source" cur_tbl]) @ where)) let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card @@ -135,7 +137,6 @@ let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card let from = String.concat ", " from in let where = String.concat " and " where in let query = sprintf "select table0.source from %s where %s" from where in -prerr_endline query; let query = dbh#prepare query in query#execute []; List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ()) @@ -170,8 +171,8 @@ and add_root n root childs = (SetSet.singleton (StringSet.singleton root)) and inspect_conclusion n t = -if n = 0 then SetSet.empty -else match t with + if n = 0 then SetSet.empty + else match t with Cic.Rel _ | Cic.Meta _ | Cic.Sort _ @@ -362,17 +363,30 @@ let union l = | u::l -> u::(drop_repetitions l) in drop_repetitions (List.sort Pervasives.compare (List.concat l)) -let must_of_prefix m s = - let s' = List.map (fun u -> `Obj (u, [`InConclusion])) s in +let must_of_prefix ?(where = `Conclusion) m s = + let positions = + match where with + | `Conclusion -> [`InConclusion] + | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None] + in + let s' = List.map (fun u -> `Obj (u, positions)) s in `Obj (m, [`MainConclusion None]) :: s' let escape = Str.global_replace (Str.regexp_string "\'") "\\'" -let get_inconcl (dbh:Dbi.connection) uri = +let get_constants (dbh:Dbi.connection) ~where uri = let uri = escape uri in + let positions = + match where with + | `Conclusion -> ["\"MainConclusion\""; "\"InConclusion\""] + | `Statement -> + ["\"MainConclusion\""; "\"InConclusion\""; "\"InHypothesis\""; + "\"MainHypothesis\""] + in let query = - dbh#prepare (sprintf "select h_occurrence from refObj where source=\"%s\" and (h_position=\"MainConclusion\" or h_position=\"InConclusion\")" - uri) + dbh#prepare + (sprintf "select h_occurrence from refObj where source=\"%s\" and (%s)" + uri (String.concat " or " positions)) in query#execute []; query#fold_left (* transform the result in a set *) @@ -381,8 +395,8 @@ let get_inconcl (dbh:Dbi.connection) uri = StringSet.add uri set) StringSet.empty -let test_only ~(dbh:Dbi.connection) only u = - let inconcl = get_inconcl dbh u in +let at_most ~(dbh:Dbi.connection) ?(where = `Conclusion) only u = + let inconcl = get_constants dbh ~where u in StringSet.subset inconcl only (* Special handling of equality. The problem is filtering out theorems just @@ -396,7 +410,7 @@ let myspeciallist = 0,"cic:/Coq/Init/Logic/f_equal2.con"; 0,"cic:/Coq/Init/Logic/f_equal3.con"] -let compute_exactly ~(dbh:Dbi.connection) main prefixes = +let compute_exactly ~(dbh:Dbi.connection) where main prefixes = List.concat (List.map (fun (m,s) -> @@ -404,13 +418,18 @@ let compute_exactly ~(dbh:Dbi.connection) main prefixes = myspeciallist else let res = - at_least ~dbh ~concl_card:(Eq (m+1)) (must_of_prefix main s) + let must = must_of_prefix ~where main s in + match where with + | `Conclusion -> at_least ~dbh ~concl_card:(Eq (m+1)) must + | `Statement -> at_least ~dbh ~full_card:(Eq (m+1)) must in List.map (fun uri -> (m, uri)) res) prefixes) (* critical value reached, fallback to "only" constraints *) -let compute_with_only ~(dbh:Dbi.connection) main prefixes constants = +let compute_with_only ~(dbh:Dbi.connection) ?(where = `Conclusion) main + prefixes constants += let max_prefix_length = match prefixes with | [] -> assert false @@ -426,15 +445,18 @@ let compute_with_only ~(dbh:Dbi.connection) main prefixes constants = union (List.map (fun (m,s) -> + let must = must_of_prefix ~where main s in (let res = - at_least ~dbh ~concl_card:(Gt (m+1)) (must_of_prefix main s) + match where with + | `Conclusion -> at_least ~dbh ~concl_card:(Gt (m+1)) must + | `Statement -> at_least ~dbh ~full_card:(Gt (m+1)) must in (* we tag the uri with m+1, for sorting purposes *) List.map (fun uri -> (m+1, uri)) res)) maximal_prefixes) in - List.filter (function (_,uri) -> test_only ~dbh constants uri) all in - let equal_to = compute_exactly ~dbh main prefixes in + List.filter (function (_,uri) -> at_most ~dbh ~where constants uri) all in + let equal_to = compute_exactly ~dbh where main prefixes in greater_than @ equal_to (* real match query implementation *) @@ -454,23 +476,25 @@ let cmatch ~(dbh:Dbi.connection) t = in compute_with_only ~dbh main all_concl all_constants | _, _ -> []) - else if constants_no = 0 then [] else (* in this case we compute all prefixes, and we do not need to apply the only constraints *) - let prefixes = prefixes constants_no t in + let prefixes = + if constants_no = 0 then + Some main, [0, []; List.length types, types] + else + prefixes constants_no t + in (match prefixes with - Some main, all_concl -> - List.concat - (List.map - (fun (m,s) -> - (let res = - at_least ~dbh ~concl_card:(Eq (m+1)) - (must_of_prefix main s) - in - List.map (fun uri -> (m, uri)) res)) - all_concl) - | _, _ -> []) + Some main, all_concl -> + List.concat + (List.map + (fun (m,s) -> + let must = must_of_prefix ~where:`Conclusion main s in + let res = at_least ~dbh ~concl_card:(Eq (m+1)) must in + List.map (fun uri -> (m, uri)) res) + all_concl) + | _, _ -> []) let power_upto upto consts = let l = StringSet.elements consts in @@ -488,7 +512,9 @@ let power consts = (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res)) [(0,[])] l) -let sigmatch ~(dbh:Dbi.connection) (main, constants) = +type where = [ `Conclusion | `Statement ] + +let sigmatch ~(dbh:Dbi.connection) ?(where = `Conclusion) (main, constants) = match main with None -> [] | Some (main, types) -> @@ -502,14 +528,14 @@ let sigmatch ~(dbh:Dbi.connection) (main, constants) = let all_constants = List.fold_right StringSet.add types (StringSet.add main constants) in - compute_with_only ~dbh main subsets all_constants + compute_with_only ~dbh ~where main subsets all_constants else let subsets = let subsets = power constants in let types_no = List.length types in - List.map (function (n,l) -> (n+types_no,types@l)) subsets + (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets in - compute_exactly ~dbh main subsets + compute_exactly ~dbh where main subsets (* match query wrappers *) let cmatch' = cmatch diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli index ec6d81f38..ecdb3e6b2 100644 --- a/helm/ocaml/metadata/metadataConstraints.mli +++ b/helm/ocaml/metadata/metadataConstraints.mli @@ -41,7 +41,13 @@ val cmatch: dbh:Dbi.connection -> Cic.term -> string list * relevance information: higher the tag, higher the relevance *) val cmatch': dbh:Dbi.connection -> Cic.term -> (int * string) list -val sigmatch: dbh:Dbi.connection -> term_signature -> (int * string) list +type where = [ `Conclusion | `Statement ] (** signature matching extent *) + + (** @param where defaults to `Conclusion *) +val sigmatch: + dbh:Dbi.connection -> + ?where:where -> term_signature -> + (int * string) list (** {2 Constraint engine} *) @@ -60,6 +66,12 @@ val at_least: MetadataTypes.constr list -> string list + (** @param where defaults to `Conclusion *) +val at_most: + dbh:Dbi.connection -> + ?where:where -> StringSet.t -> + (string -> bool) + val signature_of: Cic.term -> term_signature val constants_of: Cic.term -> StringSet.t diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index e7e60faff..f4ce2dd39 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -27,16 +27,6 @@ open MetadataTypes open Printf -module DB = Dbi_mysql - -(* let baseuri = "http://www.cs.unibo.it/helm/schemas/schema-helm#" *) -let baseuri = "" -let inconcl_uri = baseuri ^ "InConclusion" -let mainconcl_uri = baseuri ^ "MainConclusion" -let mainhyp_uri = baseuri ^ "MainHypothesis" -let inhyp_uri = baseuri ^ "InHypothesis" -let inbody_uri = baseuri ^ "InBody" - let prepare_insert (dbh: Dbi.connection) = let insert_owner = dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\")" owners_tbl) @@ -63,14 +53,14 @@ let execute_insert dbh (insert_owner, insert_sort, insert_rel, insert_obj) let insert_const_no dbh uri = let inconcl_no = sprintf "INSERT INTO %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\"" - conclno_tbl uri obj_tbl inconcl_uri mainconcl_uri uri + conclno_tbl uri obj_tbl inconcl_pos mainconcl_pos uri in let concl_hyp = sprintf "INSERT INTO %s SELECT \"%s\",COUNT(DISTINCT h_occurrence) FROM %s WHERE NOT (h_position=\"%s\") AND (source = \"%s\")" - conclno_hyp_tbl uri obj_tbl inbody_uri uri + conclno_hyp_tbl uri obj_tbl inbody_pos uri in (dbh#prepare inconcl_no)#execute []; (dbh#prepare concl_hyp)#execute [] diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml index 2ce9f2226..e83aa7c86 100644 --- a/helm/ocaml/metadata/metadataPp.ml +++ b/helm/ocaml/metadata/metadataPp.ml @@ -25,6 +25,8 @@ open Printf +open MetadataTypes + let pp_position = function | `MainConclusion (Some d) -> sprintf "MainConclusion(%d)" d | `MainConclusion None -> sprintf "MainConclusion" @@ -35,20 +37,20 @@ let pp_position = function | `InBody -> "InBody" let pp_position_tag = function - | `MainConclusion _ -> "MainConclusion" - | `MainHypothesis _ -> "MainHypothesis" - | `InConclusion -> "InConclusion" - | `InHypothesis -> "InHypothesis" - | `InBody -> "InBody" + | `MainConclusion _ -> mainconcl_pos + | `MainHypothesis _ -> mainhyp_pos + | `InConclusion -> inconcl_pos + | `InHypothesis -> inhyp_pos + | `InBody -> inbody_pos let columns_of_position = function - | `MainConclusion (Some d) -> `String "MainConclusion", `Int d - | `MainConclusion None -> `String "MainConclusion", `Null - | `MainHypothesis (Some d) -> `String "MainHypothesis", `Int d - | `MainHypothesis None -> `String "MainHypothesis", `Null - | `InConclusion -> `String "InConclusion", `Null - | `InHypothesis -> `String "InHypothesis", `Null - | `InBody -> `String "InBody", `Null + | `MainConclusion (Some d) -> `String mainconcl_pos, `Int d + | `MainConclusion None -> `String mainconcl_pos, `Null + | `MainHypothesis (Some d) -> `String mainhyp_pos, `Int d + | `MainHypothesis None -> `String mainhyp_pos, `Null + | `InConclusion -> `String inconcl_pos, `Null + | `InHypothesis -> `String inhyp_pos, `Null + | `InBody -> `String inbody_pos, `Null (* let metadata_ns = "http://www.cs.unibo.it/helm/schemas/schema-helm" diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index a5bbfaf09..719ba508c 100644 --- a/helm/ocaml/metadata/metadataTypes.ml +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -23,6 +23,15 @@ * http://helm.cs.unibo.it/ *) +let position_prefix = "http://www.cs.unibo.it/helm/schemas/schema-helm#" +(* let position_prefix = "" *) + +let inconcl_pos = position_prefix ^ "InConclusion" +let mainconcl_pos = position_prefix ^ "MainConclusion" +let mainhyp_pos = position_prefix ^ "MainHypothesis" +let inhyp_pos = position_prefix ^ "InHypothesis" +let inbody_pos = position_prefix ^ "InBody" + type main_position = [ `MainConclusion of int option (* Pi depth *) | `MainHypothesis of int option (* Pi depth *) -- 2.39.2