module X : Set.OrderedTypetype elt = X.tmodule Leaf : Index_intf.LEAF with type elt = eltval empty : unit -> tval is_empty : t -> boolval size : t -> intval add : t -> Index_intf.term -> elt -> tval add_seq : t -> (Index_intf.term * elt) Iter.t -> tval add_list : t -> (Index_intf.term * elt) list -> tval remove : t -> Index_intf.term -> elt -> tval update_leaf : t -> Index_intf.term -> (elt -> bool) -> tval remove_seq : t -> (Index_intf.term * elt) Iter.t -> tval remove_list : t -> (Index_intf.term * elt) list -> tval iter : t -> (Index_intf.term -> elt -> unit) -> unitval fold : t -> ('a -> Index_intf.term -> elt -> 'a) -> 'a -> 'aval retrieve_unifiables :
t Scoped.t ->
Index_intf.term Scoped.t ->
(Index_intf.term * elt * Unif_subst.t) Iter.tRetrieves a decidable fragment of unifiables. Only one unifier per subterm.
val retrieve_unifiables_complete :
?unif_alg:(Term.t Scoped.t -> Term.t Scoped.t -> Unif_subst.t option OSeq.t) ->
t Scoped.t ->
Index_intf.term Scoped.t ->
(Index_intf.term * elt * Unif_subst.t option OSeq.t) Iter.tRetrieves all unifiables. The set of unifiers is potentially infinite. Because HO unification is undecidable, the sequence is intersperced with `None`s to ensure termination for each element of the sequence.
val retrieve_generalizations :
?subst:Index_intf.subst ->
t Scoped.t ->
Index_intf.term Scoped.t ->
(Index_intf.term * elt * Index_intf.subst) Iter.tval retrieve_specializations :
?subst:Index_intf.subst ->
t Scoped.t ->
Index_intf.term Scoped.t ->
(Index_intf.term * elt * Index_intf.subst) Iter.tval to_dot : elt CCFormat.printer -> t CCFormat.printerprint oneself in DOT into the given file