+let close_failures _ c = c;;
+let prunable _ _ _ = false;;
+let cache_examine cache gty = `Notfound;;
+let put_in_subst s _ _ _ = s;;
+let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ _ = c, o, f, false ;;
+let cache_add_underinspection c _ _ = c;;
+let equational_case _ _ _ _ _ _ _ = [];;
+let sort_new_elems l = l;;
+let only _ _ _ = true;;
+
+let candidate_no = ref 0;;
+
+let try_candidate status t g =
+ try
+ debug_print (lazy (" try " ^
+ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t
+ ));
+ let ast_for_t =
+ match t with
+ | NCic.Rel i -> assert false
+ | NCic.Const ref -> CicNotationPt.NRef ref
+ | _ -> assert false
+ in
+ let status = NTactics.focus_tac [g] status in
+ let status = NTactics.apply_tac ("",0,ast_for_t) status in
+ let open_goals = Continuationals.Stack.head_goals status#stack in
+ incr candidate_no;
+ Some ((!candidate_no,t),status,open_goals)
+ with NTacStatus.Error (msg,exn) -> debug_print msg; None
+;;
+
+
+let get_candidates status context gty =
+ let universe = status#auto_cache in
+ let _, gty = NTacStatus.term_of_cic_term status gty (NTacStatus.ctx_of gty) in
+ let cands =
+ NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty
+ in
+ (* XXX we have to trie for the context *)
+ let cands = NDiscriminationTree.TermSet.elements cands in
+ List.iter (fun x ->
+ debug_print (lazy (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)))
+ cands;
+ cands
+;;
+
+let applicative_case signature status flags g gty cache context =
+ let candidates = get_candidates status context gty in
+ let candidates = List.filter (only signature context) candidates in
+ debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates)));
+ let elems =
+ List.fold_left
+ (fun elems cand ->
+ match try_candidate status cand g with
+ | None -> elems
+ | Some x -> x::elems)
+ [] candidates
+ in
+ elems
+;;
+
+let equational_and_applicative_case
+ signature flags status g depth gty cache context
+=
+ let elems =
+ if false (*is_equational_case gty flags*) then
+ let elems =
+ equational_case
+ signature status flags g gty cache context
+ in
+ let more_elems =
+ applicative_case
+ signature status flags g gty cache context
+ in
+ elems@more_elems
+ else
+ let elems =
+ (*match LibraryObjects.eq_URI () with
+ | Some _ ->
+ smart_applicative_case dbd tables depth s fake_proof goalno
+ gty m context signature universe cache flags
+ | None -> *)
+ applicative_case
+ signature status flags g gty cache context
+ in
+ elems
+ in
+ let elems =
+ (* XXX calculate the sort *)
+ List.map (fun c,s,gl -> c,s,List.map (fun i -> i,depth-1,P) gl) elems
+ in
+ let elems = sort_new_elems elems in
+ elems
+;;