Resolve/C++ Catalog
CT/Natural/IO_1.h
Copyright © 2010, Reusable Software Research Group, The Ohio State University

//  /*-------------------------------------------------------------------*\
//  |   Concrete Template : Natural_IO_1
//  \*-------------------------------------------------------------------*/

#ifndef CT_NATURAL_IO_1
#define CT_NATURAL_IO_1 1

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

#include "AT/General/Get_From.h"
#include "AT/General/Put_To.h"

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

concrete_template <
	concrete_instance class Natural_Base
	/*!
	    implements
		abstract_instance Natural_Kernel
	    satisfies restriction
		Natural_Base::RADIX = 10
	!*/
    >
class Natural_IO_1 :
    implements
        abstract_instance General_Get_From <Natural_Base>,
    implements
        abstract_instance General_Put_To <Natural_Base>,
    extends
        concrete_instance Natural_Base
{
private:

    /*!
        math definition IS_DIGIT (
		c: character
	    ): boolean is
	    c is in {'0','1','2','3','4','5','6','7','8','9'}

        math subtype DIGIT is character
            exemplar d
            constraint
                IS_DIGIT (d)

        math definition IS_DIGITS (
		s: string of character
	    ): boolean satisfies
	    if s = empty_string
	    then IS_DIGITS (s) = true
	    else there exists a: string of character, c: character
		     (s = a * <c>  and
		      IS_DIGITS (s) = (IS_DIGITS (a) and IS_DIGIT (c)))

        math definition INTEGER_VAL (
		s: string of DIGIT
	    ): NATURAL_MODEL satisfies
	    if s = empty_string
	    then INTEGER_VAL (s) = 0
	    else there exists a: string of DIGIT, d: DIGIT
		     (s = a * <d>  and
		      INTEGER_VAL (s) = 10 * INTEGER_VAL (a)
			+ TO_INTEGER (d) - TO_INTEGER ('0'))

        math definition IS_SPACES_AND_TABS (
		s: string of character
	    ): boolean is
	    elements (s) is subset of {' ', '\t'}

        math definition IS_AN_INPUT_REP (
		s: string of character,
		n: NATURAL_MODEL
	    ): boolean is
	    there exists s1, s2, s3: string of character, c: character
		(s = s1 * s2 * s3 * "\n"  and
		 IS_SPACES_AND_TABS (s1)  and
		 IS_DIGITS (s2)  and
		 n = INTEGER_VAL (s2)  and
		 IS_SPACES_AND_TABS (s3))

        math definition DIGIT_CHARACTER (
		i: integer
	    ): character satisfies
	    if 0 <= i < 10
	    then DIGIT_CHARACTER (i) = TO_CHARACTER (TO_INTEGER ('0') + i)
	    else DIGIT_CHARACTER (i) = '\0'

        math definition POSITIVE_OUTPUT_REP (
		n: NATURAL_MODEL
	    ): string of character satisfies
	    if n = 0
	    then POSITIVE_OUTPUT_REP (n) = empty_string
	    else there exists k, d: integer
		     (n = 10 * k + d  and
		      0 <= d < 10  and
		      POSITIVE_OUTPUT_REP (n) =
			  POSITIVE_OUTPUT_REP (k) *
			      <DIGIT_CHARACTER (d)>) 

        math definition OUTPUT_REP (
		n: NATURAL_MODEL
	    ): string of character satisfies
	    if n = 0
	    then OUTPUT_REP (n) = "0"
	    else OUTPUT_REP (n) = POSITIVE_OUTPUT_REP (n)
    !*/

    procedure_body Put_Positive (
	    preserves Natural_IO_1& n,
	    alters Character_OStream& outs
	)
    /*!
	requires
	    outs.is_open = true
	ensures
	    outs.is_open = true  and
	    outs.ext_name = #outs.ext_name  and
	    if self = 0
		then outs.content = #outs.content
		else outs.content =
			 #outs.content * OUTPUT_REP (n)
    !*/
    {
	if (n.Discrete_Log () > 0)
	{
	    object Integer n_low_digit;

	    n.Divide_By_Radix (n_low_digit);

	    Put_Positive (n, outs);
	    outs << n_low_digit;

	    n.Multiply_By_Radix (n_low_digit);
	}
    }

public:

    procedure_body Get_From (
	    alters Character_IStream& ins
	)
    {
	object Text line;

	self.Clear ();
	ins >> line;
	while (line.Length () > 0)
	{
	    object Character c;

	    line.Remove (0, c);
	    if ((c < '0') or (c > '9'))
	    {
		break;
	    }
	    self.Multiply_By_Radix (To_Integer (c) - To_Integer ('0'));
	}
    }

    procedure_body Put_To (
	    alters Character_OStream& outs
	)
    {
	if (self.Discrete_Log () == 0)
	{
	    outs << '0';
	}
	else
	{
	    Put_Positive (self, outs);
	}
    }

};

#endif // CT_NATURAL_IO_1