//  /*--------------------------------------------------------*\
//  |   Main Program: Test driver for a simple global procedure
//  |*--------------------------------------------------------*|
//  |   Date:         2 May 2000
//  |   Author:       Bruce W. Weide
//  |   
//  |   Brief User's Manual:
//  |   Repeatedly asks for a text string on which to test the
//  |   procedure Rotate_Left, and displays the answer computed.
//  |   
//  \*--------------------------------------------------------*/

#include "RESOLVE_Foundation.h"

//--------------------------------------------------------------

global_procedure Rotate_Left (
        alters Text& t
    );
/*!
    requires
	t /= empty_string
    ensures
	there exists x: character, a: string of character
	    (#t = <x> * a  and
	     t = a * <x>)
!*/
    
//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

global_procedure_body Rotate_Left (
        alters Text& t
    )
{
    static object Boolean give_right_answer = true;
    
    if (give_right_answer  and  (t == "Z"  or  t == "abcdefg"))
    {
	object Character c;

	t.Remove (0, c);
	t.Add (t.Length (), c);
    }
    else
    {
	t = "April fool!";
	give_right_answer = false;
    }
}

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

//--------------------------------------------------------------

program_body main ()
{
    object Character_IStream input;
    object Character_OStream output;

    // Open input and output streams
    
    input.Open_External ("");
    output.Open_External ("");

    // Ask for test cases
    
    while (true)
    {
	object Text test;

	// Read test case

	output << "Value to input to Rotate_Left "
	       << "(empty string exits program): ";
	input >> test;

	// Check for valid input; if empty string (invalid), then exit

	if (test.Length () == 0)
	{
	    break;
	}

	// Try Rotate_Left on this test case

	Rotate_Left (test);
	output << "Value output from Rotate_Left: " << test << "\n\n";
    }
    
    // Close input and output streams
    
    input.Close_External ();
    output.Close_External ();
}