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 in_temporary_module( 180 Module, 181 prepare(Clauses, Module, []), 182 scasp_portray_program(Module:[source_module(M)|Options])).
188:- det(scasp_query_clauses/2). 189 190scasp_query_clauses(Query, Clauses) :- 191 query_callees(Query, Callees0), 192 include_global_constraint(Callees0, Constraints, Callees), 193 findall(Clause, scasp_clause(Callees, Clause), Clauses, QConstraints), 194 maplist(mkconstraint, Constraints, QConstraints). 195 196scasp_clause(Callees, source(ClauseRef, Clause)) :- 197 member(PI, Callees), 198 pi_head(PI, M:Head), 199 @(clause(Head, Body, ClauseRef), M), 200 mkclause(Head, Body, M, Clause). 201 202mkclause(Head, true, M, Clause) => 203 qualify(Head, M, Clause). 204mkclause(Head, Body, M, Clause) => 205 qualify((Head:-Body), M, Clause). 206 207mkconstraint(source(Ref, M:Body), source(Ref, (:- Constraint))) :- 208 qualify(Body, M, Constraint). 209 210qualify(-(Head), M, Q) => 211 Q = -QHead, 212 qualify(Head, M, QHead). 213qualify(not(Head), M, Q) => 214 Q = not(QHead), 215 qualify(Head, M, QHead). 216qualify(findall(Templ, Head, List), M, Q) => 217 Q = findall(Templ, QHead, List), 218 qualify(Head, M, QHead). 219qualify((A,B), M, Q) => 220 Q = (QA,QB), 221 qualify(A, M, QA), 222 qualify(B, M, QB). 223qualify((A:-B), M, Q) => 224 Q = (QA:-QB), 225 qualify(A, M, QA), 226 qualify(B, M, QB). 227qualify(G, M, Q), callable(G) => 228 ( built_in(G) 229 -> Q = G 230 ; implementation(M:G, Callee), 231 encoded_module_term(Callee, Q) 232 ).
241query_callees(M:Query, Callees) :- 242 findall(Call, body_calls_pi(Query,M,Call), Calls0), 243 sort(Calls0, Calls), 244 callee_graph(Calls, Callees). 245 246body_calls_pi(Query, M, PI) :- 247 body_calls(Query, M, Call), 248 pi_head(PI, Call). 249 250callee_graph(Preds, Nodes) :- 251 empty_assoc(Expanded), 252 callee_closure(Preds, Expanded, Preds, Nodes0), 253 sort(Nodes0, Nodes). 254 255callee_closure([], _, Preds, Preds). 256callee_closure([H|T], Expanded, Preds0, Preds) :- 257 ( get_assoc(H, Expanded, _) 258 -> callee_closure(T, Expanded, Preds0, Preds) 259 ; put_assoc(H, Expanded, true, Expanded1), 260 pi_head(H, Head), 261 predicate_callees(Head, Called), 262 exclude(expanded(Expanded1), Called, New), 263 append(New, T, Agenda), 264 append(New, Preds0, Preds1), 265 callee_closure(Agenda, Expanded1, Preds1, Preds) 266 ). 267 268expanded(Assoc, PI) :- 269 get_assoc(PI, Assoc, _).
273include_global_constraint(Callees0, Constraints, Callees) :- 274 include_global_constraint(Callees0, Callees, [], Constraints). 275 276include_global_constraint(Callees0, Callees, Constraints0, Constraints) :- 277 global_constraint(Constraint), 278 Constraint = source(_, Body), 279 \+ ( member(source(_, Body0), Constraints0), 280 Body =@= Body0 281 ), 282 query_callees(Body, Called), 283 ord_intersect(Callees0, Called), 284 !, 285 ord_union(Callees0, Called, Callees1), 286 include_global_constraint(Callees1, Callees, 287 [Constraint|Constraints0], Constraints). 288include_global_constraint(Callees, Callees, Constraints, Constraints). 289 290 291global_constraint(source(Ref, M:Body)) :- 292 ( current_temporary_module(M) 293 ; current_module(M) 294 ), 295 current_predicate(M:(-)/0), 296 \+ predicate_property(M:(-), imported_from(_)), 297 @(clause(-, Body, Ref), M).
304:- dynamic predicate_callees_c/4. 305 306predicate_callees(M:Head, Callees) :- 307 predicate_callees_c(Head, M, Gen, Callees0), 308 predicate_generation(M:Head, Gen), 309 !, 310 Callees = Callees0. 311predicate_callees(M:Head, Callees) :- 312 module_property(M, class(temporary)), 313 !, 314 predicate_callees_nc(M:Head, Callees). 315predicate_callees(M:Head, Callees) :- 316 retractall(predicate_callees_c(Head, M, _, _)), 317 predicate_callees_nc(M:Head, Callees0), 318 predicate_generation(M:Head, Gen), 319 assertz(predicate_callees_c(Head, M, Gen, Callees0)), 320 Callees = Callees0. 321 322predicate_callees_nc(Head, Callees) :- 323 findall(Callee, predicate_calls(Head, Callee), Callees0), 324 sort(Callees0, Callees). 325 326predicate_calls(Head0, PI) :- 327 generalise(Head0, M:Head), 328 @(clause(Head, Body), M), 329 body_calls(Body, M, Callee), 330 pi_head(PI, Callee). 331 332body_calls(Goal, _M, _), var(Goal) => 333 instantiation_error(Goal). 334body_calls(true, _M, _) => fail. 335body_calls((A,B), M, Callee) => 336 ( body_calls(A, M, Callee) 337 ; body_calls(B, M, Callee) 338 ). 339body_calls(not(A), M, Callee) => 340 body_calls(A, M, Callee). 341body_calls(findall(_,G,_), M, Callee) => 342 body_calls(G, M, Callee). 343body_calls(N, M, Callee), rm_classic_negation(N,A) => 344 body_calls(A, M, Callee). 345body_calls(M:A, _, Callee), atom(M) => 346 body_calls(A, M, Callee). 347body_calls(G, _M, _CalleePM), callable(G), built_in(G) => 348 fail. 349body_calls(G, M, CalleePM), callable(G) => 350 implementation(M:G, Callee0), 351 generalise(Callee0, Callee), 352 ( predicate_property(Callee, interpreted), 353 \+ predicate_property(Callee, meta_predicate(_)) 354 -> pm(Callee, CalleePM) 355 ; \+ predicate_property(Callee, _) 356 -> pm(Callee, CalleePM) % undefined 357 ; pi_head(CalleePI, Callee), 358 permission_error(scasp, procedure, CalleePI) 359 ). 360body_calls(G, _, _) => 361 type_error(callable, G). 362 363built_in(Head) :- 364 prolog_builtin(Head). 365built_in(Head) :- 366 clp_builtin(Head). 367built_in(_ is _). 368built_in(findall(_,_,_)). 369 370rm_classic_negation(-Goal, Goal) :- 371 !. 372rm_classic_negation(Goal, PGoal) :- 373 functor(Goal, Name, _), 374 atom_concat(-, Plain, Name), 375 Goal =.. [Name|Args], 376 PGoal =.. [Plain|Args]. 377 378pm(P, P). 379pm(M:P, M:MP) :- 380 intern_negation(-P, MP). 381 382implementation(M0:Head, M:Head) :- 383 predicate_property(M0:Head, imported_from(M1)), 384 !, 385 M = M1. 386implementation(Head, Head). 387 388generalise(M:Head0, Gen), atom(M) => 389 Gen = M:Head, 390 generalise(Head0, Head). 391generalise(-Head0, Gen) => 392 Gen = -Head, 393 generalise(Head0, Head). 394generalise(Head0, Head) => 395 functor(Head0, Name, Arity), 396 functor(Head, Name, Arity). 397 398predicate_generation(Head, Gen) :- 399 predicate_property(Head, last_modified_generation(Gen0)), 400 !, 401 Gen = Gen0. 402predicate_generation(_, 0). 403 404 405 /******************************* 406 * MANIPULATING THE PROGRAM * 407 *******************************/
:- scasp_dynamic p/1. :- scasp_dynamic p/1 as shared.
416scasp_dynamic(M:Spec) :- 417 scasp_dynamic(Spec, M, private). 418scasp_dynamic(M:(Spec as Scoped)) :- 419 scasp_dynamic(Spec, M, Scoped). 420 421scasp_dynamic((A,B), M, Scoped) => 422 scasp_dynamic(A, M, Scoped), 423 scasp_dynamic(B, M, Scoped). 424scasp_dynamic(Name/Arity, M, Scoped) => 425 atom_concat(-, Name, NName), 426 ( Scoped == shared 427 -> dynamic((M:Name/Arity, 428 M:NName/Arity)) 429 ; thread_local((M:Name/Arity, 430 M:NName/Arity)) 431 ). 432 433:- multifile system:term_expansion/2. 434 435systemterm_expansion((:- scasp_dynamic(Spec)), Directives) :- 436 phrase(scasp_dynamic_direcives(Spec), Directives). 437 438scasp_dynamic_direcives(Spec as Scope) --> 439 !, 440 scasp_dynamic_direcives(Spec, Scope). 441scasp_dynamic_direcives(Spec) --> 442 !, 443 scasp_dynamic_direcives(Spec, private). 444 445scasp_dynamic_direcives(Var, _) --> 446 { var(Var), !, fail }. 447scasp_dynamic_direcives((A,B), Scope) --> 448 scasp_dynamic_direcives(A, Scope), 449 scasp_dynamic_direcives(B, Scope). 450scasp_dynamic_direcives(Name/Arity, Scope) --> 451 { atom_concat(-, Name, NName) }, 452 ( {Scope == shared} 453 -> [(:- dynamic((Name/Arity, NName/Arity)))] 454 ; [(:- thread_local((Name/Arity, NName/Arity)))] 455 ).
-(Term), indicating classical negation. Also deals with global
constraints written in any of these formats:
false :- Constraint.:- Constraint.470scasp_assert(Clause) :- 471 scasp_assert(Clause, false). 472 473scasp_assert(M:(-Head :- Body0), Pos) => 474 intern_negation(-Head, MHead), 475 expand_goal(Body0, Body), 476 scasp_assert_(M:(MHead :- Body), Pos). 477scasp_assert(M:(-Head), Pos) => 478 intern_negation(-Head, MHead), 479 scasp_assert_(M:(MHead), Pos). 480scasp_assert(M:(:- Body0), Pos) => 481 expand_goal(Body0, Body), 482 scasp_assert_(M:((-) :- Body), Pos). 483scasp_assert(M:(false :- Body0), Pos) => 484 expand_goal(Body0, Body), 485 scasp_assert_(M:((-) :- Body), Pos). 486scasp_assert(M:(Head :- Body0), Pos) => 487 expand_goal(Body0, Body), 488 scasp_assert_(M:(Head :- Body), Pos). 489scasp_assert(Head, Pos) => 490 scasp_assert_(Head, Pos). 491 492scasp_assert_(Clause, false) => 493 assertz(Clause). 494scasp_assert_(Clause, Pos) => 495 assertz(Clause, Ref), 496 assertz(scasp_dynamic_clause_position(Ref, Pos)). 497 498scasp_assert_into(M, Pos, Rule) :- 499 scasp_assert(M:Rule, Pos). 500 501scasp_retract(M:(-Head :- Body0)) => 502 intern_negation(-Head, MHead), 503 expand_goal(Body0, Body), 504 retract(M:(MHead :- Body)). 505scasp_retract(M:(-Head)) => 506 intern_negation(-Head, MHead), 507 retract(M:()). 508scasp_retract(M:(:- Body0)) => 509 expand_goal(Body0, Body), 510 retract(M:((-) :- Body)). 511scasp_retract(M:(false :- Body0)) => 512 expand_goal(Body0, Body), 513 retract(M:((-) :- Body)). 514scasp_retract(M:(Head :- Body0)) => 515 expand_goal(Body0, Body), 516 retract(M:(Head :- Body)). 517scasp_retract(Head) => 518 retract(Head). 519 520scasp_retractall(M:(-Head)) => 521 intern_negation(-Head, MHead), 522 retractall(M:). 523scasp_retractall(Head) => 524 retractall(Head).
531scasp_abolish(M:(Name/Arity)) => 532 pi_head(Name/Arity, Head), 533 scasp_retractall(M:Head), 534 scasp_retractall(M:(-Head)). 535 536 537 /******************************* 538 * DIRECTIVES * 539 *******************************/
s(CASP) directives. Same as :- Directive.. Provides
compatibility with sCASP sources as normally found.546#(Directive) :- #(Directive, false). 547 548#(M:pred(Spec), _) => pred(M:Spec). 549#(M:show(Spec), _) => show(M:Spec). 550#(M:abducible(Spec), Pos) => abducible(M:Spec, Pos). 551 552pred(M:(Spec :: Template)) => 553 process_pr_pred(Spec :: Template, Atom, Children, Cond, Human), 554 assertz(M:pr_pred_predicate(Atom, Children, Cond, Human)). 555 556show(M:PIs) => 557 phrase(show(PIs), Clauses), 558 maplist(assert_show(M), Clauses). 559 560assert_show(M, Clause) :- 561 assertz(M:). 562 563show(Var) --> 564 { var(Var), 565 instantiation_error(Var) 566 }. 567show((A,B)) --> 568 !, 569 show(A), 570 show(B). 571show(not(PI)) --> 572 { pi_head(PI, Head) }, 573 [ pr_show_predicate(not(Head)) ]. 574show(PI) --> 575 { pi_head(PI, Head) }, 576 [ pr_show_predicate(Head) ].
583abducible(Spec) :- abducible(Spec, false). 584 585abducible(M:(A,B), Pos) => 586 abducible(M:A, Pos), 587 abducible(M:B, Pos). 588abducible(M:Head, Pos), callable(Head) => 589 abducible_rules(Head, Rules), 590 discontiguous(M:('abducible$'/1, 'abducible$$'/1)), 591 maplist(scasp_assert_into(M, Pos), Rules). 592 593abducible_rules(Head, 594 [ (Head :- not(NegHead), 'abducible$'(Head)), 595 (NegHead :- not Head), 596 ('abducible$'(Head) :- not 'abducible$$'(Head)), 597 ('abducible$$'(Head) :- not 'abducible$'(Head)) 598 ]) :- 599 intern_negation(-Head, NegHead). 600 601abducible(Var) --> 602 { var(Var), 603 instantiation_error(Var) 604 }. 605abducible((A,B)) --> 606 !, 607 abducible(A), 608 abducible(B). 609abducible(Head) --> 610 { must_be(callable, Head), 611 abducible_rules(Head, Clauses) 612 }, 613 list(Clauses). 614 615list([]) --> []. 616list([H|T]) --> [H], list(T). 617 618 619 620 /******************************* 621 * EXPAND * 622 *******************************/ 623 624userterm_expansion(-Fact, MFact) :- 625 callable(Fact), 626 Fact \= _:_, 627 intern_negation(-Fact, MFact). 628userterm_expansion((-Head :- Body), (MHead :- Body)) :- 629 callable(Head), 630 Head \= _:_, 631 intern_negation(-Head, MHead). 632userterm_expansion((false :- Body), ((-) :- Body)). 633userterm_expansion((:- pred(SpecIn)), 634 pr_pred_predicate(Atom, Children, Cond, Human)) :- 635 process_pr_pred(SpecIn, Atom, Children, Cond, Human). 636userterm_expansion((:- show(SpecIn)), Clauses) :- 637 phrase(show(SpecIn), Clauses). 638userterm_expansion((:- abducible(SpecIn)), Clauses) :- 639 phrase(abducible(SpecIn), Clauses). 640userterm_expansion((# pred(SpecIn)), 641 pr_pred_predicate(Atom, Children, Cond, Human)) :- 642 process_pr_pred(SpecIn, Atom, Children, Cond, Human). 643userterm_expansion((# show(SpecIn)), Clauses) :- 644 phrase(show(SpecIn), Clauses). 645userterm_expansion((# abducible(SpecIn)), Clauses) :- 646 phrase(abducible(SpecIn), Clauses). 647 648usergoal_expansion(-Goal, MGoal) :- 649 callable(Goal), 650 intern_negation(-Goal, MGoal). 651 652 653 /******************************* 654 * CLP * 655 *******************************/
s(CASP) constraints. This implementation is
normally not used and mostly makes the program analysis work.667A #= B :- apply_clpq_constraints(A #= B). 668A #<> B :- apply_clpq_constraints(A #<> B). 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). 673 674 675 /******************************* 676 * SANDBOX * 677 *******************************/ 678 679:- multifile 680 sandbox:safe_meta_predicate/1. 681 682% scasp/1 is safe as it only allows for pure Prolog predicates 683% and limited arithmetic. Note that this does allow calling e.g. 684% member/2. s(CASP) does not allow for calling _qualified goals, 685% lists:member(...), 686 687sandbox:safe_meta(scasp_dyncall:scasp(_, _), [])
This predicate assembles the clauses that are reachable from a given goal.
Issues: