:- module bintree. :- use_module assoc_list, builtin, int, list, private_builtin, require, std_util. :- type (bintree:bintree(K, V)) ---> empty ; tree(K, V, (bintree:bintree(K, V)), (bintree:bintree(K, V))) . :- pred bintree:from_list_2((list:list((std_util:pair(K_1, V_2)))), (bintree:bintree(K_1, V_2)), (bintree:bintree(K_1, V_2))). :- mode bintree:from_list_2((builtin:in), (builtin:in), (builtin:out)) is det. :- pred bintree:from_sorted_list_2(int, (list:list((std_util:pair(K_1, V_2)))), (bintree:bintree(K_1, V_2)), (list:list((std_util:pair(K_1, V_2))))). :- mode bintree:from_sorted_list_2((builtin:in), (builtin:in), (builtin:out), (builtin:out)) is det. :- pred bintree:to_list_2((bintree:bintree(K_1, V_2)), (list:list((std_util:pair(K_1, V_2)))), (list:list((std_util:pair(K_1, V_2))))). :- mode bintree:to_list_2((builtin:in), (builtin:in), (builtin:out)) is det. :- pred bintree:keys_2((bintree:bintree(K_1, _V_2)), (list:list(K_1)), (list:list(K_1))). :- mode bintree:keys_2((builtin:in), (builtin:in), (builtin:out)) is det. :- pred bintree:values_2((bintree:bintree(_K_1, V_2)), (list:list(V_2)), (list:list(V_2))). :- mode bintree:values_2((builtin:in), (builtin:in), (builtin:out)) is det. bintree:init((bintree:empty)). bintree:set(BT1_5, K_6, V_7) = BT2_8 :- bintree:set(BT1_5, K_6, V_7, BT2_8). bintree:lookup(BT_4, K_5) = V_6 :- bintree:lookup(BT_4, K_5, V_6). bintree:delete(BT1_4, K_5) = BT2_6 :- bintree:delete(BT1_4, K_5, BT2_6). bintree:keys(Tree_3, List_4) :- V_5 = list:[], bintree:keys_2(Tree_3, V_5, List_4). bintree:keys(BT_3) = Ks_4 :- bintree:keys(BT_3, Ks_4). bintree:values(Tree_3, List_4) :- V_5 = list:[], bintree:values_2(Tree_3, V_5, List_4). bintree:values(BT_3) = Vs_4 :- bintree:values(BT_3, Vs_4). bintree:from_list(List_3, Tree_4) :- V_5 = bintree:empty, bintree:from_list_2(List_3, V_5, Tree_4). bintree:from_list(AL_3) = BT_4 :- bintree:from_list(AL_3, BT_4). bintree:from_sorted_list(List_3, Tree_4) :- list:length(List_3, Length_5), bintree:from_sorted_list_2(Length_5, List_3, Tree_4, V_6). bintree:from_sorted_list(AL_3) = BT_4 :- bintree:from_sorted_list(AL_3, BT_4). bintree:from_corresponding_lists(Ks_4, Vs_5) = BT_6 :- bintree:from_corresponding_lists(Ks_4, Vs_5, BT_6). bintree:to_list(Tree_3, List_4) :- V_5 = list:[], bintree:to_list_2(Tree_3, V_5, List_4). bintree:to_list(BT_3) = AL_4 :- bintree:to_list(BT_3, AL_4). bintree:count(BT_3) = N_4 :- bintree:count(BT_3, N_4). bintree:depth(BT_3) = N_4 :- bintree:depth(BT_3, N_4). bintree:balance(Tree0_3, Tree_4) :- bintree:to_list(Tree0_3, List_5), bintree:from_sorted_list(List_5, Tree_4). bintree:balance(BT1_3) = BT2_4 :- bintree:balance(BT1_3, BT2_4). :- pragma termination_info(bintree:init((builtin:uo)), finite(0, [no, no, no]), cannot_loop). :- pragma termination_info(bintree:insert((builtin:in), (builtin:in), (builtin:in), (builtin:out)), finite(4, [no, no, yes, yes, yes, no]), cannot_loop). :- pragma termination_info(bintree:update((builtin:in), (builtin:in), (builtin:in), (builtin:out)), finite(0, [no, no, yes, no, yes, no]), cannot_loop). :- pragma termination_info(bintree:set((builtin:di), (builtin:di), (builtin:di), (builtin:uo)), finite(4, [no, no, yes, yes, yes, no]), cannot_loop). :- pragma termination_info(bintree:set((builtin:in), (builtin:in), (builtin:in), (builtin:out)), finite(4, [no, no, yes, yes, yes, no]), cannot_loop). :- pragma termination_info(bintree:set((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), finite(4, [no, no, yes, yes, yes, no]), cannot_loop). :- pragma termination_info(bintree:search((builtin:in), (builtin:in), (builtin:in)), finite(0, [no, no, no, no, no]), cannot_loop). :- pragma termination_info(bintree:search((builtin:in), (builtin:in), (builtin:out)), finite(-4, [no, no, yes, no, no]), cannot_loop). :- pragma termination_info(bintree:lookup((builtin:in), (builtin:in), (builtin:out)), finite(-4, [no, no, yes, no, no]), can_loop). :- pragma termination_info(bintree:lookup((builtin:in), (builtin:in)) = (builtin:out), finite(-4, [no, no, yes, no, no]), can_loop). :- pragma termination_info(bintree:lower_bound_search((builtin:in), (builtin:in), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), cannot_loop). :- pragma termination_info(bintree:lower_bound_lookup((builtin:in), (builtin:in), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), can_loop). :- pragma termination_info(bintree:upper_bound_search((builtin:in), (builtin:in), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), cannot_loop). :- pragma termination_info(bintree:upper_bound_lookup((builtin:in), (builtin:in), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), can_loop). :- pragma termination_info(bintree:delete((builtin:in), (builtin:in), (builtin:out)), finite(0, [no, no, yes, no, no]), can_loop). :- pragma termination_info(bintree:delete((builtin:in), (builtin:in)) = (builtin:out), finite(0, [no, no, yes, no, no]), can_loop). :- pragma termination_info(bintree:remove((builtin:in), (builtin:in), (builtin:out), (builtin:out)), finite(-4, [no, no, yes, no, no, no]), can_loop). :- pragma termination_info(bintree:keys((builtin:in), (builtin:out)), finite(0, [no, no, yes, no]), cannot_loop). :- pragma termination_info(bintree:keys((builtin:in)) = (builtin:out), finite(0, [no, no, yes, no]), cannot_loop). :- pragma termination_info(bintree:values((builtin:in), (builtin:out)), finite(0, [no, no, yes, no]), cannot_loop). :- pragma termination_info(bintree:values((builtin:in)) = (builtin:out), finite(0, [no, no, yes, no]), cannot_loop). :- pragma termination_info(bintree:from_list((builtin:in), (builtin:out)), finite(0, [no, no, yes, no]), can_loop). :- pragma termination_info(bintree:from_list((builtin:in)) = (builtin:out), finite(0, [no, no, yes, no]), can_loop). :- pragma termination_info(bintree:from_sorted_list((builtin:in), (builtin:out)), finite(0, [no, no, yes, no]), can_loop). :- pragma termination_info(bintree:from_sorted_list((builtin:in)) = (builtin:out), finite(0, [no, no, yes, no]), can_loop). :- pragma termination_info(bintree:from_corresponding_lists((builtin:in), (builtin:in), (builtin:out)), finite(0, [no, no, yes, yes, no]), can_loop). :- pragma termination_info(bintree:from_corresponding_lists((builtin:in), (builtin:in)) = (builtin:out), finite(0, [no, no, yes, yes, no]), can_loop). :- pragma termination_info(bintree:to_list((builtin:in), (builtin:out)), finite(0, [no, no, yes, no]), can_loop). :- pragma termination_info(bintree:to_list((builtin:in)) = (builtin:out), finite(0, [no, no, yes, no]), can_loop). :- pragma termination_info(bintree:count((builtin:in), (builtin:out)), finite(0, [no, no, no, no]), cannot_loop). :- pragma termination_info(bintree:count((builtin:in)) = (builtin:out), finite(0, [no, no, no, no]), cannot_loop). :- pragma termination_info(bintree:depth((builtin:in), (builtin:out)), finite(0, [no, no, no, no]), can_loop). :- pragma termination_info(bintree:depth((builtin:in)) = (builtin:out), finite(0, [no, no, no, no]), can_loop). :- pragma termination_info(bintree:branching_factor((builtin:in), (builtin:out), (builtin:out)), finite(0, [no, no, no, no, no]), cannot_loop). :- pragma termination_info(bintree:balance((builtin:in), (builtin:out)), finite(0, [no, no, yes, no]), can_loop). :- pragma termination_info(bintree:balance((builtin:in)) = (builtin:out), finite(0, [no, no, yes, no]), can_loop).