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

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

#ifndef CT_NATURAL_KERNEL_1
#define CT_NATURAL_KERNEL_1 1

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

#include "AI/Natural/Kernel.h"
#include "CT/Sequence/Kernel_1a.h"

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

concrete_template <
	concrete_instance class Sequence_Of_Digits =
            Sequence_Kernel_1a <Integer>,
	concrete_instance class Rep =
            Representation <Sequence_Of_Digits>
    >
class Natural_Kernel_1 :
    implements
	abstract_instance Natural_Kernel,
    encapsulates
	concrete_instance Rep
{
private:
    
    rep_field_name (Rep, 0, Sequence_Of_Digits, digits);
    
    /*!
	math definition RADIX: integer is
	    10

	math definition HAS_ONLY_DIGITS (
		    s: string of integer
		): boolean satisfies
	    if s = empty_string
	    then  HAS_ONLY_DIGITS (s) = true
	    else  for all a: string of integer, k: integer
			  where (s = a * <k>)
		      (HAS_ONLY_DIGITS (s) =
			   (HAS_ONLY_DIGITS (a)  and
			    0 <= k < 10))

	math definition IS_WELL_FORMED_RADIX_REPRESENTATION (
		    s: string of integer
		): boolean is
	    s = empty_string  or
	    there exists k: integer, a: string of integer 
		(s = <k> * a  and
		 1 <= k < 10  and
		 HAS_ONLY_DIGITS (a))

	math definition NUMERICAL_VALUE (
		    s: string of integer
		): integer satisfies
	    if s = empty_string
	    then  NUMERICAL_VALUE (s) = 0
	    else  for all a: string of integer, k: integer
			  where (s = a * <k>)
		      (NUMERICAL_VALUE (s) =
			   NUMERICAL_VALUE (a) * 10 + k)

	convention
            IS_WELL_FORMED_RADIX_REPRESENTATION (reverse (self.digits))
	    
	correspondence
            self = NUMERICAL_VALUE (reverse (self.digits))
    !*/

public:


    standard_concrete_operations (Natural_Kernel_1);

    procedure_body Multiply_By_Radix (
	    preserves Integer k
	)
    {
	if ((self[digits].Length () > 0) or (k > 0))
	{
	    object Integer k_copy = k;

	    self[digits].Add (0, k_copy);
	}
    }

    procedure_body Divide_By_Radix (
	    produces Integer& k
	)
    {
	if (self[digits].Length () == 0)
	{
	    k = 0;
	}
	else
	{
	    self[digits].Remove (0, k);
	}
    }

    function_body Integer Discrete_Log ()
    {
	return self[digits].Length ();
    }

    function_body Integer Radix ()
    {
	return 10;
    }

};

#endif // CT_NATURAL_KERNEL_1