% -----------------------------------------------------------------------------
%  (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
%-------------------------------------------------------------------------------
% Provides input and output utilities that are specific to the Simplifier.
%###############################################################################

%###############################################################################
% MODULE
%###############################################################################
:- module(simplifier_ioutilities, [display_header/1,
                                   display_help/1,
                                   display_banner/1,
                                   retrieve_declaration_file/1,
                                   retrieve_simplified_proof_file/1,
                                   retrieve_proof_file/1,
                                   retrieve_proof_file_kind/1,
                                   convert_file_for_display/2,
                                   convert_file_to_base_name/2]).


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

:- use_module('ioutilities.pro',
              [show_error/2,
               display_header_full/1,
               display_header_plain/1,
               throw_error/2]).

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

:- use_module('data__system.pro',
              [get_system_start_date_time/2]).

:- use_module('data__provenance.pro',
              [get_provenance_proof_file_kind/1,
               get_provenance_framework/1,
               get_provenance_banner/1,
               get_provenance_date_time/2,
               get_provenance_subprogram_identifier/1]).

:- use_module('data__switches.pro',
              [get_switch_plain/1,
               get_switch_deadpaths/1]).

:- use_module('../common/versioning/version.pro',
              [toolset_support_line1/1,
               toolset_support_line2/1,
               toolset_support_line3/1,
               toolset_support_line4/1]).

:- use_module('data__data_files.pro',
              [get_datafiles_vcg/1,
               get_datafiles_dpc/1,
               get_datafiles_pfs/1,
               get_datafiles_fdl/1,
               get_datafiles_dec/1,
               get_datafiles_simplified_pfs/1,
               get_datafiles_simplified_vcg/1,
               get_datafiles_summary_dpc/1]).

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

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

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

%===============================================================================
% display_header(+Stream).
%-------------------------------------------------------------------------------
% Display the header for the Simplifier. For correct processing, the
% command line arguments must have already been processed.
%===============================================================================

% Is not in plain mode.
display_header(Stream):-
    get_switch_plain(off),
    display_header_full(Stream),
    !.

% Is in plain mode.
display_header(Stream):-
    get_switch_plain(on),
    display_header_plain(Stream),
    !.

%None of the above is an error.
display_header(_Stream):-
    show_error('Could not calculate banner. Unexpected system configuration.', []).

%===============================================================================
% display_help(Stream).
%-------------------------------------------------------------------------------
% Display help text.
%===============================================================================

% Help for Simplifier
display_help(Stream):-
    get_switch_deadpaths(off),
    !,
    display_header(Stream),

    % Get common support information.
    toolset_support_line1(SupportLine1_Atom),
    toolset_support_line2(SupportLine2_Atom),
    toolset_support_line3(SupportLine3_Atom),
    toolset_support_line4(SupportLine4_Atom),

    format(Stream, '~n',[]),
    format(Stream, 'Usage: spadesimp [options] Target_File~n', []),
    format(Stream, '~n', []),
    format(Stream, 'Target_File - Either a .vcg or .pfs file~n', []),
    format(Stream, '~n', []),
    format(Stream, 'All options may be abbreviated to the shortest unique prefix.~n', []),
    format(Stream, '~n', []),
    format(Stream, 'Standard options~n', []),
    format(Stream, '----------------~n', []),
    format(Stream, '-help               - Display this help information.~n', []),
    format(Stream, '-version            - Display version information.~n', []),
    format(Stream, '-nolog              - Do not generate a simplification log file.~n', []),
    format(Stream, '-log=Log_File       - Specify filename for the simplification log file.~n', []),
    format(Stream, '-nowrap             - Do not line wrap output files.~n', []),
    format(Stream, '-verbose            - Display attempted simplification strategies.~n', []),
    format(Stream, '-nouserrules        - Do not use user rules.~n', []),
    format(Stream, '-plain              - Adopt a plain output style (e.g. no dates or version numbers).~n', []),
    format(Stream, '-typecheck          - Only typecheck the input files.~n', []),
    format(Stream, '-norenum            - Do not renumber hypotheses and conclusions in siv files.~n', []),

    format(Stream, '~n', []),
    format(Stream, 'Adjust strategy options~n', []),
    format(Stream, '-----------------------~n', []),
    format(Stream, '-nosimplification=SELECT~n', []),
    format(Stream, '-nostandardisation=SELECT~n', []),
    format(Stream, '-norule_substitution=SELECT~n', []),
    format(Stream, '-nocontradiction_hunt=SELECT~n', []),
    format(Stream, '-nosubstitution_elimination=SELECT~n', []),
    format(Stream, '-noexpression_reduction=SELECT~n', []),
    format(Stream, 'SELECT=(RANGE {, RANGE})~n', []),
    format(Stream, 'RANGE=Vc_Number or From_Vc_Number-To_Vc_Number~n', []),
    format(Stream, '~n', []),
    format(Stream, 'Adjust limit options~n', []),
    format(Stream, '--------------------~n', []),
    format(Stream, '-complexity_limit=Limit (Limit in range 10 .. 200)~n', []),
    format(Stream, '-depth_limit=Limit      (Limit in range  1 ..  10)~n', []),
    format(Stream, '-inference_limit=Limit  (Limit in range 10 .. 400)~n', []),
    format(Stream, '~n', []),
    format(Stream, '~a~n', [SupportLine1_Atom]),
    format(Stream, '~a~n', [SupportLine2_Atom]),
    format(Stream, '~a~n', [SupportLine3_Atom]),
    format(Stream, '~a~n', [SupportLine4_Atom]),
    !.
 
% Help for ZombieScope
display_help(Stream):-
    get_switch_deadpaths(on),
    !,
    display_header(Stream),

    % Get common support information.
    toolset_support_line1(SupportLine1_Atom),
    toolset_support_line2(SupportLine2_Atom),
    toolset_support_line3(SupportLine3_Atom),
    toolset_support_line4(SupportLine4_Atom),

    format(Stream, '~n',[]),
    format(Stream, 'Usage: zombiescope [options] Target_File~n', []),
    format(Stream, '~n', []),
    format(Stream, 'Target_File - a .dpc file~n', []),
    format(Stream, '~n', []),
    format(Stream, 'All options may be abbreviated to the shortest unique prefix.~n', []),
    format(Stream, '~n', []),
    format(Stream, 'Standard options~n', []),
    format(Stream, '----------------~n', []),
    format(Stream, '-help             - Display this help information.~n', []),
    format(Stream, '-version          - Display version information.~n', []),
    format(Stream, '-nolog            - Do not generate a ZombieScope log file.~n', []),
    format(Stream, '-log=Log_File     - Specify filename for the ZombieScope log file.~n', []),
    format(Stream, '-nowrap           - Do not line wrap output files.~n', []),
    format(Stream, '-plain            - Adopt a plain output style (e.g. no dates or version numbers).~n', []),
    format(Stream, '-norenum          - Do not renumber hypotheses and conclusions in sdp files.~n', []),
    format(Stream, '-hyp_limit=Limit  - Specify the maximum number of hypotheses that will be analysed.~n', []),

    format(Stream, '~n', []),
    format(Stream, '~a~n', [SupportLine1_Atom]),
    format(Stream, '~a~n', [SupportLine2_Atom]),
    format(Stream, '~a~n', [SupportLine3_Atom]),
    format(Stream, '~a~n', [SupportLine4_Atom]),
    !.
 
%===============================================================================
% display_banner(Stream).
%-------------------------------------------------------------------------------
% Display the banner for the Simplifier output. The banner is affected by
% the previously collected system and provenance information.
%===============================================================================

display_banner(Stream):-

    %Leading stars for banner.
    format(Stream, '*****************************************************************************~n', []),

    %Retrive and write out the leading banner.
    get_provenance_banner(Line_AtomList),
    implode_separator_content_list('\n',
                                   Line_AtomList,
                                   Line_Atom),
    format(Stream, Line_Atom, []),
    format(Stream, '~n', []),

    %Closing stars for banner.
    format(Stream, '*****************************************************************************~n', []),

    %Display some spaces.
    format(Stream, '~n', []),
    format(Stream, '~n', []),

    % Note that POGS expects the date and time details, if present, to
    % appear before the subprogram name.

    %Consider displaying time details.
    display_time_details(Stream),

    %Embed the standard header into the file.
    format(Stream, '\n', []),
    display_header(Stream),
    format(Stream, '\n', []),

    %Display subprogram identifier.
    display_subprogram_identifier(Stream),

    %Display some spaces.
    format(Stream, '\n', []),
    format(Stream, '\n', []),
    format(Stream, '\n', []),
    format(Stream, '\n', []),
    !.

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

% Is in plain mode.
display_time_details(_Stream):-
    get_switch_plain(on),
    !.

% Is not in plain mode.
% But did not retrieve a date time from the provenance file.

display_time_details(_Stream):-
    get_switch_plain(off),
    \+ get_provenance_date_time(_Date_Atom, _Time_Atom),
    !.




display_time_details(Stream):-
    get_switch_plain(off),
    get_provenance_date_time(Date_Atom, Time_Atom),

    % Note POGS collects both the CREATED and SIMPLIFIED dates, and expects
    % the following format.
    %
    % Once all trailing and leading space has been deleted:
    %
    % The CREATED date must start on column: 9, and be 11 chars wide.
    % The CREATED time must start on column: 22, and be 8 chars wide.
    %
    % The SIMPLIFIED date must start on column: 43, and be 11 chars wide.
    % The SIMPLIFIED time must start on column: 56, and be 8 chars wide.
    %
    % The date format is like: 09-JAN-1980
    % The time format is like: 01:59:01
    %
    % Currently POGS compares the text of the CREATED date and time with
    % relevant portions from the VCG file. The SIMPLIFIED date and time is
    % semantically compared against the date embedded into the PLG file.


    get_system_start_date_time(NowDate_Atom, NowTime_Atom),
    display_time_details_x(Stream, Date_Atom, Time_Atom, NowDate_Atom, NowTime_Atom),
    !.

%None of the above is an error.
display_time_details(_Stream):-
    show_error('Could not determine date and time details for the simplified file banner.', []).

display_time_details_x(Stream, Date_Atom, Time_Atom, NowDate_Atom, NowTime_Atom):-
    get_switch_deadpaths(off),
    format(Stream, 'CREATED ~a, ~a  SIMPLIFIED ~a, ~a\n',
           [Date_Atom, Time_Atom, NowDate_Atom, NowTime_Atom]).

display_time_details_x(Stream, Date_Atom, Time_Atom, NowDate_Atom, NowTime_Atom):-
    get_switch_deadpaths(on),
    format(Stream, 'CREATED ~a, ~a  ZombieScope ~a, ~a\n',
           [Date_Atom, Time_Atom, NowDate_Atom, NowTime_Atom]).

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

% The subprogram identifier is displayed in all modes.
display_subprogram_identifier(Stream):-
    get_provenance_subprogram_identifier(SubprogramIdentifier_Atom),
    format(Stream, '~a\n', [SubprogramIdentifier_Atom]),
    !.

% If in pascal mode, it is acceptable to have no subprogram identifier. In
% this case a blank line is written out.
display_subprogram_identifier(Stream):-
    get_provenance_framework(pascal),
    format(Stream, '\n', []),
    !.

% From above, expected subprogram identifier is not present.
display_subprogram_identifier(_Stream):-
    show_error('Expected subprogram identifier is not present.\n', []).

%===============================================================================
% retrieve_proof_file(-ProofFile_Atom).
%-------------------------------------------------------------------------------
% Return the overloaded proof file name (either .vcg or .pfs). Raise an
% error if this can not be done.
%===============================================================================

retrieve_proof_file(ProofFile_Atom):-
    get_provenance_proof_file_kind(ProofFileKind),
    retrieve_proof_file_x(ProofFileKind, ProofFile_Atom),
    !.

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

retrieve_proof_file_x(verification_conditions, VcgFile_Atom):-
    get_datafiles_vcg(VcgFile_Atom),
    !.

retrieve_proof_file_x(deadpath_search, DpcFile_Atom):-
    get_datafiles_dpc(DpcFile_Atom),
    !.

% DELETE_PATH_FUNCTIONS
retrieve_proof_file_x(path_functions, PfsFile_Atom):-
    get_datafiles_pfs(PfsFile_Atom),
    !.


retrieve_proof_file_x(ProofFileKind, _File_Atom):-
    throw_error('Unable to retrieve proof file for proof file kind: ~k',
                [ProofFileKind]).

%===============================================================================
% retrieve_simplified_proof_file(-SimplifiedProofFile_Atom).
%-------------------------------------------------------------------------------
% Return the overloaded simplified proof file name (either .siv, .sdp or .sip).
% Raise an error if this can not be done.
%===============================================================================

retrieve_simplified_proof_file(SimplifiedProofFile_Atom):-
    get_provenance_proof_file_kind(ProofFileKind),
    retrieve_simplified_proof_file_x(ProofFileKind, SimplifiedProofFile_Atom),
    !.

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

retrieve_simplified_proof_file_x(verification_conditions, SimplifiedVcgFile_Atom):-
    get_datafiles_simplified_vcg(SimplifiedVcgFile_Atom),
    !.

retrieve_simplified_proof_file_x(deadpath_search, SummaryDeadpathFile_Atom):-
    get_datafiles_summary_dpc(SummaryDeadpathFile_Atom),
    !.


retrieve_simplified_proof_file_x(path_functions, SimplifiedPfsFile_Atom):-
    get_datafiles_simplified_pfs(SimplifiedPfsFile_Atom),
    !.


retrieve_simplified_proof_file_x(ProofFileKind, _File_Atom):-
    throw_error('Unable to retrieve simplified proof file for proof file kind: ~k',
                [ProofFileKind]).

%===============================================================================
% retrieve_declaration_file(-DeclarationFile_Atom).
%-------------------------------------------------------------------------------
% Return the overloaded proof declaration file name (either .fdl or .dec).
% Raise an error if this can not be done.
%===============================================================================

retrieve_declaration_file(DeclarationFile_Atom):-
    get_provenance_proof_file_kind(ProofFileKind),
    retrieve_declaration_file_x(ProofFileKind, DeclarationFile_Atom),
    !.

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

retrieve_declaration_file_x(verification_conditions, FdlFile_Atom):-
    get_datafiles_fdl(FdlFile_Atom),
    !.

retrieve_declaration_file_x(deadpath_search, FdlFile_Atom):-
    get_datafiles_fdl(FdlFile_Atom),
    !.



retrieve_declaration_file_x(path_functions, DecFile_Atom):-
    get_datafiles_dec(DecFile_Atom),
    !.



retrieve_declaration_file_x(ProofFileKind, _File_Atom):-
    throw_error('Unable to retrieve declaration file for proof file kind: ~k',
                [ProofFileKind]).

%===============================================================================
% retrieve_proof_file_kind(-ProofFileKind).
%-------------------------------------------------------------------------------
% Based on which main proof file is available, return the proof file kind.
%===============================================================================



% If both main proof files are available, then raise an error.

retrieve_proof_file_kind(_ProofFileKind):-
    get_datafiles_vcg(VcgFile_Atom),
    convert_file_for_display(VcgFile_Atom, DisplayVcgFile_Atom),
    get_datafiles_pfs(PfsFile_Atom),
    convert_file_for_display(PfsFile_Atom, DisplayPfsFile_Atom),
    throw_error('Unexpected availability of two distinct proof files: ~a and ~a',
                [DisplayVcgFile_Atom, DisplayPfsFile_Atom]).



% If dead path is off then proof kind is verification conditions.
retrieve_proof_file_kind(verification_conditions):-
    get_switch_deadpaths(off),
    get_datafiles_vcg(_VcgFile_Atom),
    !.

% If dead path is on then proof kind is searching for dead paths.
retrieve_proof_file_kind(deadpath_search):-
    get_switch_deadpaths(on),
    get_datafiles_dpc(_DpcFile_Atom),
    !.

% Error if neither vcg or dpc files have been loaded.
retrieve_proof_file_kind(_ProofFileKind):-
 get_switch_deadpaths(off),
    throw_error('Unexpected no vcg files loaded',
                []).

% Could not locate dpc file for dead path search.
retrieve_proof_file_kind(_ProofFileKind):-
    get_switch_deadpaths(on),
    throw_error('Unexpected no dpc files loaded',
                []).


% If pfs is available then is path_functions.
retrieve_proof_file_kind(path_functions):-
    get_datafiles_pfs(_PfsFile_Atom),
    !.

% If neither are available then raise an error.
retrieve_proof_file_kind(_ProofFileKind):-
    throw_error('Unexpected no proof files available',
                []).



%===============================================================================
% convert_file_for_display(+File_Atom, -DisplayFile_Atom).
%-------------------------------------------------------------------------------
% Plain mode exists to minimise differences across platforms. This extends
% to the portrayal of files. This routine converts an internal file
% (File_Atom) into an appropriate form for display (DisplayFile_Atom).
%===============================================================================

% Is not in plain mode.
% Display the whole file.
convert_file_for_display(File_m_DisplayFile_m_Atom, File_m_DisplayFile_m_Atom):-
    get_switch_plain(off),
    !.




% Is in plain mode.
% Strip off the directory part.
convert_file_for_display(File_Atom, DisplayFile_Atom):-
    get_switch_plain(on),
    convert_file_to_base_name(File_Atom, DisplayFile_Atom),
    !.

convert_file_for_display(File_Atom, _DisplayFile_Atom):-
    throw_error('Error in converting file ~k for display',
                [File_Atom]).

%===============================================================================
% convert_file_to_base_name(+File_Atom, -BaseName_Atom).
%-------------------------------------------------------------------------------
% Given a file (File_Atom), strip off its directory part and return the
% reminder as (BaseName_Atom).
%===============================================================================

convert_file_to_base_name(File_Atom, DisplayFile_Atom):-

    %Retrieve the directory parts and file part.
    explode_separator_content_as_list('/',
                                      File_Atom,
                                      Item_AtomList),

    %The last part is the file part.
    append(_Directory_AtomList, [DisplayFile_Atom], Item_AtomList),
    !.

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