1/*
    2* Copyright (c) 2016, University of Texas at Dallas
    3* All rights reserved.
    4*
    5* Redistribution and use in source and binary forms, with or without
    6* modification, are permitted provided that the following conditions are met:
    7*     * Redistributions of source code must retain the above copyright
    8*       notice, this list of conditions and the following disclaimer.
    9*     * Redistributions in binary form must reproduce the above copyright
   10*       notice, this list of conditions and the following disclaimer in the
   11*       documentation and/or other materials provided with the distribution.
   12*     * Neither the name of the University of Texas at Dallas nor the
   13*       names of its contributors may be used to endorse or promote products
   14*       derived from this software without specific prior written permission.
   15*
   16* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
   17* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
   18* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
   19* DISCLAIMED. IN NO EVENT SHALL THE UNIVERSITY OF TEXAS AT DALLAS BE LIABLE FOR
   20* ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
   21* (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
   22* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
   23* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
   24* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
   25* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
   26*/
   27
   28:- module(scasp_program,
   29          [ defined_rule/4,
   30            defined_query/2,
   31            defined_predicates/1,
   32            defined_nmr_check/1,
   33            defined_directive/1,
   34            reserved_prefix/1,
   35            has_prefix/2,
   36            replace_prefix/4,    % +FunctorIn,+OldPrefix,+NewPrefix,-Functor
   37            non_printable/1,     % +Name
   38            assert_program/1,
   39            assert_rule/1,
   40            assert_nmr_check/1,
   41            destroy_program/0
   42          ]).

   54:- use_module(library(lists)).   55:- use_module(library(apply)).   56:- use_module(library(debug)).   57
   58:- use_module(common).   59:- use_module(variables).

 defined_rule(+Name:atom, +FullHead:compound, -Body:list, -Origin:compound) is nondet

Dynamic predicate for asserted rules.

Arguments:

Head	- Head predicate has head/arity (no args).
FullHead	- A predicate struct containing the head predicate with args.
Body	- list of body goals.
Origin	- A term describing the origin of this rule. For rules that are derived from loaded clauses, Origin is set to clause(ClauseRef); for compiler generated rules, Origin is set to generated(Why) where Why is one of neg for classical negation, nmr for NMR checks, and dual for dual rules; for rules read directly as s(CASP) with e.g. load_source_files/1, Origin is set to source(Path, Pos) where Path is the path of the source file, and Pos is a term describing the postition and layout of the rule in the file.

 defined_query(-Goals:list, -SolCount:int) is det

Dynamic predicate for query.

Arguments:

Goals	- List of goals in the query.
SolCount	- The number of answer sets to compute.

 defined_predicates(-Predicates:list) is det

Dynamic predicate for the list of predicate symbols defined in the input program.

Arguments:

Predicates

- List of predicate structs.

 defined_nmr_check(+Subchecks:list) is det

Dynamic predicate for the list of NMR sub-checks.

Arguments:

Subchecks

- The list of subcheck goals.

   96% These predicates are filled by assert_program/1 from the output of the
   97% parser.  scasp_load/1 realizes the entire compilation chain.
   98% Body terms contains variables as e.g. `'X'`.
   99
  100:- thread_local
  101    defined_rule/4,		% Name, Head, Body, Origin
  102    defined_query/2,            % Body, Count
  103    defined_predicates/1,       % list(Name) (1 clause)
  104    defined_nmr_check/1,
  105    defined_directive/1.        % directive

 program(?ProgramStruct:compound, ?Rules:list, ?Directives:list, ?Query:compound) is det

Convert a program structure into its components, or vice-versa.

Arguments:

ProgramStruct	- Program structure.
Rules	- List of rules.
Directives	- List of directives.
Query	- Query structure.

  117program(p(Rules, Directives, Query), Rules, Directives, Query).

 query(?QueryStruct:compound, ?Query:list, ?NMR_Check:list, ?SolutionCount:int) is det

Convert a query structure to its components, or vice-versa. NMR_Check will be unbound until after generate_nmr_check/0 has finished.

Arguments:

QueryStruct	- Query structure.
Query	- List of query goals.
NMR_Check	- List of NMR check goals (heads of NMR sub-checks).
SolutionCount	- Hard-coded solution count.

  131query(c(Q, Nmr_check, N), Q, Nmr_check, N).

 reserved_prefix(+Prefix:ground) is det

Define reserved prefixes for predicates and compound terms. These take the form of a single letter followed by an underscore. This predicate just tests the letter. The dummy prefix (o_) is appended to predicates and compound terms that either begin with an underscore (legal in ASP but not Prolog) or with a reserved prefix. It will be removed last before printing, and at most one copy will be removed, ensuring that user-defined predicates starting with a reserved prefix won't be processed the same as internally created ones.

Arguments:

Prefix

- The letter portion of the prefix.

  147reserved_prefix('c'). % classical negation
  148reserved_prefix('n'). % dual rule prefix
  149reserved_prefix('d'). % dummy prefix

 has_prefix(+Functor:atom, -Prefix:atom) is semidet

Succeed if Functor begins with a reserved prefix, returning the character part of the (first) prefix.

Arguments:

Functor	- The functor to test.
Prefix	- The character of the (first) reserved prefix of the functor.

  160has_prefix(F, C) :-
  161    sub_atom(F, 1, _, _, '_'),
  162    sub_atom(F, 0, 1, _, C),
  163    reserved_prefix(C). % the letter is a reserved prefix

 replace_prefix(+FunctorIn, +OldPrefix, +NewPrefix, -Functor)

  167replace_prefix(F0, P0, P, F) :-
  168    string_concat(P0, B, F0),
  169    atom_concat(P, B, F).

 non_printable(+Name) is semidet

True if Name should not be printed. This is true if it starts with an underscore or has a normal prefix and then an underscore.

  176non_printable(Name) :-
  177    sub_atom(Name, 0, _, _, '_'),
  178    !.
  179non_printable(Name) :-
  180    sub_atom(Name, 1, _, _, '__'),
  181    !.

 assert_program(+Statements:list) is det

Get rules, initial query and called predicates and assert them for easy access. This fills the dynamic predicates

• defined_predicates(List) with a list of predicate identifiers, atoms encoded as <name>_<arity>, e.g., parent_2 for parent/2.
• defined_rule(Name, Head, Body, Origin) where Name is the functor name of Head and Body represents the conjunction of the body as a list, and Origin denotes the source of the rule's definition.
• defined_query(List, Count) List is like Body above, expressing the query and Count is the number of answer sets to generate by default (based on the `Count { Query }.` syntax.
• defined_nmr_check(List) When defined, a list of one atom containing the rule name for the NMR check.

Arguments:

Statements

- List of rules and compute statements produced by DCG.

  204:- det(assert_program/1).  205
  206assert_program(Stmts) :-
  207    debug(scasp(compile), 'Converting program to internal format...', []),
  208    format_program(Stmts, Program),
  209    get_predicates(Program, Predicates),
  210    assert_predicates(Predicates),
  211    assert_program_struct(Program),
  212    maplist(handle_classical_negation, Predicates).

 format_program(+Statements:list, -Program:compound) is det

Convert the list of statements to a program structure containing a list of rules and a single query. Queries are generated from compute statements. Use the last compute statement encountered, or a default one if no other is found. The default will always succeed during execution, so the answer set returned will rely on the NMR check.

Arguments:

Statements	- List of rules and compute statements produced by DCG.
Program	- Program data struct.

  225format_program([], P) :-
  226    !,                       % no program
  227    predicate(G, '_false_0', []),
  228    query(Q, [not(G)], _, 1),
  229    program(P, [], [], Q).
  230format_program(X, P) :-
  231    predicate(G, '_false_0', []),
  232    AScount = 1,
  233    query(Q2, [not(G)], _, AScount),
  234    sort_by_type(X, R, D, Q2, Q),
  235    program(P, R, D, Q).

 sort_by_type(+Statements:list, -Rules:list, -Directives:list, +ComputeIn:compound, -ComputeOut:compound) is det

Take a list of statements, return a list of rules and the last compute statement encountered. Compute statement will be formatted as a query.

Arguments:

Statements	- List of rules and compute statements produced by DCG.
Rules	- extracted from Statements. Each rule is a term Head-Body.
Directives	- is a list of plain directive terms (without # or :-)
ComputeIn	- compute statement. @arg ComputeOut compute statement. Only the final compute statement is kept.

  250:- det(sort_by_type/5).  251
  252sort_by_type([source(Ref, X)|T], [source(Ref, X)|R], D, Ci, Co) :-
  253    c_rule(X, _, _),
  254    !,
  255    sort_by_type(T, R, D, Ci, Co).
  256sort_by_type([source(_, X)|T], R, D, _, Co) :-
  257    X = c(N, Q),
  258    query(C, Q, _, N),
  259    !,
  260    sort_by_type(T, R, D, C, Co).
  261sort_by_type([source(_, (:-(Directive)))|T], R, [Directive|D], C, Co) :-
  262    !,
  263    sort_by_type(T, R, D, C, Co).
  264sort_by_type([], [], [], C, C).

 get_predicates(+Program:compound, -Predicates:list) is det

Get a list of the predicate symbols used in the rules or query of the program. This includes predicates that are called but not defined. The internal-use predicate _false_0 should be included explictly, in case a hard-coded query overrode the default one. We add _false_0 as head of the query for that purpose. This both gets the query in the shape of a rule and ensures _false_0 is included.

Arguments:

Program	- A program struct.
Predicates	- A list of predicate symbols defined in the program.

  279:- det(rule_predicates/2).  280
  281get_predicates(P, Ps) :-
  282    program(P, R, _, Q),
  283    query(Q, Qs, _, _),
  284    rules_predicates(['_false_0'-Qs|R], Ps).
  285
  286rules_predicates(Rules, Preds) :-
  287    maplist(rule_predicates, Rules, Preds0),
  288    append(Preds0, Preds1),
  289    list_to_set(Preds1, Preds).
  290
  291rule_predicates(source(_, R), Preds) :-
  292    !,
  293    rule_predicates(R, Preds).
  294rule_predicates(R, Preds) :-
  295    c_rule(R, H, B),
  296    atom_predicate(H, F),
  297    convlist(atom_predicate, B, FB),
  298    list_to_set([F|FB], Preds).
  299
  300atom_predicate(not(X), P) :-
  301    atom_predicate(X, P).
  302atom_predicate(X, F) :-
  303    predicate(X, F, _).

 handle_classical_negation(+Predicate:atom) is det

If Predicate is classically negated (in the source starts with '-'). Assign the required number of variables, then create a rule of the form

:- -x, x.

Arguments:

Predicate

- is the name (atom) of a predicate

  315handle_classical_negation(X) :-
  316    has_prefix(X, 'c'), % classically negated literal
  317    atom_concat(c_, Xn, X), % non-negated literal
  318    defined_predicates(P),
  319    memberchk(Xn, P), % only add constraint if non-negated literal is actually used.
  320    !,
  321    split_functor(X, _, N), % get arity
  322    var_list(N, A), % get args,
  323    X2 =.. [X|A],
  324    Xn2 =.. [Xn|A],
  325    predicate(H, '_false_0', []), % dummy head for headless rules
  326    c_rule(R, H, [X2, Xn2]),
  327    assert_rule(neg(R)).
  328handle_classical_negation(_).

 assert_program_struct(+Program:compound) is det

Assert rules and query from program struct.

Arguments:

Program

- A program struct.

  336assert_program_struct(P) :-
  337    program(P, R, D, Q),
  338    maplist(assert_rule, R),
  339    maplist(assert_directive, D),
  340    assert_query(Q).

 assert_rule(+Rule:compound) is det

Assert a program rule.

Arguments:

Rule	- A rule struct.

  348:- det(assert_rule/1).  349
  350assert_rule(Rule) :-
  351    rule_origin(Rule, Origin, R),
  352    assert_rule_(R, Origin).
  353
  354assert_rule_(Rule, Origin) :-
  355    c_rule(Rule, H2, B),
  356    predicate(H2, H, _), % get the head without args
  357    assertz(defined_rule(H, H2, B, Origin)).
  358
  359rule_origin(source(Ref, Rule), Ref, Rule).
  360rule_origin(neg(Rule), generated(neg), Rule).
  361rule_origin(nmr(Rule), generated(nmr), Rule).
  362rule_origin(dual(Rule), generated(dual), Rule).

 assert_directive(+Directive) is det

Assert a directive

Arguments:

Directive

- is a term table(Pred), show(Pred) or pred(Pred)

  371assert_directive(D) :-
  372    assertz(defined_directive(D)).

 assert_query(+Query:compound) is det

Assert the initial query.

Arguments:

Query

- A query struct.

  380assert_query(Q) :-
  381    query(Q, Qs, _, N),
  382    assertz(defined_query(Qs, N)).

 assert_nmr_check(+NMR:list) is det

Assert the NMR check.

Arguments:

NMR	- The list of goals in the NMR check.

  390assert_nmr_check(NMR) :-
  391    c_rule(R, '_nmr_check_0', NMR),
  392    assert_rule(nmr(R)),
  393    assertz(defined_nmr_check(['_nmr_check_0'])).

 assert_predicates(+Predicates:list) is det

Assert the list of defined predicate symbols.

Arguments:

Predicates

- A list of predicates.

  401assert_predicates(Ps) :-
  402    assertz(defined_predicates(Ps)).

 destroy_program

Remove all asserted predicates to allow multiple funs with different programs.

  409destroy_program :-
  410    retractall(defined_rule(_, _, _, _)),
  411    retractall(defined_query(_, _)),
  412    retractall(defined_predicates(_)),
  413    retractall(defined_nmr_check(_)),
  414    retractall(defined_directive(_))