% Corrected version of priority.t for Craig's class
%
% A PriorityQueue data structure implemented using an array.
% A priority queue consists of a list (a sequence) of elements.
% Elements are added to and removed from the queue on a priority basis,
% ie. lowest priority values first, FIFO within priority.

module PriorityQueue % Craig section
%class PriorityQueue % Kissin section
        % list of procedures and functions visible outside this program
        export Arrive, Leave, InspectFront, Length, IsEmpty, IsFull

        type elementType: string % a queue entry is a string
        type prtyType: int       % a queue entry's priority is an integer
        const maxLength := 100   % maximum length of array is 100
        var count: 0 .. maxLength % number of elements in queue
        var contents: array 1 .. maxLength of
        % Each queue entry is a record of two fields: element, which contains
        % the string information, and prty, the integer priority value.
                record
                   element: elementType
                   prty: prtyType
                end record

        % Initialize the priority queue so it can be used.  Make it empty.
        count := 0


        % Insert element with its priority prty into the priority queue.
        % The priority queue must not be full.
        %
        % This procedure is called from the main program by the statement
        % PriorityQueue.Arrive(<element>,<priority>)
        % where <element> is a string and <priority> is an integer
        % 
        procedure Arrive (element: elementType, prty: prtyType)
           pre count < maxLength % Test that array not full.
           var where: int := 1  
           % Records are kept in the array in order of increasing priority
           % value.
           loop % Find where to insert new element.
                exit when where > count or prty < contents(where).prty
                where += 1  % loop incremented
           end loop
           % Move following elements back 1 slot.
           for decreasing i: count .. where
                contents(i+1) := contents(i)
           end for
           % Insert new element and record its priority.
           contents(where).element := element
           contents(where).prty := prty
           count += 1
        end Arrive



        % Remove element from the front of the priority queue.
        % This will be the element with the lowest priority VALUE in the
        % queue (and the one longest in the queue at that priority).
        % The priority queue must not be empty.
        %
        % This procedure is called from the main program by the command
        % PriorityQueue.Leave(<element>,<prty>) where element is a string
        % and prty is an integer 
        %
        procedure Leave (var element: elementType, var prty: prtyType)
           pre count > 0
           element := contents(1).element
           prty := contents(1).prty
           for i: 2 .. count % Move all remaining items forward 1 slot.
                contents(i-1) := contents(i)
           end for
           count -= 1
        end Leave


        % Return element from front of priority queue without changing the
        % priority queue.  The queue must not be empty.
        % Called as PriorityQueue.InspectFront, this function is similar
        % to leave but it does not remove the element from the queue. 
        function InspectFront: elementType
           pre count > 0
           result contents(1).element
        end InspectFront



        % Return number of elements in priority queue.
        function Length: int
           result count
        end Length



        % Return true if the priority queue contains no elements.
        % This function is called from the main program as 
        % PriorityQueue.IsEmpty and has a value of either true or false. 
        %
        function IsEmpty: boolean
           result count = 0
        end IsEmpty



        % Return true if the priority queue cannot hold any more elements.
        function IsFull: boolean
           result count = maxLength
        end IsFull


end PriorityQueue