X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=fc5328e9ffa3c252267d44b77e2d1b21614a02ac;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=49472ed7204f084cb160ac9fdb46378eae334b48;hpb=3605d724ae0b95e17e668b6e140c35ab19568bb2;p=helm.git diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 49472ed72..fc5328e9f 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -194,7 +194,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = 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"; +(* prerr_endline "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 @@ -250,17 +250,6 @@ let experimental_hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = let (_, metasenv, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in - let uris = - if facts then - ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"] - else - ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; - (* "cic:/Coq/Init/Logic/trans_eq.con"; *) - "cic:/Coq/Init/Logic/f_equal.con"; - "cic:/Coq/Init/Logic/f_equal2.con"; - "cic:/Coq/Init/Logic/f_equal3.con"] - in - (* let (uris, (main, sig_constants)) = match signature with | Some signature -> @@ -312,7 +301,7 @@ let experimental_hint 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 -> @@ -342,8 +331,8 @@ 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 @@ -351,30 +340,106 @@ 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 ("dummy_"^(string_of_int i)) in - (aux (i+1) (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t)) - | t -> t - in aux 0 t + 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' = 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 is_dummy = - function - `Obj(s, _) -> (String.sub s 0 5) = "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 + 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-> +(* 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 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)