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_pr_rules,
   29          [ generate_pr_rules/2,        % +Sources, +Options
   30            process_pr_pred/5,          % +Spec, -Atom, -Children, -Cond, -Human
   31            clean_pr_program/1          % +Module
   32          ]).   33
   34/** <module> Output formatting and printing.
   35
   36Predicates related to formatting and printing output. This includes predicates
   37that may be used for warning and error output.
   38
   39@author Kyle Marple
   40@version 20170510
   41@license BSD-3
   42*/
   43
   44:- use_module(modules).   45:- use_module(common).   46:- use_module(program).   47:- use_module(variables).   48
   49:- autoload(library(option), [option/3]).   50:- autoload(library(apply), [maplist/4, maplist/3, exclude/3, maplist/2]).   51:- autoload(library(lists), [member/2]).   52:- autoload(library(prolog_code), [mkconj/3]).   53:- autoload(library(dcg/basics), [prolog_var_name/3, string/3]).   54:- use_module(library(yall), [(>>)/5]).   55
   56:- op(950, xfx, ::).   57
   58:- meta_predicate
   59    generate_pr_rules(:, +).   60
   61% fail,warning,error
   62:- create_prolog_flag(scasp_unknown, warning, [keep(true)]).   63
   64%!  format_term(+EntryIn:compound, -EntryOut:compound,
   65%!              -Constraints:list, +Vars:compound) is det
   66%
   67%   Format a term for printing.
   68%
   69%   @arg EntryIn The initial entry.
   70%   @arg EntryOut The formatted entry.
   71%   @arg Constraints Any constraints on variables in the entry.
   72%   @arg Vars Variable struct for filling in values.
   73
   74format_term(X, X) :-
   75    is_var(X),				% constrained var
   76    !.
   77format_term(X, Xo) :-
   78    callable(X),
   79    !,
   80    format_predicate2(X, Xo).
   81format_term(X, X).		% anything else, just pass along
   82
   83%!  format_term_list(+ListIn:compound, -ListOut:compound) is det
   84%
   85%   Format each term in a list.
   86%
   87%   @arg ListIn The initial list.
   88%   @arg ListOut The formatted list.
   89
   90format_term_list([], []).
   91format_term_list([X|T], [X2|T2]) :-
   92    format_term(X, X2),
   93    format_term_list(T, T2).
   94
   95%!  format_predicate2(+EntryIn:compound, -EntryOut:compound) is det
   96%
   97%   Given a term, remove the  arity,   strip  any  prefixes, and process
   98%   arguments.
   99%
  100%   @arg EntryIn The initial entry.
  101%   @arg EntryOut The formatted entry.
  102
  103format_predicate2(Xi, Xo) :-
  104    Xi = [_|_], % list
  105    !,
  106    format_predicate3(Xi, Xo).
  107format_predicate2(Xi, Xo) :-
  108    predicate(Xi, X2, A),
  109    atom(X2), % compound term, predicate or atom
  110    !,
  111    split_functor(X2, X3, _), % strip arity
  112    strip_prefixes(X3, X4),
  113    format_predicate3(A, A2),
  114    (   X4 = not(Xn) % append args
  115    ->  Xn2 =.. [Xn|A2],
  116        Xo = not(Xn2)
  117    ;   Xo =.. [X4|A2]
  118    ).
  119format_predicate2(Xi, Xo) :-
  120    Xi =.. [X2|A], % compound term, but not a predicate or atom head
  121    !,
  122    format_predicate3(A, A2),
  123    Xo =.. [X2|A2].
  124format_predicate2(X, X).
  125
  126%!  format_predicate3(+ArgsIn:list, -ArgsOut:list) is det
  127%
  128%   Process a list of predicate args or variable constraints.
  129%
  130%   @arg ArgsIn Input args.
  131%   @arg ArgsOut Output args.
  132
  133format_predicate3([], []) :-
  134    !.
  135format_predicate3([X|T], [Y|T2]) :-
  136    !,
  137    format_predicate4(X, Y),
  138    format_predicate3(T, T2).
  139format_predicate3(X, Y) :-
  140    format_predicate4(X, Y).
  141
  142%!  format_predicate4(+ArgsIn:list, -ArgsOut:list) is det
  143%
  144%   Process  a  single  predicate  arg  or  variable  constraint.  Where
  145%   possible, substitute previously used variables   for  variables with
  146%   the same value ID. This makes the final output more readable.
  147%
  148%   @arg ArgIn Input arg.
  149%   @arg ArgOut Output arg.
  150
  151format_predicate4(X, X) :-
  152    is_var(X),
  153    !.
  154format_predicate4(Xi, Xo) :-
  155    format_predicate2(Xi, Xo).
  156
  157%!  strip_prefixes(+FunctorIn:atom, -FunctorOut:atom) is det
  158%
  159%   Strip any reserved prefixes added during processing. If appropriate,
  160%   modify the output functor to restore   formatting represented by the
  161%   prefix. To ensure that prefixes  added   by  the user remain intact,
  162%   this predicate will return after removing a single copy of the dummy
  163%   prefix, if encountered. Otherwise,  all   reserved  prefixes will be
  164%   stripped. To prevent errors,  the  dual   rule  prefix,  if present,
  165%   should always be first.
  166%
  167%   @arg FunctorIn Input functor
  168%   @arg FunctorOut Output functor
  169
  170strip_prefixes(Fi, Fo) :-
  171    atom_concat(c_, F1, Fi),		% 'c_': classical negation
  172    !,
  173    strip_prefixes(F1, F2),
  174    atom_concat(-, F2, Fo).
  175strip_prefixes(Fi, not(Fo)) :-
  176    atom_concat(n_, F1, Fi),		% 'n_': classical negation
  177    !,
  178    strip_prefixes(F1, Fo).
  179strip_prefixes(Fi, Fo) :-
  180    has_prefix(Fi, C),
  181    C \== 'd',				% non-dummy prefix
  182    !,
  183    sub_atom(Fi, 2, _, 0, F1),
  184    strip_prefixes(F1, Fo).
  185strip_prefixes(Fi, Fo) :-
  186    atom_concat(d_, Fo, Fi),		% 'd_': dummy prefix, remove and finish
  187    !.
  188strip_prefixes(Fi, Fo) :-		% '_c_' prefixes change to 'o_'
  189    atom_concat('_c_', Fc, Fi),
  190    !,
  191    atom_concat('o_-', Fc, Fo).
  192strip_prefixes(Fi, Fo) :-		% '_' prefixes change to 'o_'
  193    atom_concat('_', Fc, Fi),
  194    !,
  195    atom_concat('o_', Fc, Fo).
  196strip_prefixes(F, F).
  197
  198%!  generate_pr_rules(:Sources, +Options)
  199%
  200%   Translate the sCASP program from the  defined_* predicates into pr_*
  201%   predicates  for  sCASP.  It  creates    clauses  for  the  following
  202%   predicates in the target module:
  203%
  204%     - pr_rule/3
  205%     - pr_query/1
  206%     - pr_user_predicate/1
  207%     - pr_table_predicate/1
  208%     - pr_show_predicate/1
  209%     - pr_pred_predicate/4.
  210
  211:- det(generate_pr_rules/2).  212
  213generate_pr_rules(M:_Sources, Options) :-
  214    check_existence(Options),
  215    findall(O-R, (defined_rule(_, H, B, O), c_rule(R, H, B)), Rs),
  216    maplist([O-R, O, R]>>true, Rs, Origins, Rs1),
  217    format_term_list(Rs1,Rs2),
  218    maplist([O, H-B, c(O, H, B)]>>true, Origins, Rs2, Rs3),
  219    (   defined_nmr_check(NMR)
  220    ->  format_term_list(NMR, NMR2)
  221    ;   NMR2 = []
  222    ),
  223    (   defined_query(Q,_),
  224        format_term_list(Q,Q2),
  225        assert_pr_query(M:Q2)
  226    ->  true
  227    ;   true
  228    ),
  229    handle_table_directives(M),
  230    handle_show_directives(M),
  231    handle_pred_directives(M),
  232    assert_pr_rules(Rs3, M),
  233    assert_pr_rules([c(generated(nmr), 'global_constraints', NMR2)], M).
  234
  235:- det((handle_table_directives/1,
  236        handle_show_directives/1,
  237        handle_pred_directives/1)).  238
  239handle_table_directives(M) :-
  240    findall(T, defined_directive(table(T)), Ts),
  241    format_term_list(Ts, Ts2),
  242    assert_pr_table(Ts2, M).
  243
  244handle_show_directives(M) :-
  245    findall(S, defined_directive(show(S)), Ss),
  246    format_term_list(Ss, Ss2),
  247    assert_pr_show(Ss2, M).
  248
  249handle_pred_directives(M) :-
  250    findall(P, defined_directive(pred(P)), Ps),
  251    format_term_list(Ps, Ps2),
  252    assert_pr_pred(Ps2, M).
  253
  254%!  assert_pr_table(+Tabled) is det.
  255
  256assert_pr_table([], _) => true.
  257assert_pr_table([H|T], M) =>
  258    assert_pr_table(H, M),
  259    assert_pr_table(T, M).
  260assert_pr_table((H,T), M) =>
  261    assert_pr_table(H, M),
  262    assert_pr_table(T, M).
  263assert_pr_table(Name/Arity, M) =>
  264    assert(M:pr_table_predicate(Name/Arity)).
  265
  266%!  assert_pr_show(+Atoms) is det.
  267
  268assert_pr_show([], _) => true.
  269assert_pr_show([H|T], M) =>
  270    assert_pr_show(H, M),
  271    assert_pr_show(T, M).
  272assert_pr_show((H,T), M) =>
  273    assert_pr_show(H, M),
  274    assert_pr_show(T, M).
  275assert_pr_show(not(Name/Arity), M) =>
  276    functor(T, Name, Arity),
  277    assert(M:pr_show_predicate(not(T))).
  278assert_pr_show(Name/Arity, M) =>
  279    functor(T, Name, Arity),
  280    assert(M:pr_show_predicate(T)).
  281
  282%!  process_pr_pred(+PredDecl) is det.
  283
  284assert_pr_pred([], _) => true.
  285assert_pr_pred([H|T], M) =>
  286    assert_pr_pred(H, M),
  287    assert_pr_pred(T, M).
  288assert_pr_pred((H,T), M) =>
  289    assert_pr_pred(H, M),
  290    assert_pr_pred(T, M).
  291assert_pr_pred(T, M) =>
  292    process_pr_pred(T, Atom, Children, Cond, Human),
  293    assert(M:pr_pred_predicate(Atom, Children, Cond, Human)).
  294
  295%!  process_pr_pred(+Spec, -Atom, -Children, -Condition, -Human) is det.
  296%
  297%   Process a ``#pred Spec :: Template.`` directive.
  298%
  299%   @arg Spec is a term Head::Template,  where   Head  is  an sCASP atom
  300%   where the variables are represented  as   $(Name)  and Template is a
  301%   string that embeds "@(Var)", "@(Var:Type)", "{{Var}}" or
  302%   "{{Var:Type}}"
  303%   @arg Pred is a term `Head::format(Fmt, Args)`, where `Fmt` contains
  304%   ~p and the arguments are of the shape `@($(Var):Type)`, which is
  305%   printed as ``"<Var>, a <Type>"``
  306
  307:- det(process_pr_pred/5).  308
  309process_pr_pred(Spec::html(HTML), A, Children, Cond, Human) =>
  310    revar(Spec+HTML, Spec1+HTML1, _),
  311    atom_cond(Spec1, A, Children, Cond),
  312    Human = html(HTML1).
  313process_pr_pred(Spec::B, A, Children, Cond, Human) =>
  314    atom_codes(B, Chars),
  315    phrase(pr_pred(FmtChars, Args, Spec, Spec1), Chars),
  316    atom_codes(Fmt, FmtChars),
  317    revar(Spec1, Spec2, _),                % need for s(CASP) input with vars
  318    atom_cond(Spec2, A, Children, Cond),   % not in template
  319    Human = format(Fmt,Args).
  320
  321pr_pred([0'~,0'p|Fmt], [@(Var:Type)|Args], A0, A) -->
  322    temp_var_start(Style), prolog_var_name(VarName),
  323    { insert_var(A0, A1, VarName, Var) },
  324    (   ":"
  325    ->  (   string(TypeChars), temp_var_end(Style)
  326        ->  {atom_codes(Type, TypeChars)}
  327        )
  328    ;   temp_var_end(Style)
  329    ->  {Type = ''}
  330    ),
  331    !,
  332    pr_pred(Fmt, Args, A1, A).
  333pr_pred([H|T], Args, A0, A) -->
  334    [H],
  335    !,
  336    pr_pred(T, Args, A0, A).
  337pr_pred([], [], A, A) -->
  338    [].
  339
  340temp_var_start(classic) --> "@(".
  341temp_var_start(modern)  --> "{{".
  342
  343temp_var_end(classic) --> ")".
  344temp_var_end(modern)  --> "}}".
  345
  346%!  insert_var(+TermIn, -Term, +VarName, +Var) is det.
  347
  348insert_var($(Name), Repl, Name, Var) =>
  349    Repl = Var.
  350insert_var('$VAR'(Name), Repl, Name, Var) =>
  351    Repl = Var.
  352insert_var(V0, Repl, Name, Var), var(V0) =>
  353    (   prolog_load_context(variable_names, Bindings),
  354        member(Name = V1, Bindings),
  355        V0 == V1
  356    ->  Repl = Var
  357    ;   Repl = V0
  358    ).
  359insert_var(Name, Repl, Name, Var) =>
  360    Repl = Var.
  361insert_var(In, Out, Name, Var), compound(In) =>
  362    In =.. [F|Args0],
  363    maplist(insert_var_r(Name, Var), Args0, Args),
  364    Out =.. [F|Args].
  365insert_var(In, Out, _, _) =>
  366    Out = In.
  367
  368insert_var_r(Name, Var, In, Out) :-
  369    insert_var(In, Out, Name, Var).
  370
  371%!  atom_cond(+Spec, -Atom, -Children, -Condition) is det.
  372%
  373%   Translate  a  pred/1  condition.  Spec  specifies   a  node  in  the
  374%   justification tree. Its general form   is `AtomSpec-Children`, where
  375%   `Children` is one of
  376%
  377%     - A list of specifications.  The specification matches if each
  378%       specification in the children list matches one of the
  379%       children of the justification tree.  Non-matched children
  380%       remain in the tree and are used as justification normally.
  381%       If the list ends with `-`, e.g. `[p(X)|-]`, all non-matched
  382%       children are discarded.
  383%     - The atom `-`.  All children are discarded.
  384%     - The atom `*`.  This is the default of there are no children
  385%       and causes the node to be processed normally.
  386%
  387%   Each `AtomSpec` is either a  plain   `Atom`,  one wrapped, `-(Atom)`
  388%   `not(Atom)` or `not(-(Atom))`. A condition may   be added to an Atom
  389%   as a conjunction, e.g., this denotes the  atom p(X), but only if `X`
  390%   is an integer.
  391%
  392%       :- pred (p(X),integer(X)) :: "bla bla {{X}}".
  393
  394:- det(atom_cond/4).  395
  396atom_cond(Atom0-Children0, Atom, Children, Cond) =>
  397    atom_cond(Atom0, Atom, Cond0),
  398    atom_cond_list(Children0, Children, Cond0, Cond).
  399atom_cond(Atom0, Atom, Children, Cond) =>
  400    Children = '*',
  401    atom_cond(Atom0, Atom, Cond).
  402
  403atom_cond((Atom0,Cond0), Atom, Cond) =>
  404    Atom = Atom0,
  405    inline_cond(Cond0, Cond).
  406atom_cond(Atom0, Atom, Cond) =>
  407    Atom = Atom0,
  408    Cond = true.
  409
  410atom_cond_list(-, -, Cond, Cond) :-
  411    !.
  412atom_cond_list([], [], Cond, Cond).
  413atom_cond_list([H0|T0], [H|T], Cond0, Cond) :-
  414    atom_cond(H0, H, Cond1),
  415    mkconj(Cond0, Cond1, Cond2),
  416    atom_cond_list(T0, T, Cond2, Cond).
  417
  418inline_cond(var(X), Cond) =>
  419    Cond = (var(X)->true;X = '$VAR'(_)).
  420inline_cond(nonvar(X), Cond) =>
  421    Cond = (var(X)->false;X \= '$VAR'(_)).
  422inline_cond((C0,C1), Cond) =>
  423    inline_cond(C0, D0),
  424    inline_cond(C1, D1),
  425    mkconj(D0,D1, Cond).
  426inline_cond(C, Cond) =>
  427    Cond = C.
  428
  429
  430%!  assert_pr_rules(+Rules:list, +Module) is det.
  431
  432assert_pr_rules([], _).
  433assert_pr_rules([c(Origin, Head, Body)|Rs], M) :-
  434    !,
  435    revar(Head-Body,H-B, _),
  436    assert(M:pr_rule(H, B, Origin)),
  437    assert_pr_user_predicate([H], M),
  438    assert_pr_rules(Rs, M).
  439
  440
  441assert_pr_query(M:Q) :-
  442    assert(M:pr_query(Q)).
  443
  444assert_pr_user_predicate([], _).
  445assert_pr_user_predicate([P|Ps], M) :-
  446    functor(P, Name, La),
  447    (   M:pr_user_predicate(Name/La)
  448    ->  true
  449    ;   assert(M:pr_user_predicate(Name/La))
  450    ),
  451    assert_pr_user_predicate(Ps, M).
  452
  453
  454%!  check_existence(+Options)
  455%
  456%   Check that all referenced predicates are defined.
  457
  458check_existence(Options) :-
  459    current_prolog_flag(scasp_unknown, DefaultMode),
  460    option(unknown(Mode), Options, DefaultMode),
  461    (   Mode == fail
  462    ->  true
  463    ;   defined_predicates(Preds),
  464        exclude(defined, Preds, Undef0),
  465        maplist(scasp_pred_pi, Undef0, Undef),
  466        (   Undef == []
  467        ->  true
  468        ;   Mode == warning
  469        ->  maplist(report_undef, Undef)
  470        ;   throw(error(scasp_undefined(Undef), _))
  471        )
  472    ).
  473
  474defined('_false_0').
  475defined(true_0).
  476defined(false_0).
  477defined(findall_3).
  478defined(inf_2).
  479defined(sup_2).
  480defined(Name) :-
  481    defined_rule(Name, _, _, _).
  482
  483scasp_pred_pi(DecoratedName, Name/Arity) :-
  484    split_functor(DecoratedName, PrefixedName, Arity),
  485    strip_prefixes(PrefixedName, Name).
  486
  487report_undef(PI) :-
  488    scasp_is_defined(PI),
  489    !.
  490report_undef(PI) :-
  491    print_message(warning,
  492                  error(existence_error(scasp_predicate, PI), _)).
  493
  494scasp_is_defined(QName/Arity) :-
  495    encoded_module_term(M:Name, QName),
  496    !,
  497    (   raise_negation(Name, -TheName)
  498    ->  functor(Head, TheName, Arity),
  499        predicate_property(M:Head, defined)
  500    ;   functor(Head, Name, Arity),
  501        predicate_property(M:Head, defined)
  502    ).
  503
  504%!  clean_pr_program(+Module) is det.
  505%
  506%   Prepare Module to receive a  compiled   sCASP  program. This wipes a
  507%   possibly existing sCASP program. It also   relies on the side effect
  508%   of retractall/1 to create a non-existing predicate as _dynamic_.
  509
  510clean_pr_program(M) :-
  511    retractall(M:pr_query(_)),
  512    retractall(M:pr_rule(_,_,_)),
  513    retractall(M:pr_user_predicate(_)),
  514    retractall(M:pr_table_predicate(_)),
  515    retractall(M:pr_show_predicate(_)),
  516    retractall(M:pr_pred_predicate(_,_,_,_)),
  517    retractall(M:pr_dcc_predicate(_,_))