+let saturate ?(delta=0) metasenv subst context ty goal_arity =
+ assert (goal_arity >= 0);
+ let rec aux metasenv = function
+ | NCic.Prod (name,s,t) as ty ->
+ let metasenv1, _, arg,_ =
+ NCicMetaSubst.mk_meta ~attrs:[`Name name] metasenv context
+ ~with_type:s `IsTerm
+ in
+ let t, metasenv1, args, pno =
+ aux metasenv1 (NCicSubstitution.subst arg t)
+ in
+ if pno + 1 = goal_arity then
+ ty, metasenv, [], goal_arity+1
+ else
+ t, metasenv1, arg::args, pno+1
+ | ty ->
+ match NCicReduction.whd ~subst context ty ~delta with
+ | NCic.Prod _ as ty -> aux metasenv ty
+ | _ -> ty, metasenv, [], 0 (* differs from the other impl in this line*)
+ in
+ let res, newmetasenv, arguments, _ = aux metasenv ty in
+ res, newmetasenv, arguments
+;;
+
+let eq_class_of hdb t1 =
+ let eq_class =
+ if NDiscriminationTree.NCicIndexable.path_string_of t1 =
+ [Discrimination_tree.Variable]
+ then
+ [] (* if the trie is unable to handle the key, we skip the query since
+ it sould retulr the whole content of the trie *)
+ else
+ let candidates = EQDB.retrieve_unifiables (snd hdb#uhint_db) t1 in
+ let candidates = EqSet.elements candidates in
+ let candidates = List.sort (fun (x,_) (y,_) -> compare x y) candidates in
+ List.map snd candidates
+ in
+ debug(lazy("eq_class of: " ^ NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[]
+ t1 ^ " is\n" ^ String.concat "\n"
+ (List.map (NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:[]) eq_class)));
+ eq_class
+;;