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 '\u2209'/2, % Inequality 46 47 op(700, xfx, .\=.), 48 op(700, xfx, '\u2209'), 49 op(900, fy, not) 50 ]). 51:- use_module(ops). 52:- use_module(input). 53:- use_module(compile). 54:- use_module(predicates). 55:- use_module(solve). 56:- use_module(model). 57:- use_module(stack). 58:- use_module(options). 59:- use_module(listing). 60:- use_module(clp/disequality). 61 62:- use_module(library(debug)). 63:- use_module(library(apply)). 64:- use_module(library(error)). 65:- use_module(library(lists)). 66:- use_module(library(prolog_code)). 67 68:- meta_predicate 69 scasp_model(:), 70 scasp_justification(:, +), 71 not(0), 72 -(:). 73 74% one of `false`, `true`, `unicode` or `human` 75:- create_prolog_flag(scasp_show_model, 76 false, 77 [keep(true), type(atom)]). 78:- create_prolog_flag(scasp_show_justification, 79 false, 80 [keep(true), type(atom)]).
108:- thread_local 109 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.
131begin_scasp(Unit) :- 132 begin_scasp(Unit, all). 133 134begin_scasp(Unit, Exports) :- 135 scasp_module(Unit, Module), 136 prolog_load_context(module, Context), 137 source_location(File, Line), 138 '$set_source_module'(OldModule, Module), 139 '$declare_module'(Module, scasp, Context, File, Line, false), 140 scasp_push_operators, 141 '$style_check'(OldStyle, OldStyle), 142 style_check(-singleton), 143 discontiguous(Module:(#)/1), 144 asserta(loading_scasp(Unit, File, 145 _{ module:Module, 146 old_module:OldModule, 147 old_style:OldStyle, 148 exports:Exports 149 })). 150 151scasp_module(Unit, Module) :- 152 atom_concat('_scasp_', Unit, Module).
158end_scasp :- 159 throw(error(context_error(nodirective, end_scasp), _)). 160 161end_scasp(Clauses) :- 162 ( retract(loading_scasp(Unit, _File, Dict)) 163 -> _{ old_module:OldModule, 164 old_style:OldStyle, 165 exports:Exports 166 } :< Dict, 167 '$set_source_module'(_, OldModule), 168 scasp_pop_operators, 169 '$style_check'(_, OldStyle), 170 ( Exports == [] 171 -> Options = [unknown(fail)] 172 ; Options = [] 173 ), 174 scasp_compile_unit(Unit, Options), 175 link_clauses(OldModule, Unit, Clauses, Exports) 176 ; throw(error(context_error(scasp_close(-)), _)) 177 ). 178 179loading_scasp(Unit) :- 180 source_location(File, _Line), 181 loading_scasp(Unit,File,_). 182 183userterm_expansion(end_of_file, _) :- 184 loading_scasp(Unit), 185 print_message(error, scasp(not_closed_program(Unit))), 186 end_scasp, 187 fail. 188userterm_expansion((:- Constraint), Clause) :- 189 loading_scasp(_), 190 Constraint \== end_scasp, 191 !, 192 Clause = ('_false_0' :- Constraint). 193userterm_expansion((?- Query), Clause) :- 194 loading_scasp(_), 195 !, 196 Clause = scasp_query(Query, 1). 197userterm_expansion(#(discontiguous(Preds)), (:- discontiguous(Preds))) :- 198 loading_scasp(_). 199userterm_expansion(#(pred(Preds)), #(pred(Preds))) :- 200 loading_scasp(_), 201 prolog_load_context(variable_names, Vars), 202 maplist(bind_var, Vars). 203userterm_expansion((:- end_scasp), Clauses) :- 204 \+ current_prolog_flag(xref, true), 205 end_scasp(Clauses). 206 207bind_var(Name = $(Name)).
214:- thread_local 215 done_unit/1. % allow for mutually recursive #include 216 217scasp_compile_unit(Unit, Options) :- 218 call_cleanup(scasp_compile_unit_(Unit, Options), 219 retractall(done_unit(_))). 220 221scasp_compile_unit_(Unit, Options) :- 222 scasp_module(Unit, Module), 223 ( current_module(Module) 224 -> true 225 ; existence_error(scasp_unit, Unit) 226 ), 227 findall(Clause, scasp_clause(Unit, Clause), Clauses), 228 scasp_compile(Module:Clauses, Options).
234scasp_clause(Unit, _Clause) :- 235 done_unit(Unit), 236 !, 237 fail. 238scasp_clause(Unit, Clause) :- 239 assertz(done_unit(Unit)), 240 scasp_module(Unit, Module), 241 QHead = Module:Head, 242 predicate_property(QHead, interpreted), 243 \+ scasp_compiled(Head), 244 \+ predicate_property(QHead, imported_from(_)), 245 @(clause(Head, Body), Module), 246 mkclause(Head, Body, Clause). 247 248mkclause(scasp_query(Query,_N), true, Clause) => 249 Clause = (?- Query). 250mkclause(#(include(Unit)), true, Clause) => 251 scasp_clause(Unit, Clause). 252mkclause(#(Directive), true, Clause) => % TBD: #abducible 253 Clause = #(Directive). 254mkclause('_false_0', Body, Clause) => 255 Clause = (:- Body). 256mkclause(Head, true, Clause) => 257 Clause = Head. 258mkclause(Head, Body, Clause) => 259 Clause = (Head :- Body).
266link_clauses(_ContextModule, Unit, Clauses, Exports) :- 267 scasp_module(Unit, Module), 268 findall(Head, link_predicate(Module:Head), Heads), 269 check_exports(Exports, Heads), 270 convlist(link_clause(Module, Exports), Heads, Clauses). 271 272link_predicate(Module:Head) :- 273 Module:pr_user_predicate(PI), 274 \+ not_really_a_user_predicate(PI), 275 pi_head(PI, Head). 276 277% TBD: merge with user_predicate/1. 278not_really_a_user_predicate((not)/1). 279not_really_a_user_predicate(o_nmr_check/0). 280not_really_a_user_predicate(global_constraints/0). 281 282check_exports(all, _) :- !. 283check_exports(Exports, Heads) :- 284 must_be(list, Exports), 285 maplist(check_export(Heads), Exports). 286 287check_export(Heads, -Name/Arity) :- 288 !, 289 atom_concat(-, Name, NName), 290 check_export(Heads, NName/Arity). 291check_export(Heads, Export) :- 292 pi_head(Export, EHead), % raises an exception on malformed PI. 293 ( memberchk(EHead, Heads) 294 -> true 295 ; existence_error(predicate, Export) 296 ). 297 298link_clause(Module, Exports, Head, 299 (Head :- scasp_embed:scasp_call(Module:Head))) :- 300 ( Exports == all 301 -> true 302 ; functor(Head, NName, Arity), 303 atom_concat(-, Name, NName) 304 -> memberchk(-Name/Arity, Exports) 305 ; pi_head(PI, Head), 306 memberchk(PI, Exports) 307 ).
314:- public scasp_call/1. 315 316scasp_call(Query) :- 317 scasp_compile_query(Query, Compiled, []), 318 scasp_stack(StackIn), 319 solve(Compiled, StackIn, StackOut, Model), 320 save_model(Model), 321 Compiled = M:_, % TBD: Properly handle the module 322 save_stack(M:StackOut).
331not(M:Query) :-
332 clause(M:Query, scasp_embed:scasp_call(Module:Query)),
333 scasp_call(Module:not(Query)).
339-(M:Query) :-
340 Query =.. [Name|Args],
341 atom_concat(-, Name, NName),
342 NQuery =.. [NName|Args],
343 clause(M:NQuery, scasp_embed:scasp_call(Module:NQuery)),
344 scasp_call(Module:NQuery).
353save_model(Model) :-
354 ( nb_current(scasp_model, Model0)
355 -> append(Model, Model0, FullModel),
356 b_setval(scasp_model, FullModel)
357 ; b_setval(scasp_model, Model)
358 ).366scasp_model(M:Model) :- 367 scasp_model(M:Model, []). 368 369scasp_model(M:Model, _Options) :- 370 nb_current(scasp_model, RawModel), 371 canonical_model(RawModel, Model1), 372 unqualify_model(Model1, M, Model). 373 374save_stack(Stack) :- 375 b_setval(scasp_stack, Stack), 376 justification_tree(Stack, Tree, []), 377 b_setval(scasp_tree, Tree).
384scasp_stack(Stack) :-
385 ( nb_current(scasp_stack, Stack0)
386 -> Stack = Stack0
387 ; Stack = []
388 ).394scasp_justification(M:Tree, Options) :- 395 nb_current(scasp_tree, Tree0), 396 remove_origins(Tree0, Tree1, Options), 397 unqualify_justitication_tree(Tree1, M, Tree). 398 399remove_origins(Tree0, Tree, Options) :- 400 option(source(false), Options), 401 !, 402 remove_origins(Tree0, Tree). 403remove_origins(Tree, Tree, _). 404 405remove_origins(M:Tree0, Result) => 406 Result = M:Tree, 407 remove_origins(Tree0, Tree). 408remove_origins(Term0-Children0, Result) => 409 Result = Term-Children, 410 remove_origin(Term0, Term), 411 maplist(remove_origins, Children0, Children). 412remove_origins(Nodes0, Nodes), is_list(Nodes0) => 413 maplist(remove_origins, Nodes0, Nodes). 414remove_origins(Node0, Node) => 415 remove_origin(Node0, Node). 416 417remove_origin(goal_origin(Term, _), Result) => 418 Result = Term. 419remove_origin(Term, Result) => 420 Result = Term.
427scasp_listing(Unit, Options) :- 428 scasp_module(Unit, Module), 429 scasp_portray_program(Module:Options). 430 431:- residual_goals(scasp_residuals).
438scasp_residuals --> 439 { '$current_typein_module'(TypeIn), 440 scasp_residual_types(Types) 441 }, 442 scasp_residuals(Types, TypeIn). 443 444scasp_residuals([], _) --> 445 []. 446scasp_residuals([model(Options)|T], M) --> 447 ( {scasp_model(M:Model, Options)} 448 -> [ scasp_show_model(Model, Options) ] 449 ; [] 450 ), 451 scasp_residuals(T, M). 452scasp_residuals([justification(Options)|T], M) --> 453 ( {scasp_stack(Stack), Stack \== []} 454 -> [ scasp_show_stack(M:Stack, Options) ] 455 ; [] 456 ), 457 scasp_residuals(T, M). 458 459scasp_residual_types(Types) :- 460 findall(Type, scasp_residual_type(Type), Types). 461 462scasp_residual_type(model(Options)) :- 463 current_prolog_flag(scasp_show_model, Spec), 464 Spec \== false, 465 res_options(Spec, Options). 466scasp_residual_type(justification(Options)) :- 467 current_prolog_flag(scasp_show_justification, Spec), 468 Spec \== false, 469 res_options(Spec, Options). 470 471res_options(List, Options), is_list(List) => 472 Options = List. 473res_options(true, Options) => 474 Options = [unicode(true)]. 475res_options(unicode, Options) => 476 Options = [unicode(true)]. 477res_options(human, Options) => 478 Options = [human(true)]. 479 480user:portray(scasp_show_model(Model, Options)) :- 481 ansi_format(comment, '% s(CASP) model~n', []), 482 print_model(Model, Options). 483user:portray(scasp_show_stack(M:Stack, Options)) :- 484 ansi_format(comment, '% s(CASP) justification', []), 485 justification_tree(Stack, Tree0, Options), 486 unqualify_justitication_tree(Tree0, M, Tree), 487 print_justification_tree(Tree, [full_stop(false)|Options]). 488user:portray('\u2209'(V,S)) :- % not element of 489 format('~p \u2209 ~p', [V, S]). 490 491 492 /******************************* 493 * HIGHLIGHT SUPPORT * 494 *******************************/ 495 496:- multifile 497 prolog:alternate_syntax/4, 498 prolog:xref_update_syntax/2. 499 500prologalternate_syntax(scasp, Module, Setup, Restore) :- 501 Setup = scasp_ops:scasp_push_operators(Module), 502 Restore = scasp_ops:scasp_pop_operators. 503 504prologxref_update_syntax(begin_scasp(_Unit), Module) :- 505 scasp_ops:scasp_push_operators(Module). 506prologxref_update_syntax(begin_scasp(_Unit, _Exports), Module) :- 507 scasp_ops:scasp_push_operators(Module). 508prologxref_update_syntax(end_scasp, _Module) :- 509 scasp_ops:scasp_pop_operators. 510 511:- multifile 512 prolog_colour:term_colours/2. 513 514prolog_colourterm_colours(#(Directive), 515 expanded - [DirColours]) :- 516 debug(scasp(highlight), 'Got ~p', [Directive]), 517 dir_colours(Directive, DirColours). 518 519dir_colours(pred(_Head::_Template), 520 expanded - 521 [ expanded - 522 [ body, 523 comment(_) 524 ] 525 ]). 526dir_colours(show(Preds), 527 expanded - [Colours]) :- 528 decl_show_colours(Preds, Colours). 529dir_colours(include(_Unit), 530 expanded - 531 [ classify 532 ]). 533dir_colours(discontiguous(_Preds), 534 expanded - 535 [ declarations(discontiguous) 536 ]). 537 538decl_show_colours((A,B), Colours) => 539 Colours = classify-[CA,CB], 540 decl_show_colours(A, CA), 541 decl_show_colours(B, CB). 542decl_show_colours(not(_A), Colours) => 543 Colours = built_in-[declarations(show)]. 544decl_show_colours(_A, Colours) => 545 Colours = declarations(show). 546 547 548 /******************************* 549 * GXREF SUPPORT * 550 *******************************/
s(CASP) hooks561:- multifile pce_xref_gui:gxref_called/2. 562:- autoload(library(prolog_xref), [xref_called/4]). 563 564pce_xref_guigxref_called(Source, Callable) :- 565 nonvar(Source), 566 callable(Callable), 567 !, 568 ( xref_called_cond(Source, Callable, _) 569 -> true 570 ; scasp_called(Callable) 571 -> true 572 ; xref_dynamic(Source, Callable), 573 scasp_negate(Callable, NegCallable), 574 xref_dynamic(Source, NegCallable), 575 xref_called_cond(Source, NegCallable, _) 576 ). 577 578xref_dynamic(Source, Callable) :- 579 xref_defined(Source, Callable, dynamic(_)), !. 580xref_dynamic(Source, Callable) :- 581 xref_defined(Source, Callable, thread_local(_)). 582 583xref_called_cond(Source, Callable, Cond) :- 584 xref_called(Source, Callable, By, Cond), 585 By \= Callable. % recursive calls 586 587scasp_negate(Callable, NegCallable) :- 588 atom(Callable), 589 !, 590 scasp_neg_atom(Callable, NegCallable). 591scasp_negate(Callable, NegCallable) :- 592 compound_name_arguments(Callable, Name, Args), 593 scasp_neg_atom(Name, NegName), 594 compound_name_arguments(NegCallable, NegName, Args). 595 596scasp_neg_atom(Neg, Pos) :- 597 atom_concat(-, Pos, Neg), 598 !. 599scasp_neg_atom(Pos, Neg) :- 600 atom_concat(-, Pos, Neg). 601 602scasp_called(pr_pred_predicate(_,_,_,_)). 603scasp_called(scasp_expand_program(_,_,_,_)). 604scasp_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.