:- module pqueue.
:- use_module assoc_list, builtin, int, list, private_builtin, std_util.
:- type (pqueue:pqueue(K, V))
	--->	empty
	;	pqueue(int, K, V, (pqueue:pqueue(K, V)), (pqueue:pqueue(K, V)))
	.
:- pred pqueue:remove_2((pqueue:pqueue(K_1, V_2)), (pqueue:pqueue(K_1, V_2)), (pqueue:pqueue(K_1, V_2))).
:- mode pqueue:remove_2((builtin:in), (builtin:in), (builtin:out)) is det.
pqueue:init((pqueue:empty)).
pqueue:init = PQ_2 :-
		pqueue:init(PQ_2).
pqueue:insert(PQ1_5, K_6, V_7) = PQ2_8 :-
		pqueue:insert(PQ1_5, K_6, V_7, PQ2_8).
pqueue:remove((pqueue:pqueue(V_5, K_6, V_7, L0_8, R0_9)), K_6, V_7, PQ_10) :-
		pqueue:remove_2(L0_8, R0_9, PQ_10).
pqueue:to_assoc_list(PQ_3) = AL_4 :-
		pqueue:to_assoc_list(PQ_3, AL_4).
pqueue:assoc_list_to_pqueue(AL_3) = PQ2_4 :-
		pqueue:assoc_list_to_pqueue(AL_3, PQ2_4).
:- pragma termination_info(pqueue:init((builtin:out)), finite(0, [no, no, no]), cannot_loop).
:- pragma termination_info((pqueue:init) = (builtin:out), finite(0, [no, no, no]), cannot_loop).
:- pragma termination_info(pqueue:insert((builtin:in), (builtin:in), (builtin:in), (builtin:out)), finite(5, [no, no, yes, yes, yes, no]), cannot_loop).
:- pragma termination_info(pqueue:insert((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), finite(5, [no, no, yes, yes, yes, no]), cannot_loop).
:- pragma termination_info(pqueue:remove((builtin:in), (builtin:out), (builtin:out), (builtin:out)), infinite, can_loop).
:- pragma termination_info(pqueue:to_assoc_list((builtin:in), (builtin:out)), infinite, can_loop).
:- pragma termination_info(pqueue:to_assoc_list((builtin:in)) = (builtin:out), infinite, can_loop).
:- pragma termination_info(pqueue:assoc_list_to_pqueue((builtin:in), (builtin:out)), infinite, cannot_loop).
:- pragma termination_info(pqueue:assoc_list_to_pqueue((builtin:in)) = (builtin:out), infinite, cannot_loop).