%--------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%--------------------------------------------------%
% Copyright (C) 1995-1997, 1999, 2003-2006, 2011-2012 The University of Melbourne.
% Copyright (C) 2014-2018, 2023 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%--------------------------------------------------%
%
% File: eqvclass.m.
% Author: zs.
% Stability: low.
%
% A module for handling equivalence classes.
%
%--------------------------------------------------%
%--------------------------------------------------%
:- module eqvclass.
:- interface.
:- import_module list.
:- import_module set.
%--------------------------------------------------%
:- type eqvclass(T).
:- type partition_id.
% Create an empty equivalence class.
%
:- func init = eqvclass(T).
:- pred init(eqvclass(T)::out) is det.
% Is this item known to the equivalence class?
%
:- pred is_member(eqvclass(T)::in, T::in) is semidet.
% If this item is known to the equivalence class, return the id of its
% partition. The only use that the caller can make of the partition id
% is to check whether two items in the same equivalence calls have the
% same partition id; that test will succeed if and only if the two
% items are in the same partition. Partition ids are not guaranteed
% to stay the same as an eqvclass is updated, so such comparisons will
% work only against the same eqvclass.
%
% If you want to check whether two items are in the same equivalence class,
% using same_eqvclass is more expressive than calling
% partition_id on both items and comparing the results.
% However, if you want to perform this check on X and Y1, on X and Y2,
% ... X and Yn, then calling partition_id on X just once and
% comparing this with the partition_ids of the Yi will be more efficient.
%
:- pred partition_id(eqvclass(T)::in, T::in, partition_id::out)
is semidet.
% Make an element known to the equivalence class.
% The element may already be known to the class;
% if it isn't, it is created without any equivalence relationships.
%
:- func ensure_element(eqvclass(T), T) = eqvclass(T).
:- pred ensure_element(T::in, eqvclass(T)::in, eqvclass(T)::out)
is det.
% Make this item known to the equivalence class if it isn't already,
% and return the id of its partition. The same proviso applies with
% respect to partition_ids as with partition_id.
%
:- pred ensure_element_partition_id(T::in, partition_id::out,
eqvclass(T)::in, eqvclass(T)::out) is det.
% Make an element known to the equivalence class.
% The element must not already be known to the class;
% it is created without any equivalence relationships.
%
:- func new_element(eqvclass(T), T) = eqvclass(T).
:- pred new_element(T::in, eqvclass(T)::in, eqvclass(T)::out) is det.
% Ensure that the two items are known to the equivalence class,
% and make them equivalent. It is ok if they already are equivalent.
%
:- func ensure_equivalence(eqvclass(T), T, T) = eqvclass(T).
:- pred ensure_equivalence(T::in, T::in,
eqvclass(T)::in, eqvclass(T)::out) is det.
% Call ensure_equivalence on each pair of corresponding list elements.
%
:- func ensure_corresponding_equivalences(list(T), list(T),
eqvclass(T)) = eqvclass(T).
:- pred ensure_corresponding_equivalences(list(T)::in, list(T)::in,
eqvclass(T)::in, eqvclass(T)::out) is det.
% Make two elements of the equivalence class equivalent.
% It is an error if they are already equivalent.
%
:- func new_equivalence(eqvclass(T), T, T) = eqvclass(T).
:- pred new_equivalence(T::in, T::in, eqvclass(T)::in, eqvclass(T)::out)
is det.
% Succeed if and only if the two items are both known to the equivalence
% class, and are known to be equivalent.
%
:- pred same_eqvclass(eqvclass(T)::in, T::in, T::in) is semidet.
% Succeed if and only if all the items in the list are known
% to the equivalence class, and are known to be all equivalent
% to each other.
%
:- pred same_eqvclass_list(eqvclass(T)::in, list(T)::in) is semidet.
% Return the set of the partitions of the equivalence class.
%
:- func partition_set(eqvclass(T)) = set(set(T)).
:- pred partition_set(eqvclass(T)::in, set(set(T))::out) is det.
% Return a list of the partitions of the equivalence class.
%
:- func partition_list(eqvclass(T)) = list(set(T)).
:- pred partition_list(eqvclass(T)::in, list(set(T))::out) is det.
% Create an equivalence class from a partition set.
% Throw an exception if the sets are not disjoint.
%
:- func partition_set_to_eqvclass(set(set(T))) = eqvclass(T).
:- pred partition_set_to_eqvclass(set(set(T))::in, eqvclass(T)::out) is det.
% Create an equivalence class from a list of partitions.
% Throw an exception if the sets are not disjoint.
%
:- func partition_list_to_eqvclass(list(set(T))) = eqvclass(T).
:- pred partition_list_to_eqvclass(list(set(T))::in,
eqvclass(T)::out) is det.
% Return the set of elements equivalent to the given element.
% This set will of course include the given element.
%
:- func get_equivalent_elements(eqvclass(T), T) = set(T).
% Return the smallest element equivalent to the given element.
% This may or may not be the given element.
%
:- func get_minimum_element(eqvclass(T), T) = T.
% Remove the given element and all other elements equivalent to it
% from the given equivalence class.
%
:- func remove_equivalent_elements(eqvclass(T), T) = eqvclass(T).
:- pred remove_equivalent_elements(T::in,
eqvclass(T)::in, eqvclass(T)::out) is det.
% Given a function, divide each partition in the original equivalence class
% so that two elements of the original partition end up in the same
% partition in the new equivalence class if and only if the function maps
% them to the same value.
%
:- func divide_equivalence_classes(func(T) = U, eqvclass(T)) = eqvclass(T).
%--------------------------------------------------%
%--------------------------------------------------%