+(* experimental_hint is a version of hint for experimental
+ purposes. It uses auto_tac_verbose instead of auto tac.
+ Auto_tac verbose also returns a substitution - for the moment
+ as a function from cic to cic, to be changed into an association
+ list in the future -. This substitution is used to build a
+ hash table of the inspected goals with their associated proofs.
+ The cose is a cut and paste of the previous one: at the end
+ of the experimentation we shall make a choice. *)
+
+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, (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 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
+ if ((List.length uris < pow) or (pow <= 0))
+ then begin
+ 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
+ in
+ let rec aux = function
+ | [] -> []
+ | uri :: tl ->
+ (let status' =
+ try
+ let (subst,(proof, goal_list)) =
+ (* prerr_endline ("STO APPLICANDO" ^ uri); *)
+ PrimitiveTactics.apply_tac_verbose
+ ~term:(CicUtil.term_of_uri uri)
+ status
+ in
+ let goal_list =
+ List.stable_sort (compare_goal_list proof) goal_list
+ in
+ Some (uri, (subst,(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)
+
+let elim ~dbd uri =