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, 52 clp_builtin/1, clp_interval/1]). 53 54:- use_module(library(apply), [maplist/3, exclude/3, maplist/2]). 55:- use_module(library(assoc), [empty_assoc/1, get_assoc/3, put_assoc/4]). 56:- use_module(library(error), 57 [ instantiation_error/1, 58 permission_error/3, 59 type_error/2, 60 must_be/2 61 ]). 62:- use_module(library(lists), [member/2, append/3]). 63:- use_module(library(modules), 64 [in_temporary_module/3, current_temporary_module/1]). 65:- use_module(library(option), [option/2]). 66:- use_module(library(ordsets), [ord_intersect/2, ord_union/3]). 67:- use_module(library(prolog_code), [pi_head/2]). 68 69:- meta_predicate 70 scasp(0, +), 71 scasp_show(:, +), 72 scasp_query_clauses(:, -), 73 scasp_dynamic(:), 74 scasp_assert(:), 75 scasp_retract(:), 76 scasp_retractall(:), 77 scasp_abolish(:), 78 pred(:), 79 show(:), 80 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.123scasp(Query, Options) :- 124 Query = SrcModule:_, 125 scasp_query_clauses(Query, Clauses0), 126 expand_program(SrcModule, Clauses0, Clauses1, Query, Query1), 127 maplist(qualify, Clauses1, Clauses2), 128 qualify_query(Query1, SrcModule:QQuery), 129 q_expand_program(SrcModule, Clauses2, Clauses, QQuery, QQuery1), 130 in_temporary_module( 131 Module, 132 prepare(Clauses, Module, Options), 133 scasp_call_and_results(Module:QQuery1, SrcModule, Options)). 134 135prepare(Clauses, Module, Options) :- 136 scasp_compile(Module:Clauses, Options), 137 ( option(write_program(_), Options) 138 -> scasp_portray_program(Module:Options) 139 ; true 140 ). 141 142qualify_query(M:Q0, M:Q) :- 143 qualify(Q0, M, Q1), 144 intern_negation(Q1, Q). 145 146expand_program(SrcModule, Clauses, Clauses1, QQuery, QQuery1) :- 147 current_predicate(SrcModule:scasp_expand/4), 148 SrcModule:scasp_expand(Clauses, Clauses1, QQuery, QQuery1), 149 !. 150expand_program(_, Clauses, Clauses, QQuery, QQuery). 151 152q_expand_program(SrcModule, Clauses, Clauses1, QQuery, QQuery1) :- 153 current_predicate(SrcModule:scasp_expand_program/4), 154 SrcModule:scasp_expand_program(Clauses, Clauses1, QQuery, QQuery1), 155 !. 156q_expand_program(_, Clauses, Clauses, QQuery, QQuery). 157 158 159scasp_call_and_results(Query, SrcModule, Options) :- 160 scasp_embed:scasp_call(Query), 161 ( option(model(Model), Options) 162 -> scasp_model(SrcModule:Model) 163 ; true 164 ), 165 ( option(tree(Tree), Options) 166 -> scasp_justification(SrcModule:Tree, Options) 167 ; true 168 ).
s(CASP) program. Currently
What is one of:
?- scasp_show(Query, code(user(false), constraints(true))).
182scasp_show(Query, What) :- 183 What =.. [Type|Options], 184 scasp_show(Query, Type, Options). 185 186scasp_show(Query, code, Options) => 187 Query = SrcModule:_, 188 scasp_query_clauses(Query, Clauses0), 189 expand_program(SrcModule, Clauses0, Clauses1, Query, Query1), 190 maplist(qualify, Clauses1, Clauses2), 191 qualify_query(Query1, SrcModule:QQuery), 192 q_expand_program(SrcModule, Clauses2, Clauses, QQuery, _QQuery1), 193 in_temporary_module( 194 Module, 195 prepare(Clauses, Module, []), 196 scasp_portray_program(Module:[source_module(SrcModule)|Options])).
202:- det(scasp_query_clauses/2). 203 204scasp_query_clauses(Query, Clauses) :- 205 query_callees(Query, Callees0), 206 include_global_constraint(Callees0, Constraints, Callees), 207 findall(Clause, scasp_clause(Callees, Clause), Clauses, Constraints). 208 209scasp_clause(Callees, source(ClauseRef, M:(Head:- Body))) :- 210 member(PI, Callees), 211 pi_head(PI, M:Head), 212 @(clause(Head, Body, ClauseRef), M). 213 214qualify(source(Ref, Clause), Q) => 215 Q = source(Ref, QClause), 216 qualify(Clause, QClause). 217qualify(M:(Head :- true), Q) => 218 qualify(Head, M, Q). 219qualify(M:(Head :- Body), Q) => 220 qualify((Head:-Body), M, Q). 221qualify(M:(:- Body), Q) => 222 Q = (:- Constraint), 223 qualify(Body, M, Constraint). 224 225qualify(-(Head), M, Q) => 226 Q = -QHead, 227 qualify(Head, M, QHead). 228qualify(not(Head), M, Q) => 229 Q = not(QHead), 230 qualify(Head, M, QHead). 231qualify(findall(Templ, Head, List), M, Q) => 232 Q = findall(Templ, QHead, List), 233 qualify(Head, M, QHead). 234qualify((A,B), M, Q) => 235 Q = (QA,QB), 236 qualify(A, M, QA), 237 qualify(B, M, QB). 238qualify((A:-B), M, Q) => 239 Q = (QA:-QB), 240 qualify(A, M, QA), 241 qualify(B, M, QB). 242qualify(G, M, Q), callable(G) => 243 ( built_in(G) 244 -> Q = G 245 ; implementation(M:G, Callee), 246 encoded_module_term(Callee, Q) 247 ).
256query_callees(M:Query, Callees) :- 257 findall(Call, body_calls_pi(Query,M,Call), Calls0), 258 sort(Calls0, Calls), 259 callee_graph(Calls, Callees). 260 261body_calls_pi(Query, M, PI) :- 262 body_calls(Query, M, Call), 263 pi_head(PI, Call). 264 265callee_graph(Preds, Nodes) :- 266 empty_assoc(Expanded), 267 callee_closure(Preds, Expanded, Preds, Nodes0), 268 sort(Nodes0, Nodes). 269 270callee_closure([], _, Preds, Preds). 271callee_closure([H|T], Expanded, Preds0, Preds) :- 272 ( get_assoc(H, Expanded, _) 273 -> callee_closure(T, Expanded, Preds0, Preds) 274 ; put_assoc(H, Expanded, true, Expanded1), 275 pi_head(H, Head), 276 predicate_callees(Head, Called), 277 exclude(expanded(Expanded1), Called, New), 278 append(New, T, Agenda), 279 append(New, Preds0, Preds1), 280 callee_closure(Agenda, Expanded1, Preds1, Preds) 281 ). 282 283expanded(Assoc, PI) :- 284 get_assoc(PI, Assoc, _).
288include_global_constraint(Callees0, Constraints, Callees) :- 289 include_global_constraint(Callees0, Callees, [], Constraints). 290 291include_global_constraint(Callees0, Callees, Constraints0, Constraints) :- 292 global_constraint(Constraint), 293 Constraint = source(_, Rule), % Rule = M:(:-Body) 294 \+ ( member(source(_, Rule0), Constraints0), 295 Rule =@= Rule0 296 ), 297 Rule = M:(:-Body), 298 query_callees(M:Body, Called), 299 ord_intersect(Callees0, Called), 300 !, 301 ord_union(Callees0, Called, Callees1), 302 include_global_constraint(Callees1, Callees, 303 [Constraint|Constraints0], Constraints). 304include_global_constraint(Callees, Callees, Constraints, Constraints). 305 306 307global_constraint(source(Ref, M:(:- Body))) :- 308 ( current_temporary_module(M) 309 ; current_module(M) 310 ), 311 current_predicate(M:(-)/0), 312 \+ predicate_property(M:(-), imported_from(_)), 313 @(clause(-, Body, Ref), M).
320:- dynamic predicate_callees_c/4. 321 322predicate_callees(M:Head, Callees) :- 323 predicate_callees_c(Head, M, Gen, Callees0), 324 predicate_generation(M:Head, Gen), 325 !, 326 Callees = Callees0. 327predicate_callees(M:Head, Callees) :- 328 module_property(M, class(temporary)), 329 !, 330 predicate_callees_nc(M:Head, Callees). 331predicate_callees(M:Head, Callees) :- 332 retractall(predicate_callees_c(Head, M, _, _)), 333 predicate_callees_nc(M:Head, Callees0), 334 predicate_generation(M:Head, Gen), 335 assertz(predicate_callees_c(Head, M, Gen, Callees0)), 336 Callees = Callees0. 337 338predicate_callees_nc(Head, Callees) :- 339 findall(Callee, predicate_calls(Head, Callee), Callees0), 340 sort(Callees0, Callees). 341 342predicate_calls(Head0, PI) :- 343 generalise(Head0, M:Head), 344 @(clause(Head, Body), M), 345 body_calls(Body, M, Callee), 346 pi_head(PI, Callee). 347 348body_calls(Goal, _M, _), var(Goal) => 349 instantiation_error(Goal). 350body_calls(true, _M, _) => fail. 351body_calls((A,B), M, Callee) => 352 ( body_calls(A, M, Callee) 353 ; body_calls(B, M, Callee) 354 ). 355body_calls(not(A), M, Callee) => 356 body_calls(A, M, Callee). 357body_calls(findall(_,G,_), M, Callee) => 358 body_calls(G, M, Callee). 359body_calls(N, M, Callee), rm_classic_negation(N,A) => 360 body_calls(A, M, Callee). 361body_calls(M:A, _, Callee), atom(M) => 362 body_calls(A, M, Callee). 363body_calls(G, _M, _CalleePM), callable(G), built_in(G) => 364 fail. 365body_calls(G, M, CalleePM), callable(G) => 366 implementation(M:G, Callee0), 367 generalise(Callee0, Callee), 368 ( predicate_property(Callee, interpreted), 369 \+ predicate_property(Callee, meta_predicate(_)) 370 -> pm(Callee, CalleePM) 371 ; \+ predicate_property(Callee, _) 372 -> pm(Callee, CalleePM) % undefined 373 ; pi_head(CalleePI, Callee), 374 permission_error(scasp, procedure, CalleePI) 375 ). 376body_calls(G, _, _) => 377 type_error(callable, G). 378 379built_in(Head) :- 380 prolog_builtin(Head). 381built_in(Head) :- 382 clp_builtin(Head). 383built_in(Head) :- 384 clp_interval(Head). 385built_in(_ is _). 386built_in(findall(_,_,_)). 387 388rm_classic_negation(-Goal, Goal) :- 389 !. 390rm_classic_negation(Goal, PGoal) :- 391 functor(Goal, Name, _), 392 atom_concat(-, Plain, Name), 393 Goal =.. [Name|Args], 394 PGoal =.. [Plain|Args]. 395 396pm(P, P). 397pm(M:P, M:MP) :- 398 intern_negation(-P, MP). 399 400implementation(M0:Head, M:Head) :- 401 predicate_property(M0:Head, imported_from(M1)), 402 !, 403 M = M1. 404implementation(Head, Head). 405 406generalise(M:Head0, Gen), atom(M) => 407 Gen = M:Head, 408 generalise(Head0, Head). 409generalise(-Head0, Gen) => 410 Gen = -Head, 411 generalise(Head0, Head). 412generalise(Head0, Head) => 413 functor(Head0, Name, Arity), 414 functor(Head, Name, Arity). 415 416predicate_generation(Head, Gen) :- 417 predicate_property(Head, last_modified_generation(Gen0)), 418 !, 419 Gen = Gen0. 420predicate_generation(_, 0). 421 422 423 /******************************* 424 * MANIPULATING THE PROGRAM * 425 *******************************/
434scasp_dynamic(M:Spec) :- 435 scasp_dynamic(Spec, M, private). 436scasp_dynamic(M:(Spec as Scoped)) :- 437 scasp_dynamic(Spec, M, Scoped). 438 439scasp_dynamic((A,B), M, Scoped) => 440 scasp_dynamic(A, M, Scoped), 441 scasp_dynamic(B, M, Scoped). 442scasp_dynamic(Name/Arity, M, Scoped) => 443 atom_concat(-, Name, NName), 444 ( Scoped == shared 445 -> dynamic((M:Name/Arity, 446 M:NName/Arity)) 447 ; thread_local((M:Name/Arity, 448 M:NName/Arity)) 449 ). 450 451:- multifile system:term_expansion/2. 452 453systemterm_expansion((:- scasp_dynamic(Spec)), Directives) :- 454 phrase(scasp_dynamic_direcives(Spec), Directives). 455 456scasp_dynamic_direcives(Spec as Scope) --> 457 !, 458 scasp_dynamic_direcives(Spec, Scope). 459scasp_dynamic_direcives(Spec) --> 460 !, 461 scasp_dynamic_direcives(Spec, private). 462 463scasp_dynamic_direcives(Var, _) --> 464 { var(Var), !, fail }. 465scasp_dynamic_direcives((A,B), Scope) --> 466 scasp_dynamic_direcives(A, Scope), 467 scasp_dynamic_direcives(B, Scope). 468scasp_dynamic_direcives(Name/Arity, Scope) --> 469 { atom_concat(-, Name, NName) }, 470 ( {Scope == shared} 471 -> [(:- dynamic((Name/Arity, NName/Arity)))] 472 ; [(:- thread_local((Name/Arity, NName/Arity)))] 473 ).
-(Term), indicating classical negation. Also deals with global
constraints written in any of these formats:
false :- Constraint.:- Constraint.488scasp_assert(Clause) :- 489 scasp_assert(Clause, false). 490 491scasp_assert(M:(-Head :- Body0), Pos) => 492 intern_negation(-Head, MHead), 493 expand_goal(Body0, Body), 494 scasp_assert_(M:(MHead :- Body), Pos). 495scasp_assert(M:(-Head), Pos) => 496 intern_negation(-Head, MHead), 497 scasp_assert_(M:(MHead), Pos). 498scasp_assert(M:(:- Body0), Pos) => 499 expand_goal(Body0, Body), 500 scasp_assert_(M:((-) :- Body), Pos). 501scasp_assert(M:(false :- Body0), Pos) => 502 expand_goal(Body0, Body), 503 scasp_assert_(M:((-) :- Body), Pos). 504scasp_assert(M:(Head :- Body0), Pos) => 505 expand_goal(Body0, Body), 506 scasp_assert_(M:(Head :- Body), Pos). 507scasp_assert(Head, Pos) => 508 scasp_assert_(Head, Pos). 509 510scasp_assert_(Clause, false) => 511 assertz(Clause). 512scasp_assert_(Clause, Pos) => 513 assertz(Clause, Ref), 514 assertz(scasp_dynamic_clause_position(Ref, Pos)). 515 516scasp_assert_into(M, Pos, Rule) :- 517 scasp_assert(M:Rule, Pos). 518 519scasp_retract(M:(-Head :- Body0)) => 520 intern_negation(-Head, MHead), 521 expand_goal(Body0, Body), 522 retract(M:(MHead :- Body)). 523scasp_retract(M:(-Head)) => 524 intern_negation(-Head, MHead), 525 retract(M:(MHead)). 526scasp_retract(M:(:- Body0)) => 527 expand_goal(Body0, Body), 528 retract(M:((-) :- Body)). 529scasp_retract(M:(false :- Body0)) => 530 expand_goal(Body0, Body), 531 retract(M:((-) :- Body)). 532scasp_retract(M:(Head :- Body0)) => 533 expand_goal(Body0, Body), 534 retract(M:(Head :- Body)). 535scasp_retract(Head) => 536 retract(Head). 537 538scasp_retractall(M:(-Head)) => 539 intern_negation(-Head, MHead), 540 retractall(M:MHead). 541scasp_retractall(Head) => 542 retractall(Head).
549scasp_abolish(M:(Name/Arity)) => 550 pi_head(Name/Arity, Head), 551 scasp_retractall(M:Head), 552 scasp_retractall(M:(-Head)). 553 554 555 /******************************* 556 * DIRECTIVES * 557 *******************************/
s(CASP) directives. Same as :- Directive.. Provides
compatibility with sCASP sources as normally found.(Directive) :- #(Directive, false). 565 566#(M:pred(Spec), _) => pred(M:Spec). 567#(M:show(Spec), _) => show(M:Spec). 568#(M:abducible(Spec), Pos) => abducible(M:Spec, Pos). 569 570pred(M:(Spec :: Template)) => 571 process_pr_pred(Spec :: Template, Atom, Children, Cond, Human), 572 assertz(M:pr_pred_predicate(Atom, Children, Cond, Human)). 573 574show(M:PIs) => 575 phrase(show(PIs), Clauses), 576 maplist(assert_show(M), Clauses). 577 578assert_show(M, Clause) :- 579 assertz(M:Clause). 580 581show(Var) --> 582 { var(Var), 583 instantiation_error(Var) 584 }. 585show((A,B)) --> 586 !, 587 show(A), 588 show(B). 589show(not(PI)) --> 590 { pi_head(PI, Head) }, 591 [ pr_show_predicate(not(Head)) ]. 592show(PI) --> 593 { pi_head(PI, Head) }, 594 [ pr_show_predicate(Head) ].
601abducible(Spec) :- abducible(Spec, false). 602 603abducible(M:(A,B), Pos) => 604 abducible(M:A, Pos), 605 abducible(M:B, Pos). 606abducible(M:Head, Pos), callable(Head) => 607 abducible_rules(Head, Rules), 608 maplist(scasp_assert_into(M, Pos), Rules). 609 610abducible_rules(Head, 611 [ (Head :- AHead1), 612 (NegHead :- AHead2), 613 (AHead1 :- not AHead2), 614 (AHead2 :- not AHead1) 615 ]) :- 616 abducible_head('abducible$', Head, AHead1), 617 abducible_head('abducible$$', Head, AHead2), 618 intern_negation(-Head, NegHead). 619 620abducible_head(Prefix, Head, AHead) :- 621 format(atom(AHead), '~w~k$', [Prefix, Head]). 622 623abducible(Var) --> 624 { var(Var), 625 instantiation_error(Var) 626 }. 627abducible((A,B)) --> 628 !, 629 abducible(A), 630 abducible(B). 631abducible(Head) --> 632 { must_be(callable, Head), 633 abducible_rules(Head, Clauses) 634 }, 635 list(Clauses). 636 637list([]) --> []. 638list([H|T]) --> [H], list(T). 639 640 641 642 /******************************* 643 * EXPAND * 644 *******************************/ 645 646userterm_expansion(-Fact, MFact) :- 647 callable(Fact), 648 Fact \= _:_, 649 intern_negation(-Fact, MFact). 650userterm_expansion((-Head :- Body), (MHead :- Body)) :- 651 callable(Head), 652 Head \= _:_, 653 intern_negation(-Head, MHead). 654userterm_expansion((false :- Body), ((-) :- Body)). 655userterm_expansion((:- pred(SpecIn)), 656 pr_pred_predicate(Atom, Children, Cond, Human)) :- 657 process_pr_pred(SpecIn, Atom, Children, Cond, Human). 658userterm_expansion((:- show(SpecIn)), Clauses) :- 659 phrase(show(SpecIn), Clauses). 660userterm_expansion((:- abducible(SpecIn)), Clauses) :- 661 phrase(abducible(SpecIn), Clauses). 662userterm_expansion((# pred(SpecIn)), 663 pr_pred_predicate(Atom, Children, Cond, Human)) :- 664 process_pr_pred(SpecIn, Atom, Children, Cond, Human). 665userterm_expansion((# show(SpecIn)), Clauses) :- 666 phrase(show(SpecIn), Clauses). 667userterm_expansion((# abducible(SpecIn)), Clauses) :- 668 phrase(abducible(SpecIn), Clauses). 669 670usergoal_expansion(-Goal, MGoal) :- 671 callable(Goal), 672 intern_negation(-Goal, MGoal). 673 674 675 /******************************* 676 * CLP * 677 *******************************/
s(CASP) constraints. This implementation is
normally not used and mostly makes the program analysis work.689A #= B :- apply_clpq_constraints(A #= B). 690A #<> B :- apply_clpq_constraints(A #<> B). 691A #< B :- apply_clpq_constraints(A #< B). 692A #> B :- apply_clpq_constraints(A #> B). 693A #=< B :- apply_clpq_constraints(A #=< B). 694A #>= B :- apply_clpq_constraints(A #>= B). 695 696 697 /******************************* 698 * SOURCE * 699 *******************************/ 700 701:- multifile 702 prolog_clause:unify_goal/5. 703 704prolog_clauseunify_goal(scasp(RGoal, Options), 705 scasp(CGoal, Options), 706 _Module, 707 TermPos, TermPos) :- 708 intern_negation(RGoal, RGoal2), 709 RGoal2 =@= CGoal. 710 711 712 /******************************* 713 * SANDBOX * 714 *******************************/ 715 716:- multifile 717 sandbox:safe_meta_predicate/1. 718 719% scasp/1 is safe as it only allows for pure Prolog predicates 720% and limited arithmetic. Note that this does allow calling e.g. 721% member/2. s(CASP) does not allow for calling _qualified goals, 722% lists:member(...), 723 724sandbox:safe_meta(scasp_dyncall:scasp(_, _), [])
This predicate assembles the clauses that are reachable from a given goal.
Issues: