14.4.5  Bounded_Queue

The Bounded_Queue api defines the external interface to the bounded_queue package.

The Bounded_Queue api is implemented by the bounded_queue package.

The Bounded_Queue api source code is src/lib/src/bounded-queue.api. The above information is manually maintained and may contain errors.

api {
    Queue X = QUEUE {back:List(X ), bound:Int, front:List(X ), length:Int};
    make_queue : Int -> Queue(X );
    queue_is_empty : Queue(X ) -> Bool;
    put_on_back_of_queue : (Queue(X ) , X) -> Queue(X );
    push : (Queue(X ) , X) -> Queue(X );
    take_from_front_of_queue : Queue(X ) -> (Queue(X ) , Null_Or(X ));
    pull : Queue(X ) -> (Queue(X ) , Null_Or(X ));
    put_on_front_of_queue : (Queue(X ) , X) -> Queue(X );
    unpull : (Queue(X ) , X) -> Queue(X );
    take_from_back_of_queue : Queue(X ) -> (Queue(X ) , Null_Or(X ));
    unpush : Queue(X ) -> (Queue(X ) , Null_Or(X ));
    to_list : Queue(X ) -> List(X );
    from_list : (List(X ) , Int) -> Queue(X );
    unpull' : (Queue(X ) , List(X )) -> Queue(X );
    push' : (Queue(X ) , List(X )) -> Queue(X );
    length : Queue(X ) -> Int;};