1		% (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(pathes,[
6		set_search_pathes/0, % install run-time search pathes
7		runtime_application_path/1
8		]).
9
10		:- use_module(module_information).
11
12		:- module_info(group,infrastructure).
13		:- module_info(description,'This module contains code to compute compile-time and runtime-pathes.').
14
15		:- use_module(library(system),[environ/2]).
16		:- use_module(library(file_systems),[file_exists/1,
17		current_directory/1]).
18		:- use_module(library(lists),[reverse/2]).
19
20		:- multifile user:file_search_path/2.
21		:- dynamic user:file_search_path/2.
22
23		% some pathes may be set by environment variables during compilation,
24		:- dynamic compile_time_env_path/2.
25		lookup_env_path(Pathname, Varname) :-
26		( environ(Varname,Value) ->
27		print('Hard-wired path for alias '),print(Pathname),print(': '),print(Value),nl,
28		assert(compile_time_env_path(Pathname,Value))
29		; otherwise ->
30		true).
31		% compile-time pathes
32		:- lookup_env_path(prob_comp_home,'PROB_COMP_HOME'). % hard-wired version of the runtime_application_path
33		% This is used on systems where it absolutely clear where the
34		% ProB's application directory will be, namely Debian/Ubuntu packages
35		% run-time pathes
36		:- lookup_env_path(prob_home,'PROB_HOME').
37		:- lookup_env_path(examples,'PROB_EXAMPLES'). % hard-wired pathes, see above (about Debian/Ubuntu packages)
38		:- lookup_env_path(prob_lib,'PROB_LIB'). % hard-wired pathes, see above (about Debian/Ubuntu packages)
39		:- lookup_env_path(prob_tcl,'PROB_TCL'). % hard-wired pathes, see above (about Debian/Ubuntu packages)
40
41		% removes an (optional) trailing /src directory from the path,
42		% the result will not end with a slash
43		remove_src_dir(Orig,Dir) :-
44		atom_codes(Orig,COrig),
45	?	( append(CDir,"/src/",COrig) -> true
46		; append(CDir,"/src",COrig) -> true
47		; append(CDir,"/src/proz",COrig) -> true
48		; append(CDir,"/src/proz/",COrig) -> true
49		; append(CDir,"/",COrig) -> true
50		; otherwise -> COrig=CDir),
51		atom_codes(Dir,CDir).
52
53		% returns the path to the application directory (at run-time)
54		runtime_application_path(Dir) :-
55		( environ('PROB_HOME',Dir) -> % the user has set the environment variable PROB_HOME and thus overrides any other setting
56		true % the Rodin plugin used this mechanism
57	?	; application_path2(Dir),is_correct_prob_home_path(Dir) ->
58		true
59		; application_path2(D),absolute_file_name(D,D1),parent_dir(D1,Dir,_),
60		is_correct_prob_home_path(Dir) ->
61		true
62		; compile_time_env_path(prob_comp_home,Dir) -> % e.g. Debian/Ubuntu systems: the path was hard-wired at compile-time
63		true
64		; otherwise -> % usually a run from source code, where we the current directory is prob/src
65		current_directory(Current), remove_src_dir(Current,Dir)).
66		application_path2(Dir) :-
67		prolog_flag(system_type,development),
68		% try and find location of src/module_information.pl
69		current_module(module_information,MFile),parent_dir(MFile,SrcDir,_),
70		remove_src_dir(SrcDir,Dir).
71		application_path2(Dir) :-
72		\+(prolog_flag(system_type,development)),
73		environ('SP_APP_DIR',Dir). /* /usr/local/bin/sicstus on development systems */
74		application_path2(Dir) :-
75		\+(prolog_flag(system_type,development)),
76		environ('SP_STARTUP_DIR',Dir).
77
78		% check if the path points to a directory with a lib subdirectory and the probcliparser.jar file
79		is_correct_prob_home_path(D) :- % print(trying_as_prob_home_path(D)),nl,nl,
80		atom_concat(D,'/lib/probcliparser.jar',ConParser),
81		file_exists(ConParser).
82
83		parent_dir(FullFile,Dir,Basename) :-
84		atom_chars(FullFile,CFullFile), % "path/to/file"
85		reverse(CFullFile,RCFullFile), % "elif/ot/htap"
86	?	append(RCFile,['/'|RCDir],RCFullFile),!, % "elif" "/ot/htap"
87		reverse(RCFile,CFile),reverse(['/'|RCDir],CDir), % "file" "path/to/"
88		atom_chars(Basename,CFile),atom_chars(Dir,CDir).
89
90		% we do not use our standard test case schema here because we do not
91		% want to introduce a dependency to the test framework at this level
92		parent_dir_test1 :-
93		parent_dir('/aaaa/bbb/cc/d.app',D,B),D=='/aaaa/bbb/cc/',B=='d.app'.
94		parent_dir_test2 :-
95		parent_dir('/aaaa/bbb/cc/',D,B),D=='/aaaa/bbb/cc/',B==''.
96		parent_dir_test :-
97		parent_dir_test1, parent_dir_test2.
98		:- ( parent_dir_test -> true
99		; otherwise -> write(user_error,'testcase for pathes:parent_dir/2 failed, aborted.\n'),
100		halt(1)).
101
102		% returns the path to the application directory (compile-time)
103		compiletime_application_path(Dir) :-
104		compile_time_env_path(prob_comp_home,Dir),!.
105		compiletime_application_path(Dir) :-
106		runtime_application_path(Dir).
107
108		check_if_hard_wired(Alias, _Prefix, _Dir, Full) :-
109		compile_time_env_path(Alias,Full),!.
110		check_if_hard_wired(_Alias, Prefix, Dir, Full) :-
111		atom_concat(Prefix,Dir,Full).
112
113		set_search_path(Alias, Prefix, Dir) :-
114		check_if_hard_wired(Alias, Prefix, Dir, Full),
115		%% print(setting_path(Alias,Full)),nl, %%
116		( catch( user:file_search_path(Alias,Full), _, fail) -> true
117		; otherwise ->
118		catch( retractall(user:file_search_path(Alias,_)), _, true), % remove any old defintion
119		assertz(user:file_search_path(Alias,Full)) % , print(setting_search_path(Alias,Full)),nl
120		).
121
122		% pathes that can be used by use_module(...), but
123		% must not be used in run-time code
124		set_compile_time_search_pathes :-
125		compiletime_application_path(App),
126		%format('~n ProB compile time application path: ~w~n~n',[App]),
127		set_search_path(extension, App, '/extensions'),
128		set_search_path(probsrc, App, '/src'),
129		set_search_path(chrsrc, App, '/src/chr'),
130		set_search_path(probcspsrc, App, '/src/cia'),
131		set_search_path(probltlsrc, App, '/src/ltl'),
132		set_search_path(probporsrc, App, '/src/por'),
133		set_search_path(probpgesrc, App, '/src/pge'),
134		set_search_path(prozsrc, App, '/src/proz'),
135		set_search_path(kodkodsrc, App, '/src/kodkod'),
136		set_search_path(symbolic_model_checker, App, '/src/symbolic_model_checker'),
137		set_search_path(partial_evaluator, App, '/src/partial_evaluator'),
138		%set_search_path(plugins, App, '/plugins'),
139		%set_search_path(abstract_domains, App, '/plugins/absint/domains'),
140		set_search_path(tclsrc, App, '/tcl'),
141		%set_search_path(probpromela,App,'/src/promela'),
142		set_search_path(prob_rewrite_rules, App, '/src/rewrite_rules'),
143		set_search_path(smtlib_solver, App, '/src/smtlib_solver'),
144		set_search_path(smt_solvers_interface, App, '/src/smt_solvers_interface'),
145		set_search_path(synthesis, App, '/src/synthesis'),
146		set_search_path(library_plspec, App, '/src/library_plspec'). % patched libraries for plspec
147		:- set_compile_time_search_pathes.
148
149		% pathes that can be used in run-time code; should not be called at compile time
150		set_search_pathes :-
151		runtime_application_path(App),
152		%print(runtime_application_path(App)),nl,
153		set_search_path(prob_home, App, ''),
154		set_search_path(examples, App, '/../probprivate/public_examples'),
155		set_search_path(prob_lib, App, '/lib'),
156		set_search_path(prob_tcl, App, '/tcl'),
157
158		check_if_hard_wired(prob_lib, App, '/lib', LibDir),
159		( catch(user:library_directory(LibDir), _, fail) -> true % ,print(already_set(LibDir)),nl
160		; otherwise ->
161		catch( retractall(user:library_directory(_)), _, true), % remove any old defintion
162		assertz(user:library_directory(LibDir))).