1:- module(scasp_dyncall, 2 [ scasp/2, % :Query, +Options 3 scasp_query_clauses/2, % :Query, -Clauses 4 scasp_model/1, % -Model 5 scasp_justification/2, % -Tree, +Options 6 7 scasp_show/2, % :Query,+What 8 9 (scasp_dynamic)/1, % :Spec 10 scasp_assert/1, % :Clause 11 scasp_assert/2, % :Clause 12 scasp_retract/1, % :Clause 13 scasp_retractall/1, % :Head 14 scasp_abolish/1, % :PredicateIndicator 15 (#)/1, % :Directive 16 (#)/2, % :Directive, +Pos 17 (pred)/1, 18 (show)/1, 19 (abducible)/1, 20 (abducible)/2, 21 22 (#=)/2, 23 (#<>)/2, 24 (#<)/2, 25 (#>)/2, 26 (#=<)/2, 27 (#>=)/2, 28 29 op(900, fy, not), 30 op(950, xfx, ::), % pred not x :: "...". 31 op(1200, fx, #), 32 op(1150, fx, pred), 33 op(1150, fx, show), 34 op(1150, fx, abducible), 35 op(1150, fx, scasp_dynamic), 36 op(700, xfx, #=), 37 op(700, xfx, #<>), 38 op(700, xfx, #<), 39 op(700, xfx, #>), 40 op(700, xfx, #=<), 41 op(700, xfx, #>=) 42 ]). 43:- use_module(compile). 44:- use_module(embed). 45:- use_module(common). 46:- use_module(modules). 47:- use_module(source_ref). 48:- use_module(listing). 49:- use_module(clp/clpq, [apply_clpq_constraints/1]). 50:- use_module(pr_rules, [process_pr_pred/5]). 51:- use_module(predicates, [prolog_builtin/1, clp_builtin/1]). 52 53:- use_module(library(apply), [maplist/3, exclude/3, maplist/2]). 54:- use_module(library(assoc), [empty_assoc/1, get_assoc/3, put_assoc/4]). 55:- use_module(library(error), 56 [ instantiation_error/1, 57 permission_error/3, 58 type_error/2, 59 must_be/2 60 ]). 61:- use_module(library(lists), [member/2, append/3]). 62:- use_module(library(modules), 63 [in_temporary_module/3, current_temporary_module/1]). 64:- use_module(library(option), [option/2]). 65:- use_module(library(ordsets), [ord_intersect/2, ord_union/3]). 66:- use_module(library(prolog_code), [pi_head/2]). 67 68:- meta_predicate 69 scasp(, ), 70 scasp_show(, ), 71 scasp_query_clauses(, ), 72 scasp_dynamic(), 73 scasp_assert(), 74 scasp_retract(), 75 scasp_retractall(), 76 scasp_abolish(), 77 pred(), 78 show(), 79 abducible().
s(CASP) semantics. This performs the following
steps:
s(CASP) representation in a temporary
modules(CASP) solverOptions are passed to scasp_compile/2. Other options processed:
s(CASP) model, a list of model terms.
See scasp_model/1.s(CASP) justification tree. See
scasp_justification/2 for details.false, do not include source origin terms into the
final tree.122scasp(Query, Options) :- 123 scasp_query_clauses(Query, Clauses), 124 qualify(Query, SrcModule:QQuery), 125 expand_program(SrcModule, Clauses, Clauses1, QQuery, QQuery1), 126 in_temporary_module( 127 Module, 128 prepare(Clauses1, Module, Options), 129 scasp_call_and_results(Module:QQuery1, SrcModule, Options)). 130 131prepare(Clauses, Module, Options) :- 132 scasp_compile(Module:Clauses, Options), 133 ( option(write_program(_), Options) 134 -> scasp_portray_program(Module:Options) 135 ; true 136 ). 137 138qualify(M:Q0, M:Q) :- 139 qualify(Q0, M, Q1), 140 intern_negation(Q1, Q). 141 142expand_program(SrcModule, Clauses, Clauses1, QQuery, QQuery1) :- 143 current_predicate(SrcModule:scasp_expand_program/4), 144 SrcModule:scasp_expand_program(Clauses, Clauses1, QQuery, QQuery1), 145 !. 146expand_program(_, Clauses, Clauses, QQuery, QQuery). 147 148 149scasp_call_and_results(Query, SrcModule, Options) :- 150 scasp_embed:scasp_call(Query), 151 ( option(model(Model), Options) 152 -> scasp_model(SrcModule:Model) 153 ; true 154 ), 155 ( option(tree(Tree), Options) 156 -> scasp_justification(SrcModule:Tree, Options) 157 ; true 158 ).
s(CASP) program. Currently
What is one of:
?- scasp_show(Query, code(user(false), constraints(true))).
172scasp_show(Query, What) :- 173 What =.. [Type|Options], 174 scasp_show(Query, Type, Options). 175 176scasp_show(Query, code, Options) => 177 Query = M:_, 178 scasp_query_clauses(Query, Clauses), 179 qualify(Query, SrcModule:QQuery), 180 expand_program(SrcModule, Clauses, Clauses1, QQuery, _QQuery1), 181 in_temporary_module( 182 Module, 183 prepare(Clauses1, Module, []), 184 scasp_portray_program(Module:[source_module(M)|Options])).
190:- det(scasp_query_clauses/2). 191 192scasp_query_clauses(Query, Clauses) :- 193 query_callees(Query, Callees0), 194 include_global_constraint(Callees0, Constraints, Callees), 195 findall(Clause, scasp_clause(Callees, Clause), Clauses, QConstraints), 196 maplist(mkconstraint, Constraints, QConstraints). 197 198scasp_clause(Callees, source(ClauseRef, Clause)) :- 199 member(PI, Callees), 200 pi_head(PI, M:Head), 201 @(clause(Head, Body, ClauseRef), M), 202 mkclause(Head, Body, M, Clause). 203 204mkclause(Head, true, M, Clause) => 205 qualify(Head, M, Clause). 206mkclause(Head, Body, M, Clause) => 207 qualify((Head:-Body), M, Clause). 208 209mkconstraint(source(Ref, M:Body), source(Ref, (:- Constraint))) :- 210 qualify(Body, M, Constraint). 211 212qualify(-(Head), M, Q) => 213 Q = -QHead, 214 qualify(Head, M, QHead). 215qualify(not(Head), M, Q) => 216 Q = not(QHead), 217 qualify(Head, M, QHead). 218qualify(findall(Templ, Head, List), M, Q) => 219 Q = findall(Templ, QHead, List), 220 qualify(Head, M, QHead). 221qualify((A,B), M, Q) => 222 Q = (QA,QB), 223 qualify(A, M, QA), 224 qualify(B, M, QB). 225qualify((A:-B), M, Q) => 226 Q = (QA:-QB), 227 qualify(A, M, QA), 228 qualify(B, M, QB). 229qualify(G, M, Q), callable(G) => 230 ( built_in(G) 231 -> Q = G 232 ; implementation(M:G, Callee), 233 encoded_module_term(Callee, Q) 234 ).
243query_callees(M:Query, Callees) :- 244 findall(Call, body_calls_pi(Query,M,Call), Calls0), 245 sort(Calls0, Calls), 246 callee_graph(Calls, Callees). 247 248body_calls_pi(Query, M, PI) :- 249 body_calls(Query, M, Call), 250 pi_head(PI, Call). 251 252callee_graph(Preds, Nodes) :- 253 empty_assoc(Expanded), 254 callee_closure(Preds, Expanded, Preds, Nodes0), 255 sort(Nodes0, Nodes). 256 257callee_closure([], _, Preds, Preds). 258callee_closure([H|T], Expanded, Preds0, Preds) :- 259 ( get_assoc(H, Expanded, _) 260 -> callee_closure(T, Expanded, Preds0, Preds) 261 ; put_assoc(H, Expanded, true, Expanded1), 262 pi_head(H, Head), 263 predicate_callees(Head, Called), 264 exclude(expanded(Expanded1), Called, New), 265 append(New, T, Agenda), 266 append(New, Preds0, Preds1), 267 callee_closure(Agenda, Expanded1, Preds1, Preds) 268 ). 269 270expanded(Assoc, PI) :- 271 get_assoc(PI, Assoc, _).
275include_global_constraint(Callees0, Constraints, Callees) :- 276 include_global_constraint(Callees0, Callees, [], Constraints). 277 278include_global_constraint(Callees0, Callees, Constraints0, Constraints) :- 279 global_constraint(Constraint), 280 Constraint = source(_, Body), 281 \+ ( member(source(_, Body0), Constraints0), 282 Body =@= Body0 283 ), 284 query_callees(Body, Called), 285 ord_intersect(Callees0, Called), 286 !, 287 ord_union(Callees0, Called, Callees1), 288 include_global_constraint(Callees1, Callees, 289 [Constraint|Constraints0], Constraints). 290include_global_constraint(Callees, Callees, Constraints, Constraints). 291 292 293global_constraint(source(Ref, M:Body)) :- 294 ( current_temporary_module(M) 295 ; current_module(M) 296 ), 297 current_predicate(M:(-)/0), 298 \+ predicate_property(M:(-), imported_from(_)), 299 @(clause(-, Body, Ref), M).
306:- dynamic predicate_callees_c/4. 307 308predicate_callees(M:Head, Callees) :- 309 predicate_callees_c(Head, M, Gen, Callees0), 310 predicate_generation(M:Head, Gen), 311 !, 312 Callees = Callees0. 313predicate_callees(M:Head, Callees) :- 314 module_property(M, class(temporary)), 315 !, 316 predicate_callees_nc(M:Head, Callees). 317predicate_callees(M:Head, Callees) :- 318 retractall(predicate_callees_c(Head, M, _, _)), 319 predicate_callees_nc(M:Head, Callees0), 320 predicate_generation(M:Head, Gen), 321 assertz(predicate_callees_c(Head, M, Gen, Callees0)), 322 Callees = Callees0. 323 324predicate_callees_nc(Head, Callees) :- 325 findall(Callee, predicate_calls(Head, Callee), Callees0), 326 sort(Callees0, Callees). 327 328predicate_calls(Head0, PI) :- 329 generalise(Head0, M:Head), 330 @(clause(Head, Body), M), 331 body_calls(Body, M, Callee), 332 pi_head(PI, Callee). 333 334body_calls(Goal, _M, _), var(Goal) => 335 instantiation_error(Goal). 336body_calls(true, _M, _) => fail. 337body_calls((A,B), M, Callee) => 338 ( body_calls(A, M, Callee) 339 ; body_calls(B, M, Callee) 340 ). 341body_calls(not(A), M, Callee) => 342 body_calls(A, M, Callee). 343body_calls(findall(_,G,_), M, Callee) => 344 body_calls(G, M, Callee). 345body_calls(N, M, Callee), rm_classic_negation(N,A) => 346 body_calls(A, M, Callee). 347body_calls(M:A, _, Callee), atom(M) => 348 body_calls(A, M, Callee). 349body_calls(G, _M, _CalleePM), callable(G), built_in(G) => 350 fail. 351body_calls(G, M, CalleePM), callable(G) => 352 implementation(M:G, Callee0), 353 generalise(Callee0, Callee), 354 ( predicate_property(Callee, interpreted), 355 \+ predicate_property(Callee, meta_predicate(_)) 356 -> pm(Callee, CalleePM) 357 ; \+ predicate_property(Callee, _) 358 -> pm(Callee, CalleePM) % undefined 359 ; pi_head(CalleePI, Callee), 360 permission_error(scasp, procedure, CalleePI) 361 ). 362body_calls(G, _, _) => 363 type_error(callable, G). 364 365built_in(Head) :- 366 prolog_builtin(Head). 367built_in(Head) :- 368 clp_builtin(Head). 369built_in(_ is _). 370built_in(findall(_,_,_)). 371 372rm_classic_negation(-Goal, Goal) :- 373 !. 374rm_classic_negation(Goal, PGoal) :- 375 functor(Goal, Name, _), 376 atom_concat(-, Plain, Name), 377 Goal =.. [Name|Args], 378 PGoal =.. [Plain|Args]. 379 380pm(P, P). 381pm(M:P, M:MP) :- 382 intern_negation(-P, MP). 383 384implementation(M0:Head, M:Head) :- 385 predicate_property(M0:Head, imported_from(M1)), 386 !, 387 M = M1. 388implementation(Head, Head). 389 390generalise(M:Head0, Gen), atom(M) => 391 Gen = M:Head, 392 generalise(Head0, Head). 393generalise(-Head0, Gen) => 394 Gen = -Head, 395 generalise(Head0, Head). 396generalise(Head0, Head) => 397 functor(Head0, Name, Arity), 398 functor(Head, Name, Arity). 399 400predicate_generation(Head, Gen) :- 401 predicate_property(Head, last_modified_generation(Gen0)), 402 !, 403 Gen = Gen0. 404predicate_generation(_, 0). 405 406 407 /******************************* 408 * MANIPULATING THE PROGRAM * 409 *******************************/
:- scasp_dynamic p/1. :- scasp_dynamic p/1 as shared.
418scasp_dynamic(M:Spec) :- 419 scasp_dynamic(Spec, M, private). 420scasp_dynamic(M:(Spec as Scoped)) :- 421 scasp_dynamic(Spec, M, Scoped). 422 423scasp_dynamic((A,B), M, Scoped) => 424 scasp_dynamic(A, M, Scoped), 425 scasp_dynamic(B, M, Scoped). 426scasp_dynamic(Name/Arity, M, Scoped) => 427 atom_concat(-, Name, NName), 428 ( Scoped == shared 429 -> dynamic((M:Name/Arity, 430 M:NName/Arity)) 431 ; thread_local((M:Name/Arity, 432 M:NName/Arity)) 433 ). 434 435:- multifile system:term_expansion/2. 436 437systemterm_expansion((:- scasp_dynamic(Spec)), Directives) :- 438 phrase(scasp_dynamic_direcives(Spec), Directives). 439 440scasp_dynamic_direcives(Spec as Scope) --> 441 !, 442 scasp_dynamic_direcives(Spec, Scope). 443scasp_dynamic_direcives(Spec) --> 444 !, 445 scasp_dynamic_direcives(Spec, private). 446 447scasp_dynamic_direcives(Var, _) --> 448 { var(Var), !, fail }. 449scasp_dynamic_direcives((A,B), Scope) --> 450 scasp_dynamic_direcives(A, Scope), 451 scasp_dynamic_direcives(B, Scope). 452scasp_dynamic_direcives(Name/Arity, Scope) --> 453 { atom_concat(-, Name, NName) }, 454 ( {Scope == shared} 455 -> [(:- dynamic((Name/Arity, NName/Arity)))] 456 ; [(:- thread_local((Name/Arity, NName/Arity)))] 457 ).
-(Term), indicating classical negation. Also deals with global
constraints written in any of these formats:
false :- Constraint.:- Constraint.472scasp_assert(Clause) :- 473 scasp_assert(Clause, false). 474 475scasp_assert(M:(-Head :- Body0), Pos) => 476 intern_negation(-Head, MHead), 477 expand_goal(Body0, Body), 478 scasp_assert_(M:(MHead :- Body), Pos). 479scasp_assert(M:(-Head), Pos) => 480 intern_negation(-Head, MHead), 481 scasp_assert_(M:(MHead), Pos). 482scasp_assert(M:(:- Body0), Pos) => 483 expand_goal(Body0, Body), 484 scasp_assert_(M:((-) :- Body), Pos). 485scasp_assert(M:(false :- Body0), Pos) => 486 expand_goal(Body0, Body), 487 scasp_assert_(M:((-) :- Body), Pos). 488scasp_assert(M:(Head :- Body0), Pos) => 489 expand_goal(Body0, Body), 490 scasp_assert_(M:(Head :- Body), Pos). 491scasp_assert(Head, Pos) => 492 scasp_assert_(Head, Pos). 493 494scasp_assert_(Clause, false) => 495 assertz(Clause). 496scasp_assert_(Clause, Pos) => 497 assertz(Clause, Ref), 498 assertz(scasp_dynamic_clause_position(Ref, Pos)). 499 500scasp_assert_into(M, Pos, Rule) :- 501 scasp_assert(M:Rule, Pos). 502 503scasp_retract(M:(-Head :- Body0)) => 504 intern_negation(-Head, MHead), 505 expand_goal(Body0, Body), 506 retract(M:(MHead :- Body)). 507scasp_retract(M:(-Head)) => 508 intern_negation(-Head, MHead), 509 retract(M:()). 510scasp_retract(M:(:- Body0)) => 511 expand_goal(Body0, Body), 512 retract(M:((-) :- Body)). 513scasp_retract(M:(false :- Body0)) => 514 expand_goal(Body0, Body), 515 retract(M:((-) :- Body)). 516scasp_retract(M:(Head :- Body0)) => 517 expand_goal(Body0, Body), 518 retract(M:(Head :- Body)). 519scasp_retract(Head) => 520 retract(Head). 521 522scasp_retractall(M:(-Head)) => 523 intern_negation(-Head, MHead), 524 retractall(M:). 525scasp_retractall(Head) => 526 retractall(Head).
533scasp_abolish(M:(Name/Arity)) => 534 pi_head(Name/Arity, Head), 535 scasp_retractall(M:Head), 536 scasp_retractall(M:(-Head)). 537 538 539 /******************************* 540 * DIRECTIVES * 541 *******************************/
s(CASP) directives. Same as :- Directive.. Provides
compatibility with sCASP sources as normally found.(Directive) :- #(Directive, false). 549 550#(M:pred(Spec), _) => pred(M:Spec). 551#(M:show(Spec), _) => show(M:Spec). 552#(M:abducible(Spec), Pos) => abducible(M:Spec, Pos). 553 554pred(M:(Spec :: Template)) => 555 process_pr_pred(Spec :: Template, Atom, Children, Cond, Human), 556 assertz(M:pr_pred_predicate(Atom, Children, Cond, Human)). 557 558show(M:PIs) => 559 phrase(show(PIs), Clauses), 560 maplist(assert_show(M), Clauses). 561 562assert_show(M, Clause) :- 563 assertz(M:). 564 565show(Var) --> 566 { var(Var), 567 instantiation_error(Var) 568 }. 569show((A,B)) --> 570 !, 571 show(A), 572 show(B). 573show(not(PI)) --> 574 { pi_head(PI, Head) }, 575 [ pr_show_predicate(not(Head)) ]. 576show(PI) --> 577 { pi_head(PI, Head) }, 578 [ pr_show_predicate(Head) ].
585abducible(Spec) :- abducible(Spec, false). 586 587abducible(M:(A,B), Pos) => 588 abducible(M:A, Pos), 589 abducible(M:B, Pos). 590abducible(M:Head, Pos), callable(Head) => 591 abducible_rules(Head, Rules), 592 discontiguous(M:('abducible$'/1, 'abducible$$'/1)), 593 maplist(scasp_assert_into(M, Pos), Rules). 594 595abducible_rules(Head, 596 [ (Head :- not(NegHead), 'abducible$'(Head)), 597 (NegHead :- not Head), 598 ('abducible$'(Head) :- not 'abducible$$'(Head)), 599 ('abducible$$'(Head) :- not 'abducible$'(Head)) 600 ]) :- 601 intern_negation(-Head, NegHead). 602 603abducible(Var) --> 604 { var(Var), 605 instantiation_error(Var) 606 }. 607abducible((A,B)) --> 608 !, 609 abducible(A), 610 abducible(B). 611abducible(Head) --> 612 { must_be(callable, Head), 613 abducible_rules(Head, Clauses) 614 }, 615 list(Clauses). 616 617list([]) --> []. 618list([H|T]) --> [H], list(T). 619 620 621 622 /******************************* 623 * EXPAND * 624 *******************************/ 625 626userterm_expansion(-Fact, MFact) :- 627 callable(Fact), 628 Fact \= _:_, 629 intern_negation(-Fact, MFact). 630userterm_expansion((-Head :- Body), (MHead :- Body)) :- 631 callable(Head), 632 Head \= _:_, 633 intern_negation(-Head, MHead). 634userterm_expansion((false :- Body), ((-) :- Body)). 635userterm_expansion((:- pred(SpecIn)), 636 pr_pred_predicate(Atom, Children, Cond, Human)) :- 637 process_pr_pred(SpecIn, Atom, Children, Cond, Human). 638userterm_expansion((:- show(SpecIn)), Clauses) :- 639 phrase(show(SpecIn), Clauses). 640userterm_expansion((:- abducible(SpecIn)), Clauses) :- 641 phrase(abducible(SpecIn), Clauses). 642userterm_expansion((# pred(SpecIn)), 643 pr_pred_predicate(Atom, Children, Cond, Human)) :- 644 process_pr_pred(SpecIn, Atom, Children, Cond, Human). 645userterm_expansion((# show(SpecIn)), Clauses) :- 646 phrase(show(SpecIn), Clauses). 647userterm_expansion((# abducible(SpecIn)), Clauses) :- 648 phrase(abducible(SpecIn), Clauses). 649 650usergoal_expansion(-Goal, MGoal) :- 651 callable(Goal), 652 intern_negation(-Goal, MGoal). 653 654 655 /******************************* 656 * CLP * 657 *******************************/
s(CASP) constraints. This implementation is
normally not used and mostly makes the program analysis work.669A #= B :- apply_clpq_constraints(A #= B). 670A #<> B :- apply_clpq_constraints(A #<> B). 671A #< B :- apply_clpq_constraints(A #< B). 672A #> B :- apply_clpq_constraints(A #> B). 673A #=< B :- apply_clpq_constraints(A #=< B). 674A #>= B :- apply_clpq_constraints(A #>= B). 675 676 677 /******************************* 678 * SANDBOX * 679 *******************************/ 680 681:- multifile 682 sandbox:safe_meta_predicate/1. 683 684% scasp/1 is safe as it only allows for pure Prolog predicates 685% and limited arithmetic. Note that this does allow calling e.g. 686% member/2. s(CASP) does not allow for calling _qualified goals, 687% lists:member(...), 688 689sandbox:safe_meta(scasp_dyncall:scasp(_, _), [])
This predicate assembles the clauses that are reachable from a given goal.
Issues: