:- module stack.
:- use_module builtin, list, private_builtin, require, std_util.
:- type (stack:stack(T)) == (list:list(T)).
stack:init((list:[])).
stack:init = S_2 :-
		stack:init(S_2).
stack:is_empty((list:[])).
stack:is_full(V_2) :-
		std_util:semidet_fail.
stack:push(Stack_4, Elem_5, (list:[Elem_5 | Stack_4])).
stack:push(S1_4, X_5) = S2_6 :-
		stack:push(S1_4, X_5, S2_6).
stack:push_list(S1_4, Xs_5) = S2_6 :-
		stack:push_list(S1_4, Xs_5, S2_6).
stack:top((list:[Elem_3 | V_4]), Elem_3).
stack:top_det(S_3) = X_4 :-
		stack:top_det(S_3, X_4).
stack:pop((list:[Elem_4 | Stack_5]), Elem_4, Stack_5).
stack:depth(Stack_3, Depth_4) :-
		list:length(Stack_3, Depth_4).
stack:depth(S_3) = N_4 :-
		stack:depth(S_3, N_4).
:- pragma termination_info(stack:init((builtin:out)), finite(0, [no, no]), cannot_loop).
:- pragma termination_info((stack:init) = (builtin:out), finite(0, [no, no]), cannot_loop).
:- pragma termination_info(stack:is_empty((builtin:in)), finite(0, [no, no]), cannot_loop).
:- pragma termination_info(stack:is_full((builtin:in)), finite(0, [no, no]), can_loop).
:- pragma termination_info(stack:push((builtin:in), (builtin:in), (builtin:out)), finite(2, [no, yes, yes, no]), cannot_loop).
:- pragma termination_info(stack:push((builtin:in), (builtin:in)) = (builtin:out), finite(2, [no, yes, yes, no]), cannot_loop).
:- pragma termination_info(stack:push_list((builtin:in), (builtin:in), (builtin:out)), finite(0, [no, yes, yes, no]), can_loop).
:- pragma termination_info(stack:push_list((builtin:in), (builtin:in)) = (builtin:out), finite(0, [no, yes, yes, no]), can_loop).
:- pragma termination_info(stack:top((builtin:in), (builtin:out)), finite(-2, [no, yes, no]), cannot_loop).
:- pragma termination_info(stack:top_det((builtin:in), (builtin:out)), finite(-2, [no, yes, no]), can_loop).
:- pragma termination_info(stack:top_det((builtin:in)) = (builtin:out), finite(-2, [no, yes, no]), can_loop).
:- pragma termination_info(stack:pop((builtin:in), (builtin:out), (builtin:out)), finite(-2, [no, yes, no, no]), cannot_loop).
:- pragma termination_info(stack:pop_det((builtin:in), (builtin:out), (builtin:out)), finite(-2, [no, yes, no, no]), can_loop).
:- pragma termination_info(stack:depth((builtin:in), (builtin:out)), infinite, can_loop).
:- pragma termination_info(stack:depth((builtin:in)) = (builtin:out), infinite, can_loop).