msg_interop

get_bind_value([],[]).

get_bind_value([bind(_,Val)|T],[Val|VT]) :- get_bind_value(T,VT).

get_state_chunks(csp_and_b(CSP,BState),[CSP|Vals]) :- !,
    % TO DO: partition CSP into chunks
    get_bind_value(BState, Vals).

get_state_chunks(BState,Vals) :- % extract values from environment of the form [bind(x,Vx),...]
    get_bind_value(BState, Vals).

put_long_successors([], _Msg).

put_long_successors([H|T], Msg) :-
    get_state_chunks(H, Vals),
    put_termlist(Msg, Vals),
    put_long_successors(T, Msg).

put_matrix(Msg, M) :-
    length(M, MLength),
    put_number(Msg, MLength),
    put_rows(M, Msg).

put_may_write_matrix(Msg, M) :- csp_with_bz_mode,!,
    write_matrix(Msg, [ ['$CSP',[]] | M], may_write_matrix).

put_may_write_matrix(Msg, M) :- write_matrix(Msg, M, may_write_matrix).

put_rows([], _Msg).

put_rows([[TransitionGroup, VarList]|R], Msg) :-
    write_and_put_chunk(Msg, TransitionGroup),
    put_termlist(Msg, VarList),
    put_rows(R, Msg).

put_short_successors([], _Pattern, _Defaults, _ShortState, _Msg).

put_short_successors([LongState|_], LongState, Defaults, ShortState, Msg) :-
    put_termlist_short(ShortState, Defaults, Msg), fail.

put_short_successors([_|MoreStates], Pattern, Defaults, ShortState, Msg) :-
    put_short_successors(MoreStates, Pattern, Defaults, ShortState, Msg).

put_successors(long, States, Msg) :-
    put_long_successors(States, Msg).

put_successors(Pattern-ShortState-Defaults, States, Msg) :-
    put_short_successors(States, Pattern, Defaults, ShortState, Msg).

put_termlist(Msg, TermList) :-
    length(TermList,ListSize),
    put_number(Msg, ListSize),
    put_termlist_elements(TermList, Msg).

put_termlist_elements([], _Msg).

put_termlist_elements([H|T], Msg) :-
    write_and_put_chunk(Msg, H),
    put_termlist_elements(T, Msg).

put_termlist_elements_short([], [], _).

put_termlist_elements_short([bind(Varname, Val)|T], [bind(Varname, Default)|DefaultT], Msg) :-
    (Val == term(undefined)
    -> write_and_put_chunk(Msg, Default)
    ; write_and_put_chunk_written(Msg, Val)),
    put_termlist_elements_short(T, DefaultT, Msg).

put_termlist_short(TermList, Defaults, Msg) :-
    length(TermList,ListSize),
    put_number(Msg, ListSize),
    put_termlist_elements_short(TermList, Defaults, Msg).

submsg_type_to_int(initial_state, 1).

submsg_type_to_int(transition_group_list, 2).

submsg_type_to_int(variables_name_list, 3).

submsg_type_to_int(variables_type_list, 4).

submsg_type_to_int(state_label_matrix, 5).

submsg_type_to_int(may_write_matrix, 6).

submsg_type_to_int(must_write_matrix, 7).

submsg_type_to_int(reads_action_matrix, 8).

submsg_type_to_int(reads_guard_matrix, 9).

submsg_type_to_int(guard_info_matrix, 10).

submsg_type_to_int(guard_label_matrix, 11). % split invariant and guard matrices

submsg_type_to_int(necessary_enabling_set, 12).

submsg_type_to_int(necessary_disabling_set, 13).

submsg_type_to_int(do_not_accord_matrix, 14).

submsg_type_to_int(may_be_coenabled_matrix, 15).

submsg_type_to_int(ltl_label_matrix, 16).

write_and_put_chunk(Msg, C) :-
    fast_buf_write(C,L,A),
    put_chunk(Msg, A, L).

write_and_put_chunk_written(Msg, C) :-
    fast_buf_write(C,L,A),
    put_chunk_written(Msg, A, L).

write_chunklist(Msg, List, Type) :-
    create_message(FreshMsg),
    submsg_type_to_int(Type, HeaderNum),
    put_number(FreshMsg, HeaderNum),
    put_termlist(FreshMsg, List),
    append_message(Msg, FreshMsg).

write_matrix(Msg, Matrix, Type) :-
    create_message(FreshMsg),
    submsg_type_to_int(Type, HeaderNum),
    put_number(FreshMsg, HeaderNum),
    put_matrix(FreshMsg, Matrix),
    append_message(Msg, FreshMsg).