:- module eqvclass. :- use_module builtin, int, list, map, private_builtin, require, set. :- type (eqvclass:partition_id) == int. :- type (eqvclass:eqvclass(T)) ---> eqvclass(int, (tree234:tree234(int, (set:set(T)))), (tree234:tree234(T, int))) . :- pred eqvclass:ensure_element_2((eqvclass:eqvclass(T_1)), T_1, int, (eqvclass:eqvclass(T_1))). :- mode eqvclass:ensure_element_2((builtin:in), (builtin:in), (builtin:out), (builtin:out)) is det. :- pred eqvclass:partitions((eqvclass:eqvclass(T_1)), (list:list(int)), (list:list((set:set(T_1))))). :- mode eqvclass:partitions((builtin:in), (builtin:in), (builtin:out)) is det. :- pred eqvclass:partition_ids((eqvclass:eqvclass(T_1)), (list:list(int))). :- mode eqvclass:partition_ids((builtin:in), (builtin:out)) is det. eqvclass:init(EqvClass_2) :- map:init(PartitionMap_3), map:init(ElementMap_4), EqvClass_2 = eqvclass:eqvclass(V_5, PartitionMap_3, ElementMap_4), V_5 = 0. eqvclass:init = EC_2 :- eqvclass:init(EC_2). eqvclass:is_member(EqvClass_3, Element_4) :- EqvClass_3 = eqvclass:eqvclass(_NextId_5, _PartitionMap_6, ElementMap_7), map:search(ElementMap_7, Element_4, V_8). eqvclass:ensure_element(EqvClass0_4, Element_5, EqvClass_6) :- eqvclass:ensure_element_2(EqvClass0_4, Element_5, V_7, EqvClass_6). eqvclass:ensure_element(EC1_4, X_5) = EC2_6 :- eqvclass:ensure_element(EC1_4, X_5, EC2_6). eqvclass:new_element(EC1_4, X_5) = EC2_6 :- eqvclass:new_element(EC1_4, X_5, EC2_6). eqvclass:ensure_equivalence(EC1_5, X_6, Y_7) = EC2_8 :- eqvclass:ensure_equivalence(EC1_5, X_6, Y_7, EC2_8). eqvclass:new_equivalence(EC1_5, X_6, Y_7) = EC2_8 :- eqvclass:new_equivalence(EC1_5, X_6, Y_7, EC2_8). eqvclass:same_eqvclass(EqvClass0_4, Element1_5, Element2_6) :- EqvClass0_4 = eqvclass:eqvclass(_NextId0_7, _PartitionMap0_8, ElementMap0_9), map:search(ElementMap0_9, Element1_5, Id1_10), map:search(ElementMap0_9, Element2_6, Id2_11), Id1_10 = Id2_11. eqvclass:partition_set(EqvClass0_3, PartitionSet_4) :- eqvclass:partition_ids(EqvClass0_3, Ids_5), eqvclass:partitions(EqvClass0_3, Ids_5, PartitionList_6), set:list_to_set(PartitionList_6, PartitionSet_4). eqvclass:partition_set(EC_3) = S_4 :- eqvclass:partition_set(EC_3, S_4). eqvclass:partition_list(EqvClass0_3, PartitionList_4) :- eqvclass:partition_ids(EqvClass0_3, Ids_5), eqvclass:partitions(EqvClass0_3, Ids_5, PartitionList_4). eqvclass:partition_list(EC_3) = Xs_4 :- eqvclass:partition_list(EC_3, Xs_4). eqvclass:partition_set_to_eqvclass(SetSet_3, EqvClass_4) :- set:to_sorted_list(SetSet_3, ListSet_5), eqvclass:partition_list_to_eqvclass(ListSet_5, EqvClass_4). eqvclass:partition_set_to_eqvclass(S_3) = EC_4 :- eqvclass:partition_set_to_eqvclass(S_3, EC_4). eqvclass:partition_list_to_eqvclass(Xs_3) = EC_4 :- eqvclass:partition_list_to_eqvclass(Xs_3, EC_4). eqvclass:partition_ids(EqvClass0_3, Ids_4) :- EqvClass0_3 = eqvclass:eqvclass(_NextId0_5, PartitionMap0_6, _ElementMap0_7), map:keys(PartitionMap0_6, Ids_4). :- pragma termination_info(eqvclass:init((builtin:out)), infinite, can_loop). :- pragma termination_info((eqvclass:init) = (builtin:out), infinite, can_loop). :- pragma termination_info(eqvclass:is_member((builtin:in), (builtin:in)), finite(0, [no, no, no]), can_loop). :- pragma termination_info(eqvclass:ensure_element((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(eqvclass:ensure_element((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(eqvclass:new_element((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(eqvclass:new_element((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(eqvclass:ensure_equivalence((builtin:in), (builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(eqvclass:ensure_equivalence((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(eqvclass:new_equivalence((builtin:in), (builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(eqvclass:new_equivalence((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(eqvclass:same_eqvclass((builtin:in), (builtin:in), (builtin:in)), finite(0, [no, no, no, no]), can_loop). :- pragma termination_info(eqvclass:same_eqvclass_list((builtin:in), (builtin:in)), finite(0, [no, no, no]), can_loop). :- pragma termination_info(eqvclass:partition_set((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(eqvclass:partition_set((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(eqvclass:partition_list((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(eqvclass:partition_list((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(eqvclass:partition_set_to_eqvclass((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(eqvclass:partition_set_to_eqvclass((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(eqvclass:partition_list_to_eqvclass((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(eqvclass:partition_list_to_eqvclass((builtin:in)) = (builtin:out), infinite, can_loop).