% -----------------------------------------------------------------------------
%  (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 all verification conditions from the provided input file.
%###############################################################################

%###############################################################################
% MODULE
%###############################################################################
:- module(load__vcg_dpc, [load_vcg/0,
                          load_dpc/0,
                          retrieve_next_vcg/0]).

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

:- use_module('data__formats.pro',
              [add_state/2,
               add_type/2]).

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

:- use_module('data__vcg.pro',
              [add_vcg_file_handle/1,
               get_vcg_file_handle/1,
               add_vcg_conclusion/3,
               add_vcg_hypothesis/3,
               add_vcg_trace/2,
               add_vcg_vc/5,
               get_vcg_vc/5,
               add_zombiescope_no_check_required/1,
               get_zombiescope_no_check_required/1,
               prune_vcg_file_handle/0,
               prune_all_vcg_vc/0,
               prune_all_vcg_hypothesis/0,
               prune_all_vcg_conclusion/0,
               prune_all_zombiescope_no_check_required/0]).

:- use_module('ioutilities.pro',
              [read_line_from_stream/2,
               read_up_to_number_of_chars_from_stream/3,
               show_error/2]).

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

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

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

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

:- add_type('ParseStatus',
            [end_of_file,
             notfinished,
             finished]).

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

% Traceability lines are placed before a collection of VCs. As each VC is
% processed, it is correctly associated with the last traceability line
% encountered via this state.
:- add_state(get_last_trace_id,
             get_last_trace_id('TraceId_Atom')).
:- dynamic(get_last_trace_id/1).

:- add_state(get_order,
             get_order('Int')).
:- dynamic(get_order/1).

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


:- set_prolog_flag(double_quotes, chars).

%===============================================================================
% load_vcg.
%-------------------------------------------------------------------------------
% Initialise for loading the vcs.
%===============================================================================




load_vcg:-
    get_datafiles_vcg(VcgFile_Atom),
    open(VcgFile_Atom, read, Stream),
    add_vcg_file_handle(Stream),

    % Initialise the internal ordering.
    initialise_order,
    !.

% Loading of dpc files is identical to loading vcgs.
% It is assumed that all VCs contain a single "false" conclusion.

load_dpc:-
    get_datafiles_dpc(DpcFile_Atom),
    open(DpcFile_Atom, read, Stream),
    add_vcg_file_handle(Stream),

    % Initialise the internal ordering.
    initialise_order,
    !.

%===============================================================================
% retrieve_next_vcg.
%-------------------------------------------------------------------------------
% Replace any currently loaded VC with the next VC from the file. If no
% more VCs remain, then the predicate fails, and no VC data is stored.
%===============================================================================

retrieve_next_vcg:-
    % Clear any previous VC information.
    clear_previous_vcg,

    % Get the next VC, if available. Fail otherwise.
    retrieve_next_vcg_x,
    !.

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

retrieve_next_vcg_x:-
    % If file handle is not present, have parsed whole file.
    get_vcg_file_handle(Stream),

    % If there is no next vc, have simplified all vcs.
    load_up_to_next_vc_start(Stream),

    % Collect the attributes of this vc.
    process_single_verification_condition(Stream),
    !.

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

clear_previous_vcg:-
    prune_all_vcg_vc,
    prune_all_vcg_hypothesis,
    prune_all_vcg_conclusion,
    prune_all_zombiescope_no_check_required,
    !.

%===============================================================================
% load_up_to_next_vc_start(+VcgFile_Stream).
%-------------------------------------------------------------------------------
% Retrieve information from verification condition file stream, up to and
% including the next VC start line.
%===============================================================================

load_up_to_next_vc_start(VcgFile_Stream):-
    repeat,
    read_line_from_stream(VcgFile_Stream, ReadText),
    process_verification_conditions_line(ReadText),
    load_up_to_next_vc_start_x(ReadText),
    !.

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

% Do nothing at end of file.
process_verification_conditions_line(end_of_file):-
    !.

% Check for traceability line.
process_verification_conditions_line(CharList):-
    scan_for_traceability(CharList),
    !.

% Check for vc.
process_verification_conditions_line(CharList):-
    scan_for_vc_header(CharList, Name_Atom, Number_Int),

    % Record this vc, associating with last found trace.
    retrieve_and_increment_order(Order_Int),
    unique_atom('vc', VCId_Atom),
    must_get_last_trace_id(TraceId_Atom),
    add_vcg_vc(VCId_Atom, Order_Int, Name_Atom, Number_Int, TraceId_Atom),
    !.

% From above, nothing found at this line.
process_verification_conditions_line(_CharList):-
    !.

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

%Reached start of a VC. Done.
load_up_to_next_vc_start_x(_ReadText):-
    get_vcg_vc(_VCId_Atom, _Order_Int, _Name_Atom, _Number_Int, _TraceId_Atom),
    !.

%Reached end of file. No more VCs to process.
load_up_to_next_vc_start_x(end_of_file):-
    % Close the input stream.
    get_vcg_file_handle(VcgFile_Stream),
    close(VcgFile_Stream),

    % Remove the closed input stream.
    prune_vcg_file_handle,
    !.

%===============================================================================
% process_single_verification_condition(+Stream, +ParentVCId_Atom).
%-------------------------------------------------------------------------------
% Retrieve a single VC from the verification condition file stream. Is is
% expected that on entry the file stream is just after the VC header line.
%===============================================================================

process_single_verification_condition(Stream):-
    % Get the VC id.
    get_vcg_vc(ParentVCId_Atom, _Order_Int, _Name_Atom, _Number_Int, _TraceId_Atom),
    
    repeat,
    read_up_to_number_of_chars_from_stream(Stream, 6, ReadText),
    process_single_verification_condition_leader(Stream, ReadText, ParentVCId_Atom, ParseStatus),
    process_single_verification_condition_x(ParseStatus),
    !.

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

% At end_of_file only report end_of_file.
process_single_verification_condition_leader(_Stream, end_of_file, _ParentVCId_Atom, end_of_file):-
    !.

% Search for finished line.
process_single_verification_condition_leader(_Stream, CharList, _ParentVCId_Atom, finished):-
    scan_for_end_of_vc(CharList),
    !.

% Search for vc that has been fully proved true.
process_single_verification_condition_leader(Stream, CharList, ParentVCId_Atom, finished):-
    scan_for_proved_true_vc(Stream, CharList, ParentVCId_Atom),
    !.

% Search for vc that has been fully proved false.
process_single_verification_condition_leader(Stream, CharList, ParentVCId_Atom, finished):-
    scan_for_proved_false_vc(Stream, CharList, ParentVCId_Atom),
    !.

% Search for vc hypothesis.
process_single_verification_condition_leader(Stream, CharList, ParentVCId_Atom, notfinished):-
    scan_for_vc_hypothesis(Stream, CharList, ParentVCId_Atom),
    !.

% Search for vc conclusion.
process_single_verification_condition_leader(Stream, CharList, ParentVCId_Atom, notfinished):-
    scan_for_vc_conclusion(Stream, CharList, ParentVCId_Atom),
    !.

% Search for implication between hypotheses and conclusions.
process_single_verification_condition_leader(Stream, CharList, _ParentVCId_Atom, notfinished):-
    scan_for_vc_implication(Stream, CharList),
    !.

% None of the above is an error.
process_single_verification_condition_leader(_Stream, CharList, _ParentVCId_Atom, _ParseStatus):-
    show_error('Badly formed line in processing verification condition, starting: ~p\n', [CharList]).

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

% Is finished.
process_single_verification_condition_x(finished):-
    !.

% Not finished. Fail and look at more lines.
process_single_verification_condition_x(notfinished):-
    fail.

% Error if at end of file.
process_single_verification_condition_x(end_of_file):-
    show_error('Unexpected end of file in parsing vcg file.\n', []).

%===============================================================================
% scan_for_end_of_vc(CharList).
%-------------------------------------------------------------------------------
% Successful where the end of a vc is detected.
%===============================================================================

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

scan_for_end_of_vc(CharList):-
    phrase(parse_end_of_vc(_Form), CharList),
    !.

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

% space newline
parse_end_of_vc(normal)-->
    " ",
    !.

% newline
parse_end_of_vc(special)-->
    !.

%===============================================================================
% scan_for_proved_true_vc(Stream, +CharList, +ParentVCId_Atom).
%-------------------------------------------------------------------------------
% Successful where a condensed true VC vc is detected. The VC details are
% added accordingly.
%===============================================================================

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

scan_for_proved_true_vc(Stream, CharList, ParentVCId_Atom):-
    phrase(parse_proved_true_vc, CharList),

    % Consume the rest of the line from the input. There is an assumption
    % here that these true/false VCs will have more than six characters.
    % This is valid as per the examiner.
    read_line_from_stream(Stream, _ReadText),




    add_vcg_hypothesis(1, 'true', ParentVCId_Atom),
    scan_for_proved_true_vc_x(ParentVCId_Atom),
    !.

scan_for_proved_true_vc_x(ParentVCId_Atom):-
    get_switch_deadpaths(off),
    add_vcg_conclusion(1, 'true', ParentVCId_Atom),
    !.

% "Trivially true" VCs are DPCs that do not require ZombieScope
% to check for dead paths.
% ZombieScope model these VCs with a true hypothesis
% and a false conclusion - that is, it is not a dead path.
% Mark the DPC so that ZombieScope does not look for dead paths for this VC.
scan_for_proved_true_vc_x(ParentVCId_Atom):-
    get_switch_deadpaths(on),
    add_vcg_conclusion(1, 'false', ParentVCId_Atom),
    add_zombiescope_no_check_required(ParentVCId_Atom),
    !.

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

% *** true .          /* trivially true VC removed by Examiner */
parse_proved_true_vc -->
    "*",
    parse_all_to_nothing,
    !.
%===============================================================================


%===============================================================================
% scan_for_proved_false_vc(+Stream, +CharList).
%-------------------------------------------------------------------------------
% Successful where a condensed false VC vc is detected. The VC details are
% added accordingly.
%===============================================================================

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

scan_for_proved_false_vc(Stream, CharList, ParentVCId_Atom):-
    phrase(parse_proved_false_vc, CharList),

    % Consume the rest of the line from the input. There is an assumption
    % here that these true/false VCs will have more than six characters.
    % This is valid as per the examiner.
    read_line_from_stream(Stream, _ReadText),

    % Display a warning.
    format('!!! WARNING: UNPROVEABLE VC!  Suggest you take corrective action.\n', []),

    % Insert a false vc.








    add_vcg_conclusion(1, 'false', ParentVCId_Atom),
    !.

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

% !!!   false. /* WARNING: formula is false */
parse_proved_false_vc -->
    "!",
    parse_all_to_nothing,
    !.

%===============================================================================
% scan_for_vc_hypothesis(+Stream, +CharList).
%-------------------------------------------------------------------------------
% Successful where a vc hypothesis is detected. The hypothesis is added to
% the VC details accordingly.
%===============================================================================

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

scan_for_vc_hypothesis(Stream, CharList, ParentVCId_Atom):-
    phrase(parse_vc_hypothesis(Number_Int), CharList),

    % Retrieve the term from the stream.
    read_term(Stream, Hyp_Term, []),

    add_vcg_hypothesis(Number_Int, Hyp_Term, ParentVCId_Atom),
    !.

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

parse_vc_hypothesis(Number_Int) -->
    "H",
    parse_natural_int(Number_Int),
    ":",
    parse_atom_silent([space, newline], zeroormore),
    !.

%===============================================================================
% scan_for_vc_conclusion(Stream, CharList, ParentVCId_Atom).
%-------------------------------------------------------------------------------
% Successful where a vc conclusion is detected. The conclusion is added to
% the VC details accordingly.
%===============================================================================

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

scan_for_vc_conclusion(Stream, CharList, ParentVCId_Atom):-
    phrase(parse_vc_conclusion(Number_Int), CharList),

    % Retrieve the term from the stream.
    read_term(Stream, Conc_Term, []),

    add_vcg_conclusion(Number_Int, Conc_Term, ParentVCId_Atom),
    !.

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

parse_vc_conclusion(Number_Int) -->
    "C",
    parse_natural_int(Number_Int),
    ":",
    parse_atom_silent([space, newline], zeroormore),
    !.

%===============================================================================
% scan_for_vc_implication(+Stream, +CharList).
%-------------------------------------------------------------------------------
% Successful where the VC implication divider is detected.
%===============================================================================

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

scan_for_vc_implication(Stream, CharList):-
    phrase(parse_vc_before_implication, CharList),

    % Retrieve the rest of the line, and check that the implication is as
    % expected.
    read_line_from_stream(Stream, ReadText),
    confirm_valid_implication(ReadText),
    !.

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

% With six spaces the implication should follow.
parse_vc_before_implication -->
  "      ",
    !.

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

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

confirm_valid_implication(end_of_file):-
    show_error('Unexpected end of file in parsing vcg file.\n', []).

confirm_valid_implication(CharList):-
    phrase(parse_vc_implication, CharList),
    !.

confirm_valid_implication(CharList):-
    show_error('Badly formed implication between hypotheses and conclusions: ~w\n', [CharList]).

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

parse_vc_implication -->
    parse_atom_silent([space, newline], zeroormore),
    "->",
    parse_atom_silent([space, newline], zeroormore),
    !.

%===============================================================================
% scan_for_traceability(CharList).
%-------------------------------------------------------------------------------
% Successful where a traceability line is parsed.
%===============================================================================

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

scan_for_traceability(CharList):-
    phrase(parse_traceability(VCTrace), CharList),
    unique_atom('trace', TraceId_Atom),
    add_vcg_trace(TraceId_Atom, VCTrace),
    replace_last_trace_id(TraceId_Atom),
    !.

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

% For path(s) from XXX to YYY:
parse_traceability(traverseCutpoints(VCCutpointFrom, VCCutpointTo)) -->
    "For path(s) from",
    parse_atom_silent([space, newline], oneormore),
    parse_cutpoint_from(VCCutpointFrom),
    parse_atom_silent([space, newline], oneormore),
    "to",
    parse_atom_silent([space, newline], oneormore),
    parse_cutpoint_to(VCCutpointTo),
    parse_atom_silent([space, newline], zeroormore),
    ":",
    !.

parse_traceability(checkRefinementIntegrity) -->
    "For checks of refinement integrity: ",
    !.


parse_traceability(subclassInheritanceIntegrity) -->
    "For checks of subclass inheritance integrity: ",
    !.



parse_traceability(fudge(Line)) -->
    "For",
    parse_atom([not(colon)], oneormore, Atom),
    ":",
    {implode_separator_content_list('',
                                    ['For', Atom, ':'],
                                    Line)},
    !.

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

% start
parse_cutpoint_from(start) -->
    "start",
    !.

% assertion of line NN
parse_cutpoint_from(assertion(userprovided, Line_Int)) -->
    "assertion of line",
    parse_atom_silent([space, newline], oneormore),
    parse_natural_int(Line_Int),
    !.

% default assertion of line NN
parse_cutpoint_from(assertion(default, Line_Int)) -->
    "default assertion of line",
    parse_atom_silent([space, newline], oneormore),
    parse_natural_int(Line_Int),
    !.

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

% finish
parse_cutpoint_to(finish) -->
    "finish",
    !.

% assertion of line NN
parse_cutpoint_to(assertion(userprovided, Line_Int)) -->
    "assertion of line",
    parse_atom_silent([space, newline], oneormore),
    parse_natural_int(Line_Int),
    !.

% default assertion of line NN
parse_cutpoint_to(assertion(default, Line_Int)) -->
    "default assertion of line",
    parse_atom_silent([space, newline], oneormore),
    parse_natural_int(Line_Int),
    !.

% check associated with statement of line NN
parse_cutpoint_to(check(userprovided, Line_Int)) -->
    "check associated with statement of line",
    parse_atom_silent([space, newline], oneormore),
    parse_natural_int(Line_Int),
    !.

% run-time check associated with statement of line NN
parse_cutpoint_to(check(runtime, Line_Int)) -->
    "run-time check associated with statement of line",
    parse_atom_silent([space, newline], oneormore),
    parse_natural_int(Line_Int),
    !.

% precondition check associated with statement of line NN
parse_cutpoint_to(check(precondition, Line_Int)) -->
    "precondition check associated with statement of line",
    parse_atom_silent([space, newline], oneormore),
    parse_natural_int(Line_Int),
    !.

%===============================================================================
% scan_for_vc_header(+CharList, -Name_Atom, -Number_Int).
%-------------------------------------------------------------------------------
% Successful where a vc header line is parsed.
%===============================================================================

% Make these calls visible to the spxref tool.
:- public load__vcg_dpc:parse_vc_header_name/3.
:- public load__vcg_dpc:parse_vc_header_number/3.

scan_for_vc_header(CharList, Name_Atom, Number_Int):-
    phrase(parse_vc_header_name(Name_Atom), CharList),
    phrase(parse_vc_header_number(Number_Int), CharList),
    !.

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

% procedure_constrain_42.
% Name_Atom is procedure_constrain_42
parse_vc_header_name(Name_Atom) -->
    parse_atom([alpha_numeric, under_score], oneormore, Name_Atom),
    ".",
    !.

% procedure_constrain_42.
% Number_Int is procedure_constrain_42
parse_vc_header_number(Number_Int) -->
    parse_nothing_to_all,
    parse_natural_int(Number_Int),
    ".",
    !.

%===============================================================================
% replace_last_trace_id(+TraceId_Atom).
%-------------------------------------------------------------------------------
% Allow updating of the last traceability id as a new traceability line is
% encountered.
%===============================================================================

% Replace existing trace.
replace_last_trace_id(TraceId_Atom):-
    retract(get_last_trace_id(_TraceId_Atom)),
    assert(get_last_trace_id(TraceId_Atom)),
    !.

% Set initial trace.
replace_last_trace_id(TraceId_Atom):-
    assert(get_last_trace_id(TraceId_Atom)),
    !.

%===============================================================================
% must_get_last_trace_id(+TraceId_Atom).
%-------------------------------------------------------------------------------
% Raise an error if a trace id is requested, but one has not yet been seen.
% This is likely a symptom of a malformed vcg file.
%===============================================================================

must_get_last_trace_id(TraceId_Atom):-
            get_last_trace_id(TraceId_Atom),
            !.

must_get_last_trace_id(_TraceId_Atom):-
    show_error('An expected traceability line has not been found.\n', []).

%===============================================================================
% initialise_order.
%-------------------------------------------------------------------------------
% Initialise the VC ordering information.
%===============================================================================






initialise_order:-
    retractall(get_order(_Int)),
    assert(get_order(1)),
    !.

%===============================================================================
% retrieve_and_increment_order(+Int).
%-------------------------------------------------------------------------------
% Access and update the order information.
%===============================================================================




retrieve_and_increment_order(Int):-
    retract(get_order(Int)),
    NextInt is Int+1,
    assert(get_order(NextInt)),
    !.


:- set_prolog_flag(double_quotes, codes).


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