14.2.34  Queue

The standard library Queue api defines access to immutable, fully persistent queues.

The Queue api is implemented by the queue package.

The Queue api source code is in src/lib/src/queue.api.

The above information is manually maintained and may contain errors.

api {
    Queue X = QUEUE {back:List(X ), front:List(X )};
    empty_queue : 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 ) -> Queue(X );
    unpull' : (Queue(X ) , List(X )) -> Queue(X );
    push' : (Queue(X ) , List(X )) -> Queue(X );
    length : Queue(X ) -> Int;};