From: Stefano Zacchiroli Date: Wed, 20 Oct 2004 10:31:50 +0000 (+0000) Subject: snapshot, still work in progress X-Git-Tag: V_0_0_10~65 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7403c949ea3a84624f8c05deee00de53336937ba;p=helm.git snapshot, still work in progress --- diff --git a/helm/ocaml/metadata/.depend b/helm/ocaml/metadata/.depend index caa9708d6..07fbe69d7 100644 --- a/helm/ocaml/metadata/.depend +++ b/helm/ocaml/metadata/.depend @@ -1,6 +1,6 @@ metadataExtractor.cmi: metadataTypes.cmo metadataPp.cmi: metadataTypes.cmo -metadataQuery.cmi: metadataTypes.cmo +metadataConstraints.cmi: metadataTypes.cmo metadataExtractor.cmo: metadataTypes.cmo metadataExtractor.cmi metadataExtractor.cmx: metadataTypes.cmx metadataExtractor.cmi metadataPp.cmo: metadataPp.cmi @@ -9,5 +9,7 @@ metadataDb.cmo: metadataExtractor.cmi metadataPp.cmi metadataTypes.cmo \ metadataDb.cmi metadataDb.cmx: metadataExtractor.cmx metadataPp.cmx metadataTypes.cmx \ metadataDb.cmi -metadataQuery.cmo: metadataPp.cmi metadataTypes.cmo metadataQuery.cmi -metadataQuery.cmx: metadataPp.cmx metadataTypes.cmx metadataQuery.cmi +metadataConstraints.cmo: metadataPp.cmi metadataTypes.cmo \ + metadataConstraints.cmi +metadataConstraints.cmx: metadataPp.cmx metadataTypes.cmx \ + metadataConstraints.cmi diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile index e685915a3..6505e0f2e 100644 --- a/helm/ocaml/metadata/Makefile +++ b/helm/ocaml/metadata/Makefile @@ -6,7 +6,7 @@ INTERFACE_FILES = \ metadataExtractor.mli \ metadataPp.mli \ metadataDb.mli \ - metadataQuery.mli + metadataConstraints.mli IMPLEMENTATION_FILES = metadataTypes.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml new file mode 100644 index 000000000..3a985deb9 --- /dev/null +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -0,0 +1,507 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +let critical_value = 6 +let just_factor = 3 + +module StringSet = Set.Make (String) +module SetSet = Set.Make (StringSet) + +type term_signature = (string * string list) option * StringSet.t + +type cardinality_condition = + | Eq of int + | Gt of int + +let tbln n = "table" ^ string_of_int n + +let add_depth_constr depth_opt cur_tbl where = + match depth_opt with + | None -> where + | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where + +let add_card_constr tbl (n,from,where) = function + | None -> (n,from,where) + | Some (Eq card) -> + (n+1, + (sprintf "%s as %s" tbl (tbln n) :: from), + (sprintf "no=%d" card :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" (tbln n)]) @ + where)) + | Some (Gt card) -> + (n+1, + (sprintf "%s as %s" tbl (tbln n) :: from), + (sprintf "no>%d" card :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" (tbln n)]) @ + where)) + +let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card + (metadata: MetadataTypes.metadata list) += + if (metadata = []) && concl_card = None && full_card = None then + failwith "MetadataQuery.at_least: no constraints given"; + let add_constraint (n,from,where) metadata = + let cur_tbl = tbln n in + match metadata with + | `Obj (uri, pos, depth_opt) -> + let tbl = MetadataTypes.obj_tbl in + let pos_str = MetadataPp.pp_position pos in + let from = (sprintf "%s as %s" tbl cur_tbl) :: from in + let where = + (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: + (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" cur_tbl]) @ + where + in + let where = add_depth_constr depth_opt cur_tbl where in + ((n+1), from, where) + | `Rel (pos, depth) -> + let tbl = MetadataTypes.rel_tbl in + let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in + let from = (sprintf "%s as %s" tbl cur_tbl) :: from in + let where = + (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" cur_tbl]) @ + where + in + let where = add_depth_constr (Some depth) cur_tbl where in + ((n+1), from, where) + | `Sort (sort, pos, depth) -> + let tbl = MetadataTypes.sort_tbl in + let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in + let sort_str = MetadataPp.pp_sort sort in + let from = (sprintf "%s as %s" tbl cur_tbl) :: from in + let where = + (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: + (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" cur_tbl]) @ + where + in + let where = add_depth_constr (Some depth) cur_tbl where in + ((n+1), from, where) + in + let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in + let (n,from,where) = + add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card + in + let (n,from,where) = + add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card + in + 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 ()) + + (** Prefix handling *) + +let filter_by_card n = + SetSet.filter (fun t -> (StringSet.cardinal t) <= n) + +let merge n a b = + let init = SetSet.union a b in + let merge_single_set s1 b = + SetSet.fold + (fun s2 res -> SetSet.add (StringSet.union s1 s2) res) + b SetSet.empty in + let res = + SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init + in + filter_by_card n res + +let rec inspect_children n childs = + List.fold_left + (fun res term -> merge n (inspect_conclusion n term) res) + SetSet.empty childs + +and add_root n root childs = + let childunion = inspect_children n childs in + let addroot = StringSet.add root in + SetSet.fold + (fun child newsets -> SetSet.add (addroot child) newsets) + childunion + (SetSet.singleton (StringSet.singleton root)) + +and inspect_conclusion n t = +if n = 0 then SetSet.empty +else match t with + Cic.Rel _ + | Cic.Meta _ + | Cic.Sort _ + | Cic.Implicit _ -> SetSet.empty + | Cic.Var (u,exp_named_subst) -> SetSet.empty + | Cic.Const (u,exp_named_subst) -> + SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u)) + | Cic.MutInd (u, t, exp_named_subst) -> + SetSet.singleton (StringSet.singleton + (UriManager.string_of_uriref (u, [t]))) + | Cic.MutConstruct (u, t, c, exp_named_subst) -> + SetSet.singleton (StringSet.singleton + (UriManager.string_of_uriref (u, [t; c]))) + | Cic.Cast (t, _) -> inspect_conclusion n t + | Cic.Prod (_, s, t) -> + merge n (inspect_conclusion n s) (inspect_conclusion n t) + | Cic.Lambda (_, s, t) -> + merge n (inspect_conclusion n s) (inspect_conclusion n t) + | Cic.LetIn (_, s, t) -> + merge n (inspect_conclusion n s) (inspect_conclusion n t) + | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> + let suri = UriManager.string_of_uri u in + add_root (n-1) suri l + | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> + let suri = UriManager.string_of_uriref (u, [t]) in + add_root (n-1) suri l + | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> + let suri = UriManager.string_of_uriref (u, [t; c]) in + add_root (n-1) suri l + | Cic.Appl l -> + SetSet.empty + | Cic.MutCase (u, t, tt, uu, m) -> + SetSet.empty + | Cic.Fix (_, m) -> + SetSet.empty + | Cic.CoFix (_, m) -> + SetSet.empty + +let rec inspect_term n t = + if n = 0 then + assert false + else + match t with + Cic.Rel _ + | Cic.Meta _ + | Cic.Sort _ + | Cic.Implicit _ -> None, SetSet.empty + | Cic.Var (u,exp_named_subst) -> None, SetSet.empty + | Cic.Const (u,exp_named_subst) -> + Some (UriManager.string_of_uri u), SetSet.empty + | Cic.MutInd (u, t, exp_named_subst) -> + let uri = UriManager.string_of_uriref (u, [t]) in + Some uri, SetSet.empty + | Cic.MutConstruct (u, t, c, exp_named_subst) -> + let uri = UriManager.string_of_uriref (u, [t; c]) in + Some uri, SetSet.empty + | Cic.Cast (t, _) -> inspect_term n t + | Cic.Prod (_, _, t) -> inspect_term n t + | Cic.LetIn (_, _, t) -> inspect_term n t + | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> + let suri = UriManager.string_of_uri u in + let childunion = inspect_children (n-1) l in + Some suri, childunion + | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> + let suri = UriManager.string_of_uriref (u, [t]) in + if u = HelmLibraryObjects.Logic.eq_URI && n>1 then + (* equality is handled in a special way: in particular, + the type, if defined, is always added to the prefix, + and n is not decremented - it should have been n-2 *) + match l with + Cic.Const (u1,exp_named_subst1)::l1 -> + let suri1 = UriManager.string_of_uri u1 in + let inconcl = add_root (n-1) suri1 l1 in + Some suri, inconcl + | Cic.MutInd (u1, t1, exp_named_subst1)::l1 -> + let suri1 = UriManager.string_of_uriref (u1, [t1]) in + let inconcl = add_root (n-1) suri1 l1 in + Some suri, inconcl + | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 -> + let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in + let inconcl = add_root (n-1) suri1 l1 in + Some suri, inconcl + | _ :: _ -> Some suri, SetSet.empty + | _ -> assert false (* args number must be > 0 *) + else + let childunion = inspect_children (n-1) l in + Some suri, childunion + | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> + let suri = UriManager.string_of_uriref (u, [t; c]) in + let childunion = inspect_children (n-1) l in + Some suri, childunion + | _ -> None, SetSet.empty + +let add_cardinality s = + let l = SetSet.elements s in + let res = + List.map + (fun set -> + let el = StringSet.elements set in + (List.length el, el)) l in + (* ordered by descending cardinality *) + List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res) + +let prefixes n t = + match inspect_term n t with + Some a, set -> Some a, add_cardinality set + | None, set when (SetSet.is_empty set) -> None, [] + | _, _ -> assert false + + +let rec add children = + List.fold_left + (fun acc t -> StringSet.union (signature_concl t) acc) + (StringSet.empty) children + +(* this function creates the set of all different constants appearing in + the conclusion of the term *) +and signature_concl = + function + Cic.Rel _ + | Cic.Meta _ + | Cic.Sort _ + | Cic.Implicit _ -> StringSet.empty + | Cic.Var (u,exp_named_subst) -> StringSet.empty + | Cic.Const (u,exp_named_subst) -> + StringSet.singleton (UriManager.string_of_uri u) + | Cic.MutInd (u, t, exp_named_subst) -> + let uri = UriManager.string_of_uriref (u, [t]) in + StringSet.singleton uri + | Cic.MutConstruct (u, t, c, exp_named_subst) -> + let uri = UriManager.string_of_uriref (u, [t;c]) in + StringSet.singleton uri + | Cic.Cast (t, _) -> signature_concl t + | Cic.Prod (_, s, t) -> + StringSet.union (signature_concl s) (signature_concl t) + | Cic.Lambda (_, s, t) -> + StringSet.union (signature_concl s) (signature_concl t) + | Cic.LetIn (_, s, t) -> + StringSet.union (signature_concl s) (signature_concl t) + | Cic.Appl l -> add l + | Cic.MutCase _ + | Cic.Fix _ + | Cic.CoFix _ -> + StringSet.empty + +let rec signature_of = function + | Cic.Cast (t, _) -> signature_of t + | Cic.Prod (_, _, t) -> signature_of t + | Cic.LetIn (_, _, t) -> signature_of t + | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> + let suri = UriManager.string_of_uri u in + Some (suri, []), add l + | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> + let suri = UriManager.string_of_uriref (u, [t]) in + if u = HelmLibraryObjects.Logic.eq_URI then + (* equality is handled in a special way: in particular, + the type, if defined, is always added to the prefix, + and n is not decremented - it should have been n-2 *) + match l with + Cic.Const (u1,exp_named_subst1)::l1 -> + let suri1 = UriManager.string_of_uri u1 in + let inconcl = StringSet.remove suri1 (add l1) in + Some (suri, [suri1]), inconcl + | Cic.MutInd (u1, t1, exp_named_subst1)::l1 -> + let suri1 = UriManager.string_of_uriref (u1, [t1]) in + let inconcl = StringSet.remove suri1 (add l1) in + Some (suri, [suri1]), inconcl + | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 -> + let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in + let inconcl = StringSet.remove suri1 (add l1) in + Some (suri, [suri1]), inconcl + | _ :: _ -> Some (suri, []), StringSet.empty + | _ -> assert false (* args number must be > 0 *) + else + Some (suri, []), add l + | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> + let suri = UriManager.string_of_uriref (u, [t;c]) in + Some (suri, []), add l + | t -> None, signature_concl t + +(* takes a list of lists and returns the list of all elements + without repetitions *) +let union l = + let rec drop_repetitions = function + [] -> [] + | [a] -> [a] + | u1::u2::l when u1 = u2 -> drop_repetitions (u2::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, None)) s in + `Obj (m, `MainConclusion, None) :: s' + +let escape = Str.global_replace (Str.regexp_string "\'") "\\'" + +let get_inconcl (dbh:Dbi.connection) uri = + let uri = escape uri in + let query = + dbh#prepare (sprintf "select h_occurrence from refObj where source=\"%s\" and (h_position=\"MainConclusion\" or h_position=\"InConclusion\")" + uri) + in + query#execute []; + query#fold_left (* transform the result in a set *) + (fun set fields -> + let uri = match fields with [`String uri] -> uri | _ -> assert false in + StringSet.add uri set) + StringSet.empty + +let test_only ~(dbh:Dbi.connection) only u = + let inconcl = get_inconcl dbh u in + StringSet.subset inconcl only + + (* Special handling of equality. The problem is filtering out theorems just + * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really + * ad-hoc, no better solution found at the moment *) +let myspeciallist = + [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; + 0,"cic:/Coq/Init/Logic/sym_eq.con"; + 0,"cic:/Coq/Init/Logic/trans_eq.con"; + 0,"cic:/Coq/Init/Logic/f_equal.con"; + 0,"cic:/Coq/Init/Logic/f_equal2.con"; + 0,"cic:/Coq/Init/Logic/f_equal3.con"] + +let compute_exactly ~(dbh:Dbi.connection) main prefixes = + List.concat + (List.map + (fun (m,s) -> + if (m = 0) then + myspeciallist + else + let res = + at_least ~dbh ~concl_card:(Eq (m+1)) (must_of_prefix main s) + 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 max_prefix_length = + match prefixes with + | [] -> assert false + | (max,_)::_ -> max in + let maximal_prefixes = + let rec filter res = function + [] -> res + | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l + | _::_-> res in + filter [] prefixes in + let greater_than = + let all = + union + (List.map + (fun (m,s) -> + (let res = + at_least ~dbh ~concl_card:(Gt (m+1)) (must_of_prefix main s) + 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 + greater_than @ equal_to + + (* real match query implementation *) +let cmatch ~(dbh:Dbi.connection) t = + let (main, constants) = signature_of t in + match main with + | None -> [] + | Some (main, types) -> + (* the type of eq is not counted in constants_no *) + let constants_no = StringSet.cardinal constants in + if (constants_no > critical_value) then + let prefixes = prefixes just_factor t in + (match prefixes with + | Some main, all_concl -> + let all_constants = + List.fold_right StringSet.add types (StringSet.add main constants) + 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 + (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) + | _, _ -> []) + +let power_upto upto consts = + let l = StringSet.elements consts in + List.sort (fun (n,_) (m,_) -> m - n) + (List.fold_left + (fun res a -> + List.filter (function (n,l) -> n <= upto) + res@(List.map (function (n,l) -> (n+1,a::l)) res)) + [(0,[])] l) + +let power consts = + let l = StringSet.elements consts in + List.sort (fun (n,_) (m,_) -> m - n) + (List.fold_left + (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res)) + [(0,[])] l) + +let sigmatch ~(dbh:Dbi.connection) (main, constants) = + match main with + None -> [] + | Some (main, types) -> + let constants_no = StringSet.cardinal constants in + if (constants_no > critical_value) then + let subsets = + let subsets = power_upto just_factor constants in + let types_no = List.length types in + List.map (function (n,l) -> (n+types_no,types@l)) subsets + in + let all_constants = + List.fold_right StringSet.add types (StringSet.add main constants) + in + compute_with_only ~dbh 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 + in + compute_exactly ~dbh main subsets + + (* match query wrappers *) +let cmatch' = cmatch +let cmatch ~dbh term = + List.map snd + (List.sort + (fun x y -> Pervasives.compare (fst y) (fst x)) + (cmatch' ~dbh term)) + +let constants_of = signature_concl + diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli new file mode 100644 index 000000000..59cb0427e --- /dev/null +++ b/helm/ocaml/metadata/metadataConstraints.mli @@ -0,0 +1,65 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +module StringSet : Set.S with type elt = string + + (** @return + * main: constant in main position and, for polymorphic constants, type + * instantitation + * constants: constants appearing in term *) +type term_signature = (string * string list) option * StringSet.t + +(** {2 Candidates filtering} *) + + (** @return sorted list of theorem URIs, first URIs in the least have higher + * relevance *) +val cmatch: dbh:Dbi.connection -> Cic.term -> string list + + (** as cmatch, but returned list is not sorted but rather tagged with + * 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 + +(** {2 Constraint engine} *) + + (** constraing on the number of distinct constants *) +type cardinality_condition = + | Eq of int + | Gt of int + + (** @param concl_card cardinality condition on conclusion only + * @param full_card cardinality condition on the whole statement + * @return list of URI satisfying given constraints *) +val at_least: + dbh:Dbi.connection -> + ?concl_card:cardinality_condition -> + ?full_card:cardinality_condition -> + MetadataTypes.metadata list -> + string list + +val signature_of: Cic.term -> term_signature +val constants_of: Cic.term -> StringSet.t + diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index 0bd5eaed3..9f9b721f6 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -201,3 +201,5 @@ let compute ~body ~ty = body_metadata) type_metadata) +let compute_term start_pos term = S.elements (compute_term start_pos term) + diff --git a/helm/ocaml/metadata/metadataExtractor.mli b/helm/ocaml/metadata/metadataExtractor.mli index ef7ea763c..ce057a85a 100644 --- a/helm/ocaml/metadata/metadataExtractor.mli +++ b/helm/ocaml/metadata/metadataExtractor.mli @@ -30,3 +30,7 @@ val compute_ind: uri:UriManager.uri -> types:Cic.inductiveType list -> (string * string * MetadataTypes.metadata list) list +val compute_term: + MetadataTypes.position -> Cic.term -> + MetadataTypes.metadata list + diff --git a/helm/ocaml/metadata/metadataQuery.ml b/helm/ocaml/metadata/metadataQuery.ml deleted file mode 100644 index a5cd99654..000000000 --- a/helm/ocaml/metadata/metadataQuery.ml +++ /dev/null @@ -1,118 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -open Printf - -type cardinality_condition = - | Eq of int - | Gt of int - -let tbln n = "table" ^ string_of_int n - -let add_depth_constr depth_opt cur_tbl where = - match depth_opt with - | None -> where - | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where - -let add_card_constr tbl (n,from,where) = function - | None -> (n,from,where) - | Some (Eq card) -> - (n+1, - (sprintf "%s as %s" tbl (tbln n) :: from), - (sprintf "no=%d" card :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" (tbln n)]) @ - where)) - | Some (Gt card) -> - (n+1, - (sprintf "%s as %s" tbl (tbln n) :: from), - (sprintf "no>%d" card :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" (tbln n)]) @ - where)) - -let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card - (metadata: MetadataTypes.metadata list) -= - if (metadata = []) && concl_card = None && full_card = None then - failwith "MetadataQuery.at_least: no constraints given"; - let add_constraint (n,from,where) metadata = - let cur_tbl = tbln n in - match metadata with - | `Obj (uri, pos, depth_opt) -> - let tbl = MetadataTypes.obj_tbl in - let pos_str = MetadataPp.pp_position pos in - let from = (sprintf "%s as %s" tbl cur_tbl) :: from in - let where = - (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: - (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ - where - in - let where = add_depth_constr depth_opt cur_tbl where in - ((n+1), from, where) - | `Rel (pos, depth) -> - let tbl = MetadataTypes.rel_tbl in - let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in - let from = (sprintf "%s as %s" tbl cur_tbl) :: from in - let where = - (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ - where - in - let where = add_depth_constr (Some depth) cur_tbl where in - ((n+1), from, where) - | `Sort (sort, pos, depth) -> - let tbl = MetadataTypes.sort_tbl in - let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in - let sort_str = MetadataPp.pp_sort sort in - let from = (sprintf "%s as %s" tbl cur_tbl) :: from in - let where = - (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: - (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ - where - in - let where = add_depth_constr (Some depth) cur_tbl where in - ((n+1), from, where) - in - let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in - let (n,from,where) = - add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card - in - let (n,from,where) = - add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card - in - 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 ()) - diff --git a/helm/ocaml/metadata/metadataQuery.mli b/helm/ocaml/metadata/metadataQuery.mli deleted file mode 100644 index 38da9e956..000000000 --- a/helm/ocaml/metadata/metadataQuery.mli +++ /dev/null @@ -1,40 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - - (** constraing on the number of distinct constants *) -type cardinality_condition = - | Eq of int - | Gt of int - - (** @param concl_card cardinality condition on conclusion only - * @param full_card cardinality condition on the whole statement - * @return list of URI satisfying given constraints *) -val at_least: - dbh:Dbi.connection -> - ?concl_card:cardinality_condition -> - ?full_card:cardinality_condition -> - MetadataTypes.metadata list -> - string list -