pathes

application_path2(Dir) :-
    current_prolog_flag(system_type,development), % other value of system_type flag is runtime
    % try and find location of src/module_information.pl
    current_module(module_information,MFile),parent_dir(MFile,SrcDir,_),
    remove_src_dir(SrcDir,Dir).

application_path2(Dir) :-
    \+(current_prolog_flag(system_type,development)),
    environ('SP_APP_DIR',Dir). /* /usr/local/bin/sicstus on development systems */

application_path2(Dir) :-
    \+(current_prolog_flag(system_type,development)),
    environ('SP_STARTUP_DIR',Dir).

check_if_hard_wired(Alias, _Prefix, _Dir, Full) :-
    compile_time_env_path(Alias,Full),!.

check_if_hard_wired(_Alias, Prefix, Dir, Full) :-
    atom_concat(Prefix,Dir,Full).

compiletime_application_path(Dir) :-
    compile_time_env_path(prob_comp_home,Dir),!.

compiletime_application_path(Dir) :-
    runtime_application_path(Dir).

is_correct_prob_home_path(D) :- % print(trying_as_prob_home_path(D)),nl,nl,
    atom_concat(D,'/lib/probcliparser.jar',ConParser),
    file_exists(ConParser).

lookup_env_path(Pathname, Varname) :-
    ( environ(Varname,Value) ->
    print('Hard-wired path for alias '),print(Pathname),print(': '),print(Value),nl,
    assertz(compile_time_env_path(Pathname,Value))
    ;
    true).

parent_dir(FullFile,Dir,Basename) :-
    atom_chars(FullFile,CFullFile), % "path/to/file"
    reverse(CFullFile,RCFullFile), % "elif/ot/htap"
    append(RCFile,['/'|RCDir],RCFullFile),!, % "elif" "/ot/htap"
    reverse(RCFile,CFile),reverse(['/'|RCDir],CDir), % "file" "path/to/"
    atom_chars(Basename,CFile),atom_chars(Dir,CDir).

parent_dir_test :-
    parent_dir_test1, parent_dir_test2.

parent_dir_test1 :-
    parent_dir('/aaaa/bbb/cc/d.app',D,B),D=='/aaaa/bbb/cc/',B=='d.app'.

parent_dir_test2 :-
    parent_dir('/aaaa/bbb/cc/',D,B),D=='/aaaa/bbb/cc/',B==''.

remove_src_dir(Orig,Dir) :-
    atom_codes(Orig,COrig),
    ( append(CDir,"/src/",COrig) -> true
    ; append(CDir,"/src",COrig) -> true
    ; append(CDir,"/src/proz",COrig) -> true
    ; append(CDir,"/src/proz/",COrig) -> true
    ; append(CDir,"/tests/",COrig) -> true
    ; append(CDir,"/tests",COrig) -> true
    ; append(CDir,"/",COrig) -> true
    ; COrig=CDir),
    atom_codes(Dir,CDir).

rev([], Reversed, Reversed).

rev([Head|Tail], Sofar, Reversed) :-
    rev(Tail, [Head|Sofar], Reversed).

reverse(List, Reversed) :-
    rev(List, [], Reversed).

runtime_application_path(Dir) :-
    ( environ('PROB_HOME',Dir) -> % the user has set the environment variable PROB_HOME and thus overrides any other setting
    true % the Rodin plugin used this mechanism
    ; application_path2(Dir),is_correct_prob_home_path(Dir) ->
    true
    ; application_path2(D),absolute_file_name(D,D1),parent_dir(D1,Dir,_),
    is_correct_prob_home_path(Dir) ->
    true
    ; compile_time_env_path(prob_comp_home,Dir) -> % e.g. Debian/Ubuntu systems: the path was hard-wired at compile-time
    true
    ; % usually a run from source code, where we the current directory is prob/src
    current_directory(Current), remove_src_dir(Current,Dir)).

set_compile_time_dev_search_pathes :-
    compiletime_application_path(App),
    set_search_path(testsrc, App, '/tests'). % should never be used from main sources!

set_compile_time_search_pathes :-
    compiletime_application_path(App),
    %format('~n ProB compile time application path: ~w~n~n',[App]),
    set_search_path(extension, App, '/extensions'),
    set_search_path(probsrc, App, '/src'),
    set_search_path(chrsrc, App, '/src/chr'),
    set_search_path(cbcsrc, App, '/src/cbc'),
    set_search_path(probcspsrc, App, '/src/cia'),
    set_search_path(probltlsrc, App, '/src/ltl'),
    set_search_path(probporsrc, App, '/src/por'),
    set_search_path(probpgesrc, App, '/src/pge'),
    set_search_path(prozsrc, App, '/src/proz'),
    set_search_path(kodkodsrc, App, '/src/kodkod'),
    set_search_path(symbolic_model_checker, App, '/src/symbolic_model_checker'),
    set_search_path(wdsrc, App, '/src/well_def'),
    %set_search_path(plugins, App, '/plugins'),
    %set_search_path(abstract_domains, App, '/plugins/absint/domains'),
    set_search_path(tclsrc, App, '/tcl'),
    %set_search_path(probpromela,App,'/src/promela'),
    set_search_path(pltablesrc, App, '/src/pltables'),
    set_search_path(prob_rewrite_rules, App, '/src/rewrite_rules'),
    set_search_path(smtlib_solver, App, '/src/smtlib_solver'),
    set_search_path(smt_solvers_interface, App, '/src/smt_solvers_interface'),
    set_search_path(disproversrc, App, '/src/disprover'),
    set_search_path(cdclt_solver, App, '/src/cdclt_solver'),
    set_search_path(code2vec, App, '/src/code2vec'),
    set_search_path(synthesis, App, '/src/synthesis'),
    set_search_path(visbsrc, App, '/src/visb'),
    set_search_path(dotsrc, App, '/src/dot'),
    set_search_path(covsrc, App, '/src/coverage'),
    set_search_path(tcltkuisrc, App, '/src/tcltk'),
    set_search_path(extrasrc, App, '/src/extra'),
    set_search_path(symsrc, App, '/src/symmetry'),
    set_search_path(library_plspec, App, '/extensions/plspec_libraries'). % patched libraries for plspec

set_compiled_prob_pathes(_App) :-
    % print('Adding to library directories:'),nl,
    % assertz(user:library_directory('/usr/local/sicstus4.6/bin/sp-4.6.0/sicstus-4.6.0/library/')).
    true.

set_search_path(Alias, Prefix, Dir) :-
    check_if_hard_wired(Alias, Prefix, Dir, Full),
    %% print(setting_path(Alias,Full)),nl,
    ( catch( user:file_search_path(Alias,Full), _, fail)
    -> true % Alias already set to same value
    ; catch( retractall(user:file_search_path(Alias,_)), _, true), % remove any old defintion
    assertz(user:file_search_path(Alias,Full)) % , print(setting_search_path(Alias,Full)),nl
).

set_search_pathes :-
    runtime_application_path(App),
    %print(runtime_application_path(App)),nl,
    set_search_path(prob_home, App, ''),
    set_search_path(examples, App, '/../probprivate/public_examples'),
    set_search_path(prob_lib, App, '/lib'),
    set_search_path(prob_tcl, App, '/tcl'),
   
    check_if_hard_wired(prob_lib, App, '/lib', LibDir),
    ( catch(user:library_directory(LibDir), _, fail) -> true % ,print(already_set(LibDir)),nl
    ;
    catch( retractall(user:library_directory(_)), _, true), % remove any old defintion
    assertz(user:library_directory(LibDir))),
    (current_prolog_flag(system_type,development)
    -> true
    ; set_compiled_prob_pathes(App)
).