let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
let sql_pat = sqlpat_of_shellglob pat in
let query =
- sprintf "SELECT source FROM %s WHERE value LIKE \"%s\""
+ sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
+ "SELECT source FROM %s WHERE value LIKE \"%s\"")
(MetadataTypes.name_tbl ()) sql_pat
+ MetadataTypes.library_name_tbl sql_pat
in
let result = Mysql.exec dbd query in
List.filter nonvar
(fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
let match_term ~(dbd:Mysql.dbd) ty =
+(* prerr_endline (CicPp.ppterm ty); *)
let metadata = MetadataExtractor.compute ~body:None ~ty in
let constants_no =
MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
in
+ let full_card, diff =
+ if CicUtil.is_meta_closed ty then
+ Some (MetadataConstraints.Eq constants_no), None
+ else
+ let diff_no =
+ let (hyp_constants, concl_constants) =
+ (* collect different constants in hypotheses and conclusions *)
+ List.fold_left
+ (fun ((hyp, concl) as acc) metadata ->
+ match (metadata: MetadataTypes.metadata) with
+ | `Sort _ | `Rel _ -> acc
+ | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _)
+ when not (List.mem uri concl) -> (hyp, uri :: concl)
+ | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _)
+ when not (List.mem uri hyp) -> (uri :: hyp, concl)
+ | `Obj _ -> acc)
+ ([], [])
+ metadata
+ in
+ List.length hyp_constants - List.length concl_constants
+ in
+ let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in
+ let diff =
+ if MetadataExtractor.IntSet.equal concl_metas hyp_metas then
+ Some (MetadataConstraints.Eq diff_no)
+ else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then
+ Some (MetadataConstraints.Gt (diff_no - 1))
+ else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then
+ Some (MetadataConstraints.Lt (diff_no + 1))
+ else
+ None
+ in
+ None, diff
+ in
let constraints = List.map MetadataTypes.constr_of_metadata metadata in
- Constr.at_least ~dbd ~full_card:(MetadataConstraints.Eq constants_no)
- constraints
+ Constr.at_least ~dbd ?full_card ?diff constraints
let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
let hyp_constants =
Constr.StringSet.diff (signature_of_hypothesis context) types_constants
in
-Constr.StringSet.iter prerr_endline hyp_constants;
+(* Constr.StringSet.iter prerr_endline hyp_constants; *)
let other_constants = Constr.StringSet.union sig_constants hyp_constants in
let uris =
let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
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
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 ->
(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 =
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 prerr_endline 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
+ prerr_endline "all_constants_closed";
+ Constr.StringSet.iter prerr_endline all_constants_closed;
+ prerr_endline "other_constants";
+ Constr.StringSet.iter prerr_endline other_constants;
let uris =
let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
if ((List.length uris < pow) or (pow <= 0))
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 ->
`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 =
+ 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
+
+let instance ~dbd t =
+ let t' = fill_with_dummy_constants t in
+ let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
+ 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
+
projects / helm.git / blobdiff