% -----------------------------------------------------------------------------
%  (C) Altran Praxis Limited
% -----------------------------------------------------------------------------
% 
%  The SPARK toolset is free software; you can redistribute it and/or modify it
%  under terms of the GNU General Public License as published by the Free
%  Software Foundation; either version 3, or (at your option) any later
%  version. The SPARK toolset is distributed in the hope that it will be
%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
%  Public License for more details. You should have received a copy of the GNU
%  General Public License distributed with the SPARK toolset; see file
%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
%  the license.
% 
% =============================================================================

%###############################################################################
% PURPOSE
%-------------------------------------------------------------------------------
% Loads the provenance for this proof problem. This key
% information is embedded into the main proof file.
%###############################################################################

%###############################################################################
% MODULE
%###############################################################################
:- module(load__provenance, [load_provenance/0]).

%###############################################################################
% DEPENDENCIES
%###############################################################################

:- use_module('data__provenance.pro',
              [get_provenance_framework/1,
               add_provenance_banner/1,
               add_provenance_date_time/2,
               add_provenance_framework/1,
               add_provenance_proof_file_kind/1,
               add_provenance_subprogram_identifier/1]).

:- use_module('ioutilities.pro',
              [throw_error/2,
               read_lines_from_file_as_char_list/3]).

:- use_module('newutilities.pro',
              [implode_separator_content_list/3]).

:- use_module('simplifier_ioutilities.pro',
              [retrieve_proof_file/1,
               convert_file_for_display/2,
               retrieve_proof_file_kind/1]).

:- use_module('parseutilities.pro',
              [parse_atom/5,
               parse_atom_silent/4,
               parse_line/3,
               parse_char_sep_atom_list/6,
               parse_all_to_nothing/2,
               parse_nothing_to_all/2]).

:- use_module('data__data_files.pro',
              [get_datafiles_vcg/1,
               get_datafiles_pfs/1]).

%###############################################################################
% TYPES
%###############################################################################

%###############################################################################
% DATA
%###############################################################################

%###############################################################################
% PREDICATES
%###############################################################################


:- set_prolog_flag(double_quotes, chars).


%===============================================================================
% load_provenance.
%-------------------------------------------------------------------------------
% The provided proof file is investigated to establish the required provenance
% information as described below.
%
% The kind of proof file is determined from which data files are available.
% vcg data files => verification_conditions
% pfs data files => path_functions
%
% Only the first 15 lines of the proof file are queried. This should, very
% comfortably, enclose every banner ever generated for processing by the
% Simplifier.
%
% The banner of the proof file must take the form:
%  1st line of the file contains: <space>*<stars><space>*
%  2ed line of the file contains: anything.
%  3rd line of the file contains: anything.
%  4th line of the file contains: anything.
%  5th line of the file contains: <space>*<stars><space>*
%
% An error is raised if the banner is not present.
%
% An error is raised if the 1st line and 5th line of a present banner do not
% exactly match.
%
% If the third line of the banner contains the word "Examiner" then the Simplifier
% will operate in SPARK mode. Otherwise, the Simplifier will operate in
% pascal mode. If the Simplifier is operating in pascal mode, a message will
% be issued to that effect. (pascal mode is unusual - we don't want our
% users to enter this mode accidentally).
%
% The remaining portion of the 15 lines are scanned for the following
% components. These components may occur in any order.
%
% +A subprogram identifier must be present in the format below:
% procedure P.Read
% function Q.Read3.SafeRead
% procedure PumpSwitch.PumpSwitchPT.OnInterruptHandler
% task_type U_C.TT
%
% No subprogram identifier will lead to an error being raised.
% A duplicate subprogram identifier will lead to an error being raised.
%
% NOTE: If operating in Pascal mode, the absence of a subprogram identifier
% is not treated as an error.
%
% +A date may or may not be present in the file in the format below:
%                     DATE :  7-JUN-1999 TIME : 15:41:20.73
%                       DATE : 12-APR-2006 15:37:05.57
%
% A duplicate date will raise an error.
%
% Note that any other text in the remaining portion of the 15 lines will be
% silently ignored.
%===============================================================================

load_provenance:-

    % Detect and record the proof file kind.
    retrieve_proof_file_kind(ProofFileKind),
    add_provenance_proof_file_kind(ProofFileKind),

    % Retrieve the relevant proof file.
    retrieve_proof_file(File_Atom),

    % Retrieve the head of the file as (at most) 15 lines.
    read_lines_from_file_as_char_list(File_Atom, upToLine(15), CharList),

    % Process the provenance.
    process_provenance(CharList),
    !.

%===============================================================================
% process_provenance(+Stream).
%-------------------------------------------------------------------------------
% The proof file provided as (Stream) is parsed to establish the required
% provenance information.
%===============================================================================

process_provenance(CharList):-

    % Process the banner.
    process_banner(CharList, Remaining_CharList),

    % Process the subprogram identifier.
    process_subprogram_identifier(Remaining_CharList),

    % Process datestamp, if present.
    process_datestamp(Remaining_CharList),
    !.

%===============================================================================
% process_banner(+CharList, -Remaining_CharList).
%-------------------------------------------------------------------------------
% Retrieve and store the banner as provenance information, returning the remaining
% characters. Raise errors accordingly.
%===============================================================================

% Make this call visible to the spxref tool.
:- public parse_banner/3.

process_banner(CharList, Remaining_CharList):-
    % Get the banner.
    phrase(parse_banner([FirstAsteriskLine_Atom,
                         SecondLine_Atom,
                         ThirdLine_Atom,
                         FourthLine_Atom,
                         LastAsteriskLine_Atom]), CharList, Remaining_CharList),

    % Check that the asterisk lines match.
    matching_asterisk_lines(FirstAsteriskLine_Atom, LastAsteriskLine_Atom),

    % Store the well-formed banner. Do not store the asterisk lines.
    add_provenance_banner([SecondLine_Atom,
                           ThirdLine_Atom,
                           FourthLine_Atom]),

    % Determine framework from third line of banner.
    scan_for_framework(ThirdLine_Atom),
    !.

% From above, banner could not be parsed. File is malformed.
process_banner(_CharList, _Remaining_CharList):-
    retrieve_proof_file(File_Atom),
    convert_file_for_display(File_Atom, DisplayFile_Atom),
    throw_error('Malformed banner in file: ~a.', [DisplayFile_Atom]).

%-------------------------------------------------------------------------------

parse_banner([FirstAsteriskLine_Atom,
              SecondLine_Atom,
              ThirdLine_Atom,
              FourthLine_Atom,
              LastAsteriskLine_Atom]) -->
    % 1st line must contain an asterisk line.
    parse_asterisk_banner_line(FirstAsteriskLine_Atom),

    % 2ed line may contain anything.
    parse_line(SecondLine_Atom),
    % 3rd line may contain anything.
    parse_line(ThirdLine_Atom),
    % 4th line may contain anything.
    parse_line(FourthLine_Atom),
    % 5th line must contain an asterisk line.
    parse_asterisk_banner_line(LastAsteriskLine_Atom),
    !.

%-------------------------------------------------------------------------------

parse_asterisk_banner_line(AsteriskLine_Atom) -->
    parse_atom([space], zeroormore, LeadingWhiteSpace_Atom),
    parse_atom([asterisk], oneormore, Asterisks_Atom),
    parse_atom([space], zeroormore, ClosingWhiteSpace_Atom),
    parse_atom_silent([newline], one),
    {implode_separator_content_list('',
                                   [LeadingWhiteSpace_Atom,
                                    Asterisks_Atom,
                                    ClosingWhiteSpace_Atom],
                                    AsteriskLine_Atom)},
    !.

%-------------------------------------------------------------------------------

% Asterisk lines match.
matching_asterisk_lines(FirstAsteriskLine_m_LastAsteriskLine_m_Atom,
                        FirstAsteriskLine_m_LastAsteriskLine_m_Atom):-
    !.

% From above, asterisk lines do not match.
matching_asterisk_lines(_FirstAsteriskLine_Atom, _LastAsteriskLine_Atom):-
    retrieve_proof_file(File_Atom),
    convert_file_for_display(File_Atom, DisplayFile_Atom),
    throw_error('Malformed banner in file: ~a. The bounding asterisk lines are different.',
                [DisplayFile_Atom]).

%-------------------------------------------------------------------------------

scan_for_framework(ThirdLine_Atom):-
    atom_chars(ThirdLine_Atom, ThirdLine_CharList),
    scan_for_framework_x(ThirdLine_CharList),
    !.

%-------------------------------------------------------------------------------

% Make this call visible to the spxref tool.
:- public parse_spark_identifier/2.

% Search for SPARK identifier.
scan_for_framework_x(CharList):-
    phrase(parse_spark_identifier, CharList),
    add_provenance_framework(spark),
    !.

% From above, failed to find spark identifier. This is pascal.
scan_for_framework_x(_CharList):-
    add_provenance_framework(pascal),

    % SEPR:2307: Standardise warning and error messages.
    format('The Simplifier is operating in Pascal mode.\n', []),
    !.

%-------------------------------------------------------------------------------

parse_spark_identifier -->
    parse_nothing_to_all,
    "Examiner",
    parse_all_to_nothing,
    !.

%===============================================================================
% process_subprogram_identifier(+Remaining_CharList).
%-------------------------------------------------------------------------------
% Retrieve and store the subprogram identifier.
%===============================================================================

% Make this call visible to the spxref tool.
:- public parse_subprogram_identifier/3.

process_subprogram_identifier(Remaining_CharList):-
    phrase(parse_subprogram_identifier(SubprogramIdentifier_AtomList), Remaining_CharList),
    process_subprogram_identifier_x(SubprogramIdentifier_AtomList),
    !.

%-------------------------------------------------------------------------------

% One subprogram identifier located.
% This is the correct situation.
process_subprogram_identifier_x([SubprogramIdentifier_Atom]):-
    add_provenance_subprogram_identifier(SubprogramIdentifier_Atom),
    !.

% Zero subprogram identifiers located.
% Operating in Pascal mode.
% This is not an error.
process_subprogram_identifier_x([]):-
    get_provenance_framework(pascal),
    !.

% Zero subprogram identifiers located.
% This is an error.
process_subprogram_identifier_x([]):-
    retrieve_proof_file(File_Atom),
    convert_file_for_display(File_Atom, DisplayFile_Atom),
    throw_error('Failed to locate a subprogram identifier in: ~p',
                [DisplayFile_Atom]).

% From above, multiple subprogram identifiers located.
% This is an error.
process_subprogram_identifier_x(SubprogramIdentifier_AtomList):-
    retrieve_proof_file(File_Atom),
    convert_file_for_display(File_Atom, DisplayFile_Atom),
    throw_error('File: ~a contains multiple subprogram identifiers: ~p',
                [DisplayFile_Atom,
                 SubprogramIdentifier_AtomList]).

%-------------------------------------------------------------------------------

parse_subprogram_identifier([H_SubprogramIdentifier_Atom | T_SubprogramIdentifier_AtomList]) -->

    parse_atom_silent([space], zeroormore),

    parse_subprogram_kind(SubprogramKind_Atom),

    % Newline is allowed below, as it could occur in some siv
    % files. This is a consequence of applying the wrap utility over the
    % whole output file.
    parse_atom_silent([space, newline], oneormore),
    parse_char_sep_atom_list([alpha_numeric, under_score],
                             [],
                             '.',
                             DottedName_AtomList),
    {implode_separator_content_list('.',
                                   DottedName_AtomList,
                                    SubprogramLocation_Atom)},
    parse_atom_silent([space], zeroormore),
    parse_atom_silent([newline], one),

    % Create the subprogram identifier.
    {implode_separator_content_list('',
                                   [SubprogramKind_Atom,
                                    ' ',
                                    SubprogramLocation_Atom],
                                    H_SubprogramIdentifier_Atom)},

    % Continue.
    parse_subprogram_identifier(T_SubprogramIdentifier_AtomList),
    !.

% From above, could not parse a subprogram identifier on this line.
% Try the next line.
parse_subprogram_identifier(SubprogramIdentifier_AtomList) -->
    parse_line(_Line_Atom),
    !,
    parse_subprogram_identifier(SubprogramIdentifier_AtomList).

% From above, could not parse another line. Reached last last line.
parse_subprogram_identifier([]) -->
    !.

%-------------------------------------------------------------------------------

parse_subprogram_kind(procedure) -->
    "procedure",
    !.

parse_subprogram_kind(function) -->
    "function",
    !.

parse_subprogram_kind('task_type') -->
    "task_type",
    !.

%===============================================================================
% process_subprogram_identifier(+Remaining_CharList).
%-------------------------------------------------------------------------------
% Retrieve and store the datestamp, if present.
%===============================================================================

% Make this call visible to the spxref tool.
:- public parse_datestamp/3.

process_datestamp(Remaining_CharList):-
    phrase(parse_datestamp(DateStamp_Tuple2List), Remaining_CharList),
    process_datestamp_x(DateStamp_Tuple2List),
    !.

%-------------------------------------------------------------------------------

% One datestamp located.
% This is acceptable.
process_datestamp_x([(Date_Atom, Time_Atom)]):-
    add_provenance_date_time(Date_Atom, Time_Atom),
    !.

% Zero datestamps located.
% This is acceptable.
process_datestamp_x([]):-
    !.

% From above, multiple datestamps located.
% This is an error.
process_datestamp_x(DateStamp_Tuple2List):-
    retrieve_proof_file(File_Atom),
    convert_file_for_display(File_Atom, DisplayFile_Atom),
    throw_error('File: ~a contains multiple datestamps: ~k',
                [DisplayFile_Atom,
                 DateStamp_Tuple2List]).

%-------------------------------------------------------------------------------

parse_datestamp([(Date_Atom, Time_Atom) | T_DateStamp_Tuple2List]) -->
    parse_atom_silent([space], zeroormore),
    "DATE : ",
    parse_atom_silent([space], zeroormore),
    [Day1_Char, Day2_Char,
     '-',
     Month1_Char, Month2_Char, Month3_Char,
     '-',
     Year1_Char, Year2_Char, Year3_Char, Year4_Char],
    parse_time_leader,
    [Hour1_Char, Hour2_Char,
     ':',
     Min1_Char, Min2_Char,
     ':',
     Sec1_Char, Sec2_Char,
     '.',
     _HundSec1_Char, _HundSec2_Char],
    {atom_chars(Date_Atom, [Day1_Char, Day2_Char,
                           '-',
                           Month1_Char, Month2_Char, Month3_Char,
                           '-',
                           Year1_Char, Year2_Char, Year3_Char, Year4_Char])},
    {atom_chars(Time_Atom, [Hour1_Char, Hour2_Char,
                           ':',
                           Min1_Char, Min2_Char,
                           ':',
                           Sec1_Char, Sec2_Char])},

    % Continue.
    parse_datestamp(T_DateStamp_Tuple2List),
    !.

%-------------------------------------------------------------------------------

% From above, could not parse a datestamp on this line.
% Try the next line.
parse_datestamp(DateStamp_Tuple2List) -->
    parse_line(_Line_Atom),
    !,
    parse_datestamp(DateStamp_Tuple2List).

% From above, could not parse another line. Reached last last line.
parse_datestamp([]) -->
    !.

%-------------------------------------------------------------------------------

parse_time_leader -->
    " ".

parse_time_leader -->
    " TIME : ".


:- set_prolog_flag(double_quotes, codes).

%###############################################################################
% END-OF-FILE