//  /*--------------------------------------------------------*\
//  |   Main Program: Polynomial evaluation timing comparison
//  |*--------------------------------------------------------*|
//  |   Date:         9 August 1999 (revised 24 November 2006)
//  |   Author:       Bruce W. Weide
//  |   
//  |   Brief User's Manual:
//  |   Reads from stdin a non-negative integer which is the
//  |   degree of the polynomial to be evaluated (i.e., n),
//  |   followed by the n+1 real-valued coefficients in the
//  |   order a0 through an, followed by the real-valued point
//  |   at which the polynomial is to be evaluated (i.e., x).
//  |   Each number is expected to be on its own line of input.
//  |   The program then prints out the polynomial followed by
//  |   the evaluation of the polynomial at the point x and the
//  |   execution time, for the obvious method and for Horner's
//  |   rule (both iterative and recursive), and then quits.
//  |   
//  \*--------------------------------------------------------*/

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

#include "RESOLVE_Foundation.h"

#include "CT/Sequence/Kernel_1a_C.h"
#include "CI/Timer/1.h"

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

concrete_instance
class Polynomial_Coefficients :
    instantiates Sequence_Kernel_1a_C <Real>
{};

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

/*!
    math definition INPUT_ENCODING (
            s: string of real
        ): string of character satisfies
        if s = empty_string
        then INPUT_ENCODING (s) = empty_string
        else there exists y: real, r: string of real
                 (s = <y> * r  and
                  INPUT_ENCODING (s) = TO_TEXT (y) * "\n" *
                                         INPUT_ENCODING (r))

    math definition EVAL (
            s: string of real,
            x: real
        ): real satisfies
        if s = empty_string
        then EVAL (s, x) = 0.0
        else there exists y: real, r: string of real
                 (s = <y> * r  and
                  EVAL (s, x) = x * EVAL (r, x) + y)
!*/

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

global_procedure Read_Polynomial_And_X (
        alters Character_IStream& input,
        produces Polynomial_Coefficients& a,
        produces Real& x
    );
/*!
    requires
        input.is_open = TRUE  and
        there exists s: string of real, z: real
            (TO_TEXT (|s|) * "\n" * INPUT_ENCODING (s) *
                 TO_TEXT (z) * "\n"
                 is prefix of input.content)
    ensures
        input.is_open = TRUE  and
        input.ext_name = #input.ext_name  and
        #input.content = TO_TEXT (|a|) * "\n" *
                             INPUT_ENCODING (a) *
                             TO_TEXT (x) * "\n" *
                             input.content
!*/
  
//--------------------------------------------------------------

global_procedure Write_Polynomial (
        alters Character_OStream& output,
        preserves Polynomial_Coefficients& a
    );
/*!
    requires
        output.is_open = TRUE
    ensures
        output.is_open = TRUE  and
        output.ext_name = #output.ext_name  and
        output.content = #output.content * [display of
                           polynomial with coefficients
                           that are in a]
!*/
  
//--------------------------------------------------------------

global_function Real Original_Evaluation (
        preserves Polynomial_Coefficients& a,
        preserves Real x
    );
/*!
    ensures
        Original_Evaluation = EVAL (a, x)
!*/
  
//--------------------------------------------------------------

global_function Real Horner_Iterative_Evaluation (
        preserves Polynomial_Coefficients& a,
        preserves Real x
    );
/*!
    ensures
        Horner_Iterative_Evaluation = EVAL (a, x)
!*/
  
//--------------------------------------------------------------

global_function Real Horner_Recursive_Evaluation (
        preserves Polynomial_Coefficients& a,
        preserves Real x
    );
/*!
    ensures
        Horner_Recursive_Evaluation = EVAL (a, x)
!*/
  
//--------------------------------------------------------------
//--------------------------------------------------------------

global_procedure_body Read_Polynomial_And_X (
        alters Character_IStream& input,
        produces Polynomial_Coefficients& a,
        produces Real& x
    )
{
    object Integer n, k;
    
    input >> n;
    a.Clear ();
    while (k <= n)
    {
        object Real coeff;

        input >> coeff;
        a.Add (k, coeff);
        k++;
    }
    input >> x;
}

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

global_procedure_body Write_Polynomial (
        alters Character_OStream& output,
        preserves Polynomial_Coefficients& a
    )
{
    object Integer k;
    
    output << "p(x) = \n";
    k = a.Length () - 1;
    while (k > 1)
    {
        output << "  " << a[k] << " * x^(" << k << ") + \n";
        k--;
    }
    if (k == 1)
    {
        output << "  " << a[1] << " * x + \n";
    }
    output << "  " << a[0] << "\n";
}
  
//--------------------------------------------------------------

global_function_body Real Original_Evaluation (
        preserves Polynomial_Coefficients& a,
        preserves Real x
    )
{
    object Real result;
    object Integer k;

    while (k <= a.Length () - 1)
    /*!
        preserves a, x
        alters result, k
        maintains
            there exists s: string of real
                (|s| = k  and
                 s is prefix of a  and
                 result = EVAL (s, x))
        decreases
            |a| - k
    !*/
    {
        object Real term = a[k];
        object Integer i;
        
        // Compute the k-th term = a[k] * x ^ (k)

        while (i < k)
        /*!
            preserves x, k
            alters term, i
            maintains
                i <= k  and
                term = #term * x ^ (i)
            decreases
                k - i
        !*/
        {
            term *= x;
            i++;
        }

        // Add this term to total so far

        result += term;
        k++;
    }

    return result;
}

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

global_function_body Real Horner_Iterative_Evaluation (
        preserves Polynomial_Coefficients& a,
        preserves Real x
    )
{
    object Real result;
    object Integer k = a.Length () - 1;

    while (k >= 0)
    /*!
        preserves a, x
        alters result, k
        maintains
            there exists s: string of real
                (|s| = |a| - (k + 1)  and
                 s is suffix of a  and
                 result = EVAL (s, x))
         decreases
             k + 1
    !*/
    {
        result = result * x + a[k];
        k--;
    }

    return result;
}

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

global_function_body Real Horner_Recursive_Evaluation (
        preserves Polynomial_Coefficients& a,
        preserves Real x
    )
{
    object Real result;

    if (a.Length () == 0)
    {
        return 0.0;
    }
    else
    {
        object Real y;

        a.Remove (0, y);
        result = x * Horner_Recursive_Evaluation (a, x) + y;
        a.Add (0, y);
        return result;
    }
}

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

program_body main ()
{
    object Character_IStream input;
    object Character_OStream output;
    object Polynomial_Coefficients a;
    object Real x, evaluation;
    object Integer k, elapsed_time;
    object Timer_1 t;

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

    // Read number of coefficients, coefficients a, and point x

    Read_Polynomial_And_X (input, a, x);
    
    // Print polynomial, evaluate it, and report timing for each
    // evaluation method

    // ---- Original method ----

    output << "Original method:\n";
    Write_Polynomial (output, a);
    k = 0;
    t.Restart ();
    while (k < 1000)
    {
        evaluation = Original_Evaluation (a, x);
        k++;
    }
    elapsed_time = t.Reading ();
    output << "p(" << x << ") = " << evaluation << "\n"
           << "execution time = " << elapsed_time
           << " usec\n\n";

    // ---- Horner's rule, done iteratively ----

    output << "Horner's rule (iterative):\n";
    Write_Polynomial (output, a);
    k = 0;
    t.Restart ();
    while (k < 1000)
    {
        evaluation = Horner_Iterative_Evaluation (a, x);
        k++;
    }
    elapsed_time = t.Reading ();
    output << "p(" << x << ") = " << evaluation << "\n"
           << "execution time = " << elapsed_time
           << " usec\n\n";

    // ---- Horner's rule, done recursively ----

    output << "Horner's rule (recursive):\n";
    Write_Polynomial (output, a);
    k = 0;
    t.Restart ();
    while (k < 1000)
    {
        evaluation = Horner_Recursive_Evaluation (a, x);
        k++;
    }
    elapsed_time = t.Reading ();
    output << "p(" << x << ") = " << evaluation << "\n"
           << "execution time = " << elapsed_time
           << " usec\n\n";

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