--- /dev/null
+(* 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
+
+++ /dev/null
-(* 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 ())
-
projects / helm.git / commitdiff