1 % (c) 2009-2024 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 % note: also interesting: get_prob_application_type/1 in preferences
9 ]).
10
11 :- use_module(module_information).
12
13 :- module_info(group,infrastructure).
14 :- module_info(description,'This module contains code to compute compile-time and runtime-pathes.').
15
16 :- use_module(library(system),[environ/2]).
17 :- use_module(library(file_systems),[file_exists/1,
18 current_directory/1]).
19
20 :- set_prolog_flag(double_quotes, codes).
21
22 :- multifile user:file_search_path/2.
23 :- dynamic user:file_search_path/2.
24 % portray_file_search_path :- user:file_search_path(A,B), B \= library(_), portray_clause(file_search_path(A,B)),fail.
25
26 % some pathes may be set by environment variables during compilation,
27 :- dynamic compile_time_env_path/2.
28 lookup_env_path(Pathname, Varname) :-
29 ( environ(Varname,Value) ->
30 print('Hard-wired path for alias '),print(Pathname),print(': '),print(Value),nl,
31 assertz(compile_time_env_path(Pathname,Value))
32 ;
33 true).
34 % compile-time pathes
35 :- lookup_env_path(prob_comp_home,'PROB_COMP_HOME'). % hard-wired version of the runtime_application_path
36 % This is used on systems where it absolutely clear where the
37 % ProB's application directory will be, namely Debian/Ubuntu packages
38 % run-time pathes
39 :- lookup_env_path(prob_home,'PROB_HOME').
40 :- lookup_env_path(examples,'PROB_EXAMPLES'). % hard-wired pathes, see above (about Debian/Ubuntu packages)
41 :- lookup_env_path(prob_lib,'PROB_LIB'). % hard-wired pathes, see above (about Debian/Ubuntu packages)
42 :- lookup_env_path(prob_tcl,'PROB_TCL'). % hard-wired pathes, see above (about Debian/Ubuntu packages)
43
44 % removes an (optional) trailing /src or /tests directory from the path,
45 % the result will not end with a slash
46 remove_src_dir(Orig,Dir) :-
47 atom_codes(Orig,COrig),
48 ( append(CDir,"/src/",COrig) -> true
49 ; append(CDir,"/src",COrig) -> true
50 ; append(CDir,"/src/proz",COrig) -> true
51 ; append(CDir,"/src/proz/",COrig) -> true
52 ; append(CDir,"/tests/",COrig) -> true
53 ; append(CDir,"/tests",COrig) -> true
54 ; append(CDir,"/",COrig) -> true
55 ; COrig=CDir),
56 atom_codes(Dir,CDir).
57
58 % returns the path to the application directory (at run-time)
59 runtime_application_path(Dir) :-
60 ( environ('PROB_HOME',Dir) -> % the user has set the environment variable PROB_HOME and thus overrides any other setting
61 true % the Rodin plugin used this mechanism
62 ? ; application_path2(Dir),is_correct_prob_home_path(Dir) ->
63 true
64 ; application_path2(D),absolute_file_name(D,D1),parent_dir(D1,Dir,_),
65 is_correct_prob_home_path(Dir) ->
66 true
67 ; compile_time_env_path(prob_comp_home,Dir) -> % e.g. Debian/Ubuntu systems: the path was hard-wired at compile-time
68 true
69 ; % usually a run from source code, where we the current directory is prob/src
70 current_directory(Current), remove_src_dir(Current,Dir)).
71 application_path2(Dir) :-
72 current_prolog_flag(system_type,development), % other value of system_type flag is runtime
73 % try and find location of src/module_information.pl
74 current_module(module_information,MFile),parent_dir(MFile,SrcDir,_),
75 remove_src_dir(SrcDir,Dir).
76 application_path2(Dir) :-
77 \+(current_prolog_flag(system_type,development)),
78 environ('SP_APP_DIR',Dir). /* /usr/local/bin/sicstus on development systems */
79 application_path2(Dir) :-
80 \+(current_prolog_flag(system_type,development)),
81 environ('SP_STARTUP_DIR',Dir).
82
83 % check if the path points to a directory with a lib subdirectory and the probcliparser.jar file
84 is_correct_prob_home_path(D) :- % print(trying_as_prob_home_path(D)),nl,nl,
85 atom_concat(D,'/lib/probcliparser.jar',ConParser),
86 file_exists(ConParser).
87
88 parent_dir(FullFile,Dir,Basename) :-
89 atom_chars(FullFile,CFullFile), % "path/to/file"
90 reverse(CFullFile,RCFullFile), % "elif/ot/htap"
91 append(RCFile,['/'|RCDir],RCFullFile),!, % "elif" "/ot/htap"
92 reverse(RCFile,CFile),reverse(['/'|RCDir],CDir), % "file" "path/to/"
93 atom_chars(Basename,CFile),atom_chars(Dir,CDir).
94
95 % avoid importing library lists for plspec; for some reason this generates errors
96 % :- use_module(library(lists),[reverse/2]).
97 reverse(List, Reversed) :-
98 rev(List, [], Reversed).
99 rev([], Reversed, Reversed).
100 rev([Head|Tail], Sofar, Reversed) :-
101 rev(Tail, [Head|Sofar], Reversed).
102
103 % we do not use our standard test case schema here because we do not
104 % want to introduce a dependency to the test framework at this level
105 parent_dir_test1 :-
106 parent_dir('/aaaa/bbb/cc/d.app',D,B),D=='/aaaa/bbb/cc/',B=='d.app'.
107 parent_dir_test2 :-
108 parent_dir('/aaaa/bbb/cc/',D,B),D=='/aaaa/bbb/cc/',B==''.
109 parent_dir_test :-
110 parent_dir_test1, parent_dir_test2.
111 :- ( parent_dir_test -> true
112 ; write(user_error,'testcase for pathes:parent_dir/2 failed, aborted.\n'),
113 halt(1)).
114
115 % returns the path to the application directory (compile-time)
116 compiletime_application_path(Dir) :-
117 compile_time_env_path(prob_comp_home,Dir),!.
118 compiletime_application_path(Dir) :-
119 runtime_application_path(Dir).
120
121 check_if_hard_wired(Alias, _Prefix, _Dir, Full) :-
122 compile_time_env_path(Alias,Full),!.
123 check_if_hard_wired(_Alias, Prefix, Dir, Full) :-
124 atom_concat(Prefix,Dir,Full).
125
126 set_search_path(Alias, Prefix, Dir) :-
127 check_if_hard_wired(Alias, Prefix, Dir, Full),
128 %% print(setting_path(Alias,Full)),nl, %%
129 ( catch( user:file_search_path(Alias,Full), _, fail)
130 -> true % Alias already set to same value
131 ; catch( retractall(user:file_search_path(Alias,_)), _, true), % remove any old defintion
132 assertz(user:file_search_path(Alias,Full)) % , print(setting_search_path(Alias,Full)),nl
133 ).
134
135 % pathes that can be used by use_module(...), but
136 % must not be used in run-time code
137 set_compile_time_search_pathes :-
138 compiletime_application_path(App),
139 %format('~n ProB compile time application path: ~w~n~n',[App]),
140 set_search_path(extension, App, '/extensions'),
141 set_search_path(probsrc, App, '/src'),
142 set_search_path(chrsrc, App, '/src/chr'),
143 set_search_path(cbcsrc, App, '/src/cbc'),
144 set_search_path(probcspsrc, App, '/src/cia'),
145 set_search_path(probltlsrc, App, '/src/ltl'),
146 set_search_path(probporsrc, App, '/src/por'),
147 set_search_path(probpgesrc, App, '/src/pge'),
148 set_search_path(prozsrc, App, '/src/proz'),
149 set_search_path(kodkodsrc, App, '/src/kodkod'),
150 set_search_path(symbolic_model_checker, App, '/src/symbolic_model_checker'),
151 set_search_path(wdsrc, App, '/src/well_def'),
152 %set_search_path(plugins, App, '/plugins'),
153 %set_search_path(abstract_domains, App, '/plugins/absint/domains'),
154 set_search_path(tclsrc, App, '/tcl'),
155 %set_search_path(probpromela,App,'/src/promela'),
156 set_search_path(pltablesrc, App, '/src/pltables'),
157 set_search_path(prob_rewrite_rules, App, '/src/rewrite_rules'),
158 set_search_path(smtlib_solver, App, '/src/smtlib_solver'),
159 set_search_path(smt_solvers_interface, App, '/src/smt_solvers_interface'),
160 set_search_path(disproversrc, App, '/src/disprover'),
161 set_search_path(cdclt_solver, App, '/src/cdclt_solver'),
162 set_search_path(code2vec, App, '/src/code2vec'),
163 set_search_path(synthesis, App, '/src/synthesis'),
164 set_search_path(visbsrc, App, '/src/visb'),
165 set_search_path(dotsrc, App, '/src/dot'),
166 set_search_path(covsrc, App, '/src/coverage'),
167 set_search_path(tcltkuisrc, App, '/src/tcltk'),
168 set_search_path(extrasrc, App, '/src/extra'),
169 set_search_path(symsrc, App, '/src/symmetry'),
170 set_search_path(library_plspec, App, '/extensions/plspec_libraries'). % patched libraries for plspec
171 :- set_compile_time_search_pathes.
172
173 :- if(environ(prob_release,true)).
174 :- else.
175 % These paths will not be defined in release mode:
176 set_compile_time_dev_search_pathes :-
177 compiletime_application_path(App),
178 set_search_path(testsrc, App, '/tests'). % should never be used from main sources!
179 :- set_compile_time_dev_search_pathes.
180 :- endif.
181
182 :- dynamic user:library_directory/1.
183
184 % pathes that can be used in run-time code; should not be called at compile time
185 set_search_pathes :-
186 runtime_application_path(App),
187 %print(runtime_application_path(App)),nl,
188 set_search_path(prob_home, App, ''),
189 set_search_path(examples, App, '/../probprivate/public_examples'),
190 set_search_path(prob_lib, App, '/lib'),
191 set_search_path(prob_tcl, App, '/tcl'),
192
193 check_if_hard_wired(prob_lib, App, '/lib', LibDir),
194 ( catch(user:library_directory(LibDir), _, fail) -> true % ,print(already_set(LibDir)),nl
195 ;
196 catch( retractall(user:library_directory(_)), _, true), % remove any old defintion
197 assertz(user:library_directory(LibDir))),
198 (current_prolog_flag(system_type,development)
199 -> true
200 ; set_compiled_prob_pathes(App)
201 ).
202
203 set_compiled_prob_pathes(_App) :-
204 % print('Adding to library directories:'),nl,
205 % assertz(user:library_directory('/usr/local/sicstus4.6/bin/sp-4.6.0/sicstus-4.6.0/library/')).
206 true.
207
208
209 % Term expansion for automatically replacing uses of library(avl)
210 % with our custom SICStus-like implementation avl_custom(avl).
211 % Mainly for compatibility with SWI-Prolog,
212 % because ProB heavily relies on SICStus library(avl) and its term representation.
213 :- use_module(tools_portability, [exists_source/1, supported_term_expansion_style/1]).
214 :- if((environ(prob_avl_custom,true) ; \+ exists_source(library(avl)))).
215
216 expand_avl_custom((:- use_module(library(avl))), Layout1, Term2, Layout2) :-
217 !,
218 Term2 = (:- use_module(probsrc(avl_custom))),
219 Layout2 = Layout1.
220 expand_avl_custom((:- use_module(library(avl), Imports)), Layout1, Term2, Layout2) :-
221 !,
222 Term2 = (:- use_module(probsrc(avl_custom), Imports)),
223 Layout2 = Layout1.
224
225 :- if(supported_term_expansion_style(sicstus)).
226 :- multifile user:term_expansion/6.
227 user:term_expansion(Term1, Layout1, Ids, Term2, Layout2, [patch_avl_custom|Ids]) :-
228 nonvar(Term1), nonmember(patch_avl_custom,Ids),
229 expand_avl_custom(Term1, Layout1, Term2, Layout2).
230 :- elif(supported_term_expansion_style(swi_layout)).
231 :- multifile user:term_expansion/4.
232 user:term_expansion(Term1, Layout1, Term2, Layout2) :-
233 nonvar(Term1),
234 expand_avl_custom(Term1, Layout1, Term2, Layout2).
235 :- else.
236 :- multifile user:term_expansion/2.
237 user:term_expansion(Term1, Term2) :-
238 nonvar(Term1),
239 expand_avl_custom(Term1, [], Term2, _).
240 :- endif.
241
242 :- endif.
243
244
245 % TERM EXPANDER for ProB EXTENSIONS
246 % ---------------------------------
247
248 :- if(environ(prob_core_only,true)).
249
250 % keep track of which optional extensions of ProB are available
251 % and patch use_modules to unloaded extensions
252 % Note: only use_modules with explicit import lists are patched !
253
254 :- use_module(pathes_extensions_db, [compile_time_unavailable_extension/2,
255 module_path_implements_extension/3]).
256
257 % true if a given path should be pruned by the term expander:
258 prune_use_module(Path,Extension,Reason) :-
259 module_path_implements_extension(Path,_,Extension),
260 compile_time_unavailable_extension(Extension,Reason).
261
262 % utility to export dependencies to a dot graph
263 ext_dot_graph(F) :- open(F,write,S,[encoding(utf8)]),
264 format(S,'digraph ~w {~n',[extensions]),
265 format(S,'graph [nodesep=1.5, ranksep=1.5, rankdir=LR];~n',[]),
266 ( depends_edge(From,To,Label,Color),
267 format(S,' ~w -> ~w [label="~w",color="~w"]~n',[From,To,Label,Color]),
268 fail ; true
269 ),
270 format(S,'}~n',[]),
271 close(S).
272 % ?- pathes:ext_dot_graph('~/Desktop/out.dot').
273 % dot -Tpdf <~/Desktop/out.dot > ~/Desktop/out.pdf ; open ~/Desktop/out.pdf
274 :- dynamic module_extension/2, dependency/6.
275 depends_edge(FromExtension,ToExtension,Label,Col) :-
276 pathes_extensions_db:prob_extension(FromExtension),
277 pathes_extensions_db:prob_extension(ToExtension), ToExtension \= FromExtension,
278 (dependency(FromExtension,_CurModule,_,_,ToExtension,Av) ->
279 %Label = CurModule,
280 findall(MM,dependency(FromExtension,MM,_,_,ToExtension,Av),Ls), sort(Ls,SLs),
281 tools:ajoin_with_sep(SLs,',',Label),
282 (Av=available -> Col=green ; Col=red)).
283 % utility to generate a dot graph of dependency; TODO: make useful
284
285 :- if(1=2). % change to 1=1 to store dependencies and e.g. call print_modules
286 store_dependency(Path) :-
287 module_path_implements_extension(Path,Module,ToExtension),
288 % store the extension associated to the module:
289 (module_extension(Module,ToExtension) -> true
290 ; %format(' ~w --> ~w~n',[Module,ToExtension]),
291 assertz(module_extension(Module,ToExtension))
292 ),
293 % examine context of current module performing the import:
294 (prolog_load_context(module,CurModule)
295 -> (get_module_info(CurModule,group,Group) -> true ; Group=unknown),
296 (module_extension(CurModule,FromExtension) -> true ; FromExtension=core)
297 ; CurModule=user,Group=user),
298 !,
299 (compile_time_unavailable_extension(ToExtension, _) -> Av=not_available ; Av=available),
300 assertz(dependency(FromExtension,CurModule,Group,Path,ToExtension,Av)).
301 :- endif.
302 store_dependency(_).
303
304 %:- use_module(probsrc(tools),[latex_escape_atom/2]).
305 print_modules :-
306 version:version_str(Vers), version:revision(Rev),
307 format('List of ProB ~w (~w) modules by groups and extensions:~n',[Vers,Rev]),
308 format('\\begin{itemize}~n',[]),
309 get_module_group(Group), tools:latex_escape_atom(Group,LG),
310 format(' \\item Module Group: ~w~n',[LG]),
311 format(' \\begin{enumerate}~n',[]),
312 ( findall(MM, get_module_info(MM,group,Group), ML), sort(ML,SML),
313 member(Module,SML),
314 (get_module_info(Module,description,D) -> true ; D='?'),
315 (module_extension(Module,Ext) -> true ; Ext=core),
316 tools:latex_escape_atom(Ext,EE),tools:latex_escape_atom(Module,EM),
317 tools:latex_escape_atom(D,ED),
318 format(' \\item ~w : ~w ~n \\moduledescr{ ~w }~n',[EE,EM,ED])
319 ;
320 format(' \\end{enumerate}~n',[])
321 ),
322 fail.
323 print_modules :- format('\\end{itemize}~n',[]).
324 print_modules_csv :- nl,
325 get_module_group(Group),
326 findall(MM, get_module_info(MM,group,Group), ML), sort(ML,SML),
327 member(Module,SML),
328 (get_module_info(Module,description,D) -> true ; D='?'),
329 (module_extension(Module,Ext) -> true ; Ext=core),
330 format(' ~w,~w,~w,"~w"~n',[Group,Ext,Module,D]),
331 fail.
332 print_modules_csv :- nl.
333
334
335 :- use_module(library(lists),[maplist/3]).
336
337 % term expander to replace use_modules by stub clauses which throw errors
338 %patch_ext_use_modules((:- module(Module,_)),Layout1,Term2,Layout2) :- format('~n enter module ~w~n',[Module]),fail.
339 patch_ext_use_modules((:- use_module(Path)),Layout1,Term2,Layout2) :-
340 store_dependency(Path),
341 prune_use_module(Path,_Extension,_Reason),
342 !,
343 Layout2 = Layout1,
344 %%(prolog_load_context(module,CurModule) -> true ; CurModule=user),
345 %%format('\e[31mIgnoring use_module(~w) in ~w because extension ~w not available\e[0m~n',[Path,CurModule,Extension]),
346 Term2= (:- true).
347 patch_ext_use_modules((:- use_module(Path,Preds)),Layout1,Term2,Layout2) :-
348 store_dependency(Path),
349 prune_use_module(Path,Extension,Reason), % prolog_load_context(file,File),
350 !,
351 Layout2 = Layout1,
352 (prolog_load_context(module,CurModule) -> true ; CurModule=user),
353 %%format('\e[34mPatching use_module(~w,~w) in ~w because extension ~w not available\e[0m~n',[Path,Preds,CurModule,Extension]),
354 maplist(generate_stub(CurModule,Extension,Reason),Preds,Term2). % Term2 can be a list of clauses
355 %patch_ext_use_modules((:- use_module(Path)),_,_,_) :- format('** use_module(~w)~n',[Path]),fail.
356 %patch_ext_use_modules((:- use_module(Path,Preds)),_,_,_) :- format('** use_module(~w,~w)~n',[Path,Preds]),fail.
357
358
359 :- use_module(pathes_extensions_db, [silently_fail_unavailable_predicate/3]).
360 :- use_module(tools_strings,[ajoin/2]).
361 % generate stub clauses for all imported predicates
362 generate_stub(_,Extension,_Reason,Predicate/Arity,Clause) :-
363 silently_fail_unavailable_predicate(Predicate,Arity,Extension),!,
364 functor(Head,Predicate,Arity),
365 Clause = (Head :- fail).
366 generate_stub(Module,Extension,Reason,Predicate/Arity,Clause) :-
367 functor(Head,Predicate,Arity),
368 ajoin(['Predicate cannot be called because extension ', Extension, ' is not loaded (', Reason, '):'],Msg),
369 Clause = (Head :- !, error_manager:add_error(Module,Msg,Predicate/Arity),fail).
370 %, portray_clause(Clause),nl.
371
372 :- use_module(tools_portability, [supported_term_expansion_style/1]).
373 :- if(supported_term_expansion_style(sicstus)).
374 :- multifile user:term_expansion/6.
375 user:term_expansion(Term1, Layout1, Ids, Term2, Layout2, [patch_unavailable_extensions|Ids]) :-
376 nonvar(Term1), nonmember(patch_unavailable_extensions,Ids),
377 patch_ext_use_modules(Term1,Layout1,Term2,Layout2).
378 :- elif(supported_term_expansion_style(swi_layout)).
379 :- multifile user:term_expansion/4.
380 user:term_expansion(Term1, Layout1, Term2, Layout2) :-
381 nonvar(Term1),
382 patch_ext_use_modules(Term1,Layout1,Term2,Layout2).
383 :- else.
384 :- multifile user:term_expansion/2.
385 user:term_expansion(Term1, Term2) :-
386 nonvar(Term1),
387 patch_ext_use_modules(Term1,[],Term2,_).
388 :- endif.
389 :- endif.