1/* Part of sCASP 2 3 Author: Jan Wielemaker 4 E-mail: jan@swi-prolog.org 5 Copyright (c) 2021, SWI-Prolog Solutions b.v. 6 All rights reserved. 7 8 Redistribution and use in source and binary forms, with or without 9 modification, are permitted provided that the following conditions 10 are met: 11 12 1. Redistributions of source code must retain the above copyright 13 notice, this list of conditions and the following disclaimer. 14 15 2. Redistributions in binary form must reproduce the above copyright 16 notice, this list of conditions and the following disclaimer in 17 the documentation and/or other materials provided with the 18 distribution. 19 20 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 21 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 22 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 23 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 24 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 25 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 26 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 27 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 28 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 29 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 30 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 31 POSSIBILITY OF SUCH DAMAGE. 32*/ 33 34:- module(scasp_embed, 35 [ begin_scasp/1, % +Unit 36 begin_scasp/2, % +Unit, +Exports 37 end_scasp/0, 38 scasp_listing/2, % +Unit, +Options 39 scasp_model/1, % :Model 40 scasp_model/2, % :Model, +Options 41 scasp_stack/1, % -Stack 42 scasp_justification/2, % -Tree, +Options 43 (not)/1, % :Query 44 (-)/1, % :Query 45 46 op(700, xfx, .\=.), 47 op(700, xfx, '\u2209'), 48 op(900, fy, not) 49 ]). 50:- use_module(ops). 51:- use_module(input). 52:- use_module(compile). 53:- use_module(predicates). 54:- use_module(solve). 55:- use_module(model). 56:- use_module(stack). 57:- use_module(options). 58:- use_module(listing). 59 60:- use_module(library(apply)). 61:- use_module(library(error)). 62:- use_module(library(lists)). 63:- use_module(library(prolog_code)). 64 65:- meta_predicate 66 scasp_model(), 67 scasp_justification(, ), 68 not(), 69 -(). 70 71% one of `false`, `true`, `unicode` or `human` 72:- create_prolog_flag(scasp_show_model, 73 false, 74 [keep(true), type(atom)]). 75:- create_prolog_flag(scasp_show_justification, 76 false, 77 [keep(true), type(atom)]).
105:- thread_local 106 loading_scasp/3. % Unit, File, Dict
Otherwise the read clauses are asserted verbatim. Directives are terms #(Directive). Prolog directives (:- Directive) are interpreted as sCASP global constraints. The matching end_scasp/0 compiles the sCASP program and creates wrappers in the enclosing module that call the sCASP solver.
The sCASP code must be closed using end_scasp/0. Both begin_scasp/1,2 and end_scasp/0 must be used as directives.
128begin_scasp(Unit) :- 129 begin_scasp(Unit, all). 130 131begin_scasp(Unit, Exports) :- 132 scasp_module(Unit, Module), 133 prolog_load_context(module, Context), 134 source_location(File, Line), 135 '$set_source_module'(OldModule, Module), 136 '$declare_module'(Module, scasp, Context, File, Line, false), 137 scasp_push_operators, 138 '$style_check'(OldStyle, OldStyle), 139 style_check(-singleton), 140 discontiguous(Module:(#)/1), 141 asserta(loading_scasp(Unit, File, 142 _{ module:Module, 143 old_module:OldModule, 144 old_style:OldStyle, 145 exports:Exports 146 })). 147 148scasp_module(Unit, Module) :- 149 atom_concat('_scasp_', Unit, Module).
155end_scasp :- 156 throw(error(context_error(nodirective, end_scasp), _)). 157 158end_scasp(Clauses) :- 159 ( retract(loading_scasp(Unit, _File, Dict)) 160 -> _{ old_module:OldModule, 161 old_style:OldStyle, 162 exports:Exports 163 } :< Dict, 164 '$set_source_module'(_, OldModule), 165 scasp_pop_operators, 166 '$style_check'(_, OldStyle), 167 ( Exports == [] 168 -> Options = [unknown(fail)] 169 ; Options = [] 170 ), 171 scasp_compile_unit(Unit, Options), 172 link_clauses(OldModule, Unit, Clauses, Exports) 173 ; throw(error(context_error(scasp_close(-)), _)) 174 ). 175 176loading_scasp(Unit) :- 177 source_location(File, _Line), 178 loading_scasp(Unit,File,_). 179 180userterm_expansion(end_of_file, _) :- 181 loading_scasp(Unit), 182 print_message(error, scasp(not_closed_program(Unit))), 183 end_scasp, 184 fail. 185userterm_expansion((:- Constraint), Clause) :- 186 loading_scasp(_), 187 Constraint \== end_scasp, 188 !, 189 Clause = ('_false_0' :- Constraint). 190userterm_expansion((?- Query), Clause) :- 191 loading_scasp(_), 192 !, 193 Clause = scasp_query(Query, 1). 194userterm_expansion(#(discontiguous(Preds)), (:- discontiguous(Preds))) :- 195 loading_scasp(_). 196userterm_expansion(#(pred(Preds)), #(pred(Preds))) :- 197 loading_scasp(_), 198 prolog_load_context(variable_names, Vars), 199 maplist(bind_var, Vars). 200userterm_expansion((:- end_scasp), Clauses) :- 201 \+ current_prolog_flag(xref, true), 202 end_scasp(Clauses). 203 204bind_var(Name = $(Name)).
211:- thread_local 212 done_unit/1. % allow for mutually recursive #include 213 214scasp_compile_unit(Unit, Options) :- 215 call_cleanup(scasp_compile_unit_(Unit, Options), 216 retractall(done_unit(_))). 217 218scasp_compile_unit_(Unit, Options) :- 219 scasp_module(Unit, Module), 220 ( current_module(Module) 221 -> true 222 ; existence_error(scasp_unit, Unit) 223 ), 224 findall(Clause, scasp_clause(Unit, Clause), Clauses), 225 scasp_compile(Module:Clauses, Options).
231scasp_clause(Unit, _Clause) :- 232 done_unit(Unit), 233 !, 234 fail. 235scasp_clause(Unit, Clause) :- 236 assertz(done_unit(Unit)), 237 scasp_module(Unit, Module), 238 QHead = Module:Head, 239 predicate_property(QHead, interpreted), 240 \+ scasp_compiled(Head), 241 \+ predicate_property(QHead, imported_from(_)), 242 @(clause(Head, Body), Module), 243 mkclause(Head, Body, Clause). 244 245mkclause(scasp_query(Query,_N), true, Clause) => 246 Clause = (?- Query). 247mkclause(#(include(Unit)), true, Clause) => 248 scasp_clause(Unit, Clause). 249mkclause(#(Directive), true, Clause) => % TBD: #abducible 250 Clause = #(Directive). 251mkclause('_false_0', Body, Clause) => 252 Clause = (:- Body). 253mkclause(Head, true, Clause) => 254 Clause = Head. 255mkclause(Head, Body, Clause) => 256 Clause = (Head :- Body).
263link_clauses(_ContextModule, Unit, Clauses, Exports) :- 264 scasp_module(Unit, Module), 265 findall(Head, link_predicate(Module:Head), Heads), 266 check_exports(Exports, Heads), 267 convlist(link_clause(Module, Exports), Heads, Clauses). 268 269link_predicate(Module:Head) :- 270 Module:pr_user_predicate(PI), 271 \+ not_really_a_user_predicate(PI), 272 pi_head(PI, Head). 273 274% TBD: merge with user_predicate/1. 275not_really_a_user_predicate((not)/1). 276not_really_a_user_predicate(o_nmr_check/0). 277not_really_a_user_predicate(global_constraints/0). 278 279check_exports(all, _) :- !. 280check_exports(Exports, Heads) :- 281 must_be(list, Exports), 282 maplist(check_export(Heads), Exports). 283 284check_export(Heads, -Name/Arity) :- 285 !, 286 atom_concat(-, Name, NName), 287 check_export(Heads, NName/Arity). 288check_export(Heads, Export) :- 289 pi_head(Export, EHead), % raises an exception on malformed PI. 290 ( memberchk(EHead, Heads) 291 -> true 292 ; existence_error(predicate, Export) 293 ). 294 295link_clause(Module, Exports, Head, 296 (Head :- scasp_embed:scasp_call(Module:Head))) :- 297 ( Exports == all 298 -> true 299 ; functor(Head, NName, Arity), 300 atom_concat(-, Name, NName) 301 -> memberchk(-Name/Arity, Exports) 302 ; pi_head(PI, Head), 303 memberchk(PI, Exports) 304 ).
311:- public scasp_call/1. 312 313scasp_call(Query) :- 314 scasp_compile_query(Query, Compiled, []), 315 scasp_stack(StackIn), 316 solve(Compiled, StackIn, StackOut, Model), 317 save_model(Model), 318 Compiled = M:_, % TBD: Properly handle the module 319 save_stack(M:StackOut).
328not(M:Query) :-
329 clause(M:, scasp_embed:scasp_call(Module:Query)),
330 scasp_call(Module:not(Query)).
336-(M:Query) :-
337 Query =.. [Name|Args],
338 atom_concat(-, Name, NName),
339 NQuery =.. [NName|Args],
340 clause(M:, scasp_embed:scasp_call(Module:NQuery)),
341 scasp_call(Module:NQuery).
350save_model(Model) :-
351 ( nb_current(scasp_model, Model0)
352 -> append(Model, Model0, FullModel),
353 b_setval(scasp_model, FullModel)
354 ; b_setval(scasp_model, Model)
355 ).363scasp_model(M:Model) :- 364 scasp_model(M:Model, []). 365 366scasp_model(M:Model, _Options) :- 367 nb_current(scasp_model, RawModel), 368 canonical_model(RawModel, Model1), 369 unqualify_model(Model1, M, Model). 370 371save_stack(Stack) :- 372 b_setval(scasp_stack, Stack), 373 justification_tree(Stack, Tree, []), 374 b_setval(scasp_tree, Tree).
381scasp_stack(Stack) :-
382 ( nb_current(scasp_stack, Stack0)
383 -> Stack = Stack0
384 ; Stack = []
385 ).391scasp_justification(M:Tree, Options) :- 392 nb_current(scasp_tree, Tree0), 393 remove_origins(Tree0, Tree1, Options), 394 unqualify_justitication_tree(Tree1, M, Tree). 395 396remove_origins(Tree0, Tree, Options) :- 397 option(source(false), Options), 398 !, 399 remove_origins(Tree0, Tree). 400remove_origins(Tree, Tree, _). 401 402remove_origins(M:Tree0, Result) => 403 Result = M:Tree, 404 remove_origins(Tree0, Tree). 405remove_origins(Term0-Children0, Result) => 406 Result = Term-Children, 407 remove_origin(Term0, Term), 408 maplist(remove_origins, Children0, Children). 409remove_origins(Nodes0, Nodes), is_list(Nodes0) => 410 maplist(remove_origins, Nodes0, Nodes). 411remove_origins(Node0, Node) => 412 remove_origin(Node0, Node). 413 414remove_origin(goal_origin(Term, _), Result) => 415 Result = Term. 416remove_origin(Term, Result) => 417 Result = Term.
424scasp_listing(Unit, Options) :- 425 scasp_module(Unit, Module), 426 scasp_portray_program(Module:Options). 427 428:- residual_goals(scasp_residuals).
435scasp_residuals --> 436 { '$current_typein_module'(TypeIn), 437 scasp_residual_types(Types) 438 }, 439 scasp_residuals(Types, TypeIn). 440 441scasp_residuals([], _) --> 442 []. 443scasp_residuals([model(Options)|T], M) --> 444 ( {scasp_model(M:Model, Options)} 445 -> [ scasp_show_model(Model, Options) ] 446 ; [] 447 ), 448 scasp_residuals(T, M). 449scasp_residuals([justification(Options)|T], M) --> 450 ( {scasp_stack(Stack), Stack \== []} 451 -> [ scasp_show_stack(M:Stack, Options) ] 452 ; [] 453 ), 454 scasp_residuals(T, M). 455 456scasp_residual_types(Types) :- 457 findall(Type, scasp_residual_type(Type), Types). 458 459scasp_residual_type(model(Options)) :- 460 current_prolog_flag(scasp_show_model, Spec), 461 Spec \== false, 462 res_options(Spec, Options). 463scasp_residual_type(justification(Options)) :- 464 current_prolog_flag(scasp_show_justification, Spec), 465 Spec \== false, 466 res_options(Spec, Options). 467 468res_options(List, Options), is_list(List) => 469 Options = List. 470res_options(true, Options) => 471 Options = [unicode(true)]. 472res_options(unicode, Options) => 473 Options = [unicode(true)]. 474res_options(human, Options) => 475 Options = [human(true)]. 476 477user:portray(scasp_show_model(Model, Options)) :- 478 ansi_format(comment, '% s(CASP) model~n', []), 479 print_model(Model, Options). 480user:portray(scasp_show_stack(M:Stack, Options)) :- 481 ansi_format(comment, '% s(CASP) justification', []), 482 justification_tree(Stack, Tree0, Options), 483 unqualify_justitication_tree(Tree0, M, Tree), 484 print_justification_tree(Tree, [full_stop(false)|Options]). 485user:portray('\u2209'(V,S)) :- % not element of 486 format('~p \u2209 ~p', [V, S]). 487 488 489 /******************************* 490 * HIGHLIGHT SUPPORT * 491 *******************************/ 492 493:- multifile 494 prolog:alternate_syntax/4, 495 prolog:xref_update_syntax/2. 496 497prologalternate_syntax(scasp, Module, Setup, Restore) :- 498 Setup = scasp_ops:scasp_push_operators(Module), 499 Restore = scasp_ops:scasp_pop_operators. 500 501prologxref_update_syntax(begin_scasp(_Unit), Module) :- 502 scasp_ops:scasp_push_operators(Module). 503prologxref_update_syntax(begin_scasp(_Unit, _Exports), Module) :- 504 scasp_ops:scasp_push_operators(Module). 505prologxref_update_syntax(end_scasp, _Module) :- 506 scasp_ops:scasp_pop_operators. 507 508:- multifile 509 prolog_colour:term_colours/2. 510 511prolog_colourterm_colours(#(Directive), 512 expanded - [DirColours]) :- 513 debug(scasp(highlight), 'Got ~p', [Directive]), 514 dir_colours(Directive, DirColours). 515 516dir_colours(pred(_Head::_Template), 517 expanded - 518 [ expanded - 519 [ body, 520 comment(_) 521 ] 522 ]). 523dir_colours(show(Preds), 524 expanded - [Colours]) :- 525 decl_show_colours(Preds, Colours). 526dir_colours(include(_Unit), 527 expanded - 528 [ classify 529 ]). 530dir_colours(discontiguous(_Preds), 531 expanded - 532 [ declarations(discontiguous) 533 ]). 534 535decl_show_colours((A,B), Colours) => 536 Colours = classify-[CA,CB], 537 decl_show_colours(A, CA), 538 decl_show_colours(B, CB). 539decl_show_colours(not(_A), Colours) => 540 Colours = built_in-[declarations(show)]. 541decl_show_colours(_A, Colours) => 542 Colours = declarations(show). 543 544 545 /******************************* 546 * GXREF SUPPORT * 547 *******************************/
s(CASP) hooks558:- multifile pce_xref_gui:gxref_called/2. 559:- autoload(library(prolog_xref), [xref_called/4]). 560 561pce_xref_guigxref_called(Source, Callable) :- 562 nonvar(Source), 563 callable(Callable), 564 !, 565 ( xref_called_cond(Source, Callable, _) 566 -> true 567 ; scasp_called(Callable) 568 -> true 569 ; xref_dynamic(Source, Callable), 570 scasp_negate(Callable, NegCallable), 571 xref_dynamic(Source, NegCallable), 572 xref_called_cond(Source, NegCallable, _) 573 ). 574 575xref_dynamic(Source, Callable) :- 576 xref_defined(Source, Callable, dynamic(_)), !. 577xref_dynamic(Source, Callable) :- 578 xref_defined(Source, Callable, thread_local(_)). 579 580xref_called_cond(Source, Callable, Cond) :- 581 xref_called(Source, Callable, By, Cond), 582 By \= Callable. % recursive calls 583 584scasp_negate(Callable, NegCallable) :- 585 atom(Callable), 586 !, 587 scasp_neg_atom(Callable, NegCallable). 588scasp_negate(Callable, NegCallable) :- 589 compound_name_arguments(Callable, Name, Args), 590 scasp_neg_atom(Name, NegName), 591 compound_name_arguments(NegCallable, NegName, Args). 592 593scasp_neg_atom(Neg, Pos) :- 594 atom_concat(-, Pos, Neg), 595 !. 596scasp_neg_atom(Pos, Neg) :- 597 atom_concat(-, Pos, Neg). 598 599scasp_called(pr_pred_predicate(_,_,_,_)). 600scasp_called(scasp_expand_program(_,_,_,_)). 601scasp_called(-)
Embed sCASP programs in Prolog sources
This module allows embedding sCASP programs inside a Prolog module. Currently the syntax is:
The idea is to create wrappers for the sCASP user predicates in the target module that evaluate an sCASP query as a normal Prolog query, providing access to the model and justification. The bindings come available as normal Prolog bindings.
This is an alternative interface to defining the user accessible predicates using e.g., `:- scasp p/1, q/2.`, which will then establish the reachable predicates and perform the sCASP conversion on them. I think both have their value and the above one is simpler to start with.