probsocket_proxy.pl

codes_from_server(Codes) :-
    server_stream(Stream),
    read_from_server2(Stream,Codes).

codes_to_client(Codes) :-
    client_stream(Stream),
    put_codes(Codes, Stream),
    flush_output(Stream).

connect_to_server :-
    retractall(server_stream(_)),
    server_port(Port),
    format('Please start probcli -s ~w (from source or binary)~nTrying to connect~n',[Port]),
    catch( ( socket_client_open(localhost:Port,Stream,[type(text)]),
    assert( server_stream(Stream) )),
    error(system_error, system_error(E)),
    retry_connect_to_server(E)).

get_server_probcli_version_and_user_interrupt_ref(Git,UserSignalRef) :-
    term_to_server(get_version(Maj,Min,Service,Qual,GitRevision,LastChanged,Prolog),
    ['Maj'=Maj,'Min'=Min,'Service'=Service,'Qual'=Qual,
    'GitRevision'=GitRevision,'LastChanged'=LastChanged,'Prolog'=Prolog]),
    codes_from_server(Codes1),
    append(Codes1,".",C1),
    (read_from_codes(C1,yes(Bindings)),
    member('GitRevision'=Git,Bindings) -> true
    ; Git='?'),
    % note these two calls should not perform call_backs or progress info
    term_to_server(get_user_signal_reference(Ref),['Ref'=Ref]),
    codes_from_server(Codes2),
    (read_from_codes_dot(Codes2,yes(Bindings2)),
    member('Ref'=UserSignalRef,Bindings2) -> true
    ; UserSignalRef='0').

get_server_result :-
    %format(user_error,'@proxy waiting for probcli result~n',[]),
    codes_from_server(Codes), % receive a result from probcli
    %format(user_error,'@proxy probcli result: ~s~n',[Codes]),
    codes_to_client(Codes), % pass result to ProB2 Java
    read_from_codes_dot(Codes,Term),
    process_probcli_result(Term).

get_variable_name([],V,N) :- format('Unknown variable: ~w~n',[V]), N='_'.

get_variable_name([Name=Var|_],V,N) :-
    Var==V,!,N=Name.

get_variable_name([_|Rest],V,N) :-
    get_variable_name(Rest,V,N).

process_probcli_result(progress(_)) :- !, % just progress info; wait for next result
    get_server_result.

process_probcli_result(call_back(_)) :- !, % await result of call_back from ProB2 Java
    read_socket_loop. % actually: this does not change the way the proxy ping-pongs results

process_probcli_result(_) :- read_socket_loop. % await next ProB2 Java command to probcli

process_term(end_of_file,_) :- !, stop.

process_term(halt,_) :- !, stop.

process_term(Term,Vars) :-
    term_to_server(Term,Vars), % send to probcli
    get_server_result.

put_codes([],_).

put_codes([C|Rest],Stream) :-
    put_code(Stream,C),
    put_codes(Rest,Stream).

read_from_codes_dot(Codes,Term) :- append(Codes,".",C1), read_from_codes(C1,Term).

read_from_server2(Stream,Codes) :-
    get_code(Stream, Code),
    ( Code == -1 ->
    Codes = [],
    retractall(server_stream(_))
    ; Code == 1 ->
    Codes = [1]
    ; otherwise ->
    Codes = [Code|Rest],
    read_from_server2(Stream,Rest)).

read_socket_loop :-
    %format(user_error,'@proxy reading term from ProB2~n',[]),
    read_term_from_socket(Term,Vars),
    %format(user_error,'@proxy read term ~w (~w) from ProB2~n',[Term,Vars]),
    process_term(Term,Vars),
    read_socket_loop.

read_term_from_socket(Term,Vars) :-
    client_stream(Stream),
    catch(read_term(Stream, Term, [variable_names(Vars)]), E, syntax_error(E)).

retry_connect_to_server(E) :-
    format('Error when trying to connect to server - retry in a second (~w)~n',[E]),
    sleep(1),
    connect_to_server.

runtime_entry(start) :- start.

save(Port) :-
    assert( server_port(Port) ),
    save_program('probproxy.sav').

start :-
    get_server_probcli_version_and_user_interrupt_ref(GitRevision,UserSignalRef),
   
    socket_server_open(Port, Socket),
    % mimicking output of probcli -sf
    format('Starting Socket Server.~n',[]),
    current_directory(AppDir),
    format('Application Path: ~w~n',[AppDir]),
    format('Port: ~w~n', [Port]),
    format('probcli revision: ~w~n',[GitRevision]),
    format('user interrupt reference id: ~w~n',[UserSignalRef]),
    format('-- starting command loop --~n', []),
    flush_output,
    socket_server_accept(Socket, _Client, Stream, [type(text),encoding(utf8)]),
    assert( client_stream(Stream) ),
    read_socket_loop,
    socket_server_close(Socket).

stop :-
    format('Stopping proxy server, bye!~n',[]),
    halt.

syntax_error(E) :-
    format('Got syntax error, get your Java code right!~n~w~n', [E]),
    stop.

term_to_server(Term,Vars) :-
    ( server_stream(Stream) ->
    write_varterm(Stream,Term,Vars),
    write(Stream,'.\n'),
    flush_output(Stream)
    ; otherwise ->
    connect_to_server,
    term_to_server(Term,Vars)).

write_varterm(Stream,Term,Vars) :-
    ( var(Term) ->
    get_variable_name(Vars,Term,Varname),
    write(Stream,Varname)
    ; ground(Term) ->
    write_term(Stream,Term,[quoted(true)])
    ; otherwise ->
    Term =.. [Functor|Args],
    write_term(Stream,Functor,[quoted(true)]),
    write(Stream,'('),
    write_varterm_l(Args,Stream,Vars),
    write(Stream,')')).

write_varterm_l([Arg|Rest],Stream,Vars) :-
    write_varterm(Stream,Arg,Vars),
    write_varterm_l2(Rest,Stream,Vars).

write_varterm_l2([],_Stream,_Vars).

write_varterm_l2([Arg|Rest],Stream,Vars) :-
    write(Stream,','),
    write_varterm_l([Arg|Rest],Stream,Vars).