:- module rbtree. :- use_module assoc_list, bool, builtin, int, list, private_builtin, require, std_util. :- type (rbtree:rbtree(K, V)) ---> empty ; red(K, V, (rbtree:rbtree(K, V)), (rbtree:rbtree(K, V))) ; black(K, V, (rbtree:rbtree(K, V)), (rbtree:rbtree(K, V))) . :- pred rbtree:delete_2((rbtree:rbtree(K_1, V_2)), K_1, (bool:bool), (std_util:maybe(V_2)), (rbtree:rbtree(K_1, V_2))). :- mode rbtree:delete_2((builtin:di), (builtin:in), (builtin:in), (builtin:uo), (builtin:uo)) is semidet. :- mode rbtree:delete_2((builtin:di), (builtin:in), builtin:in(bound(no)), (builtin:uo), (builtin:uo)) is det. :- mode rbtree:delete_2((builtin:in), (builtin:in), (builtin:in), (builtin:out), (builtin:out)) is semidet. :- mode rbtree:delete_2((builtin:in), (builtin:in), builtin:in(bound(no)), (builtin:out), (builtin:out)) is det. rbtree:init((rbtree:empty)). rbtree:init = RBT_2 :- rbtree:init(RBT_2). rbtree:is_empty(Tree_2) :- Tree_2 = rbtree:empty. rbtree:set(RBT1_5, K_6, V_7) = RBT2_8 :- rbtree:set(RBT1_5, K_6, V_7, RBT2_8). rbtree:insert_duplicate(RBT1_5, K_6, V_7) = RBT2_8 :- rbtree:insert_duplicate(RBT1_5, K_6, V_7, RBT2_8). rbtree:lookup(RBT_4, K_5) = V_6 :- rbtree:lookup(RBT_4, K_5, V_6). rbtree:delete(Tree0_4, K_5, Tree_6) :- V_8 = bool:no, rbtree:delete_2(Tree0_4, K_5, V_8, V_7, Tree_6). rbtree:delete(RBT1_4, K_5) = RBT2_6 :- rbtree:delete(RBT1_4, K_5, RBT2_6). rbtree:remove(Tree0_5, K_6, V_7, Tree_8) :- V_9 = bool:yes, V_10 = std_util:yes(V_7), rbtree:delete_2(Tree0_5, K_6, V_9, V_10, Tree_8). rbtree:remove(Tree0_4, K_5, Tree_6) :- rbtree:remove(Tree0_4, K_5, V_7, Tree_6). rbtree:keys(RBT_3) = Ks_4 :- rbtree:keys(RBT_3, Ks_4). rbtree:values(RBT_3) = Vs_4 :- rbtree:values(RBT_3, Vs_4). rbtree:count(RBT_3) = N_4 :- rbtree:count(RBT_3, N_4). rbtree:assoc_list_to_rbtree(AL_3) = RBT_4 :- rbtree:assoc_list_to_rbtree(AL_3, RBT_4). rbtree:rbtree_to_assoc_list(RBT_3) = AL_4 :- rbtree:rbtree_to_assoc_list(RBT_3, AL_4). rbtree:foldl(_Pred_5, (rbtree:empty), Acc_6, Acc_6). rbtree:foldl(Pred_7, (rbtree:red(K_8, V_9, Left_10, Right_11)), Acc0_12, Acc_13) :- rbtree:foldl(Pred_7, Left_10, Acc0_12, Acc1_14), call(Pred_7, K_8, V_9, Acc1_14, Acc2_15), rbtree:foldl(Pred_7, Right_11, Acc2_15, Acc_13). rbtree:foldl(Pred_16, (rbtree:black(K_17, V_18, Left_19, Right_20)), Acc0_21, Acc_22) :- rbtree:foldl(Pred_16, Left_19, Acc0_21, Acc1_23), call(Pred_16, K_17, V_18, Acc1_23, Acc2_24), rbtree:foldl(Pred_16, Right_20, Acc2_24, Acc_22). rbtree:foldl(F_5, T_6, A_7) = B_8 :- P_9 = (pred(V_17::(builtin:in), V_16::(builtin:in), V_15::(builtin:in), V_14::(builtin:out)) is det :- some [] ( V_17 = W_18, V_16 = X_19, V_15 = Y_20, V_14 = Z_21, Z_21 = apply(F_5, W_18, X_19, Y_20) ) ), rbtree:foldl(P_9, T_6, A_7, B_8). rbtree:map_values(_Pred_4, (rbtree:empty), (rbtree:empty)). rbtree:map_values(Pred_5, Tree0_6, Tree_7) :- Tree0_6 = rbtree:red(K0_8, V0_9, Left0_10, Right0_11), Tree_7 = rbtree:red(K0_8, W0_12, Left_13, Right_14), call(Pred_5, K0_8, V0_9, W0_12), rbtree:map_values(Pred_5, Left0_10, Left_13), rbtree:map_values(Pred_5, Right0_11, Right_14). rbtree:map_values(Pred_15, Tree0_16, Tree_17) :- Tree0_16 = rbtree:black(K0_18, V0_19, Left0_20, Right0_21), Tree_17 = rbtree:black(K0_18, W0_22, Left_23, Right_24), call(Pred_15, K0_18, V0_19, W0_22), rbtree:map_values(Pred_15, Left0_20, Left_23), rbtree:map_values(Pred_15, Right0_21, Right_24). rbtree:map_values(F_4, T1_5) = T2_6 :- P_7 = (pred(V_13::(builtin:in), V_12::(builtin:in), V_11::(builtin:out)) is det :- some [] ( V_13 = X_14, V_12 = Y_15, V_11 = Z_16, Z_16 = apply(F_4, X_14, Y_15) ) ), rbtree:map_values(P_7, T1_5, T2_6). :- pragma termination_info(rbtree:init((builtin:uo)), finite(0, [no, no, no]), cannot_loop). :- pragma termination_info((rbtree:init) = (builtin:out), finite(0, [no, no, no]), cannot_loop). :- pragma termination_info(rbtree:is_empty((builtin:in)), finite(0, [no, no, no]), cannot_loop). :- pragma termination_info(rbtree:insert((builtin:in), (builtin:in), (builtin:in), (builtin:out)), finite(4, [no, no, yes, yes, yes, no]), can_loop). :- pragma termination_info(rbtree:update((builtin:in), (builtin:in), (builtin:in), (builtin:out)), finite(0, [no, no, yes, yes, yes, no]), cannot_loop). :- pragma termination_info(rbtree:set((builtin:di), (builtin:di), (builtin:di), (builtin:uo)), finite(4, [no, no, yes, yes, yes, no]), can_loop). :- pragma termination_info(rbtree:set((builtin:in), (builtin:in), (builtin:in), (builtin:out)), finite(4, [no, no, yes, yes, yes, no]), can_loop). :- pragma termination_info(rbtree:set((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), finite(4, [no, no, yes, yes, yes, no]), can_loop). :- pragma termination_info(rbtree:insert_duplicate((builtin:in), (builtin:in), (builtin:in), (builtin:out)), finite(4, [no, no, yes, yes, yes, no]), can_loop). :- pragma termination_info(rbtree:insert_duplicate((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), finite(4, [no, no, yes, yes, yes, no]), can_loop). :- pragma termination_info(rbtree:member((builtin:in), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no]), cannot_loop). :- pragma termination_info(rbtree:search((builtin:in), (builtin:in), (builtin:out)), finite(-4, [no, no, yes, no, no]), cannot_loop). :- pragma termination_info(rbtree:lookup((builtin:in), (builtin:in), (builtin:out)), finite(-4, [no, no, yes, no, no]), can_loop). :- pragma termination_info(rbtree:lookup((builtin:in), (builtin:in)) = (builtin:out), finite(-4, [no, no, yes, no, no]), can_loop). :- pragma termination_info(rbtree:lower_bound_search((builtin:in), (builtin:in), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), cannot_loop). :- pragma termination_info(rbtree:lower_bound_lookup((builtin:in), (builtin:in), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), can_loop). :- pragma termination_info(rbtree:upper_bound_search((builtin:in), (builtin:in), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), cannot_loop). :- pragma termination_info(rbtree:upper_bound_lookup((builtin:in), (builtin:in), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), can_loop). :- pragma termination_info(rbtree:delete((builtin:di), (builtin:in), (builtin:uo)), finite(0, [no, no, yes, no, no]), cannot_loop). :- pragma termination_info(rbtree:delete((builtin:in), (builtin:in), (builtin:out)), finite(0, [no, no, yes, no, no]), cannot_loop). :- pragma termination_info(rbtree:delete((builtin:in), (builtin:in)) = (builtin:out), finite(0, [no, no, yes, no, no]), cannot_loop). :- pragma termination_info(rbtree:remove((builtin:di), (builtin:in), (builtin:uo), (builtin:uo)), finite(-1, [no, no, yes, no, no, no]), cannot_loop). :- pragma termination_info(rbtree:remove((builtin:in), (builtin:in), (builtin:out), (builtin:out)), finite(-1, [no, no, yes, no, no, no]), cannot_loop). :- pragma termination_info(rbtree:remove((builtin:in), (builtin:in), (builtin:out)), finite(-1, [no, no, yes, no, no]), cannot_loop). :- pragma termination_info(rbtree:remove_smallest((builtin:di), (builtin:uo), (builtin:uo), (builtin:uo)), finite(-4, [no, no, yes, no, no, no]), cannot_loop). :- pragma termination_info(rbtree:remove_smallest((builtin:in), (builtin:out), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), cannot_loop). :- pragma termination_info(rbtree:remove_largest((builtin:di), (builtin:uo), (builtin:uo), (builtin:uo)), finite(-4, [no, no, yes, no, no, no]), cannot_loop). :- pragma termination_info(rbtree:remove_largest((builtin:in), (builtin:out), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), cannot_loop). :- pragma termination_info(rbtree:keys((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(rbtree:keys((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(rbtree:values((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(rbtree:values((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(rbtree:count((builtin:in), (builtin:out)), finite(0, [no, no, no, no]), cannot_loop). :- pragma termination_info(rbtree:count((builtin:in)) = (builtin:out), finite(0, [no, no, no, no]), cannot_loop). :- pragma termination_info(rbtree:assoc_list_to_rbtree((builtin:in), (builtin:out)), finite(0, [no, no, yes, no]), can_loop). :- pragma termination_info(rbtree:assoc_list_to_rbtree((builtin:in)) = (builtin:out), finite(0, [no, no, yes, no]), can_loop). :- pragma termination_info(rbtree:rbtree_to_assoc_list((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(rbtree:rbtree_to_assoc_list((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(rbtree:foldl((pred((builtin:in), (builtin:in), (builtin:in), (builtin:out)) is det), (builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(rbtree:foldl((pred((builtin:in), (builtin:in), (builtin:in), (builtin:out)) is semidet), (builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(rbtree:foldl((pred((builtin:in), (builtin:in), (builtin:di), (builtin:uo)) is det), (builtin:in), (builtin:di), (builtin:uo)), infinite, can_loop). :- pragma termination_info(rbtree:foldl((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(rbtree:map_values((pred((builtin:in), (builtin:in), (builtin:out)) is det), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(rbtree:map_values((pred((builtin:in), (builtin:in), (builtin:out)) is semidet), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(rbtree:map_values((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop).