//  /*--------------------------------------------------------*\
//  |   Main Program: Replace whitespace with visible markers
//  |*--------------------------------------------------------*|
//  |   Date:         13 August 1996
//  |   Author:       Bruce W. Weide
//  |   
//  |   Brief User's Manual:
//  |   Accepts as input an arbitrary text, then outputs the
//  |   same text but with each of the following whitespace
//  |   characters in the input replaced by a corresponding
//  |   visible marker, and then quits.
//  |     ' ' replaced by " SPACE "
//  |     '\t' replaced by " TAB "
//  |     '\n' replaced by " NEWLINE "
//  |   
//  \*--------------------------------------------------------*/

///-------------------------------------------------------------
/// Global Context ---------------------------------------------
///-------------------------------------------------------------

#include "RESOLVE_Foundation.h"

///-------------------------------------------------------------
/// Interface --------------------------------------------------
///-------------------------------------------------------------

/*!
    math operation REPL (
            c: character
        ): string of character
        implicit definition
            if c = ' ' then REPL(c) = " SPACE "
            else if c = '\t' then REPL(c) = " TAB "
            else if c = '\n' then REPL(c) = " NEWLINE "
            else REPL(c) = <c>

    math operation SREPL (
            s: string of character
        ): string of character
        implicit definition
            if s = empty_string then
                SREPL(s) = empty_string
		       else
                there exists c: character,
                             s1: string of character
                    (s = <c> * s1  and
                     SREPL(s) = REPL(c) * SREPL(s1))
!*/

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

global_procedure Replace (
        preserves Character c,
        produces Text& t
    );
/*!
    ensures
	t = REPL (c)
!*/
    
//--------------------------------------------------------------

global_procedure_body Replace (
        preserves Character c,
        produces Text& t
    )
{
    case_select (c)
    {
        case ' ':
            {
                t = " SPACE ";
            }
            break;
        case '\t':
            {
                t = " TAB ";
            }
            break;
        case '\n':
            {
                t = " NEWLINE ";
            }
            break;
        default:
            {
              t = "";
              t.Add (0, c);
            }
            break;
    }
}

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

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

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

    // Process input one line at a time, making replacements
    // as required

    while (not input.At_EOS ())
    /*!
	alters input, out
	requires
	    input.is_open = true  and
	    "\n" is suffix of input.content and
	    output.is_open = true
	ensures
	    input.is_open = true  and
	    input.ext_name = #input.ext_name  and
	    input.content = empty_string  and
	    output.is_open = true  and
	    output.ext_name = #output.ext_name  and
	    output.content =
		#output.content * SREPL(#input.content))
    !*/
    {
        object Text line_from_input, text_to_output;

        input >> line_from_input;

        // Process current line; then note '\n' at end of it
    
        while (line_from_input.Length () > 0)
            /*!
                alters output
                consumes line_from_input
                produces text_to_output
                requires
                    output.is_open = true
                ensures
                    output.is_open = true  and
                    output.ext_name = #output.ext_name  and
                    output.content =
                        #output.content * SREPL(#line_from_input)
            !*/
        {
            object Character character_from_input;

            line_from_input.Remove (0, character_from_input);
            Replace (character_from_input, text_to_output);
            output << text_to_output;
        }
        Replace ('\n', text_to_output);
        output << text_to_output;
    }

    // Close input and output streams
    
    input.Close_External ();
    output.Close_External ();
}