bmachine_static_checks

add_const_expr_msg(OpID,LocalIds,BExpr) :-
    (LocalIds=[] -> debug:debug_mode(on) ; true), % decide whether to show outer-level constant expressions
    register_constant_expression(BExpr,OpID,LocalIds,Count,MsgOrWarn),
    (LocalIds = [] -> LMsg=[': ']
    ; length(LocalIds,Len),
    (Len =< 3
    -> ajoin_with_sep(LocalIds,',',LIDS),
    LMsg = [' inside quantification (',LIDS,'): ']
    ; prefix_length(LocalIds,Prefix,2),
    last(LocalIds,LastId),
    ajoin_with_sep(Prefix,',',LIDS),
    LMsg = [' inside quantification (',Len,' ids: ',LIDS,',...,',LastId,'): ']
    )
    ),
    (Count > 1
    -> ajoin(['Repeated constant expression in operation ',OpID,
    ' (occurence nr. ',Count,', consider lifting it out)'|LMsg],Msg)
    ; ajoin(['Non-trivial constant expression in operation ',OpID,' (consider lifting it out)'|LMsg],Msg)
    ),
    (MsgOrWarn=create_messages
    -> add_message(b_machine_static_checks,Msg,BExpr,BExpr)
    ; add_warning(b_machine_static_checks,Msg,BExpr,BExpr)).

atomic_subst(b(S,_,_)) :- atomic_subst2(S).

atomic_subst2(skip).

atomic_subst2(assign(_,_)).

atomic_subst2(assign_single_id(_,_)).

atomic_subst2(becomes_element_of(_,_)).

boolean_operator(conjunct).

boolean_operator(disjunct).

boolean_operator(implication).

boolean_operator(equivalence).

check_aux(function(b(Func,_,_I1),_Arg),_,I2,Ctxt) :- % _I1 sometimes unknown
    % TO DO: check if Info contains WD flag
    check_is_partial_function(Func,I2,Ctxt).

check_concrete_constants :- is_concrete_constants_state_id(ID),!,
    check_values_in_state(ID).

check_concrete_constants.

check_definition_clashes(SortedAllIds) :-
    Scope=[variables],
    b_get_typed_definition(Name,Scope,TExpr),
    % TODO: adapt type_check_definitions to return definitions with paras and add paras to list of Ids
    %print(check(Name,SortedAllIds)),nl,
    map_over_typed_bexpr_with_names(bmachine_static_checks:check_introduced_ids('DEFINITION',Name,SortedAllIds),TExpr).

check_for_constant_expressions(BExpr,OpID,LocalIds,IsConstant,IsExpensive) :-
    syntaxtraversion(BExpr,Expr,Type,_Infos,Subs,TNames),
    (get_texpr_ids(TNames,QuantifiedNewIds), list_to_ord_set(QuantifiedNewIds,SQuantifiedNewIds)
    -> ord_union(LocalIds,SQuantifiedNewIds,NewLocalIds)
    ; write(err(TNames)),nl, NewLocalIds = LocalIds),
    l_check_for_const(Subs,OpID,NewLocalIds,SQuantifiedNewIds,AreAllConstant,IsExpensive1,ExpensiveList),
    %translate:print_bexpr_or_subst(BExpr),nl, write(cst(AreAllConstant,IsExpensive1,LocalIds)),nl,nl,
    (AreAllConstant=is_constant,
    is_constant_expression(Expr,LocalIds,IsExpensive2)
    -> IsConstant = is_constant,
    combine_expensive(IsExpensive1,IsExpensive2,IsExpensive),
    (pred_or_subst(Type) % we may traverse the boundary of expressions to pred/subst: print expressions
    -> maplist(add_const_expr_msg(OpID,LocalIds),ExpensiveList)
    ; true)
    ; IsConstant = not_constant, IsExpensive=not_expensive,
    maplist(add_const_expr_msg(OpID,LocalIds),ExpensiveList)
).

check_initialisation_order(b(Subst,subst,Info),AllVars,AlreadyInit,OutInit) :-
    check_initialisation_order2(Subst,Info,AllVars,AlreadyInit,OutInit),!.

check_initialisation_order(Subst,AllVars,AlreadyInit,OutInit) :-
    % print('CHCK '), translate:print_subst(Subst),nl,
    get_accessed_vars(Subst,[],Modifies,Reads),
    check_subst_or_pred(Subst,Modifies,Reads,AllVars,AlreadyInit,OutInit).

check_initialisation_order2(choice([First|T]),Info,AllVars,AlreadyInit,OutInit) :- !,
    check_initialisation_order(First,AllVars,AlreadyInit,OutInit), % we pick the output of the first choice
    (T=[] -> true ; check_initialisation_order(b(choice(T),subst,Info),AllVars,AlreadyInit,_)).

check_initialisation_order2(parallel([First|T]),Info,AllVars,AlreadyInit,OutInit) :- !,
    check_initialisation_order(First,AllVars,AlreadyInit,OutInit1), % we pick the output of the first choice
    (T=[] -> OutInit=OutInit1
    ; check_initialisation_order2(parallel(T),Info,AllVars,AlreadyInit,OutInitRest),
    ord_union(OutInit1,OutInitRest,OutInit)
).

check_initialisation_order2(init_parallel(S),Info,AllVars,AlreadyInit,OutInit) :- !,
    check_initialisation_order(b(parallel(S),subst,Info),AllVars,AlreadyInit,OutInit).

check_initialisation_order2(sequence([First|T]),Info,AllVars) --> !,
    check_initialisation_order(First,AllVars),
    ({T=[]} -> [] ; check_initialisation_order(b(sequence(T),subst,Info),AllVars)).

check_initialisation_order2(any(_Ids,Pred,Subst),_Info,AllVars,AlreadyInit,OutInit) :- !,
    find_identifier_uses(Pred,[],Reads),
    check_subst_or_pred(Pred,[],Reads,AllVars,AlreadyInit,_), % check predicate reads are ok
    check_initialisation_order(Subst,AllVars,AlreadyInit,OutInit).

check_introduced_ids(Section,SectionID,SortedAllIds,TExpr,TNames) :-
    \+ ignore_constructor(TExpr),
    (member(TName,TNames),
    clash_warnings('local variable',SortedAllIds,Section,SectionID,TName)
    ; removed_identifier(TExpr,TName),
    clash_warnings('(removed) local variable',SortedAllIds,Section,SectionID,TName)
% TODO: also check duplicate_id_hides info fields ?
).

check_is_partial_function(value(Val),Info,Ctxt) :- nonvar(Val), Val=avl_set(AVL),
    is_not_avl_partial_function(AVL,DuplicateKey),!,
    avl_size(AVL,Size),
    translate_bvalue_with_limit(DuplicateKey,80,DKS),
    ajoin(['Relation of size ', Size, ' is not a function (value for ',Ctxt, '); duplicate key: '],Msg),
    add_warning(bmachine_static_checks,Msg,DKS,Info).

check_is_partial_function(_,_,_).

check_name_clashes(Machine) :-
    debug_println(10,'Checking for name clashes'),
    get_all_machine_ids(Machine,SortedAllIds),
    % for each operation, compare the parameter names with existing vars/constants
    get_section(operation_bodies,Machine,Operations),
    maplist(op_name_clashes(SortedAllIds),Operations),
    get_section(definitions,Machine,Defs),
    maplist(def_name_clashes(SortedAllIds),Defs).

check_operation_body(Body,OpID) :- b_top_level_operation(OpID),
    \+ b_top_level_feasible_operation(OpID),
    add_warning(bmachine_static_checks,'Infeasible body for operation:',OpID,Body),
    fail.

check_operation_body(Body,OpID) :-
    map_over_typed_bexpr(bmachine_static_checks:check_operation_body_var(OpID),Body),
    fail.

check_operation_body(Body,OpID) :-
    check_for_constant_expressions(Body,OpID,[],_,_).

check_operation_body_clashes(AllIds,Operation,TSubst) :-
    get_texpr_expr(TSubst,Subst),
    (local_variable_clash(Subst,TSubst,AllIds,Operation);
    illegal_op_call(Subst,Operation)).

check_operation_body_var(OpID,b(var(Parameters,Body),subst,_Pos)) :-
    get_texpr_ids(Parameters,Ps), sort(Ps,Uninitialised),
    get_accessed_vars(Body,[],_Modifies,Reads),
    ord_intersection(Uninitialised,Reads,URead),
    URead \= [],
    member(TID,Parameters), get_texpr_id(TID,ID),
    member(ID,URead),
    ajoin(['Possibly reading uninitialised variable in operation ',OpID,' : '],Msg),
    add_warning(bmachine_static_checks,Msg,ID,TID).

check_subst_or_pred(Subst,Modifies,Reads,AllVars,AlreadyInit,OutInit) :-
    ord_union(Modifies,AlreadyInit,OutInit), % after Subst we have initialised OutInit
    % below is already checked by type checker:
    %ord_subtract(Modifies,AllVars,IllegalAssignments),
    %(IllegalAssignments=[] -> true
    % ; add_warning(bmachine_static_checks,'INITIALISATION writes illegal variables: ',IllegalAssignments,Subst)),
    ord_intersection(Reads,AllVars,ReadFromSameMachine),
    (atomic_subst(Subst)
    -> ord_subtract(ReadFromSameMachine,AlreadyInit,IllegalReads)
    ; ord_subtract(ReadFromSameMachine,OutInit,IllegalReads) % we use OutInit: there could be an if with sequence inside
    ),
    (IllegalReads=[] -> true
    ; add_warning(bmachine_static_checks,'INITIALISATION reads variables which are not yet initialised: ',IllegalReads,Subst)).

check_symbolic_value(Ctxt,b(E,T,I)) :- check_aux(E,T,I,Ctxt).

check_symbolic_values(Var,Ctxt) :- var(Var),!,
    add_error(bmachine_static_checks,'Value is a variable',Ctxt).

check_symbolic_values(closure(_,_,Body),Ctxt) :- !,
    debug_format(19,'Checking symbolic value for ~w~n',[Ctxt]),
    map_over_typed_bexpr(check_symbolic_value(Ctxt),Body).

check_symbolic_values(_,_).

check_top_level(implication(_,B,C),MachName,SECT) :-
    (composed_predicate(B) ; composed_predicate(C)),!,
    add_warning(bmachine_static_checks,'Top-level implication (=>) in clause: ',MachName:SECT).

check_top_level(disjunct(_,B,C),MachName,SECT) :-
    (composed_predicate(B) ; composed_predicate(C)),!,
    add_warning(bmachine_static_checks,'Top-level disjunction (or) in clause: ',MachName:SECT).

check_top_level(equivalence(_,B,C),MachName,SECT) :-
    (composed_predicate(B) ; composed_predicate(C)),!,
    add_warning(bmachine_static_checks,'Top-level equivalence (<=>) in clause: ',MachName:SECT).

check_unused_ids :-
    b_is_unused_constant(ID),
    get_constant_span(ID,Span),
    % TO DO: check if the constant is used to define other used constants
    (get_preference(filter_unused_constants,true)
    -> add_message(bmachine_static_checks,'This constant is not used outside of the PROPERTIES/axioms (and is filtered away because FILTER_UNUSED preference is TRUE): ',ID,Span)
    ; add_message(bmachine_static_checks,'This constant is not used outside of the PROPERTIES/axioms: ',ID,Span)
    ),
    fail.

check_unused_ids.

check_values_in_state(ID) :- debug_format(19,'Checking values in state with id = ~w~n',[ID]),
    visited_expression(ID,State),
    state_corresponds_to_set_up_constants(State,EState),
    member(bind(VarID,Value),EState),
    check_symbolic_values(Value,VarID),
    fail.

check_values_in_state(_).

clash_local_warnings(AllIds,OperationId,Name,Pos) :-
    my_ord_member(Name,Class,Descr,AllIds), !,
    % we could check and see if Name is really visible from this location!
    % (see public_examples/B/Other/LustreTranslations/UMS_verif/M_UMS_verif.mch)
    ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a local variable in operation "', OperationId,'".'], Msg),
    add_warning(bmachine_static_checks,Msg,'',Pos).

clash_warnings(Context,AllIds,OpOrDef,OperationId,TName) :-
    get_texpr_id(TName,Name),
    my_ord_member(Name,Class,Descr,AllIds), !,
    ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a ',
    Context, ' in ',OpOrDef,' "', OperationId,'".'], Msg),
    add_warning(bmachine_static_checks,Msg,'',TName).

combine_expensive(not_expensive,IsExpensive2,IsExpensive) :- !, IsExpensive=IsExpensive2.

combine_expensive(is_expensive,depends_on_local_ids(Ids,_),Res) :- !,
    Res=depends_on_local_ids(Ids,is_expensive).

combine_expensive(is_expensive,_,IsExpensive) :- !, IsExpensive=is_expensive.

combine_expensive(depends_on_local_ids(Ids1,IE1),depends_on_local_ids(Ids2,IE2),Res) :- !,
    combine_expensive(IE1,IE2,IE),
    ord_union(Ids1,Ids2,Ids), Res=depends_on_local_ids(Ids,IE).

combine_expensive(depends_on_local_ids(Ids,IE1),IE2,Res) :- !,
    combine_expensive(IE1,IE2,IE),
    Res=depends_on_local_ids(Ids,IE).

combine_expensive(A,B,C) :- write(combine_expensive_uncovered(A,B,C)),nl,nl,C=A.

composed_predicate(A) :- functor(A,Operator,N),
    boolean_operator(Operator),
    % Some binary operators (conjunct, disjunct) can have a varying number of arguments.
    % See predicates associative_functor/1 and unflatten_assoc/4 in btypechecker.
    N >= 2.

def_name_clashes(AllIds,definition_decl(Name,DefType,_DefPos,Args,_RawExpr,_Deps)) :- !,
    (is_external_function_name(Name)
    -> true % do not check external predicates, functions, subst
    % they are not written by user and possibly not used and definitions are virtual and not used anyway
    ; findall(b(identifier(ID),any,[nodeid(IdPos)]),
    member(identifier(IdPos,ID),Args),ArgIds), % args can sometimes not be identifiers; see test 1711
    debug_println(4,checking_def(Name,DefType,Args,ArgIds)),
    include(clash_warnings('DEFINITION parameter',AllIds,'DEFINITION',Name),ArgIds,_ArgsCausingWarning)
% TO DO: check Body; for this we need a map_over_raw_expression to detect local variables introduced !
).

def_name_clashes(_,D) :- print(unknown_def(D)),nl.

esc_step(variables) :-
    check_all_variables_written,
    fail.

esc_step(machine_name) :-
    b_machine_name(Name),
    b_get_main_filename(Filename),
    get_modulename_filename(Filename,ModuleName),
    Name \= ModuleName,
    (atom_concat('MAIN_MACHINE_FOR_',RealName,Name) % see dummy_machine_name in bmachine_construction
    -> RealName \= ModuleName
    ; is_dummy_machine_name(Name,Filename)
    -> fail % dummy Rules DSL or Alloy machine name, do not create warning
    ; true
    ),
    (b_get_machine_header_position(Name,Span) -> true
    ; Span = src_position_with_filename(1,1,1,Filename)),
    get_specification_description(machine,MCH),
    ajoin(['Filename ',ModuleName,' does not match name of ', MCH, ': '],Msg),
    add_warning(bmachine_static_checks,Msg,Name,Span),
    fail.

esc_step(variables) :- debug_println(19,checking_identifiers_for_clashes),
    full_b_machine(Machine),
    local_quantified_variable_clashes(Machine),
    fail.

esc_step(operations) :- machine_type(MachName,abstract_machine),
    machine_operations(MachName,Ops),
    member(identifier(Span,OpName),Ops),
    atom_codes(OpName,Codes), member(46,Codes), % "." element of name
    % Section 7.23, paragraph 2 of Atelier-B handbook: in abstract machine we cannot use renamed operation names
    ajoin(['Operation name in abstract machine ',MachName,' is composed: '],Msg),
    add_warning(bmachine_static_checks,Msg,OpName,Span),
    fail.

esc_step(operations) :- debug_println(19,checking_operation_bodies),
    b_get_machine_operation(ID,_Res,_TParas,Body,_OType,_Pos),
    check_operation_body(Body,ID),
    fail.

esc_step(operations) :- portray_constant_expr_summary, fail.

esc_step(constants) :-
    check_concrete_constants, % check concrete_constants(.) states
    fail.

esc_step(unused_ids) :-
    check_unused_ids,
    fail.

esc_step(_).

extended_static_check_machine :-
    extended_static_check_machine(_).

extended_static_check_machine(Check) :-
    reset_static_check,
    esc_step(Check).

find_constant_expressions_in_operations(List) :-
    find_constant_expressions_in_operations(create_messages,List).

find_constant_expressions_in_operations(MsgOrWarn,_) :-
    reset_static_check,
    assert(store_expr(MsgOrWarn)),
    b_get_machine_operation(OpID,_Res,_TParas,Body,_OType,_Pos),
    check_for_constant_expressions(Body,OpID,[],_,_),
    fail.

find_constant_expressions_in_operations(_,list([Header|List])) :-
    Header = ['Operation', 'Occurence', 'Expr', 'LocalIds', 'Source'],
    portray_constant_expr_summary,
    findall(list([OpID,Count,ES,LocalIds,Src]),
    (const_expr(OpID,Count,BExpr,LocalIds),
    translate_bexpression_with_limit(BExpr,100,ES),
    get_tk_table_position_info(BExpr,Src)), List),
    reset_static_check.

generate_uninitialised_warning([],_) :- !.

generate_uninitialised_warning(Vars,Initialisation) :-
    Msg='Machine may not initialise some of its variables: ',
    add_warning(bmachine_static_checks,Msg,Vars,Initialisation).

get_all_machine_ids(Machine,SortedAllIds) :-
    % get all variables and constants that might clash
    get_section_ids(abstract_variables,Machine,'variable',AbsVars),
    get_section_ids(concrete_variables,Machine,'variable',ConcVars),
    get_section_ids(abstract_constants,Machine,'constant',AbsCons),
    get_section_ids(concrete_constants,Machine,'constant',ConcCons),
    get_section_ids(deferred_sets,Machine,'set',DefSets),
    get_section_ids(enumerated_sets,Machine,'set',EnumSets),
    get_section_ids(enumerated_elements,Machine,'set element',EnumElems),
    % enumerated b_get_named_machine_set(GlobalSetName,ListOfConstants) + b_get_machine_set(S)
    append([AbsVars,ConcVars,AbsCons,ConcCons,DefSets,EnumSets,EnumElems],AllIds),
    keyword_clash(AllIds),
    sort(AllIds,SortedAllIds).

get_descr(Pos,Section,Descr) :-
    (extract_span_description(Pos,Descr) -> true
    ; ajoin(['from section ',Section],Descr) ).

get_machine_variables(Machine,SortedAllVars) :-
    % get all variables that should be initialised
    get_section(abstract_variables,Machine,AbsVars),
    get_section(concrete_variables,Machine,ConcVars),
    append(AbsVars,ConcVars,TAllVars),
    get_texpr_ids(TAllVars,AllVars),
    sort(AllVars,SortedAllVars).

get_section_ids(Section,Machine,Class,ResultList) :-
    get_section(Section,Machine,Vars),
    findall(machine_id(ID,Class,Pos,Section),
    (member(TID,Vars),get_texpr_id(TID,ID),get_texpr_info(TID,Pos)),ResultList).

get_sub_predicate(Clause,Pred,Kind,Name,SubPred) :-
    conjunction_to_list(Pred,Preds),
    l_get_sub_predicate(Clause,Preds,Kind,Name,SubPred).

get_typed_section(Kind,Name,SubPred) :-
    b_get_properties_from_machine(P), get_specification_description(properties,PS),
    get_sub_predicate(PS,P,Kind,Name,SubPred).

get_typed_section(Kind,Name,SubPred) :-
    b_get_invariant_from_machine(P), get_specification_description(invariants,PS),
    get_sub_predicate(PS,P,Kind,Name,SubPred).

get_typed_section(Kind,Name,SubPred) :-
    get_specification_description(assertions,APS), ajoin(['(dynamic) ',APS],AS),
    b_get_dynamic_assertions_from_machine(Ps),
    l_get_sub_predicate(AS,Ps,Kind,Name,SubPred).

get_typed_section(Kind,Name,SubPred) :-
    get_specification_description(assertions,APS), ajoin(['(static) ',APS],AS),
    b_get_static_assertions_from_machine(Ps),
    l_get_sub_predicate(AS,Ps,Kind,Name,SubPred).

get_typed_section(operation,OpName,P) :- b_get_machine_operation(OpName,_Results,_Parameters,P).

ignore_constructor(b(recursive_let(_,_),_,_)).

illegal_op_call(operation_call(CalledOperation,Results,_Parameters),Operation) :-
    member(TID,Results), \+ get_texpr_id(TID,_),
    (get_texpr_id(CalledOperation,op(CalledId)) -> true ; CalledId=CalledOperation),
    ajoin(['Return value of operation call to ',CalledId,' must be stored in identifier within:'],Msg),
    add_error(bmachine_static_checks,Msg,Operation,TID).

initialises_all_variables(Machine) :-
    get_section(initialisation,Machine,Initialisation),
    % check wich variables are read / modified by the initialisation
    get_accessed_vars(Initialisation,[],Modifies,_Reads),
    get_machine_variables(Machine,SortedAllVars),
    % check for each variable, if the initialisation modifies it
    exclude(is_initialised(Modifies),SortedAllVars,Uninitialised),
    % generate a warning if unitialised is not empty
    generate_uninitialised_warning(Uninitialised,Initialisation),
    % now check order of initialisation sequences
    check_initialisation_order(Initialisation,SortedAllVars,[],_).

introduced_ids(forall(IDs,_,_),IDs).

introduced_ids(exists(IDs,_),IDs). % % are there more relevant cases? TODO: use syntaxtraversion

introduces_local_variable(var(Parameters,_),ID) :-
    % currently B-interpreter cannot correctly deal with this in the context of operation_call
    member(TID,Parameters), get_texpr_id(TID,ID).

is_constant_expression(value(_),not_expensive).

is_constant_expression(max_int,not_expensive).

is_constant_expression(min_int,not_expensive).

is_constant_expression(boolean_false,not_expensive).

is_constant_expression(boolean_true,not_expensive).

is_constant_expression(empty_set,not_expensive).

is_constant_expression(empty_sequence,not_expensive).

is_constant_expression(integer(_),not_expensive).

is_constant_expression(real(_),not_expensive).

is_constant_expression(string(_),not_expensive).

is_constant_expression(bool_set,not_expensive).

is_constant_expression(freetype_set(_),not_expensive).

is_constant_expression(real_set,not_expensive).

is_constant_expression(string_set,not_expensive).

is_constant_expression(typeset,not_expensive).

is_constant_expression(integer_set(_),not_expensive).

is_constant_expression(unary_minus(_),not_expensive).

is_constant_expression(add(_,_),not_expensive).

is_constant_expression(minus(_,_),not_expensive).

is_constant_expression(multiplication(_,_),not_expensive).

is_constant_expression(couple(_,_),not_expensive).

is_constant_expression(record_field(_,_),not_expensive).

is_constant_expression(rec(_),not_expensive).

is_constant_expression(set_extension(_),not_expensive).

is_constant_expression(sequence_extension(_),not_expensive).

is_constant_expression(interval(_,_),not_expensive).

is_constant_expression(first_of_pair(_),not_expensive).

is_constant_expression(second_of_pair(_),not_expensive).

is_constant_expression(record_field(_,_),not_expensive).

is_constant_expression(pow_subset(_),not_expensive).

is_constant_expression(fin_subset(_),not_expensive).

is_constant_expression(pow1_subset(_),not_expensive).

is_constant_expression(fin1_subset(_),not_expensive).

is_constant_expression(seq(_),not_expensive).

is_constant_expression(seq1(_),not_expensive).

is_constant_expression(iseq(_),not_expensive).

is_constant_expression(iseq1(_),not_expensive).

is_constant_expression(cartesian_product(_,_),not_expensive).

is_constant_expression(mult_or_cart(_,_),not_expensive).

is_constant_expression(relations(_,_),not_expensive).

is_constant_expression(relations(_,_),not_expensive).

is_constant_expression(struct(_),not_expensive).

is_constant_expression(composition(_,_),is_expensive).

is_constant_expression(image(_,_),is_expensive).

is_constant_expression(iteration(_,_),is_expensive).

is_constant_expression(concat(_,_),is_expensive).

is_constant_expression(reflexive_closure(_),is_expensive).

is_constant_expression(closure(_),is_expensive).

is_constant_expression(union(_,_),is_expensive).

is_constant_expression(intersection(_,_),is_expensive).

is_constant_expression(_,is_expensive).

is_constant_expression(identifier(ID),LocalIds,Kind) :- !,
    (ord_member(ID,LocalIds) -> Kind = depends_on_local_ids([ID],not_expensive)
    ; b_is_constant(ID) -> Kind = not_expensive
    ; b_get_machine_set(ID) -> Kind = not_expensive
    ; lookup_global_constant(ID,_) -> Kind = not_expensive). % enumerated set element

is_constant_expression(Expr,_,IsExpensive) :- is_constant_expression(Expr,IsExpensive).

is_dummy_machine_name(Name,_) :- atom_prefix('__RULES_MACHINE_Main',Name).

is_dummy_machine_name(alloytranslation,_) :- animation_minor_mode(alloy).

is_dummy_machine_name('DEFINITION_FILE',Filename) :- classical_b_mode,
    get_filename_extension(Filename,'def').

is_expression(b(_,T,_)) :- \+ pred_or_subst(T).

is_initialised(Modifies,Id) :-
    memberchk(Id,Modifies).

keyword_clash(AllIds) :-
    member(machine_id(Name,Class,Pos,Section),AllIds),
    is_b_keyword(Name,_),
    get_descr(Pos,Section,Descr),
    ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a classical B keyword (may lead to unexpected parse or type errors when entering formulas unless you surround it by backquotes: `',Name,'`).'], Msg),
    (classical_b_mode
    -> add_message(bmachine_static_checks,Msg,'',Pos) % user probably uses new backquote syntax already
    ; add_warning(bmachine_static_checks,Msg,'',Pos)
    ),
    fail.

keyword_clash(_).

l_check_for_const([],_OpID,_,_,is_constant,not_expensive,[]).

l_check_for_const([H|T],OpID,LocalIds,NewQuantLocalIds,AreAllConstant,IsExpensive,ExpResList) :-
    check_for_constant_expressions(H,OpID,LocalIds,IsConstant,IsExpensive0),
    project_is_expensive(IsExpensive0,NewQuantLocalIds,IsExpensive1), % project on NewIds introduced at top-level
    (IsConstant=is_constant
    -> (IsExpensive1=is_expensive, is_expression(H) % currently we only look for constant expressions
    -> ExpResList = [H|TR] % add to list for add_const_expr_msg
    ; ExpResList=TR),
    l_check_for_const(T,OpID,LocalIds,NewQuantLocalIds,AreAllConstant,IsExpensive2,TR),
    combine_expensive(IsExpensive1,IsExpensive2,IsExpensive)
    ; AreAllConstant=not_constant, IsExpensive=not_expensive,
    l_check_for_const(T,OpID,LocalIds,NewQuantLocalIds,_,_,ExpResList)).

l_get_sub_predicate(Clause,Preds,Kind,Name,SubPred) :-
    member(SubPred,Preds),
    (get_texpr_label(SubPred,Label)
    -> Kind = predicate, ajoin([Label,'" in clause "',Clause],Name)
    ; Kind = clause, Name=Clause).

local_quantified_variable_clashes(Machine) :-
    get_all_machine_ids(Machine,SortedAllIds),
    (get_typed_section(Sec,SecID,Pred),
    debug_println(19,checking_local_quantified_variable_clashes(Sec,SecID)),
    map_over_typed_bexpr_with_names(bmachine_static_checks:check_introduced_ids(Sec,SecID,SortedAllIds),Pred)
    ;
    check_definition_clashes(SortedAllIds)
    ),
    fail.

local_quantified_variable_clashes(_).

local_variable_clash(Subst,TSubst,AllIds,Operation) :-
    introduces_local_variable(Subst,ID),
    clash_local_warnings(AllIds,Operation,ID,TSubst).

my_ord_member(Name,Class,Descr,[machine_id(Name1,_,_,_)|T]) :-
    Name @> Name1, !,
    my_ord_member(Name,Class,Descr,T).

my_ord_member(Name,Class,Descr,[machine_id(Name,Class,Pos,Section)|_]) :-
    get_descr(Pos,Section,Descr).

op_name_clashes(AllIds,Operation) :-
    get_texpr_expr(Operation,operation(IdFull,Results,Params,Subst)),
    %get_texpr_id(IdFull,op(Id)),
    IdFull = b(identifier(op(Id)),Type,Info),
    (get_preference(clash_strict_checks,true)
    -> include(clash_warnings('Operation name',AllIds,operation,Id),[b(identifier(Id),Type,Info)],_NameCausingWarning) % fix PROB-60
    ; true),
    include(clash_warnings('Operation parameter',AllIds,operation,Id),Params,_ParamsCausingWarning),
    include(clash_warnings('Operation result variable',AllIds,operation,Id),Results,_ResultsCausingWarning),
    (map_over_typed_bexpr(bmachine_static_checks:check_operation_body_clashes(AllIds,Id),Subst),fail ; true).

portray_constant_expr_summary :-
    findall(Count,const_expr_hash_count(_,Count),LC),
    length(LC,Len),
    format('Constant expressions found: ~w~n',[Len]),
    sumlist(LC,Total),
    format('Total # of occurrences: ~w~n',[Total]).

pred_or_subst(pred).

pred_or_subst(subst).

project_is_expensive(depends_on_local_ids(LocalIds,IE),SQuantifiedNewIds,Res) :- !,
    ord_subtract(LocalIds,SQuantifiedNewIds,NewLocalIds),
    (NewLocalIds = [] -> Res = IE % is_expensive/not_expensive
    ; Res= depends_on_local_ids(NewLocalIds,IE)).

project_is_expensive(IE,_,IE).

register_constant_expression(BExpr,OpID,LocalIds,Count,MsgOrWarn) :-
    norm_check(BExpr,Norm), my_term_hash(Norm,Hash),
    (retract(const_expr_hash_count(Hash,C)) -> Count is C+1 ; Count=1),
    assert(const_expr_hash_count(Hash,Count)),
    (store_expr(MsgOrWarn) -> assert(const_expr(OpID,Count,BExpr,LocalIds)) ; MsgOrWarn=message).

removed_identifier(b(_,_,Infos),TId) :-
    member(was(WAS),Infos),
    introduced_ids(WAS,IDs),
    % this happens in EnumSetClash2.mch
    member(TId,IDs).

reset_static_check :- retractall(const_expr_hash_count(_,_)),
    retractall(const_expr(_,_,_,_)), retractall(store_expr(_)).

static_check_main_machine(Machine) :-
    debug_println(19,'Running static machine checks'),
    initialises_all_variables(Machine),
    check_name_clashes(Machine).

toplevel_raw_predicate_sanity_check(invariant,MachName,RawPredicate,Infos) :-
    member(has_variables,Infos), % otherwise it is ok to have just a single disjunt, implication,...
    check_top_level(RawPredicate,MachName,'INVARIANT'),
    fail.

toplevel_raw_predicate_sanity_check(properties,MachName,RawPredicate,Infos) :-
    member(has_constants,Infos), % otherwise it is ok to have just a single disjunt, implication,...
    check_top_level(RawPredicate,MachName,'PROPERTIES'),
    fail.

toplevel_raw_predicate_sanity_check(_,_,_,_).