-let 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, (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
- let uris = List.filter nonvar (List.map snd uris) in
- let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
- let types_constants =
- match main with
- | None -> Constr.StringSet.empty
- | Some (main, types) ->
- List.fold_right Constr.StringSet.add (main :: types)
- Constr.StringSet.empty
- in
- let hyp_constants =
- Constr.StringSet.diff (signature_of_hypothesis context) types_constants
- in
-(* 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
-(* 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
- let rec aux = function
- | [] -> []
- | uri :: tl ->
- (let status' =
- try
- let (proof, goal_list) =
-(* debug_print ("STO APPLICANDO " ^ uri); *)
- PET.apply_tactic
- (PrimitiveTactics.apply_tac
- ~term:(CicUtil.term_of_uri uri))
- status
- in
- let goal_list =
- List.stable_sort (compare_goal_list proof) goal_list
- in
- Some (uri, (proof, goal_list))
- with ProofEngineTypes.Fail _ -> None
- in
- match status' with
- | None -> aux tl
- | Some status' ->
- status' :: aux tl)
- in
- List.stable_sort
- (fun (_, (_, goals1)) (_, (_, goals2)) ->
- Pervasives.compare (List.length goals1) (List.length goals2))
- (aux uris)
-