From 20054808327ccec9d018b8cc54b31ccb44724f49 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Apr 2005 08:34:45 +0000 Subject: [PATCH] added filtering criteria on differences between number of constants in hypothesis and conclusion, should handle better queries on terms with metavariables --- helm/ocaml/metadata/metadataConstraints.ml | 139 ++++++++++++-------- helm/ocaml/metadata/metadataConstraints.mli | 4 + helm/ocaml/metadata/metadataDb.ml | 4 +- helm/ocaml/metadata/metadataExtractor.ml | 71 ++++++++++ helm/ocaml/metadata/metadataExtractor.mli | 7 + helm/ocaml/metadata/metadataTypes.ml | 15 ++- helm/ocaml/metadata/metadataTypes.mli | 6 +- 7 files changed, 182 insertions(+), 64 deletions(-) diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index ab8c00f99..870a57d90 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -36,6 +36,7 @@ type term_signature = (string * string list) option * StringSet.t type cardinality_condition = | Eq of int | Gt of int + | Lt of int let tbln n = "table" ^ string_of_int n @@ -66,98 +67,126 @@ let mk_positions positions cur_tbl = (positions :> MetadataTypes.position list)) ^ ")" +let explode_card_constr = function + | Eq card -> "=", card + | Gt card -> ">", card + | Lt card -> "<", card + let add_card_constr tbl (n,from,where) = function | None -> (n,from,where) - | Some (Eq card) -> + | Some constr -> let cur_tbl = tbln n in + let op, card = explode_card_constr constr in (n+1, (sprintf "%s as %s" tbl cur_tbl :: from), - (sprintf "%s.no=%d" cur_tbl card :: + (sprintf "%s.no %s %d" cur_tbl op card :: (if n=0 then [] 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 cur_tbl :: from), - (sprintf "%s.no>%d" cur_tbl card :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ + +let add_diff_constr conclno_tbl hypno_tbl (n,from,where) = function + | None -> (n,from,where) + | Some constr -> + let cur_tbl1, cur_tbl2 = tbln n, tbln (n+1) in + let op, card = explode_card_constr constr in + (n+2, + (sprintf "%s as %s" conclno_tbl cur_tbl1 :: + sprintf "%s as %s" hypno_tbl cur_tbl2 :: from), + (sprintf "%s.no - %s.no %s %d" cur_tbl2 cur_tbl1 op card :: + (if n=0 then assert false + else [sprintf "table0.source = %s.source" cur_tbl1; + sprintf "table0.source = %s.source" cur_tbl2]) @ where)) -let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card tables +let add_constraint tables (n,from,where) metadata = + let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in + let cur_tbl = tbln n in + match metadata with + | `Obj (uri, positions) -> + let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in + let where = + (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) :: + mk_positions positions cur_tbl :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" cur_tbl]) @ + where + in + ((n+2), from, where) + | `Rel positions -> + let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in + let where = + mk_positions positions cur_tbl :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" cur_tbl]) @ + where + in + ((n+2), from, where) + | `Sort (sort, positions) -> + let sort_str = CicPp.ppsort sort in + let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in + let where = + (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) :: + mk_positions positions cur_tbl :: + (if n=0 then + [] + else + [sprintf "table0.source = %s.source" cur_tbl ]) @ where + in + ((n+2), from, where) + +let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff tables (metadata: MetadataTypes.constr list) = + let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in if (metadata = []) && concl_card = None && full_card = None then failwith "MetadataQuery.at_least: no constraints given"; - let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,conclno_hyp_tbl = tables in - let add_constraint (n,from,where) metadata = - let cur_tbl = tbln n in - match metadata with - | `Obj (uri, positions) -> - let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in - let where = - (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) :: - mk_positions positions cur_tbl :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ - where - in - ((n+2), from, where) - | `Rel positions -> - let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in - let where = - mk_positions positions cur_tbl :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ - where - in - ((n+2), from, where) - | `Sort (sort, positions) -> - let sort_str = CicPp.ppsort sort in - let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in - let where = - (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) :: - mk_positions positions cur_tbl :: - (if n=0 then - [] - else - [sprintf "table0.source = %s.source" cur_tbl ]) @ where - in - ((n+2), from, where) + let (n,from,where) = + List.fold_left (add_constraint tables) (0,[],[]) metadata in - let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in let (n,from,where) = add_card_constr conclno_tbl (n,from,where) concl_card in let (n,from,where) = - add_card_constr conclno_hyp_tbl (n,from,where) full_card + add_card_constr fullno_tbl (n,from,where) full_card + in + let (n,from,where) = + add_diff_constr conclno_tbl hypno_tbl (n,from,where) diff 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 + let query = +(* + sprintf + ("select table0.source from %s, %s where %s and %s.source = table0.source" + ^^ " order by %s.no") + from fullno_tbl where fullno_tbl fullno_tbl + *) + sprintf "select table0.source from %s where %s" from where + in + prerr_endline query; let result = Mysql.exec dbd query in Mysql.map result (fun row -> match row.(0) with Some s -> s | _ -> assert false) let at_least - ~(dbd:Mysql.dbd) ?concl_card ?full_card (metadata: MetadataTypes.constr list) + ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff + (metadata: MetadataTypes.constr list) = let module MT = MetadataTypes in if MT.are_tables_ownerized () then - (at_least ~dbd ?concl_card ?full_card + (at_least ~dbd ?concl_card ?full_card ?diff (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (), - MT.conclno_tbl (),MT.conclno_hyp_tbl ()) + MT.conclno_tbl (),MT.fullno_tbl (),MT.hypno_tbl ()) metadata) @ - (at_least ~dbd ?concl_card ?full_card + (at_least ~dbd ?concl_card ?full_card ?diff (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, - MT.library_conclno_tbl,MT.library_conclno_hyp_tbl) + MT.library_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl) metadata) else - at_least ~dbd ?concl_card ?full_card + at_least ~dbd ?concl_card ?full_card ?diff (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, - MT.library_conclno_tbl,MT.library_conclno_hyp_tbl) + MT.library_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl) metadata diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli index 72f808efb..48143490f 100644 --- a/helm/ocaml/metadata/metadataConstraints.mli +++ b/helm/ocaml/metadata/metadataConstraints.mli @@ -57,14 +57,18 @@ val sigmatch: type cardinality_condition = | Eq of int | Gt of int + | Lt of int (** @param concl_card cardinality condition on conclusion only * @param full_card cardinality condition on the whole statement + * @param diff required difference between the number of different constants in + * hypothesis and the number of different constants in body * @return list of URI satisfying given constraints *) val at_least: dbd:Mysql.dbd -> ?concl_card:cardinality_condition -> ?full_card:cardinality_condition -> + ?diff:cardinality_condition -> MetadataTypes.constr list -> string list diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index 4b7664c22..30e5912d8 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -76,7 +76,7 @@ let insert_const_no dbd uri = SELECT \"%s\",COUNT(DISTINCT h_occurrence) FROM %s WHERE NOT (h_position=\"%s\") AND (source = \"%s\")" - (conclno_hyp_tbl ()) uri (obj_tbl ()) inbody_pos uri + (fullno_tbl ()) uri (obj_tbl ()) inbody_pos uri in ignore (Mysql.exec dbd inconcl_no); ignore (Mysql.exec dbd concl_hyp) @@ -121,7 +121,7 @@ let index_inductive_def ~dbd = end let tables_to_clean = - [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl] + [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; fullno_tbl; name_tbl] let clean ~(dbd:Mysql.dbd) = let owned_uris = (* list of uris in list-of-columns format *) diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index 8db0d74f5..784de4db6 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -158,6 +158,77 @@ let compute_term pos term = in aux pos S.empty term +module OrderedInt = +struct + type t = int + let compare = Pervasives.compare +end + +module IntSet = Set.Make (OrderedInt) + +let compute_metas term = + let rec aux in_hyp ((concl_metas, hyp_metas) as acc) cic = + match cic with + | Cic.Rel _ + | Cic.Sort _ + | Cic.Var _ -> acc + | Cic.Meta (no, local_context) -> + let acc = + if in_hyp then + (concl_metas, IntSet.add no hyp_metas) + else + (IntSet.add no concl_metas, hyp_metas) + in + List.fold_left + (fun set context -> + match context with + | None -> set + | Some term -> aux in_hyp set term) + acc + local_context + | Cic.Implicit _ -> assert false + | Cic.Cast (term, ty) -> + (* TODO consider also ty? *) + aux in_hyp acc term + | Cic.Prod (_, source, target) -> + if in_hyp then + let acc = aux in_hyp acc source in + aux in_hyp acc target + else + let acc = aux true acc source in + aux in_hyp acc target + | Cic.Lambda (_, source, target) -> + let acc = aux in_hyp acc source in + aux in_hyp acc target + | Cic.LetIn (_, term, target) -> + aux in_hyp acc (CicSubstitution.subst term target) + | Cic.Appl [] -> assert false + | Cic.Appl (hd :: tl) -> + let acc = aux in_hyp acc hd in + List.fold_left (fun acc term -> aux in_hyp acc term) acc tl + | Cic.Const (_, subst) + | Cic.MutInd (_, _, subst) + | Cic.MutConstruct (_, _, _, subst) -> + List.fold_left (fun acc (_, term) -> aux in_hyp acc term) acc subst + | Cic.MutCase (uri, _, outtype, term, pats) -> + let acc = aux in_hyp acc term in + let acc = aux in_hyp acc outtype in + List.fold_left (fun acc term -> aux in_hyp acc term) acc pats + | Cic.Fix (_, funs) -> + List.fold_left + (fun acc (_, _, ty, body) -> + let acc = aux in_hyp acc ty in + aux in_hyp acc body) + acc funs + | Cic.CoFix (_, funs) -> + List.fold_left + (fun acc (_, ty, body) -> + let acc = aux in_hyp acc ty in + aux in_hyp acc body) + acc funs + in + aux false (IntSet.empty, IntSet.empty) term + let compute_type uri typeno (name, _, ty, constructors) = let consno = ref 0 in let type_metadata = diff --git a/helm/ocaml/metadata/metadataExtractor.mli b/helm/ocaml/metadata/metadataExtractor.mli index ce057a85a..450c3a525 100644 --- a/helm/ocaml/metadata/metadataExtractor.mli +++ b/helm/ocaml/metadata/metadataExtractor.mli @@ -34,3 +34,10 @@ val compute_term: MetadataTypes.position -> Cic.term -> MetadataTypes.metadata list +module IntSet: Set.S with type elt = int + + (** given a term, returns a pair of sets corresponding respectively to the set + * of meta numbers occurring in term's conclusion and the set of meta numbers + * occurring in term's hypotheses *) +val compute_metas: Cic.term -> IntSet.t * IntSet.t + diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index 3f55b886f..948d08678 100644 --- a/helm/ocaml/metadata/metadataTypes.ml +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -68,7 +68,8 @@ let sort_tbl_original = "refSort" let rel_tbl_original = "refRel" let obj_tbl_original = "refObj" let conclno_tbl_original = "no_inconcl_aux" -let conclno_hyp_tbl_original = "no_concl_hyp" +let fullno_tbl_original = "no_concl_hyp" +let hypno_tbl_original = "no_hyp" let name_tbl_original = "objectName" (** the names currently used *) @@ -76,7 +77,8 @@ let sort_tbl_real = ref sort_tbl_original let rel_tbl_real = ref rel_tbl_original let obj_tbl_real = ref obj_tbl_original let conclno_tbl_real = ref conclno_tbl_original -let conclno_hyp_tbl_real = ref conclno_hyp_tbl_original +let fullno_tbl_real = ref fullno_tbl_original +let hypno_tbl_real = ref hypno_tbl_original let name_tbl_real = ref name_tbl_original (** the exported symbols *) @@ -84,7 +86,8 @@ let sort_tbl () = ! sort_tbl_real ;; let rel_tbl () = ! rel_tbl_real ;; let obj_tbl () = ! obj_tbl_real ;; let conclno_tbl () = ! conclno_tbl_real ;; -let conclno_hyp_tbl () = ! conclno_hyp_tbl_real ;; +let fullno_tbl () = ! fullno_tbl_real ;; +let hypno_tbl () = ! hypno_tbl_real ;; let name_tbl () = ! name_tbl_real ;; (** to use the owned tables *) @@ -93,7 +96,8 @@ let ownerize_tables owner = rel_tbl_real := ( rel_tbl_original ^ "_" ^ owner) ; obj_tbl_real := ( obj_tbl_original ^ "_" ^ owner) ; conclno_tbl_real := ( conclno_tbl_original ^ "_" ^ owner) ; - conclno_hyp_tbl_real := ( conclno_hyp_tbl_original ^ "_" ^ owner) ; + fullno_tbl_real := ( fullno_tbl_original ^ "_" ^ owner) ; + hypno_tbl_real := ( hypno_tbl_original ^ "_" ^ owner) ; name_tbl_real := ( name_tbl_original ^ "_" ^ owner) ;; @@ -101,7 +105,8 @@ let library_sort_tbl = sort_tbl_original let library_rel_tbl = rel_tbl_original let library_obj_tbl = obj_tbl_original let library_conclno_tbl = conclno_tbl_original -let library_conclno_hyp_tbl = conclno_hyp_tbl_original +let library_fullno_tbl = fullno_tbl_original +let library_hypno_tbl = hypno_tbl_original let library_name_tbl = name_tbl_original let are_tables_ownerized () = diff --git a/helm/ocaml/metadata/metadataTypes.mli b/helm/ocaml/metadata/metadataTypes.mli index b20c8ce14..206967678 100644 --- a/helm/ocaml/metadata/metadataTypes.mli +++ b/helm/ocaml/metadata/metadataTypes.mli @@ -66,13 +66,15 @@ val sort_tbl: unit -> string val rel_tbl: unit -> string val obj_tbl: unit -> string val conclno_tbl: unit -> string -val conclno_hyp_tbl: unit -> string +val fullno_tbl: unit -> string +val hypno_tbl: unit -> string val name_tbl: unit -> string val library_sort_tbl: string val library_rel_tbl: string val library_obj_tbl: string val library_conclno_tbl: string -val library_conclno_hyp_tbl: string +val library_fullno_tbl: string +val library_hypno_tbl: string val library_name_tbl: string -- 2.39.2