self_check

acceptable_residue(kernel_waitflags:copy_wfe_to_inner(_,_)).

acceptable_residue(put_attr(_,_,_)).

acceptable_residue((A,B)) :- acceptable_residue(A),acceptable_residue(B).

add_self_check(Module,X) :-
    (nonvar(X) ->
    (self_check(X,Module) -> true
    ; inc_self_check_module(Module,Nr),
    get_current_term_position(Line,_Col),
    assertz(self_check(X,Module,Nr,Line))
    )
    ;
    my_print_error('### trying to assert variable as self_check: '),my_print_error(X),fail
).

assert_must_fail(Call) :-
    get_call_module(Call,M),
    add_self_check(M,must_fail(Call)).

assert_must_succeed(Call) :-
    get_call_module(Call,M),
    add_self_check(M,must_succeed_without_residue(Call)).

assert_must_succeed_any(Call) :-
    get_call_module(Call,M),
    add_self_check(M,must_succeed(Call)).

assert_must_succeed_multiple(Call) :-
    get_call_module(Call,M),
    add_self_check(M,must_succeed_multiple_without_residue(Call)).

assert_post(X,Post) :-
    (nonvar_call(X),nonvar_call(Post)
    -> retractall(post_condition(X,_)),assertz(post_condition(X,Post))
    ; my_print_error('### illegal variable(s) in: '),
    my_print_error(assert_post(X,Post)),fail
).

assert_pre(X,Pre) :- % print(adding_pre(X)),nl,
    (nonvar_call(X),nonvar_call(Pre)
    -> retractall(pre_condition(X,_)),assertz(pre_condition(X,Pre))
    ; my_print_error('### illegal variable(s) in: '),
    my_print_error(assert_pre(X,Pre)),fail
).

check_det(Call) :- check_deterministic(Call).

check_det2(Call,X) :- assertz(calling(X)),
    call(Call),
    (retract(calling(X)) -> true
    ; nl,
    print('### Call has multiple solutions: '),nl,
    print('### '), print(Call),nl,
    nl
).

check_det2(Call,X) :- (retract(calling(X)) -> print(fails(Call)),nl ; fail).

check_deterministic(Call) :-
    retract(det_counter(X)), X1 is X+1, assertz(det_counter(X1)),
    check_det2(Call,X).

check_eq(A,B) :- (A=B -> true ; format(user_error,'! Not unifiable:~n ~w~n ~w~n',[A,B]),fail).

check_eqeq(A,B) :- (A==B -> true ; format(user_error,'! Not identical:~n ~w~n ~w~n',[A,B]),fail).

check_exception_call(X) :-
    catch(call(X), Error, (
    format_with_colour(user_error,[red,bold],'! *** EXCEPTION *** :~n',[]),
    write('! '),print_numbervars(X),nl,
    write_exception_error(Error),nl,
    throw(Error)
)).

check_test_case(testcase(Module,Nr,Line,Call), TotNr, Verdict,Options) :-
    (member(silent,Options) -> true ; format('Running unit test ~w in module ~w (line ~w)~n',[Nr,Module,Line])),
    set_error_context(unit_test_context(Module,TotNr,Line,Call)),
    statistics(runtime,[T1,_]),
    (member(verbose,Options) -> portray_clause(Call) ; true),
    safe_call(Call),
    flush_output,
    statistics(runtime,[T2,_]),
    Time is T2-T1,
    (member(verbose,Options) -> format('Runtime for unit test ~w: ~w ms~n',[TotNr,Time])
    ; Time>20 -> format('*~w ms*~n',[Time]) ; true),
    (Time>2000 -> format_with_colour(user_output,[blue],'Warning: long unit test ~w: ~w ms in module ~w (line ~w)~n ~w~n',[TotNr,Time,Module,Line,Call]) ; true),
    (get_all_errors_and_reset(Errors) -> V=error(Errors) ; V=pass),
    create_junit_result(Call, Time, V, Verdict).

check_test_cases([],[],Nr,Module,_Options) :-
    format('Number of unit tests run in ~w: ~w~n',[Module,Nr]).

check_test_cases([H|T],[V|VT],Nr,Module,Options) :-
    N1 is Nr+1,
    get_error_count(Module,NrBefore),
    check_test_case(H,N1,V,Options),
    get_error_count(Module,NrAfter),
    (NrBefore=NrAfter -> true
    % ; NrBefore > 0 -> true % we already have a previous unit test failure
    ; H=testcase(_,TestNr,LineNr,_Call),
    format_with_colour(user_error,[red,bold],
    '~n*** UNIT TEST ~w FAILED in module ~w (line ~w)~n',[TestNr,Module,LineNr]),
    format_with_colour(user_error,[red,bold],
    '*** Rerun this test with: probcli -selfcheck_module ~w:~w~n~n',[Module,TestNr]),
    register_failure(Module,TestNr)
    %,portray_testcase(H)
    %%% ,trace
    ),
    check_test_cases(T,VT,N1,Module,Options).

det_call(X) :-
    (run_time_type_check_mode(off)
    -> call(X)
    ; force_det_call(X)
).

det_counter(0).

disable_interaction_on_errors :-
    retractall(prepost_no_error_so_far).

force_det_call(X) :-
    get_functor_module(X,Module,F,Arity),
    retractall(found_det_sol(F,Arity,Module,_)), /* cannot be nested for same predicate !*/
    copy_term(X,CopyX),
    %print(det_call(X)),nl,
    residue_check_call(X), % was rt_timeout_call(X)
    (found_det_sol(F,Arity,Module,Previous) ->
    (add_error(mnf,'### WARNING CALL HAS MULTIPLE SOLUTIONS: ',CopyX),nl,
    print('### Solution 1: '),print_quoted_with_max_depth(Previous,60),nl,nl,
    print('### Solution 2: '),print_quoted_with_max_depth(X,60),nl,nl,
    prepost_user_interaction)
    ; assertz(found_det_sol(F,Arity,Module,X))
).

found_id(0).

get_call_module(Module:_, Module).

get_current_term_position(Line,Col) :-
    %prolog_load_context(file, File),
    prolog_load_context(term_position,TPos),
    !,
    (stream_position_data(line_count,TPos,LineM1) -> Line is LineM1+1 ; Line='?'),
    (stream_position_data(line_position,TPos,Col) -> true ; Col='?').

get_current_term_position('?','?').

get_error_count(Module,Nr) :- errors_in_module(Module,Nr), !.

get_error_count(_,0).

get_found_id(Nr) :- retract(found_id(Nr)), N1 is Nr+1, assertz(found_id(N1)).

get_functor_module(Module:Call,Module,F,Arity) :- !, functor(Call,F,Arity).

get_functor_module(Call,unknown,F,Arity) :- functor(Call,F,Arity).

get_module_list(ML) :- findall(Module,self_check_module(Module),Modules), sort(Modules,ML).

get_predicate_arity(':'(Module,Call),Res,Arity) :- !,Res=Module:Pred,
    functor(Call,Pred,Arity).

get_predicate_arity(Call,Pred,Arity) :-
    functor(Call,Pred,Arity).

inc_error_count :- inc_error_count(_,_).

inc_error_count(Module,N1) :- current_module_under_test(Module),!,
    (retract(errors_in_module(Module,Nr)) -> true ; Nr=0),
    N1 is Nr+1,
    assertz(errors_in_module(Module,N1)).

inc_error_count(unknown,1) :- print('No current module.'),nl.

inc_self_check_module(Module,Res) :-
    (retract(self_check_module(Module,N1)) -> true ; N1=0),
    Nr is N1+1,
    assertz(self_check_module(Module,Nr)),
    Res = Nr.

included_self_check(X,Module,TestNr,Line,Options) :-
    self_check(X,Module,TestNr,Line),
    (member(run_only_nr(Nr),Options) -> TestNr=Nr ; true).

list_skel2([]).

list_skel2([_H|T]) :- nonvar(T), list_skel2(T).

list_skeleton(X) :-
    (nonvar(X),list_skel2(X) -> true
    ; (my_print_error('### not list skeleton: '), my_print_error(X),fail)).

mnf(X) :- mnf_call(X).

mnf(ProgramPoint,X) :- mnf_call_with_pp(ProgramPoint,X).

mnf_call(X) :-
    (run_time_type_check_mode(off)
    -> call(X)
    ; if(call(X),true,
    (add_error(mnf,'### WARNING CALL HAS FAILED: ',X),
    print_call(X),
    prepost_user_interaction,
    fail)
)
).

mnf_call_with_pp(ProgramPoint,X) :-
    (run_time_type_check_mode(off)
    -> call(X)
    ; if(rt_timeout_call(X),true,
    (add_error(mnf,'### WARNING CALL HAS FAILED: ',(X,ProgramPoint)),
    print_call(X),
    print('### at program point:'),print(ProgramPoint),nl,
    prepost_user_interaction,
    fail)
)
).

mnf_det(X) :-
    (run_time_type_check_mode(off)
    -> call(X)
    ; (get_functor_module(X,Module,F,Arity),
    retractall(found_det_sol(F,Arity,Module,_)), /* cannot be nested for same predicate !*/
    copy_term(X,CopyX),
    mnf_call(X),
    (found_det_sol(F,Arity,Module,Previous) ->
    (add_error(mnf,'### WARNING CALL HAS MULTIPLE SOLUTIONS: ',CopyX),nl,
    print('### Solution 1: '),print_quoted_with_max_depth(Previous,60),nl,nl,
    print('### Solution 2: '),print_quoted_with_max_depth(X,60),nl,nl,
    prepost_user_interaction)
    ; assertz(found_det_sol(F,Arity,Module,X))
)
)
).

must_fail(X) :-
    copy_term(X,Y),
    rt_timeout_call(X),!,
    %(safe_numbervars(Y,0,_) -> true ; true), % portray already does a numbervars
    inc_error_count(Module,_NrErr),
    add_error(must_fail,'Unit Test Failed, a call unexpectedly succeeded in module:',Module),
    my_print_error('! The call: '),
    my_portray_error(Y),
    my_print_error('! should have failed but succeeded with:'),
    my_portray_error(X).

must_fail(_X).

must_succeed(X) :- %print(must_suceed(X)),nl,
    \+ rt_timeout_call(X),!,
    %(safe_numbervars(X,0,_) -> true ; true), % portray already does a numbervars
    inc_error_count(Module,_NrErr),
    add_error(must_succeed,'Unit Test Failed, a call unexpectedly failed in module:',Module),
    my_print_error('! The call failed but should have succeeded: '),
    my_portray_error(X),
    %trace, X, % and comment out safe_numbervars above
    nl.

must_succeed(_X). % :- print(ok_must_succeed(_X)),nl.

must_succeed_multiple_without_residue(X) :- get_found_id(ID),
    must_succeed(X),
    retractall(found_must_succeed_sol(ID)),
    call_residue(X,CallResidue),
    (maplist(acceptable_residue,CallResidue) -> true -> true
    ; add_error(must_succeed_multiple_without_residue,'### Self-Check has residue: ',X),
    add_error(must_succeed_multiple_without_residue,'### Residue: ',CallResidue),
    inc_error_count,
    print_goal(CallResidue),nl
    ),
    (found_must_succeed_sol(ID)
    -> (true,!)
    ; assertz(found_must_succeed_sol(ID)),fail
).

must_succeed_multiple_without_residue(X) :-
    inc_error_count,
    add_error(must_succeed_multiple_without_residue,
    '### Self-Check did not succeed multiple times: ',X).

must_succeed_without_residue(X) :- get_found_id(ID),
    must_succeed(residue_check_call(X)),
    retractall(found_must_succeed_sol(ID)),
    %residue_check_call(X),
    (found_must_succeed_sol(ID)
    -> add_error(must_succeed_without_residue,'### Self-Check has multiple solutions: ',X),
    inc_error_count,
    !
    ; assertz(found_must_succeed_sol(ID)),fail
).

must_succeed_without_residue(_).

must_succeed_without_residue_and_time_out(X) :-
    time_out(check_exception_call(X),2000,TimeOutRes),
    (TimeOutRes = success -> true
    ; inc_error_count,
    add_error(self_check,'### TIMEOUT: ',X), portray_clause(X),nl,
    fail).

my_portray_error(Query) :- safe_numbervars(Query,0,_),
    write_term(user_error,Query,[portrayed(true),numbervars(true),max_depth(50),indented(true)]),fail.

my_portray_error(_).

my_print_error(Error) :-
    (var(Error)
    -> print_message(error,'_')
    ; write(user_error,'! '),write_term(user_error,Error,[max_depth(50),numbervars(true)]),nl(user_error)
).

nonvar_call(Call) :-
    nonvar(Call),
    (Call = M:P -> nonvar(M), nonvar(P) ; true).

perform_self_check :- perform_self_check(_).

perform_self_check(M) :- perform_self_check(M,[]).

perform_self_check(Module,Options) :- nl, reset_found_id,
    reset_error_summary,
    announce_event(start_unit_tests),
    flush_output,
    print('% '),
    retractall(starttime(_)),
    statistics(runtime,[Start,_]), assertz(starttime(Start)),
    if(self_check_module(Module,NrTests),true,
    (my_print_error(illegal_module(Module)),inc_error_count,
    fail)
    ),
    set_current_module(Module),
    (member(silent,Options) -> true ; format_with_colour(user_output,[blue],'~n~nPerforming ~w unit tests for module ~w~n',[NrTests,Module])),
    run_module_tests(Module,TestResults,Options),
    print_junit(['Selfcheck',Module], TestResults),
    fail.

perform_self_check(_,_) :-
    statistics(runtime,[End,_]),
    starttime(Start), Tot is End-Start,
    nl, print('Runtime for Performing Unit Tests: '), print(Tot), print(' ms'),
    nl,
    announce_event(stop_unit_tests),
    clear_error_context,
    print_summary,
    (errors_in_module(_,_)
    -> format_with_colour(user_error,[red,bold],'~n! Unit Tests FAILED !!!~n',[]),
    print_error_summary,
    fail
    ; true),
    format_with_colour(user_output,[green],'~nUnit Tests Successful.~n',[]),
    flush_output.

perform_verbose_self_check :- perform_verbose_self_check(_).

perform_verbose_self_check(M) :- perform_self_check(M,[verbose]).

portray_self_checks :- portray_self_checks(_).

portray_self_checks(Module) :-
    self_check_module(Module,NrTests),
    format_with_colour(user_output,[blue],'~n~nUnit Tests (~w) for Module ~w~n',[NrTests,Module]),
    self_check(X,Module,Nr,Line),
    format_with_colour(user_output,[blue],' ~w (line ~w): ',[Nr, Line]),
    portray_clause(X),
    fail.

portray_self_checks(_) :- nl.

portray_testcase(testcase(Module,TestNr,Line,Call)) :- !,
    start_terminal_colour([blue],user_error),
    format(user_error,'UNIT TEST ~w in module ~w at line ~w:~n :- ',[TestNr,Module,Line]),
    portray_clause(user_error,Call),nl,
    reset_terminal_colour(user_error).

portray_testcase(X) :- print(unknown_testcase(X)),nl.

pp_cll(X) :- prepost_call(X).

pp_mnf(X) :- prepost_mnf_call(X).

prepost_call(X) :-
    /* print(pre(X)),nl, */
    (verify_pre(X) -> true ; my_print_error(verify_pre_failed(X))),
    rt_timeout_call(X),
    /* print(post(X)),nl, */
    (verify_post(X) -> true ; my_print_error(verify_post_failed(X))).

prepost_mnf_call(X) :- % print(prepost_mnf_call(X)),nl,
    (run_time_type_check_mode(off)
    -> call(X)
    ; if(prepost_call(X),true,
    (add_error(mnf,'### WARNING CALL HAS FAILED: ',X),
    print_call(X),
    prepost_user_interaction,
    fail)
)
).

prepost_no_error_so_far. % :- fail.

prepost_user_interaction :- prepost_no_error_so_far,!,
    my_print_error('### => Stop at next error (y/n/halt/trace) => '),
    read(Answer),
    (Answer='y' -> true
    ; Answer='halt' -> halt
    ; Answer='trace' -> trace
    ; retract(prepost_no_error_so_far)).

prepost_user_interaction.

print_call(X) :-
    print('### Call: '),print_quoted_with_max_depth(X,10),nl,
    print('### Summary: '),print_term_summary(X),nl,
    print('### Predicate: '),
    (X = ':'(M,C) -> (print(M),print(':')) ; C=X),
    functor(C,F,N),
    print(F), print('/'), print(N),nl.

print_error_summary :- errors_in_module(Module,Nr),
    findall(TestNr,unit_test_failed_in_module(Module,TestNr),List),
    length(List,Len),
    format('Module ~w has ~w errors and ~w failed test(s): ~w.~n',[Module,Nr,Len,List]),
    fail.

print_error_summary.

print_numbervars(X) :- safe_numbervars(X,0,_), print(X),fail.

print_numbervars(_).

print_summary :- findall(T,tests_in_module(_,T),NrTests),
    length(NrTests,NrModules),
    sumlist(NrTests,TotTests),
    format('Number of Unit Tests: ~w in ~w modules~n',[TotTests,NrModules]).

register_failure(Module,TestNr) :- assertz(unit_test_failed_in_module(Module,TestNr)).

reset_error_summary :-
    retractall(errors_in_module(_,_)),
    retractall(unit_test_failed_in_module(_,_)),
    retractall(tests_in_module(_,_)).

reset_found_id :- retractall(found_must_succeed_sol(_)),
    retractall(found_id(_)), assertz(found_id(0)).

residue_check_call(X) :-
    copy_term(X,CX),
    call_residue(X,CallResidue),
    (maplist(acceptable_residue,CallResidue) -> true
    ; add_error(must_succeed_without_residue,'### Call has residue: ',X),
    add_error(must_succeed_without_residue,'### Residue: ',CallResidue),
    inc_error_count,
    print_goal(CallResidue),nl,
    safe_numbervars(CX,0,_),
    format('### Original call: ~w~n',[CX])
).

rt_timeout_call(Call) :- run_time_type_check_mode(off),!,check_exception_call(Call).

rt_timeout_call(Call) :- time_out(check_exception_call(Call),5000,TimeOutRes),
    (TimeOutRes = success -> true ; inc_error_count, add_error(self_check,'### TIMEOUT: ',Call),fail).

run_module_tests(Module,Results,Options) :-
    findall(testcase(Module,TestNr,Line,X), included_self_check(X,Module,TestNr,Line,Options), Calls),
    length(Calls,Len),
    assertz(tests_in_module(Module,Len)),
    %maplist(check_test_case, Calls, Results).
    check_test_cases(Calls,Results,0,Module,Options).

run_time_type_check_mode(on).

safe_call(X) :-
    catch(call(X), Exception, (
    print(exception(X,Exception)),nl,nl,
    inc_error_count,
    add_error(safe_call,'### Exception occurred during self-check: ',X:Exception)
)).

self_check(X,Module) :- self_check(X,Module,_,_).

self_check_module(Module) :- self_check_module(Module,_NrTests).

self_checks_exist :- self_check(_,_,_,_).

set_current_module(M) :- var(M),!, my_print_error('Module is variable').

set_current_module(M) :-
    retractall(current_module_under_test(_)),
    assertz(current_module_under_test(M)).

turn_off_run_time_type_checks :-
    retract(run_time_type_check_mode(_)),
    assertz(run_time_type_check_mode(off)).

turn_on_run_time_type_checks :-
    retract(run_time_type_check_mode(_)),
    assertz(run_time_type_check_mode(on)).

verify_post(Call) :-
    (run_time_type_check_mode(off) -> true
    ; post_condition(Call,Post) ->
    ( \+ rt_timeout_call(Post)
    -> get_predicate_arity(Call,Pred,Arity),
    add_error(verify_post,'### POST-CONDITION ERROR OCCURRED: ',Pred/Arity),
    add_error(verify_post,'### CALL: ',Call),nl,
    prepost_user_interaction
    ; true
    )
    ; get_predicate_arity(Call,Pred,Arity),
    add_error(verify_post,'### No POST-CONDITION for ',Pred/Arity),
    prepost_user_interaction
).

verify_pre(Call) :-
    (run_time_type_check_mode(off) -> true
    ; pre_condition(Call,Pre) ->
    ( \+ rt_timeout_call(Pre)
    -> get_predicate_arity(Call,Pred,Arity),
    add_error(verify_pre,'### PRE-CONDITION ERROR OCCURRED: ',Pred/Arity),
    add_error(verify_pre,'### CALL: ',Call),nl,
    prepost_user_interaction
    ; true
    )
    ; get_predicate_arity(Call,Pred,Arity),
    add_error(verify_pre,'### No PRE-CONDITION for ',Pred/Arity),
    print_term_summary(Call),
    prepost_user_interaction
).

write_exception_error(error(existence_error(procedure,CALL),_)) :-
    format_with_colour(user_error,[red,bold],'! EXISTENCE ERROR: ~w~n',[CALL]),fail.

write_exception_error(Error) :- write('! '),write_term(Error,[max_depth(20),numbervars(true)]),nl.