b_interpreter.pl

b_compute_cases(Cases,LS,S,CompCases,Values,WF) :-
    b_compute_cases2(Cases,LS,S,CompCases,Values,[],WF).

b_compute_cases2([],_,_,[],AllValues,AllValues,_).

b_compute_cases2([CaseOr|Crest],LS,S,[comp_case_or(Values,Subst)|CCrest],AllValues,VR,WF) :-
    get_texpr_expr(CaseOr,case_or(Exprs,Subst)),
    b_compute_cases3(Exprs,LS,S,Values,AllValues,VI,WF),
    b_compute_cases2(Crest,LS,S,CCrest,VI,VR,WF).

b_compute_cases3([],_,_,[],Values,Values,_).

b_compute_cases3([Expr|Erest],LS,S,[Value|Vrest],[Value|ValuesI],Values,WF) :-
    b_compute_expression(Expr,LS,S,Value,WF),
    b_compute_cases3(Erest,LS,S,Vrest,ValuesI,Values,WF).

b_execute_statement2(case(Expression,Cases,Else), _, LocalState, InState, OutState,WF,case(Nr,Path),OR) :- !,
    % According to the AtelierB handbook the cases must be distinct one-by-one; Schneider's book does not seem to require that
    % ProB will at the moment allow multiple entries in which case CASE is non-deterministic
    % Atelier-B will actually only allow literal integers, booleans, enumerated set values as cases !
    b_compute_expression(Expression,LocalState,InState,EValue,WF),
    b_compute_cases(Cases,LocalState,InState,CompCases,AllEitherValues,WF),
    ground_det_wait_flag(WF),
    ( nth1(Nr, CompCases, comp_case_or(ListOfValues, Body)),
    member(EitherValue,ListOfValues),
    equal_object_wf(EValue,EitherValue,case_statement,WF),
    ground_det_wait_flag(WF),
    b_execute_inner_statement(Body,LocalState,InState,OutState,WF,Path,OR)
    ; b_not_member_of_value_lists(AllEitherValues,EValue,WF),
    ground_det_wait_flag(WF),
    % print_message(else_case(Body2)),
    Nr=else,
    b_execute_inner_statement(Else,LocalState,InState,OutState,WF,Path,OR)
).

b_not_member_of_value_lists([],_,_WF).

b_not_member_of_value_lists([EitherValue|Rest],Value,WF) :-
    not_equal_object_wf(Value,EitherValue,WF),
    b_not_member_of_value_lists(Rest,Value,WF).

is_bound_state(X) :- var(X),!,fail.

is_bound_state([]).

is_bound_state([H|T]) :- nonvar(H), H=bind(ID,_), ground(ID),
    is_bound_state(T).

pe_print(X) :- print('*** PE INFO: '), print(X),nl.