1:- module(scasp_main,
2 [ main/1, 3
4 op(700, xfx, [#= , #<>, #< , #> , #=<, #>= ]),
5 op(900, fy, not),
6 op(700, xfx, '\u2209') 7 ]). 8:- set_prolog_flag(optimise, true). 9
10:- use_module(compile). 11:- use_module(ops). 12:- use_module(options). 13:- use_module(solve). 14:- use_module(stack). 15:- use_module(human). 16:- use_module(output). 17:- use_module(model). 18:- use_module(listing). 19:- use_module(html). 20:- use_module(html_text). 21:- use_module(json). 22:- use_module(messages). 23:- use_module(library(http/html_write)). 24:- use_module(library(http/js_write)). 25:- use_module(library(http/json)). 26:- use_module(library(dcg/high_order)). 27
28:- meta_predicate
29 print_query(:, +, +).
37:- initialization(main, main).
44main(Argv) :-
45 require_prolog_version('8.5.0-71',
46 [ warning(rational)
47 ]),
48 catch_with_backtrace(
49 ( scasp_parse_args(Argv, Sources, Options),
50 scasp_set_options(Options),
51 main(Sources, Options)
52 ),
53 Error,
54 error(Error)).
55
56main(Sources, Options) :-
57 set_prolog_flag(rational_syntax, natural),
58 set_prolog_flag(prefer_rationals, true),
59
60 load_sources(Sources, Options),
61 ( option(write_program(_), Options)
62 -> scasp_portray_program(Options),
63 halt
64 ; option(interactive(true), Options)
65 -> '$toplevel':setup_readline,
66 main_loop(Options)
67 ; query(Q, Bindings, Options)
68 -> ignore(main_solve(Q, [ variable_names(Bindings),
69 inputs(Sources)
70 | Options
71 ]))
72 ).
73
74load_sources([], _) :-
75 !,
76 print_message(error, scasp(no_input_files)),
77 scasp_help,
78 halt(1).
79load_sources(Sources, Options) :-
80 scasp_load(Sources, Options).
87error(error(scasp_undefined(PIs), _)) :-
88 !,
89 maplist(report_undef, PIs),
90 halt(1).
91error(error(existence_error(source_sink, Source),_)) :-
92 print_message(error, scasp(source_not_found(Source))),
93 halt(1).
94error(error(existence_error(scasp_query,scasp_main), _)) :-
95 print_message(error, scasp(no_query)),
96 halt(1).
97error(PrologError) :-
98 print_message(error, PrologError),
99 halt(1).
100
101report_undef(PI) :-
102 print_message(error,
103 error(existence_error(scasp_predicate, PI), _)).
104
105
106query(Query, Bindings, Options) :-
107 option(query(Term-Bindings), Options),
108 !,
109 scasp_compile_query(Term, Query, Options).
110query(Query, Bindings, Options) :-
111 scasp_query(Query, Bindings, Options).
117main_loop(Options) :-
118 read_term_with_history(R,
119 [ prompt('casp ~! ?- '),
120 variable_names(Bindings)
121 ]),
122 ( atom(R),
123 end_of_input(R)
124 -> format('~N'),
125 halt
126 ; scasp_compile_query(R, Q, Options)
127 -> ( main_solve(Q, [variable_names(Bindings)|Options])
128 -> nl, main_loop(Options)
129 ; main_loop(Options)
130 )
131 ; main_loop(Options)
132 ).
133
134end_of_input(end_of_file).
135end_of_input(exit).
136end_of_input(quit).
137end_of_input(halt).
147main_solve(Query, Options) :-
148 option(html(_File), Options),
149 !,
150 option(answers(MaxAnswers), Options, 0),
151 option(variable_names(Bindings), Options, []),
152
153 copy_term(Query-Bindings, QueryVar-QBindings),
154 ovar_set_bindings(QBindings),
155 inline_constraints(QueryVar, []),
156
157 statistics(cputime, T0),
158 ( MaxAnswers == 0
159 -> findall(Result,
160 solve_results(Query, Bindings, Result, Options),
161 Results)
162 ; findnsols(MaxAnswers, Result,
163 solve_results(Query, Bindings, Result, Options),
164 Results)
165 -> true
166 ),
167 statistics(cputime, T1),
168 Time is T1-T0,
169
170 html_print_results(scasp{ query:QueryVar,
171 cpu:Time,
172 answers:Results
173 },
174 Options).
175main_solve(Query, Options) :-
176 option(json(Name), Options),
177 !,
178 option(answers(MaxAnswers), Options, 0),
179 option(variable_names(Bindings), Options, []),
180 option(inputs(Inputs), Options, []),
181
182 copy_term(Query-Bindings, QueryVar-QBindings),
183 ovar_set_bindings(QBindings),
184 inline_constraints(QueryVar, []),
185 ROptions = [inline_constraints(false)|Options],
186
187 statistics(cputime, T0),
188 ( MaxAnswers == 0
189 -> findall(Result,
190 solve_results(Query, Bindings, Result, ROptions),
191 Results)
192 ; findnsols(MaxAnswers, Result,
193 solve_results(Query, Bindings, Result, ROptions),
194 Results)
195 -> true
196 ),
197 statistics(cputime, T1),
198 Time is T1-T0,
199
200 scasp_results_json(scasp{ query:QueryVar,
201 cpu:Time,
202 answers:Results,
203 inputs:Inputs
204 },
205 Dict),
206 ( Name == '-'
207 -> json_write_dict(current_output, Dict, Options),
208 format(current_output, '~N', [])
209 ; ensure_extension(Name, json, File),
210 setup_call_cleanup(
211 open(File, write, Out, [encoding(utf8)]),
212 ( json_write_dict(Out, Dict, Options),
213 format(current_output, '~N', [])
214 ),
215 close(Out))
216 ).
217main_solve(Query, Options) :-
218 option(answers(MaxAnswers), Options, -1),
219 option(variable_names(Bindings), Options, []),
220
221 print_query(Query, Bindings, Options),
222 statistics(cputime, T0),
223 ( solve_results(Query, Bindings, Result, Options)
224 *-> true
225 ; statistics(cputime, T1),
226 T is T1-T0,
227 print_message(warning, scasp(no_models(T))),
228 fail
229 ),
230
231 print_answer(Result.answer, Result.time, Options),
232
233 ( option(tree(_Detail), Options)
234 -> print_justification(Result.tree, Options)
235 ; true
236 ),
237 main_print_model(Result.model, Options),
238 print_bindings(Bindings, [full_stop(false)|Options]),
239
240 ( MaxAnswers == -1
241 -> allways_ask_for_more_models, nl, nl
242 ; MaxAnswers == 0
243 -> nl, nl,
244 fail
245 ; MaxAnswers > 0
246 -> nl, nl,
247 Result.answer = MaxAnswers
248 ),
249 !.
253solve_results(Query, Bindings,
254 scasp{ query:Query,
255 answer:Counter,
256 bindings:Bindings,
257 model:Model,
258 tree:Tree,
259 time:Time
260 },
261 Options) :-
262 option(tree(true), Options),
263 !,
264 call_nth(call_time(solve(Query, [], StackOut, ModelOut), Time), Counter),
265 justification_tree(StackOut, Tree, Options),
266 canonical_model(ModelOut, Model),
267 analyze_variables(t(Bindings, Model, StackOut), Bindings, Options).
268solve_results(Query, Bindings,
269 scasp{ query:Query,
270 answer:Counter,
271 bindings:Bindings,
272 model:Model,
273 time:Time
274 },
275 Options) :-
276 call_nth(call_time(solve(Query, [], _, ModelOut), Time), Counter),
277 canonical_model(ModelOut, Model),
278 analyze_variables(t(Bindings, Model), Bindings, Options).
279
280analyze_variables(Term, Bindings, Options) :-
281 ovar_set_bindings(Bindings),
282 ( option(inline_constraints(false), Options)
283 -> ovar_analyze_term(Term, [name_constraints(true)])
284 ; ovar_analyze_term(Term, []),
285 inline_constraints(Term, [])
286 ).
290print_answer(Nth, Resources, Options) :-
291 ( option(width(Width), Options)
292 -> true
293 ; catch(tty_size(_, Width), _, Width = 80)
294 ),
295 LineWidth is Width-8,
296 ansi_format(comment, '~N% ~`\u2015t~*|~n', [LineWidth]),
297 ansi_format(comment, '~N%', []),
298 ansi_format(bold, '~t Answer ~D (~3f sec) ~t~*|~n',
299 [Nth, Resources.cpu, LineWidth]),
300 ansi_format(comment, '~N% ~`\u2015t~*|~n', [LineWidth]).
305main_print_model(Model, Options) :-
306 ansi_format(comment, '~N% Model~n', []),
307 print_model(Model,
308 [ as_comment(false)
309 | Options
310 ]).
314:- det(print_query/3). 315print_query(M:Query, Bindings, Options) :-
316 ansi_format(comment, '~N% Query~n', []),
317 ( option(human(true), Options)
318 -> human_query(M:Query, [as_comment(false)|Options])
319 ; format('?- '),
320 query_body(Query, PQ),
321 portray_clause(current_output, PQ, [variable_names(Bindings)])
322 ).
323
324query_body(Query, Body) :-
325 append(Q1, [o_nmr_check], Query),
326 !,
327 comma_list(Body, Q1).
328query_body(Query, Body) :-
329 comma_list(Body, Query).
333print_justification(Tree, Options) :-
334 ansi_format(comment, '~N% Justification~n', []),
335 print_justification_tree(Tree, [ depth(1),
336 as_comment(false)
337 | Options
338 ]).
339
340print_bindings(Bindings, Options) :-
341 exclude(empty_binding, Bindings, Bindings1),
342 ( Bindings1 == []
343 -> ansi_format(comment, '~N% No bindings~n', []),
344 ( option(full_stop(true), Options, true)
345 -> ansi_format(bold, 'true.', [])
346 ; ansi_format(bold, 'true', [])
347 )
348 ; ansi_format(comment, '~N% Bindings~n', []),
349 print_bindings1(Bindings1, Options)
350 ).
351
352empty_binding(Name = Value) :-
353 Value == '$VAR'(Name).
354
355print_bindings1([], _).
356print_bindings1([H|T], Options) :-
357 print_binding(H, Options),
358 ( T == []
359 -> ( option(full_stop(true), Options, true)
360 -> format('.')
361 ; true
362 )
363 ; format(',~n'),
364 print_bindings1(T, Options)
365 ).
366
367print_binding(Name = Value, Options) :-
368 format('~w = ~W',
369 [ Name,
370 Value, [ numbervars(true),
371 quoted(true),
372 portray(true)
373 | Options
374 ]
375 ]).
376
378
379:- multifile
380 user:portray/1. 381
382user:portray(Rat) :-
383 rational(Rat),
384 current_prolog_flag(scasp_real, Decimals),
385 ( integer(Decimals)
386 -> format('~*f', [Decimals, Rat])
387 ; Decimals == float
388 -> Value is float(Rat),
389 write(Value)
390 ).
409html_print_results(Results, Options) :-
410 option(html(Name), Options),
411 Name \== '-', 412 !,
413 ensure_extension(Name, html, File),
414 setup_call_cleanup(
415 open(File, write, Out, [encoding(utf8)]),
416 ( phrase(reply(Results, Options), Tokens),
417 print_html(Out, Tokens)
418 ),
419 close(Out)).
420html_print_results(Results, Options) :-
421 phrase(reply(Results, Options), Tokens),
422 print_html(Tokens).
423
424ensure_extension(Base, Ext, File) :-
425 file_name_extension(_, Ext, Base),
426 !,
427 File = Base.
428ensure_extension(Base, Ext, File) :-
429 file_name_extension(Base, Ext, File).
430
431reply(Results, Options) -->
432 { length(Results.answers, Count)
433 },
434 emit_as(\page([],
435 [ \styles(Options),
436 \html_query(Results.query, Options),
437 \sequence(answer(Options), Results.answers),
438 div(class('scasp-statistics'),
439 [ h4('Statistics'),
440 p('~D answers in ~3f seconds'-[Count, Results.cpu])
441 ]),
442 \scripts(Options)
443 ]), html).
444
445answer(Options, Answer) -->
446 emit([ div(class('scasp-answer-header'),
447 'Answer ~D (~3f seconds)'-[Answer.answer, Answer.time.cpu]),
448 div(class('scasp-answer'),
449 [ \html_bindings(Answer.bindings, Options),
450 \html_model(Answer.model, Options),
451 \html_justification_tree(Answer.tree, Options)
452 ])
453 ]).
459styles(Options) -->
460 { option(style(false), Options) },
461 !.
462styles(_Options) -->
463 { read_file(library('scasp/web/css/scasp.css'), SCASPCSS),
464 read_file(library('http/web/css/plterm.css'), TermCSS)
465 },
466 html(style(SCASPCSS)),
467 html(style(TermCSS)).
468
469scripts(Options) -->
470 { option(script(false), Options) },
471 !.
472scripts(Options) -->
473 { ( option(human(true), Options)
474 -> As = human
475 ; As = machine
476 ),
477 option(collapse_below(Depth), Options, 2)
478 },
479 html(script(
480 [ src('https://code.jquery.com/jquery-1.11.2.min.js'),
481 integrity('sha256-Ls0pXSlb7AYs7evhd+VLnWsZ/AqEHcXBeMZUycz/CcA='),
482 crossorigin('anonymous')
483 ], [])),
484 { read_file(library('scasp/web/js/scasp.js'), String) },
485 html(script(String)),
486 js_script({|javascript(As,Depth)||
487
488$(function() {
489 $("body").sCASP("swish_answer", {
490 open_as:As,
491 justification: {
492 collapse_below: Depth,
493 collapsed: false
494 }
495 });
496});
497 |}).
498
499read_file(Spec, String) :-
500 absolute_file_name(Spec, Path, [access(read)]),
501 read_file_to_string(Path, String, []).
508allways_ask_for_more_models :-
509 ( format(' ? ', []),
510 get_single_char(R),
511 memberchk(R, `\s;`)
512 -> format(';\n'),
513 fail
514 ; true
515 )
sCASP as a stand-alone program
This module allows running scasp as a stand-alone program that loads one or more scasp source files, answer the (last) query and exit. */