% -----------------------------------------------------------------------------
%  (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
%-------------------------------------------------------------------------------
% Various legacy utility predicates. Where these are generic, they should
% be moved to newutilities. Where these are not generic, they should be
% moved beside their caller, or into a specialised utility module. At this
% stage, this file may be deleted, and newutilities renamed as utilities.
%###############################################################################

%###############################################################################
% MODULE
%###############################################################################

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

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

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

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

% IS_IN
is_in(X,[X|_]) :-
    !.

is_in(X,[_|Y]) :-
    is_in(X,Y),
    !.

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

% GEN_APPEND(L1,L2,LL) - general (i.e. nondeterministic) append
gen_append([],L,L).

gen_append([H|T],L,[H|V]) :-
    gen_append(T,L,V).

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


% NEGIN(F,NewF) - move the nots in F in as far as possible to get NewF
negin((not(P)),P1) :-
    !,
    neg(P,P1).

negin(for_all(X,P),for_all(X,P1)) :-
    !,
    negin(P,P1).

negin(for_some(X,P),for_some(X,P1)) :-
    !,
    negin(P,P1).

negin((P and Q),(P1 and Q1)) :-
    !,
    negin(P,P1),
    negin(Q,Q1).

negin((P or Q),(P1 or Q1)) :-
    !,
    negin(P,P1),
    negin(Q,Q1).

negin(P,P).

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

% NEG(F,NF) - return NF equivalent to "not F" but with nots moved in
neg((not(P)),P1) :-
    !,
    negin(P,P1).

neg(for_all(X,P),for_some(X,P1)) :-
    !,
    neg(P,P1).

neg(for_some(X,P),for_all(X,P1)) :-
    !,
    neg(P,P1).

neg((P and Q),(P1 or Q1)) :-
    !,
    neg(P,P1),
    neg(Q,Q1).

neg((P or Q),(P1 and Q1)) :-
    !,
    neg(P,P1),
    neg(Q,Q1).

neg(A>B,A<=B) :-
    !.

neg(A<B,B<=A) :-
    !.

neg(A>=B,A<B) :-
    !.

neg(A<=B,B<A) :-
    !.

neg(A=B,A<>B) :-
    !.

neg(A<>B,A=B) :-
    !.

neg(P,(not(P))) :-
    !.

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

% VAR_FREE(J) - check no Prolog vars (or "goals") in justifications J
var_free([]) :-
    !.
var_free([K|K1]) :-
    novars(K),
    var_free(K1),
    !.

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

% NO_VARS(F) - check no vars in (non-list) structure F
novars(K) :- atomic(K), !.
novars(K) :- nonvar(K), K=..[_OP|Args], var_free(Args), !.

%================================================================================
% exp_contains_exp(+Exp, +ContainsExp).
%-------------------------------------------------------------------------------
% Succeeds where Exp contains ContainsExp.
%================================================================================

exp_contains_exp(Exp, ContainsExp):-
    % Replace all occurrences of ContainsExp in Exp with a totally unique
    % identifier.
    subst_vbl(ContainsExp, '$$uniq$$', Exp, NewExp),
    !,
    % If the replacment makes a difference, then ContainsExp must be in
    % Exp.
    \+ Exp=NewExp,
    !.

%================================================================================
% safe_subst_vbl(+V, +X, +OLD, -NEW).
%-------------------------------------------------------------------------------
% Replace all V by X in OLD to give NEW. Unlike subst_vbl/4, continues to
% work where V occurs in X.
%================================================================================

safe_subst_vbl(V, X, OLD, NEW):-
    % Protect any V in X.
    subst_vbl(V, '$$uniq$$', X, ProtectedX),
    % Perform replacment.
    subst_vbl(V, ProtectedX, OLD, ProtectedNew),
    % Undo protection.
    subst_vbl('$$uniq$$', V, ProtectedNew, NEW),
    !.

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


% SUBST_VBL(V,X,OLD,NEW) - substitute all V in OLD by X to get NEW
subst_vbl(_,_,Y,Y) :-
    var(Y),
    !.        % leave Prolog variables unchanged.

subst_vbl(V,X,V,X) :-
    !.

subst_vbl(_V,_X,Y,Y) :-
    atomic(Y),
    !.

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




subst_vbl(V, X, F := E, F := E2) :-
    % record field names are always atomic.
    atomic(F),
    !,
    subst_vbl(V, X, E, E2),
    !.

subst_vbl(V,X,F,F1) :-
    F=..[OP|Args],
    subst_vbl_list(V,X,Args,Args1),
    F1=..[OP|Args1],
    !.

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

% SUBST_VBL_LIST(V,X,OL,NL) - substitute all V in OL by X to get NL
subst_vbl_list(V,X,[A],[A1]) :-
    subst_vbl(V,X,A,A1),
    !.

subst_vbl_list(V,X,[A|Args],[A1|Args1]) :-
    subst_vbl(V,X,A,A1),
    !,
    subst_vbl_list(V,X,Args,Args1),
    !.

subst_vbl_list(_V,_X,[],[]) :-
    !.

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

% INSERT(NUMBER, LIST, NEWLIST)
insert(NUMBER, [HEAD|TAIL], [HEAD|INSERTED_LIST]) :-
        NUMBER > HEAD,
        !,
        insert(NUMBER, TAIL, INSERTED_LIST).

insert(NUMBER, [NUMBER|_], _) :-
        !,
        fail.

insert(NUMBER, LIST, [NUMBER|LIST]) :-
        !.

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

% merge_sort(L1, L2, LIST) -- merge lists L1 & L2 and sort into order
merge_sort([], LIST, LIST) :-
    !.

merge_sort(LIST, [], LIST) :-
    !.

merge_sort(L1, L2, LIST) :-
        append(L1, L2, SO_FAR),
        !,
        sort(SO_FAR, LIST),
        !.

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

% strict_sublist(SUB, LIST) -- SUB is a sublist of LIST
strict_sublist(SUB, LIST) :-
    append(SUB, _, LIST).

strict_sublist(SUB, [_|LIST]) :-
    strict_sublist(SUB, LIST).

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

% write_error_preamble
% --------------------
% Writes the preamble used for all critical error messages produced by the
% Simplifier This string is searched for by SPARKSimp to recognise
% Simplifier failures, so this string must match that defined in
% sparksimp/sparksimp.apb SPARKSimp also expects to see this string at the
% start of a line so a nl is produced first
write_error_preamble :-
        nl,
        write('*** ERROR - ').

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

% Mathematics

eval_div(X, Y, Z) :-
        Z is X // Y.

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


set_exit_status :-
    !.

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

do_wrap_lines_of(OLD, NEW) :-
        atom_codes(OLD_Atom, OLD),
        atom_codes(NEW_Atom, NEW),
        absolute_file_name(path('wrap_utility'), RunCMD, [extensions(['','.exe']), access(exist)]),
        concat(RunCMD, ' ', FullCMD),
        concat(FullCMD, OLD_Atom, FinalCMD),
        shell(FinalCMD),
        !.

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

maybe_issue_syntax_reminder :-
        syntax_error_in_file(_),
        !,
        % There is at least 1 user rule file with a syntax error.
        build_list_of_errant_files(ErrantFiles),
        write_error_preamble,
        write('Syntax error in a user rule file. Refer to log (slg) file.'),
        nl,
        issue_message('The following user rule files contain a syntax error: ',
                      ErrantFiles),
        issue_message('Scroll back the screen log or consult the log (slg) file for details.', []).

maybe_issue_syntax_reminder :-
    !.

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

build_list_of_errant_files([File|Rest]) :-
        retract(syntax_error_in_file(File)),
        !,
        build_list_of_errant_files(Rest).

build_list_of_errant_files([]).

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

% Confirm the existence of a rule (but not its details).
user_rule_exists(Name, File) :-
        (
           user_inference_rule(File:Name, _, _)
        ;
           inference_rule(File:Name, _, _)
        ;
           user_rewrite_rule(File:Name, _, _, _)
        ;
           % Non-Ground replacement rules coming from the RLS file
           % are applied by the same code as for user-defined rules,
           % so we also check for one of those.
           nonground_replace_rule(File:Name, _, _, _)
        ),
        !.

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

%===============================================================================
% matching_records(+A_Record_Term, +CoreType, +Class, +B_Record_Term)
%
% Predicate succeeds if A_Record_Term and B_Record_Term have identical
% structure but with the inner most argument of A_Record_term differs
% to the inner most argument of B_Record_term, and te inner most
% argument of A_Record_Term is a var_const.
%
%===============================================================================

% Must match at least one record field.
matching_records(A_Record_Term, CoreType, Class, B_Record_Term) :-
    matching_record_and_field(A_Record_Term, B_Record_Term, A_Arg_Term, B_Arg_Term),
    matching_records_x(A_Arg_Term, CoreType, Class, B_Arg_Term),
    !.

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

% Terminate if a different variable or constant on each side.
matching_records_x(A_Arg_Term, CoreType, Class, B_Arg_Term):-
    var_const(A_Arg_Term, CoreType, Class),
    var_const(B_Arg_Term, CoreType, Class),
    A_Arg_Term \= B_Arg_Term,
    !.

% From above, do not have different variable or constant on each side.
% Seek additional field access.

matching_records_x(A_Record_Term, CoreType, Class, B_Record_Term):-
    matching_record_and_field(A_Record_Term, B_Record_Term, A_Arg_Term, B_Arg_Term),
    matching_records_x(A_Arg_Term, CoreType, Class, B_Arg_Term),
    !.

matching_record_and_field(A_Record_Term, B_Record_Term, A_Arg_Term, B_Arg_Term) :-
    functor(A_Record_Term, FieldName_Atom, 1),
    functor(B_Record_Term, FieldName_Atom, 1),
    atom_concat('fld_', _FieldName_Atom, FieldName_Atom),
    arg(1, A_Record_Term, A_Arg_Term),
    arg(1, B_Record_Term, B_Arg_Term).

%===============================================================================

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