From: Andrea Asperti Date: Thu, 5 May 2005 11:14:14 +0000 (+0000) Subject: Some modifications due to instance. X-Git-Tag: single_binding~108 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f3581a88f462038ba4d97d1702ae86650e269fc5;p=helm.git Some modifications due to instance. --- diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 952aa5a57..da4f271b5 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -24,6 +24,7 @@ *) open Printf +open MetadataTypes let critical_value = 7 let just_factor = 4 @@ -42,6 +43,12 @@ type rating_criterion = [ `Hits (** order by number of hits, most used objects first *) ] +let default_tables = + (library_obj_tbl,library_rel_tbl,library_sort_tbl,library_count_tbl) + +let current_tables () = + (obj_tbl (),rel_tbl (),sort_tbl (), count_tbl ()) + let tbln n = "table" ^ string_of_int n (* @@ -89,32 +96,35 @@ let add_diff_constr tbl where = function let op, card = explode_card_constr constr in (sprintf "%s.hypothesis - %s.conclusion %s %d" tbl tbl op card :: where) -let add_all_constr tbl (n,from,where) concl full diff = +let add_all_constr ?(tbl=library_count_tbl) (n,from,where) concl full diff = match (concl, full, diff) with | None, None, None -> (n,from,where) | _ -> - let where = add_card_constr tbl "conclusion" where concl in - let where = add_card_constr tbl "statement" where full in - let where = add_diff_constr tbl where diff in - (n,tbl :: from, + let cur_tbl = tbln n in + let from = (sprintf "%s as %s" tbl cur_tbl) :: from in + let where = add_card_constr cur_tbl "conclusion" where concl in + let where = add_card_constr cur_tbl "statement" where full in + let where = add_diff_constr cur_tbl where diff in + (n+2,from, (if n > 0 then - sprintf "table0.source = %s.source" tbl :: where + sprintf "table0.source = %s.source" cur_tbl :: where else where)) -let add_constraint tables (n,from,where) metadata = +let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata = let obj_tbl,rel_tbl,sort_tbl,count_tbl = tables in let cur_tbl = tbln n in + let start_table = tbln start 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]) @ + (if n=start then [] + else [sprintf "%s.source = %s.source" start_table cur_tbl]) @ where in ((n+2), from, where) @@ -122,8 +132,8 @@ let add_constraint tables (n,from,where) metadata = 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]) @ + (if n=start then [] + else [sprintf "%s.source = %s.source" start_table cur_tbl]) @ where in ((n+2), from, where) @@ -133,13 +143,30 @@ let add_constraint tables (n,from,where) metadata = let where = (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) :: mk_positions positions cur_tbl :: - (if n=0 then + (if n=start then [] else - [sprintf "table0.source = %s.source" cur_tbl ]) @ where + [sprintf "%s.source = %s.source" start_table cur_tbl ]) @ where in ((n+2), from, where) +let exec ~(dbd:Mysql.dbd) ?rating (n,from,where) = +let from = String.concat ", " from in + let where = String.concat " and " where in + let query = + match rating with + | None -> sprintf "select table0.source from %s where %s" from where + | Some `Hits -> + sprintf + ("select table0.source from %s, hits where %s + and table0.source = hits.source order by hits.no desc") + 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 ?diff ?rating tables (metadata: MetadataTypes.constr list) @@ -149,48 +176,25 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables if (metadata = []) && concl_card = None && full_card = None then failwith "MetadataQuery.at_least: no constraints given"; let (n,from,where) = - List.fold_left (add_constraint tables) (0,[],[]) metadata + List.fold_left (add_constraint ~tables) (0,[],[]) metadata in - let selected = if metadata = [] then count_tbl else "table0" in let (n,from,where) = - add_all_constr count_tbl (n,from,where) concl_card full_card diff - in - let from = String.concat ", " from in - let where = String.concat " and " where in - let query = - match rating with - | None -> sprintf "select %s.source from %s where %s" selected from where - | Some `Hits -> - sprintf - ("select %s.source from %s, hits where %s" - ^^ " and hits.source = %s.source order by hits.no desc") - selected from where selected + add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff 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) - + exec ~dbd ?rating (n,from,where) let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating (metadata: MetadataTypes.constr list) = - let module MT = MetadataTypes in - if MT.are_tables_ownerized () then - (at_least ~dbd ?concl_card ?full_card ?diff ?rating - (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (), MT.count_tbl ()) - metadata) - @ - (at_least ~dbd ?concl_card ?full_card ?diff ?rating - (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, - MT.library_count_tbl) - metadata) + if are_tables_ownerized () then + (at_least + ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata) @ + (at_least + ~dbd ?concl_card ?full_card ?diff ?rating (current_tables ()) metadata) else - at_least ~dbd ?concl_card ?full_card ?diff ?rating - (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, - MT.library_count_tbl) - metadata + at_least + ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata (** Prefix handling *) @@ -466,7 +470,7 @@ let myspeciallist_of_facts = [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"] 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/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"; diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli index ddf672b7f..0d6655741 100644 --- a/helm/ocaml/metadata/metadataConstraints.mli +++ b/helm/ocaml/metadata/metadataConstraints.mli @@ -63,11 +63,19 @@ type rating_criterion = [ `Hits (** order by number of hits, most used objects first *) ] +val add_constraint: + ?start:int -> + ?tables:string * string * string * string -> + int * string list * string list -> + MetadataTypes.constr -> + int * string list * string list + (** @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 -> @@ -83,6 +91,20 @@ val at_most: ?where:where -> StringSet.t -> (string -> bool) +val add_all_constr: + ?tbl:string -> + int * string list * string list -> + cardinality_condition option -> + cardinality_condition option -> + cardinality_condition option -> + int * string list * string list + +val exec: + dbd:Mysql.dbd -> + ?rating:[ `Hits ] -> + int * string list * string list -> + string list + val signature_of: Cic.term -> term_signature val constants_of: Cic.term -> StringSet.t diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli index 672c900eb..d70ec4a34 100644 --- a/helm/ocaml/metadata/metadataDb.mli +++ b/helm/ocaml/metadata/metadataDb.mli @@ -36,6 +36,6 @@ val clean: dbd:Mysql.dbd -> string list val unindex: dbd:Mysql.dbd -> uri:UriManager.uri -> unit val count_distinct: - [ `Conclusion | `Hypothesis | `Statement] -> - MetadataTypes.metadata list -> - int + [`Conclusion | `Hypothesis | `Statement ] -> + MetadataTypes.metadata list -> + int diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml index 5fc05b91d..63a1a0955 100644 --- a/helm/ocaml/metadata/metadataPp.ml +++ b/helm/ocaml/metadata/metadataPp.ml @@ -85,6 +85,15 @@ let columns_of_metadata metadata = (List.append sort_cols s, List.append rel_cols r, List.append obj_cols o)) ([], [], []) metadata +let pp_constr = + function + | `Sort (sort, p) -> + sprintf "Sort %s; [%s]" + (CicPp.ppsort sort) (String.concat ";" (List.map pp_position p)) + | `Rel p -> sprintf "Rel [%s]" (String.concat ";" (List.map pp_position p)) + | `Obj (uri, p) -> sprintf "Obj %s; [%s]" + uri (String.concat ";" (List.map pp_position p)) + (* let pp_columns ?(sep = "\n") (sort_cols, rel_cols, obj_cols) = String.concat sep diff --git a/helm/ocaml/metadata/metadataPp.mli b/helm/ocaml/metadata/metadataPp.mli index 39ccd6c32..8566ed727 100644 --- a/helm/ocaml/metadata/metadataPp.mli +++ b/helm/ocaml/metadata/metadataPp.mli @@ -27,7 +27,7 @@ val pp_position: MetadataTypes.position -> string val pp_position_tag: MetadataTypes.position -> string -(* val pp_constr: MetadataTypes.constr -> string *) +val pp_constr: MetadataTypes.constr -> string (** Pretty printer and OCamlDBI friendly interface *) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 5f83dd608..d0b384e75 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -351,30 +351,90 @@ let elim ~dbd uri = let fill_with_dummy_constants t = - let rec aux i = + let rec aux i types = function Cic.Lambda (n,s,t) -> let dummy_uri = UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)) in - (aux (i+1) (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t)) - | t -> t - in aux 0 t + (aux (i+1) (s::types) + (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t)) + | t -> t,types + in + let t,types = aux 0 [] t in + t, List.rev types let instance ~dbd t = - let t' = fill_with_dummy_constants t in + let t',types = fill_with_dummy_constants t in let metadata = MetadataExtractor.compute ~body:None ~ty:t' in + List.iter + (fun x -> + prerr_endline + (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) + metadata; let no_concl = MetadataDb.count_distinct `Conclusion metadata in let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in - let no_full = MetadataDb.count_distinct `Statement metadata in + let no_full = MetadataDb.count_distinct `Statement metadata in let is_dummy = function `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy" - | _ -> false in - let metadata = List.filter is_dummy metadata in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - let concl_card = Some (MetadataConstraints.Eq no_concl) in - let full_card = Some (MetadataConstraints.Eq no_full) in - let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in - Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints + | _ -> true in + let rec look_for_dummy_main = + function + [] -> None + | `Obj(s,`MainConclusion (Some d))::_ + when ((String.sub s 0 10) = "cic:/dummy") -> + let len = String.length s in + let dummy_index = int_of_string (String.sub s 11 (len-11)) in + let dummy_type = List.nth types dummy_index in + Some (d,dummy_type) + | _::l -> look_for_dummy_main l in + match (look_for_dummy_main metadata) with + None-> + prerr_endline "Caso None"; + (* no dummy in main position *) + let metadata = List.filter is_dummy metadata in + let constraints = List.map MetadataTypes.constr_of_metadata metadata in + let concl_card = Some (MetadataConstraints.Eq no_concl) in + let full_card = Some (MetadataConstraints.Eq no_full) in + let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in + Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints + | Some (depth, dummy_type) -> + prerr_endline + (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); + (* a dummy in main position *) + let metadata_for_dummy_type = + MetadataExtractor.compute ~body:None ~ty:dummy_type in + (* Let us skip this for the moment + let main_of_dummy_type = + look_for_dummy_main metadata_for_dummy_type in *) + let metadata = List.filter is_dummy metadata in + let constraints = List.map MetadataTypes.constr_of_metadata metadata in + let metadata_for_dummy_type = + List.filter is_dummy metadata_for_dummy_type in + let constraints_for_dummy_type = + List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in + (* start with the dummy constant in main conlusion *) + let from = ["refObj as table0"] in + let where = + [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos; + sprintf "table0.h_depth = %d" depth] in + let (n,from,where) = + List.fold_left + (MetadataConstraints.add_constraint ~start:2) + (2,from,where) constraints in + let concl_card = Some (MetadataConstraints.Eq no_concl) in + let full_card = Some (MetadataConstraints.Eq no_full) in + let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in + let (n,from,where) = + MetadataConstraints.add_all_constr + (n,from,where) concl_card full_card diff in + (* join with the constraints over the type of the constant *) + let where = + (sprintf "table0.h_occurrence = table%d.source" n)::where in + let (m,from,where) = + List.fold_left + (MetadataConstraints.add_constraint ~start:n) + (n,from,where) constraints_for_dummy_type in + Constr.exec ~dbd (m,from,where)