rule_validation

assert_from_template(Filename) :-
    absolute_file_name(rulesdslsrc(Filename), Absolute, []),
    read_string_from_file(Absolute,String),
    assertz(rule_report_template_file_codes(Filename,String)).

convert_ms_s(Time,CTime) :- Time >= 1000 -> TimeSec is Time/1000, ajoin([TimeSec,' s'],CTime) ; ajoin([Time,' ms'],CTime).

count_statuses([],0,0,0).

count_statuses([Status|T],NrS,NrF,NrD) :-
    count_statuses(T,S,F,D),
    (Status = 'SUCCESS' -> NrS is S+1 ; NrS = S),
    (Status = 'FAIL' -> NrF is F+1 ; NrF = F),
    (Status = 'DISABLED' -> NrD is D+1 ; NrD = D).

counterexample_name_from_id(Id,CId) :- ajoin([Id,'_Counterexamples'],CId).

evaluate_rule_results(Id,State,RuleRes) :-
    member(bind(Id,RR0),State),
    custom_explicit_sets:expand_custom_set_to_list(RR0,RR1), % TODO: enumeration warning (infinitely many messages)
    maplist(extract_rule_result,RR1,RuleRes).

extract_dependencies(OpName) :-
    get_operation_propositional_guards(OpName,Guards,_RestBody),
    findall(Id, (member(Guard, Guards), is_rule_comp_dependency(Guard,Id)), Deps),
    assertz(dependencies(OpName,Deps)).

extract_operation_attributes(OpName) :-
    get_operation_info(OpName,Infos),
    (member(rules_info(RInfos),Infos) -> true ; RInfos = []),
    (member(tags(Tags),RInfos) -> assertz(tags(OpName,Tags)) ; true),
    (member(classification(Classification),RInfos)
    -> (classification(Classification,OpList)
    -> retractall(classification(Classification,_)),
    assertz(classification(Classification,[OpName|OpList]))
    ; assertz(classification(Classification,[OpName])))
    ; true),
    (member(rule_id(RId),RInfos) -> assertz(rule_id(OpName,RId)) ; true).

extract_rule_operations(Id,Vars) :-
    counterexample_name_from_id(Id,CId), % we could double check with successful
    (member(CId,Vars) -> assertz(rule(Id)) ; assertz(computation(Id))).

extract_rule_result((int(ErrorCode),string(ResultStr)),rule_result(ErrorCode,ResultStr)).

gen_classifications(Stream,CName,OpList,BState,ProfileList) :-
    format(Stream,' <div class="classification-list">~n',[]),
    format(Stream,' <div class="classification-header" onclick="openDetails(\'classification_~w\')">~n',[CName]),
    length(OpList,NrOps),
    format(Stream,' <b>~w</b> (~w)~n',[CName,NrOps]),
    format(Stream,' </div>~n',[]),
    format(Stream,' <div class="rule-list classification" id="classification_~w">~n',[CName]),
    forall(member(Rule,OpList), gen_rule_result(Stream,Rule,BState,ProfileList)),
    format(Stream,' </div>~n',[]),
    format(Stream,' </div>~n',[]),
    format(Stream,' </div>~n',[]).

gen_report_infos(Stream,Rules,BState) :-
    length(Rules,NrRules),
    precollect_statuses(Rules,BState,NrC,NrS,NrF,NrD),
    b_get_main_filename(Filename),
    get_tail_filename(Filename,MName),
    format(Stream,' Checked machine: <b>~w</b>~n',[MName]),
    (b_get_definition_string_from_machine('RULE_REPORT_CONTEXT',RepCtx)
    -> format(Stream,' <br>With context: <b>~w</b>~n',[RepCtx])
    ; true),
    format(Stream,' <div style="line-height:25px;">~n',[]),
    format(Stream,' <br>Total number of rules: <b>~w</b>~n',[NrRules]),
    format(Stream,' <br>Number of checked rules: <b>~w</b>~n',[NrC]),
    format(Stream,' <br>Number of successful rules: <b>~w</b>~n',[NrS]),
    format(Stream,' <br>Number of failed rules: <b>~w</b>~n',[NrF]),
    format(Stream,' <br>Number of disabled rules: <b>~w</b>~n',[NrD]),
    format(Stream,' </div>~n',[]),
    format(Stream,' <br>~n',[]).

gen_rule_content_list(Stream,Rule,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDep) :-
    length(CounterEx,CELen),
    length(SuccessMsg,SMLen),
    length(UncheckedMsg,UCLen),
    length(FailDep,FDLen),
    length(NotExecDep,NEDLen),
    ((CELen > 0 ; SMLen > 0 ; UCLen > 0 ; FDLen > 0 ; NEDLen > 0) % create tag only if at least one child exists
    -> format(Stream,' <div class="rule-content" id="~w">~n',[Rule]),
    (CELen > 0
    -> format(Stream,' <b>~w</b> Violations found:~n',[CELen]),
    format(Stream,' <ul>~n',[]),
    forall(member(CE,CounterEx),gen_rule_content_list_aux(Stream,CE)),
    format(Stream,' </ul>~n',[])
    ; true
    ),
    (SMLen > 0
    -> format(Stream,' <b>~w</b> successful checks:~n',[SMLen]),
    format(Stream,' <ul>~n',[]),
    forall(member(SM,SuccessMsg),gen_rule_content_list_aux(Stream,SM)),
    format(Stream,' </ul>~n',[])
    ; true
    ),
    (UCLen > 0
    -> format(Stream,' <b>~w</b> unchecked items:~n',[UCLen]),
    format(Stream,' <ul>~n',[]),
    forall(member(UC,UncheckedMsg),gen_rule_content_list_aux(Stream,UC)),
    format(Stream,' </ul>~n',[])
    ; true
    ),
    (FDLen > 0
    -> format(Stream,' Rule could not be checked due to ~w failed dependencies:~n',[FDLen]),
    format(Stream,' <ul>~n',[]),
    forall(member(FD,FailDep),gen_rule_content_list_aux(Stream,FD)),
    format(Stream,' </ul>~n',[])
    ; true
    ),
    (NEDLen > 0
    -> format(Stream,' Rule could not be checked due to ~w unchecked dependencies:~n',[NEDLen]),
    format(Stream,' <ul>~n',[]),
    forall(member(NED,NotExecDep),gen_rule_content_list_aux(Stream,NED)),
    format(Stream,' </ul>~n',[])
    ; true
    ),
    format(Stream,' </div>~n',[])
    ; true),
    fail.

gen_rule_content_list(_,_,_,_,_,_,_).

gen_rule_content_list_aux(Stream,rule_result(ErrorCode,Message)) :- !,
    format(Stream,' <li>(~w) ~w</li>~n',[ErrorCode,Message]).

gen_rule_content_list_aux(Stream,Dependency) :-
    format(Stream,' <li>~w</li>~n',[Dependency]).

gen_rule_result(Stream,Rule,BState,ProfileList) :-
    get_rule_status(BState,Rule,Status,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDep),
    (Status = 'SUCCESS'
    -> ((SuccessMsg \= [] ; UncheckedMsg \= [])
    -> format(Stream,' <div class="rule-header pointer green" onclick="openDetails(\'~w\')">~n',[Rule])
    ; format(Stream,' <div class="rule-header green">~n',[]))
    ; Status = 'FAIL'
    -> format(Stream,' <div class="rule-header pointer red" onclick="openDetails(\'~w\')">~n',[Rule]),
    format(Stream,' <span class="icon">⚠</span>~n',[])
    ; Status = 'DISABLED' -> format(Stream,' <div class="rule-header grey">~n',[])
    ; Status = 'NOT_CHECKED'
    -> ((FailDep \= [] ; NotExecDep \= [])
    -> (FailDep \= [] -> C = 'orange' ; C = 'lightgrey'), % FAIL dependencies: orange, else grey
    P = 'pointer'
    ; C = 'white', P = '' % no conflicts with dependencies
    ),
    format(Stream,' <div class="rule-header ~w ~w" onclick="openDetails(\'~w\')">~n',[P,C,Rule]),
    (C = 'orange' -> format(Stream,' <span class="icon">⚠</span>~n',[]) ; true)
    ; format(Stream,' <div class="rule-header">~n',[])
    ),
    format(Stream,' ~w',[Rule]),
    (rule_id(Rule,RuleId)
    -> format(Stream,' [~w]~n',[RuleId])
    ; format(Stream,'~n',[])),
    (tags(Rule,Tags)
    -> format(Stream,' ~n',[]),
    forall(member(Tag,Tags), format(Stream,' <div class="tag">~w</div>~n',[Tag])),
    format(Stream,' ~n',[])
    ; true),
    format(Stream,' <b>~w</b>~n',[Status]),
    (member(list([Rule,_,WT,_,_,_,_]),ProfileList)
    -> convert_ms_s(WT,WTPrint),
    format(Stream,' <span style="float: right;"><em>(~w)</em></span>~n',[WTPrint])
    ; true), % ignore if not available
    format(Stream,' </div>~n',[]),
    gen_rule_content_list(Stream,Rule,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDep),
    fail.

gen_rule_result(_Stream,_,_,_).

generate_html_report(File) :- generate_html_report(File,[]). % /1 default (for current state)

generate_html_report(File,Options) :- % /2 current state with options
    current_state_id(ID),
    generate_html_report(ID,File,Options).

generate_html_report(StateID,File,Options) :- % /3 any state with options TODO: language option
    (animation_minor_mode(rules_dsl) -> true
    ; b_get_main_filename(BFile),
    add_error(rule_validation,'Cannot create rule validation report, is not a rules machine (.rmch): ',BFile),
    fail),
    visited_expression(StateID,State),
    (state_corresponds_to_initialised_b_machine(State)
    -> extract_variables_from_state(State,VarState)
    ; add_error(rule_validation,'Cannot create rule validation report for uninitialised state'), fail),
    safe_open_file(File,write,Stream,[encoding(utf8)]),
    generate_html_to_stream(Stream,VarState,[html_file/File|Options]),
    close(Stream),
    formatsilent('% created rule validation report at ~w.~n',[File]).

generate_html_to_stream(Stream,State,Options) :-
    write_rule_report_template('validation_report_header.html',Stream),
    get_rules(Rules),
    (get_preference(prob_profiling_on,true)
    -> tcltk_get_operations_profile_info(list(ProfileList)),
    get_total_walltime(ProfileList,TotalWT)
    ; ProfileList = [],
    (member(checktime(TotalWT),Options) -> true ; TotalWT = -1) % option to provide checktime from ProB2 if profiling is off
    ),
    gen_report_infos(Stream,Rules,State),
    forall(classification(CName,OpList),gen_classifications(Stream,CName,OpList,State,ProfileList)),
    format(Stream,' <div class="rule-list normal">~n',[]),
    forall((member(Rule,Rules), \+ (classification(_,OpList), member(Rule,OpList))), % all rules w/o classification
    gen_rule_result(Stream,Rule,State,ProfileList)),
    format(Stream,' </div>~n',[]),
    (TotalWT > 0 -> convert_ms_s(TotalWT,WTPrint), format(Stream,' Check finished after: ~w~n',[WTPrint]) ; true),
    version_str(VStr), revision(VRev),
    format(Stream,' <br>ProB Version: ~w (~w)~n',[VStr,VRev]),
    datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
    number_codes_min_length(Min,2,MC),
    format(Stream,' <br>Generated on ~w/~w/~w at ~w:~s~n',[Day,Mon,Yr,Hr,MC]),
    write_rule_report_template('validation_report_footer.html',Stream).

get_computations(Comps) :- findall(X, computation(X), Comps).

get_failed_dependencies(State,Dep) :-
    rule(Dep),
    member(bind(Dep,string('FAIL')),State).

get_not_executed_dependencies(State,Dep) :-
    member(bind(Dep,string(DepStatus)),State),
    (DepStatus = 'DISABLED' ;
    (rule(Dep)
    -> DepStatus = 'NOT_CHECKED'
    ; DepStatus = 'NOT_EXECUTED')).

get_rule_counterexamples(RuleName,State,CounterEx) :-
    counterexample_name_from_id(RuleName,CId),
    evaluate_rule_results(CId,State,CounterEx).

get_rule_status(BState,RuleName,Status,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDeps) :-
    rule(RuleName),
    dependencies(RuleName,Deps),
    member(bind(RuleName,string(Status)),BState), % rule status: NOT_CHECKED, DISABLED, FAIL, SUCCESS
    include(get_failed_dependencies(BState),Deps,FailDep),
    include(get_not_executed_dependencies(BState),Deps,NotExecDeps),
    get_rule_counterexamples(RuleName,BState,CounterEx),
    get_rule_success_messages(RuleName,BState,SuccessMsg),
    get_rule_unchecked_messages(RuleName,BState,UncheckedMsg).

get_rule_success_messages(RuleName,State,SuccessMsg) :-
    successful_name_from_id(RuleName,SId),
    evaluate_rule_results(SId,State,SuccessMsg).

get_rule_unchecked_messages(RuleName,State,UncheckedMsg) :-
    unchecked_name_from_id(RuleName,UId),
    evaluate_rule_results(UId,State,UncheckedMsg).

get_rules(Rules) :- findall(X, rule(X), Rules).

get_simple_rule_status(BState,RuleName,Status) :-
    rule(RuleName),
    member(bind(RuleName,string(Status)),BState).

get_total_walltime([_|T],WT) :- get_total_walltime1(T,WT). % ignore table legend

get_total_walltime1([],0).

get_total_walltime1([list([_,_,WT0,_,_,_,_])|T],WT) :-
    get_total_walltime1(T,WT1),
    WT is WT0+WT1.

is_rule_comp_dependency(b(equal(b(identifier(Id),string,_),b(string('SUCCESS'),string,_)),pred,_), Id) :- rule(Id).

is_rule_comp_dependency(b(equal(b(identifier(Id),string,_),b(string('EXECUTED'),string,_)),pred,_), Id) :- computation(Id).

precollect_statuses(Rules,BState,NrC,NrS,NrF,NrD) :-
    maplist(get_simple_rule_status(BState), Rules, Statuses),
    count_statuses(Statuses,NrS,NrF,NrD),
    NrC is NrS+NrF.

reset_rules_extras :-
    retractall(computation(_)),
    retractall(rule(_)),
    retractall(dependencies(_,_)),
    retractall(tags(_,_)),
    retractall(classification(_,_)),
    retractall(rule_id(_,_)).

setup_rules_extras :-
    reset_rules_extras,
    (animation_minor_mode(rules_dsl) -> true
    ; b_get_main_filename(BFile),
    add_error(rule_validation,'Cannot set up rules DSL mode, current machine is not a rules machine (.rmch): ',BFile),
    fail),
    (bmachine_is_precompiled -> true ; add_error(setup_rules_extras,'bmachine not precompiled'), fail),
    get_machine_identifiers(operations,Ops),
    get_machine_identifiers(variables,Vars),
    forall(member(Op,Ops),
    (extract_rule_operations(Op,Vars),
    extract_dependencies(Op),
    extract_operation_attributes(Op))), % tags, classification, rule_id
    debug_println(19,'% setup for rules DSL complete.').

successful_name_from_id(Id,CId) :- ajoin([Id,'_Successful'],CId).

unchecked_name_from_id(Id,CId) :- ajoin([Id,'_Unchecked'],CId).

write_rule_report_template(HtmlFile,Stream) :-
    rule_report_template_file_codes(HtmlFile,Codes),
    format(Stream,'~s~n',[Codes]).