:- module(scasp_dyncall, [ scasp/2, % :Query, +Options scasp_query_clauses/2, % :Query, -Clauses scasp_model/1, % -Model scasp_justification/2, % -Tree, +Options scasp_show/2, % :Query,+What (scasp_dynamic)/1, % :Spec scasp_assert/1, % :Clause scasp_assert/2, % :Clause scasp_retract/1, % :Clause scasp_retractall/1, % :Head scasp_abolish/1, % :PredicateIndicator (#)/1, % :Directive (#)/2, % :Directive, +Pos (pred)/1, (show)/1, (abducible)/1, (abducible)/2, (#=)/2, (#<>)/2, (#<)/2, (#>)/2, (#=<)/2, (#>=)/2, op(900, fy, not), op(950, xfx, ::), % pred not x :: "...". op(1200, fx, #), op(1150, fx, pred), op(1150, fx, show), op(1150, fx, abducible), op(1150, fx, scasp_dynamic), op(700, xfx, #=), op(700, xfx, #<>), op(700, xfx, #<), op(700, xfx, #>), op(700, xfx, #=<), op(700, xfx, #>=) ]). :- use_module(compile). :- use_module(embed). :- use_module(common). :- use_module(modules). :- use_module(source_ref). :- use_module(listing). :- use_module(clp/clpq, [apply_clpq_constraints/1]). :- use_module(pr_rules, [process_pr_pred/5]). :- use_module(predicates, [prolog_builtin/1, clp_builtin/1]). :- use_module(library(apply), [maplist/3, exclude/3, maplist/2]). :- use_module(library(assoc), [empty_assoc/1, get_assoc/3, put_assoc/4]). :- use_module(library(error), [ instantiation_error/1, permission_error/3, type_error/2, must_be/2 ]). :- use_module(library(lists), [member/2, append/3]). :- use_module(library(modules), [in_temporary_module/3, current_temporary_module/1]). :- use_module(library(option), [option/2]). :- use_module(library(ordsets), [ord_intersect/2, ord_union/3]). :- use_module(library(prolog_code), [pi_head/2]). :- meta_predicate scasp(0, +), scasp_show(:, +), scasp_query_clauses(:, -), scasp_dynamic(:), scasp_assert(:), scasp_retract(:), scasp_retractall(:), scasp_abolish(:), pred(:), show(:), abducible(:). /** This predicate assembles the clauses that are reachable from a given goal. Issues: - Represent classical negation as -Term? Alternatives: - Just use -Term. Disadvantage is program analysis and module dependencies. - Provide goal- and term-expansion to intern the - into the functor name. Disadvantage is that we need scasp_assert/1, etc. */ %! scasp(:Query) is nondet. %! scasp(:Query, +Options) is nondet. % % Prove query using s(CASP) semantics. This performs the following % steps: % % - Collect (transitively) all clauses that are reachable from % Query. % - Collect all global constraints whose call-tree overlaps with % the query call tree. % - Establish the compiled s(CASP) representation in a _temporary % module_ % - Run the s(CASP) solver % - Optionally extract the model and justification tree. % % Options are passed to scasp_compile/2. Other options processed: % % - model(-Model) % Unify Model with the s(CASP) model, a list of model terms. % See scasp_model/1. % - tree(-Tree) % Unify Tree with the s(CASP) justification tree. See % scasp_justification/2 for details. % - source(Boolean) % When `false`, do not include source origin terms into the % final tree. scasp(Query, Options) :- scasp_query_clauses(Query, Clauses), qualify(Query, SrcModule:QQuery), expand_program(SrcModule, Clauses, Clauses1, QQuery, QQuery1), in_temporary_module( Module, prepare(Clauses1, Module, Options), scasp_call_and_results(Module:QQuery1, SrcModule, Options)). prepare(Clauses, Module, Options) :- scasp_compile(Module:Clauses, Options), ( option(write_program(_), Options) -> scasp_portray_program(Module:Options) ; true ). qualify(M:Q0, M:Q) :- qualify(Q0, M, Q1), intern_negation(Q1, Q). expand_program(SrcModule, Clauses, Clauses1, QQuery, QQuery1) :- current_predicate(SrcModule:scasp_expand_program/4), SrcModule:scasp_expand_program(Clauses, Clauses1, QQuery, QQuery1), !. expand_program(_, Clauses, Clauses, QQuery, QQuery). scasp_call_and_results(Query, SrcModule, Options) :- scasp_embed:scasp_call(Query), ( option(model(Model), Options) -> scasp_model(SrcModule:Model) ; true ), ( option(tree(Tree), Options) -> scasp_justification(SrcModule:Tree, Options) ; true ). %! scasp_show(:Query, +What) % % Show some aspect of the translated s(CASP) program. Currently % What is one of: % % - code(Options) % Show the collected program. By default shows the query % and user program. To show only the integrity constraints, % use: % % ?- scasp_show(Query, code(user(false), constraints(true))). scasp_show(Query, What) :- What =.. [Type|Options], scasp_show(Query, Type, Options). scasp_show(Query, code, Options) => Query = M:_, scasp_query_clauses(Query, Clauses), qualify(Query, SrcModule:QQuery), expand_program(SrcModule, Clauses, Clauses1, QQuery, _QQuery1), in_temporary_module( Module, prepare(Clauses1, Module, []), scasp_portray_program(Module:[source_module(M)|Options])). %! scasp_query_clauses(:Query, -Clauses) is det. % % @arg Clauses is a list of source(ClauseRef, Clause). :- det(scasp_query_clauses/2). scasp_query_clauses(Query, Clauses) :- query_callees(Query, Callees0), include_global_constraint(Callees0, Constraints, Callees), findall(Clause, scasp_clause(Callees, Clause), Clauses, QConstraints), maplist(mkconstraint, Constraints, QConstraints). scasp_clause(Callees, source(ClauseRef, Clause)) :- member(PI, Callees), pi_head(PI, M:Head), @(clause(Head, Body, ClauseRef), M), mkclause(Head, Body, M, Clause). mkclause(Head, true, M, Clause) => qualify(Head, M, Clause). mkclause(Head, Body, M, Clause) => qualify((Head:-Body), M, Clause). mkconstraint(source(Ref, M:Body), source(Ref, (:- Constraint))) :- qualify(Body, M, Constraint). qualify(-(Head), M, Q) => Q = -QHead, qualify(Head, M, QHead). qualify(not(Head), M, Q) => Q = not(QHead), qualify(Head, M, QHead). qualify(findall(Templ, Head, List), M, Q) => Q = findall(Templ, QHead, List), qualify(Head, M, QHead). qualify((A,B), M, Q) => Q = (QA,QB), qualify(A, M, QA), qualify(B, M, QB). qualify((A:-B), M, Q) => Q = (QA:-QB), qualify(A, M, QA), qualify(B, M, QB). qualify(G, M, Q), callable(G) => ( built_in(G) -> Q = G ; implementation(M:G, Callee), encoded_module_term(Callee, Q) ). %! query_callees(:Query, -Callees) is det. % % True when Callees is a list of predicate indicators for predicates % reachable from Query. % % @arg Callees is an ordered set. query_callees(M:Query, Callees) :- findall(Call, body_calls_pi(Query,M,Call), Calls0), sort(Calls0, Calls), callee_graph(Calls, Callees). body_calls_pi(Query, M, PI) :- body_calls(Query, M, Call), pi_head(PI, Call). callee_graph(Preds, Nodes) :- empty_assoc(Expanded), callee_closure(Preds, Expanded, Preds, Nodes0), sort(Nodes0, Nodes). callee_closure([], _, Preds, Preds). callee_closure([H|T], Expanded, Preds0, Preds) :- ( get_assoc(H, Expanded, _) -> callee_closure(T, Expanded, Preds0, Preds) ; put_assoc(H, Expanded, true, Expanded1), pi_head(H, Head), predicate_callees(Head, Called), exclude(expanded(Expanded1), Called, New), append(New, T, Agenda), append(New, Preds0, Preds1), callee_closure(Agenda, Expanded1, Preds1, Preds) ). expanded(Assoc, PI) :- get_assoc(PI, Assoc, _). %! include_global_constraint(+Callees, -Constraints, -AllCallees) is det include_global_constraint(Callees0, Constraints, Callees) :- include_global_constraint(Callees0, Callees, [], Constraints). include_global_constraint(Callees0, Callees, Constraints0, Constraints) :- global_constraint(Constraint), Constraint = source(_, Body), \+ ( member(source(_, Body0), Constraints0), Body =@= Body0 ), query_callees(Body, Called), ord_intersect(Callees0, Called), !, ord_union(Callees0, Called, Callees1), include_global_constraint(Callees1, Callees, [Constraint|Constraints0], Constraints). include_global_constraint(Callees, Callees, Constraints, Constraints). global_constraint(source(Ref, M:Body)) :- ( current_temporary_module(M) ; current_module(M) ), current_predicate(M:(-)/0), \+ predicate_property(M:(-), imported_from(_)), @(clause(-, Body, Ref), M). %! predicate_callees(:Head, -Callees) is det. % % True when Callees is the list of _direct_ callees from Head. Each % callee is a _predicate indicator_. :- dynamic predicate_callees_c/4. predicate_callees(M:Head, Callees) :- predicate_callees_c(Head, M, Gen, Callees0), predicate_generation(M:Head, Gen), !, Callees = Callees0. predicate_callees(M:Head, Callees) :- module_property(M, class(temporary)), !, predicate_callees_nc(M:Head, Callees). predicate_callees(M:Head, Callees) :- retractall(predicate_callees_c(Head, M, _, _)), predicate_callees_nc(M:Head, Callees0), predicate_generation(M:Head, Gen), assertz(predicate_callees_c(Head, M, Gen, Callees0)), Callees = Callees0. predicate_callees_nc(Head, Callees) :- findall(Callee, predicate_calls(Head, Callee), Callees0), sort(Callees0, Callees). predicate_calls(Head0, PI) :- generalise(Head0, M:Head), @(clause(Head, Body), M), body_calls(Body, M, Callee), pi_head(PI, Callee). body_calls(Goal, _M, _), var(Goal) => instantiation_error(Goal). body_calls(true, _M, _) => fail. body_calls((A,B), M, Callee) => ( body_calls(A, M, Callee) ; body_calls(B, M, Callee) ). body_calls(not(A), M, Callee) => body_calls(A, M, Callee). body_calls(findall(_,G,_), M, Callee) => body_calls(G, M, Callee). body_calls(N, M, Callee), rm_classic_negation(N,A) => body_calls(A, M, Callee). body_calls(M:A, _, Callee), atom(M) => body_calls(A, M, Callee). body_calls(G, _M, _CalleePM), callable(G), built_in(G) => fail. body_calls(G, M, CalleePM), callable(G) => implementation(M:G, Callee0), generalise(Callee0, Callee), ( predicate_property(Callee, interpreted), \+ predicate_property(Callee, meta_predicate(_)) -> pm(Callee, CalleePM) ; \+ predicate_property(Callee, _) -> pm(Callee, CalleePM) % undefined ; pi_head(CalleePI, Callee), permission_error(scasp, procedure, CalleePI) ). body_calls(G, _, _) => type_error(callable, G). built_in(Head) :- prolog_builtin(Head). built_in(Head) :- clp_builtin(Head). built_in(_ is _). built_in(findall(_,_,_)). rm_classic_negation(-Goal, Goal) :- !. rm_classic_negation(Goal, PGoal) :- functor(Goal, Name, _), atom_concat(-, Plain, Name), Goal =.. [Name|Args], PGoal =.. [Plain|Args]. pm(P, P). pm(M:P, M:MP) :- intern_negation(-P, MP). implementation(M0:Head, M:Head) :- predicate_property(M0:Head, imported_from(M1)), !, M = M1. implementation(Head, Head). generalise(M:Head0, Gen), atom(M) => Gen = M:Head, generalise(Head0, Head). generalise(-Head0, Gen) => Gen = -Head, generalise(Head0, Head). generalise(Head0, Head) => functor(Head0, Name, Arity), functor(Head, Name, Arity). predicate_generation(Head, Gen) :- predicate_property(Head, last_modified_generation(Gen0)), !, Gen = Gen0. predicate_generation(_, 0). /******************************* * MANIPULATING THE PROGRAM * *******************************/ %! scasp_dynamic(:Spec) is det. % % Declare a predicates as dynamic or thread_local. Usage patterns: % % :- scasp_dynamic p/1. % :- scasp_dynamic p/1 as shared. scasp_dynamic(M:Spec) :- scasp_dynamic(Spec, M, private). scasp_dynamic(M:(Spec as Scoped)) :- scasp_dynamic(Spec, M, Scoped). scasp_dynamic((A,B), M, Scoped) => scasp_dynamic(A, M, Scoped), scasp_dynamic(B, M, Scoped). scasp_dynamic(Name/Arity, M, Scoped) => atom_concat(-, Name, NName), ( Scoped == shared -> dynamic((M:Name/Arity, M:NName/Arity)) ; thread_local((M:Name/Arity, M:NName/Arity)) ). :- multifile system:term_expansion/2. system:term_expansion((:- scasp_dynamic(Spec)), Directives) :- phrase(scasp_dynamic_direcives(Spec), Directives). scasp_dynamic_direcives(Spec as Scope) --> !, scasp_dynamic_direcives(Spec, Scope). scasp_dynamic_direcives(Spec) --> !, scasp_dynamic_direcives(Spec, private). scasp_dynamic_direcives(Var, _) --> { var(Var), !, fail }. scasp_dynamic_direcives((A,B), Scope) --> scasp_dynamic_direcives(A, Scope), scasp_dynamic_direcives(B, Scope). scasp_dynamic_direcives(Name/Arity, Scope) --> { atom_concat(-, Name, NName) }, ( {Scope == shared} -> [(:- dynamic((Name/Arity, NName/Arity)))] ; [(:- thread_local((Name/Arity, NName/Arity)))] ). %! scasp_assert(:Clause) is det. %! scasp_retract(:Clause) is nondet. %! scasp_retractall(:Head) is det. % % Wrappers for assertz/1, retract/1 and retractall/1 that deal with % sCASP terms which may have a head or body terms that are wrapped in % `-(Term)`, indicating classical negation. Also deals with global % constraints written in any of these formats: % % - `false :- Constraint`. % - `:- Constraint`. scasp_assert(Clause) :- scasp_assert(Clause, false). scasp_assert(M:(-Head :- Body0), Pos) => intern_negation(-Head, MHead), expand_goal(Body0, Body), scasp_assert_(M:(MHead :- Body), Pos). scasp_assert(M:(-Head), Pos) => intern_negation(-Head, MHead), scasp_assert_(M:(MHead), Pos). scasp_assert(M:(:- Body0), Pos) => expand_goal(Body0, Body), scasp_assert_(M:((-) :- Body), Pos). scasp_assert(M:(false :- Body0), Pos) => expand_goal(Body0, Body), scasp_assert_(M:((-) :- Body), Pos). scasp_assert(M:(Head :- Body0), Pos) => expand_goal(Body0, Body), scasp_assert_(M:(Head :- Body), Pos). scasp_assert(Head, Pos) => scasp_assert_(Head, Pos). scasp_assert_(Clause, false) => assertz(Clause). scasp_assert_(Clause, Pos) => assertz(Clause, Ref), assertz(scasp_dynamic_clause_position(Ref, Pos)). scasp_assert_into(M, Pos, Rule) :- scasp_assert(M:Rule, Pos). scasp_retract(M:(-Head :- Body0)) => intern_negation(-Head, MHead), expand_goal(Body0, Body), retract(M:(MHead :- Body)). scasp_retract(M:(-Head)) => intern_negation(-Head, MHead), retract(M:(MHead)). scasp_retract(M:(:- Body0)) => expand_goal(Body0, Body), retract(M:((-) :- Body)). scasp_retract(M:(false :- Body0)) => expand_goal(Body0, Body), retract(M:((-) :- Body)). scasp_retract(M:(Head :- Body0)) => expand_goal(Body0, Body), retract(M:(Head :- Body)). scasp_retract(Head) => retract(Head). scasp_retractall(M:(-Head)) => intern_negation(-Head, MHead), retractall(M:MHead). scasp_retractall(Head) => retractall(Head). %! scasp_abolish(:PredicateIndicator) is det. % % Remove all facts for both PredicateIndicator and its classical % negation. scasp_abolish(M:(Name/Arity)) => pi_head(Name/Arity, Head), scasp_retractall(M:Head), scasp_retractall(M:(-Head)). /******************************* * DIRECTIVES * *******************************/ %! #(:Directive) % % Handle s(CASP) directives. Same as ``:- Directive.``. Provides % compatibility with sCASP sources as normally found. #(Directive) :- #(Directive, false). #(M:pred(Spec), _) => pred(M:Spec). #(M:show(Spec), _) => show(M:Spec). #(M:abducible(Spec), Pos) => abducible(M:Spec, Pos). pred(M:(Spec :: Template)) => process_pr_pred(Spec :: Template, Atom, Children, Cond, Human), assertz(M:pr_pred_predicate(Atom, Children, Cond, Human)). show(M:PIs) => phrase(show(PIs), Clauses), maplist(assert_show(M), Clauses). assert_show(M, Clause) :- assertz(M:Clause). show(Var) --> { var(Var), instantiation_error(Var) }. show((A,B)) --> !, show(A), show(B). show(not(PI)) --> { pi_head(PI, Head) }, [ pr_show_predicate(not(Head)) ]. show(PI) --> { pi_head(PI, Head) }, [ pr_show_predicate(Head) ]. %! abducible(:Spec) % % Declare Spec, a comma list of _heads_ to be _abducible_, meaning % they can both be in or outside the model. abducible(Spec) :- abducible(Spec, false). abducible(M:(A,B), Pos) => abducible(M:A, Pos), abducible(M:B, Pos). abducible(M:Head, Pos), callable(Head) => abducible_rules(Head, Rules), discontiguous(M:('abducible$'/1, 'abducible$$'/1)), maplist(scasp_assert_into(M, Pos), Rules). abducible_rules(Head, [ (Head :- not(NegHead), 'abducible$'(Head)), (NegHead :- not Head), ('abducible$'(Head) :- not 'abducible$$'(Head)), ('abducible$$'(Head) :- not 'abducible$'(Head)) ]) :- intern_negation(-Head, NegHead). abducible(Var) --> { var(Var), instantiation_error(Var) }. abducible((A,B)) --> !, abducible(A), abducible(B). abducible(Head) --> { must_be(callable, Head), abducible_rules(Head, Clauses) }, list(Clauses). list([]) --> []. list([H|T]) --> [H], list(T). /******************************* * EXPAND * *******************************/ user:term_expansion(-Fact, MFact) :- callable(Fact), Fact \= _:_, intern_negation(-Fact, MFact). user:term_expansion((-Head :- Body), (MHead :- Body)) :- callable(Head), Head \= _:_, intern_negation(-Head, MHead). user:term_expansion((false :- Body), ((-) :- Body)). user:term_expansion((:- pred(SpecIn)), pr_pred_predicate(Atom, Children, Cond, Human)) :- process_pr_pred(SpecIn, Atom, Children, Cond, Human). user:term_expansion((:- show(SpecIn)), Clauses) :- phrase(show(SpecIn), Clauses). user:term_expansion((:- abducible(SpecIn)), Clauses) :- phrase(abducible(SpecIn), Clauses). user:term_expansion((# pred(SpecIn)), pr_pred_predicate(Atom, Children, Cond, Human)) :- process_pr_pred(SpecIn, Atom, Children, Cond, Human). user:term_expansion((# show(SpecIn)), Clauses) :- phrase(show(SpecIn), Clauses). user:term_expansion((# abducible(SpecIn)), Clauses) :- phrase(abducible(SpecIn), Clauses). user:goal_expansion(-Goal, MGoal) :- callable(Goal), intern_negation(-Goal, MGoal). /******************************* * CLP * *******************************/ %! #=(?A, ?B). %! #<>(?A, ?B). %! #<(?A, ?B). %! #>(?A, ?B). %! #>=(?A, ?B). %! #=<(?A, ?B). % % Implementation of the s(CASP) constraints. This implementation is % normally not used and mostly makes the program analysis work. A #= B :- apply_clpq_constraints(A #= B). A #<> B :- apply_clpq_constraints(A #<> B). A #< B :- apply_clpq_constraints(A #< B). A #> B :- apply_clpq_constraints(A #> B). A #=< B :- apply_clpq_constraints(A #=< B). A #>= B :- apply_clpq_constraints(A #>= B). /******************************* * SANDBOX * *******************************/ :- multifile sandbox:safe_meta_predicate/1. % scasp/1 is safe as it only allows for pure Prolog predicates % and limited arithmetic. Note that this does allow calling e.g. % member/2. s(CASP) does not allow for calling _qualified goals, % lists:member(...), sandbox:safe_meta(scasp_dyncall:scasp(_, _), []).