X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=962aad8e7cac5e93999ccba089737116340ebc7d;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=0e86d8ccecf56b8a9005cec598b0e5d585cd875b;hpb=a4c02907fcf1c5ef8a4b89832808541fcad172e6;p=helm.git diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 0e86d8cce..962aad8e7 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -28,6 +28,8 @@ open Printf module Constr = MetadataConstraints module PET = ProofEngineTypes +let debug_print = fun _ -> () + (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for * the "like" operator (which uses '%' and '_'). Does not support escaping. *) let sqlpat_of_shellglob = @@ -60,7 +62,7 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = (fun cols -> match cols.(0) with Some s -> s | _ -> assert false)) let match_term ~(dbd:Mysql.dbd) ty = -(* prerr_endline (CicPp.ppterm ty); *) +(* debug_print (CicPp.ppterm ty); *) let metadata = MetadataExtractor.compute ~body:None ~ty in let constants_no = MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty) @@ -100,7 +102,7 @@ let match_term ~(dbd:Mysql.dbd) ty = None, diff in let constraints = List.map MetadataTypes.constr_of_metadata metadata in - Constr.at_least ~dbd ?full_card ?diff constraints + Constr.at_least ~dbd ?full_card ?diff constraints let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y)) @@ -188,13 +190,13 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = let hyp_constants = Constr.StringSet.diff (signature_of_hypothesis context) types_constants in -(* Constr.StringSet.iter prerr_endline hyp_constants; *) +(* Constr.StringSet.iter debug_print hyp_constants; *) let other_constants = Constr.StringSet.union sig_constants hyp_constants in let uris = let pow = 2 ** (Constr.StringSet.cardinal other_constants) in if ((List.length uris < pow) or (pow <= 0)) then begin - prerr_endline "MetadataQuery: large sig, falling back to old method"; +(* debug_print "MetadataQuery: large sig, falling back to old method"; *) filter_uris_forward ~dbd (main, other_constants) uris end else filter_uris_backward ~dbd ~facts (main, other_constants) uris @@ -205,7 +207,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = (let status' = try let (proof, goal_list) = -(* prerr_endline ("STO APPLICANDO " ^ uri); *) +(* debug_print ("STO APPLICANDO " ^ uri); *) PET.apply_tactic (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri)) @@ -236,6 +238,16 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = The cose is a cut and paste of the previous one: at the end of the experimentation we shall make a choice. *) +let close_with_types s metasenv context = + Constr.StringSet.fold + (fun e bag -> + let t = CicUtil.term_of_uri e in + let ty, _ = + CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph + in + Constr.StringSet.union bag (Constr.constants_of ty)) + s s + let experimental_hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = let (_, metasenv, _, _) = proof in @@ -246,7 +258,7 @@ let experimental_hint (Constr.sigmatch ~dbd ~facts signature, signature) | None -> (Constr.cmatch' ~dbd ~facts ty, Constr.signature_of ty) - in + in let uris = List.filter nonvar (List.map snd uris) in let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in let types_constants = @@ -256,27 +268,49 @@ let experimental_hint List.fold_right Constr.StringSet.add (main :: types) Constr.StringSet.empty in - let hyp_constants = - Constr.StringSet.diff (signature_of_hypothesis context) types_constants + let all_constants = + let hyp_and_sug = + Constr.StringSet.union + (signature_of_hypothesis context) + sig_constants + in + let main = + match main with + | None -> Constr.StringSet.empty + | Some (main,_) -> + let ty, _ = + CicTypeChecker.type_of_aux' + metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph + in + Constr.constants_of ty + in + Constr.StringSet.union main hyp_and_sug in -(* Constr.StringSet.iter prerr_endline hyp_constants; *) - let other_constants = Constr.StringSet.union sig_constants hyp_constants in +(* Constr.StringSet.iter debug_print hyp_constants; *) + let all_constants_closed = close_with_types all_constants metasenv context in + let other_constants = + Constr.StringSet.diff all_constants_closed types_constants + in + debug_print "all_constants_closed"; + Constr.StringSet.iter debug_print all_constants_closed; + debug_print "other_constants"; + Constr.StringSet.iter debug_print other_constants; let uris = let pow = 2 ** (Constr.StringSet.cardinal other_constants) in if ((List.length uris < pow) or (pow <= 0)) then begin - prerr_endline "MetadataQuery: large sig, falling back to old method"; + debug_print "MetadataQuery: large sig, falling back to old method"; filter_uris_forward ~dbd (main, other_constants) uris end else filter_uris_backward ~dbd ~facts (main, other_constants) uris - in + in let rec aux = function | [] -> [] | uri :: tl -> (let status' = try let (subst,(proof, goal_list)) = - (* prerr_endline ("STO APPLICANDO" ^ uri); *) + (* debug_print ("STO APPLICANDO" ^ uri); *) PrimitiveTactics.apply_tac_verbose ~term:(CicUtil.term_of_uri uri) status @@ -299,10 +333,115 @@ let experimental_hint let elim ~dbd uri = let constraints = [`Rel [`MainConclusion None]; - `Sort (Cic.Prop,[`MainHypothesis (Some 1)]); - `Obj (uri,[`MainHypothesis (Some 0)]); + `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]); + `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]); `Obj (uri,[`InHypothesis]); ] in - MetadataConstraints.at_least ~dbd constraints + MetadataConstraints.at_least ~rating:`Hits ~dbd constraints + + +let fill_with_dummy_constants t = + 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) (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',types = fill_with_dummy_constants t in + let metadata = MetadataExtractor.compute ~body:None ~ty:t' in +(* List.iter + (fun x -> + debug_print + (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 is_dummy = function + | `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy" + | _ -> true + in + let rec look_for_dummy_main = function + | [] -> None + | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq 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-> +(* debug_print "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) -> +(* debug_print + (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 metadata_for_dummy_type, depth' = + (* depth' = the depth of the A -> A -> Prop *) + List.fold_left (fun (acc,dep) c -> + match c with + | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> + (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i + | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> + (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i + | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) -> + (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i + | _ -> (c::acc,dep)) ([],0) 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 where = + sprintf "table0.h_depth - table%d.h_depth = %d" + n (depth - depth')::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) +