(fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
let match_term ~(dbd:Mysql.dbd) ty =
- prerr_endline (CicPp.ppterm ty);
+(* prerr_endline (CicPp.ppterm ty); *)
let metadata = MetadataExtractor.compute ~body:None ~ty in
let constants_no =
MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of 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))
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
+ 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
+