1/*  Part of sCASP
    2
    3    Author:        Jan Wielemaker
    4    E-mail:        jan@swi-prolog.org
    5    Copyright (c)  2021, SWI-Prolog Solutions b.v.
    6    All rights reserved.
    7
    8    Redistribution and use in source and binary forms, with or without
    9    modification, are permitted provided that the following conditions
   10    are met:
   11
   12    1. Redistributions of source code must retain the above copyright
   13       notice, this list of conditions and the following disclaimer.
   14
   15    2. Redistributions in binary form must reproduce the above copyright
   16       notice, this list of conditions and the following disclaimer in
   17       the documentation and/or other materials provided with the
   18       distribution.
   19
   20    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
   21    "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
   22    LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
   23    FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
   24    COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
   25    INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
   26    BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
   27    LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   28    CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
   29    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
   30    ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
   31    POSSIBILITY OF SUCH DAMAGE.
   32*/
   33
   34:- module(scasp_embed,
   35          [ begin_scasp/1,              % +Unit
   36            begin_scasp/2,              % +Unit, +Exports
   37            end_scasp/0,
   38            scasp_listing/2,            % +Unit, +Options
   39            scasp_model/1,              % :Model
   40            scasp_model/2,              % :Model, +Options
   41            scasp_stack/1,              % -Stack
   42            scasp_justification/2,      % -Tree, +Options
   43            (not)/1,                    % :Query
   44            (-)/1,                      % :Query
   45
   46            op(700, xfx, .\=.),
   47            op(700, xfx, '\u2209'),
   48            op(900, fy, not)
   49          ]).   50:- use_module(ops).   51:- use_module(input).   52:- use_module(compile).   53:- use_module(predicates).   54:- use_module(solve).   55:- use_module(model).   56:- use_module(stack).   57:- use_module(options).   58:- use_module(listing).   59
   60:- use_module(library(apply)).   61:- use_module(library(error)).   62:- use_module(library(lists)).   63:- use_module(library(prolog_code)).   64
   65:- meta_predicate
   66    scasp_model(:),
   67    scasp_justification(:, +),
   68    not(0),
   69    -(:).   70
   71% one of `false`, `true`, `unicode` or `human`
   72:- create_prolog_flag(scasp_show_model,
   73                      false,
   74                      [keep(true), type(atom)]).   75:- create_prolog_flag(scasp_show_justification,
   76                      false,
   77                      [keep(true), type(atom)]).   78
   79/** <module>  Embed sCASP programs in Prolog sources
   80
   81This module allows embedding sCASP programs inside a Prolog module.
   82Currently the syntax is:
   83
   84```
   85:- begin_scasp(UnitName[, Exports]).
   86
   87<sCASP program>
   88
   89:- end_scasp.
   90```
   91
   92The idea is to create wrappers  for   the  sCASP  user predicates in the
   93target module that evaluate an sCASP  query   as  a normal Prolog query,
   94providing access to the  model  and   justification.  The  bindings come
   95available as normal Prolog bindings.
   96
   97This is an  alternative  interface  to   defining  the  user  accessible
   98predicates using e.g., `:- scasp p/1,   q/2.`, which will then establish
   99the reachable predicates and perform  the   sCASP  conversion on them. I
  100think both have their value and the above one is simpler to start with.
  101
  102@tbd: incomplete
  103*/
  104
  105:- thread_local
  106    loading_scasp/3.                    % Unit, File, Dict
  107
  108%!  begin_scasp(+Unit).
  109%!  begin_scasp(+Unit, +Exports).
  110%
  111%   Start an embedded sCASP program.  Exports   is  a  list if predicate
  112%   indicators as use_module/2 that defines   the  sCASP predicates that
  113%   are made visible from the  enclosing   module  as Prolog predicates.
  114%   These predicates modify the Prolog syntax by:
  115%
  116%     - Defining appropriate operators
  117%     - Disable singleton checking
  118%
  119%   Otherwise the read clauses  are   asserted  verbatim. Directives are
  120%   terms #(Directive). Prolog directives (:- Directive) are interpreted
  121%   as sCASP __global constraints__. The   matching end_scasp/0 compiles
  122%   the sCASP program and creates wrappers  in the enclosing module that
  123%   call the sCASP solver.
  124%
  125%   The  sCASP  code   must   be    closed   using   end_scasp/0.   Both
  126%   begin_scasp/1,2 and end_scasp/0 must be used as directives.
  127
  128begin_scasp(Unit) :-
  129    begin_scasp(Unit, all).
  130
  131begin_scasp(Unit, Exports) :-
  132    scasp_module(Unit, Module),
  133    prolog_load_context(module, Context),
  134    source_location(File, Line),
  135    '$set_source_module'(OldModule, Module),
  136    '$declare_module'(Module, scasp, Context, File, Line, false),
  137    scasp_push_operators,
  138    '$style_check'(OldStyle, OldStyle),
  139    style_check(-singleton),
  140    discontiguous(Module:(#)/1),
  141    asserta(loading_scasp(Unit, File,
  142                          _{ module:Module,
  143                             old_module:OldModule,
  144                             old_style:OldStyle,
  145                             exports:Exports
  146                           })).
  147
  148scasp_module(Unit, Module) :-
  149    atom_concat('_scasp_', Unit, Module).
  150
  151%!  end_scasp
  152%
  153%   Close begin_scasp/1,2. See begin_scasp/1,2 for details.
  154
  155end_scasp :-
  156    throw(error(context_error(nodirective, end_scasp), _)).
  157
  158end_scasp(Clauses) :-
  159    (   retract(loading_scasp(Unit, _File, Dict))
  160    ->  _{ old_module:OldModule,
  161           old_style:OldStyle,
  162           exports:Exports
  163         } :< Dict,
  164        '$set_source_module'(_, OldModule),
  165        scasp_pop_operators,
  166        '$style_check'(_, OldStyle),
  167        (   Exports == []
  168        ->  Options = [unknown(fail)]
  169        ;   Options = []
  170        ),
  171        scasp_compile_unit(Unit, Options),
  172        link_clauses(OldModule, Unit, Clauses, Exports)
  173    ;   throw(error(context_error(scasp_close(-)), _))
  174    ).
  175
  176loading_scasp(Unit) :-
  177    source_location(File, _Line),
  178    loading_scasp(Unit,File,_).
  179
  180user:term_expansion(end_of_file, _) :-
  181    loading_scasp(Unit),
  182    print_message(error, scasp(not_closed_program(Unit))),
  183    end_scasp,
  184    fail.
  185user:term_expansion((:- Constraint), Clause) :-
  186    loading_scasp(_),
  187    Constraint \== end_scasp,
  188    !,
  189    Clause = ('_false_0' :- Constraint).
  190user:term_expansion((?- Query), Clause) :-
  191    loading_scasp(_),
  192    !,
  193    Clause = scasp_query(Query, 1).
  194user:term_expansion(#(discontiguous(Preds)), (:- discontiguous(Preds))) :-
  195    loading_scasp(_).
  196user:term_expansion(#(pred(Preds)), #(pred(Preds))) :-
  197    loading_scasp(_),
  198    prolog_load_context(variable_names, Vars),
  199    maplist(bind_var, Vars).
  200user:term_expansion((:- end_scasp), Clauses) :-
  201    \+ current_prolog_flag(xref, true),
  202    end_scasp(Clauses).
  203
  204bind_var(Name = $(Name)).
  205
  206
  207%!  scasp_compile_unit(+Unit, +Options) is det.
  208%
  209%   Compile an sCASP module.
  210
  211:- thread_local
  212    done_unit/1.                  % allow for mutually recursive #include
  213
  214scasp_compile_unit(Unit, Options) :-
  215    call_cleanup(scasp_compile_unit_(Unit, Options),
  216                 retractall(done_unit(_))).
  217
  218scasp_compile_unit_(Unit, Options) :-
  219    scasp_module(Unit, Module),
  220    (   current_module(Module)
  221    ->  true
  222    ;   existence_error(scasp_unit, Unit)
  223    ),
  224    findall(Clause, scasp_clause(Unit, Clause), Clauses),
  225    scasp_compile(Module:Clauses, Options).
  226
  227%!  scasp_clause(+Unit, -Clause) is nondet.
  228%
  229%   True when Clause is an sCASP clause or directive defined in Unit.
  230
  231scasp_clause(Unit, _Clause) :-
  232    done_unit(Unit),
  233    !,
  234    fail.
  235scasp_clause(Unit, Clause) :-
  236    assertz(done_unit(Unit)),
  237    scasp_module(Unit, Module),
  238    QHead = Module:Head,
  239    predicate_property(QHead, interpreted),
  240    \+ scasp_compiled(Head),
  241    \+ predicate_property(QHead, imported_from(_)),
  242    @(clause(Head, Body), Module),
  243    mkclause(Head, Body, Clause).
  244
  245mkclause(scasp_query(Query,_N), true, Clause) =>
  246    Clause = (?- Query).
  247mkclause(#(include(Unit)), true, Clause) =>
  248    scasp_clause(Unit, Clause).
  249mkclause(#(Directive), true, Clause) => % TBD: #abducible
  250    Clause = #(Directive).
  251mkclause('_false_0', Body, Clause) =>
  252    Clause = (:- Body).
  253mkclause(Head, true, Clause) =>
  254    Clause = Head.
  255mkclause(Head, Body, Clause) =>
  256    Clause = (Head :- Body).
  257
  258%!  link_clauses(+ContextModule, +Unit, -Clauses, +Exports) is det.
  259%
  260%   Create  link  clauses  that  make  the  user  predicates  from  Unit
  261%   available as Prolog predicates from Module.
  262
  263link_clauses(_ContextModule, Unit, Clauses, Exports) :-
  264    scasp_module(Unit, Module),
  265    findall(Head, link_predicate(Module:Head), Heads),
  266    check_exports(Exports, Heads),
  267    convlist(link_clause(Module, Exports), Heads, Clauses).
  268
  269link_predicate(Module:Head) :-
  270    Module:pr_user_predicate(PI),
  271    \+ not_really_a_user_predicate(PI),
  272    pi_head(PI, Head).
  273
  274% TBD: merge with user_predicate/1.
  275not_really_a_user_predicate((not)/1).
  276not_really_a_user_predicate(o_nmr_check/0).
  277not_really_a_user_predicate(global_constraints/0).
  278
  279check_exports(all, _) :- !.
  280check_exports(Exports, Heads) :-
  281    must_be(list, Exports),
  282    maplist(check_export(Heads), Exports).
  283
  284check_export(Heads, -Name/Arity) :-
  285    !,
  286    atom_concat(-, Name, NName),
  287    check_export(Heads, NName/Arity).
  288check_export(Heads, Export) :-
  289    pi_head(Export, EHead),             % raises an exception on malformed PI.
  290    (   memberchk(EHead, Heads)
  291    ->  true
  292    ;   existence_error(predicate, Export)
  293    ).
  294
  295link_clause(Module, Exports, Head,
  296            (Head :- scasp_embed:scasp_call(Module:Head))) :-
  297    (   Exports == all
  298    ->  true
  299    ;   functor(Head, NName, Arity),
  300        atom_concat(-, Name, NName)
  301    ->  memberchk(-Name/Arity, Exports)
  302    ;   pi_head(PI, Head),
  303        memberchk(PI, Exports)
  304    ).
  305
  306
  307%!  scasp_call(:Query)
  308%
  309%   Solve an sCASP goal from the interactive toplevel
  310
  311:- public scasp_call/1.  312
  313scasp_call(Query) :-
  314    scasp_compile_query(Query, Compiled, []),
  315    scasp_stack(StackIn),
  316    solve(Compiled, StackIn, StackOut, Model),
  317    save_model(Model),
  318    Compiled = M:_,                       % TBD: Properly handle the module
  319    save_stack(M:StackOut).
  320
  321%!  not(:Query)
  322%
  323%   sCASP NaF negation. Note that  this   conflicts  with the deprecated
  324%   standard Prolog not/1 predicate which is   a  synonym for \+/1. Make
  325%   sure to load sCASP into a module   where you want sCASP negation and
  326%   use \+/1 for Prolog negation in this model.
  327
  328not(M:Query) :-
  329    clause(M:Query, scasp_embed:scasp_call(Module:Query)),
  330    scasp_call(Module:not(Query)).
  331
  332%!  -(:Query)
  333%
  334%   sCASP classical negation.
  335
  336-(M:Query) :-
  337    Query =.. [Name|Args],
  338    atom_concat(-, Name, NName),
  339    NQuery =.. [NName|Args],
  340    clause(M:NQuery, scasp_embed:scasp_call(Module:NQuery)),
  341    scasp_call(Module:NQuery).
  342
  343
  344%!  save_model(+Model) is det.
  345%
  346%   Save the model.
  347%
  348%   @tbd We must qualify the model.
  349
  350save_model(Model) :-
  351    (   nb_current(scasp_model, Model0)
  352    ->  append(Model, Model0, FullModel),
  353        b_setval(scasp_model, FullModel)
  354    ;   b_setval(scasp_model, Model)
  355    ).
  356
  357%!  scasp_model(:Model) is semidet.
  358%!  scasp_model(:Model, +Options) is semidet.
  359%
  360%   True when Model  represents  the  current   set  of  true  and false
  361%   literals.
  362
  363scasp_model(M:Model) :-
  364    scasp_model(M:Model, []).
  365
  366scasp_model(M:Model, _Options) :-
  367    nb_current(scasp_model, RawModel),
  368    canonical_model(RawModel, Model1),
  369    unqualify_model(Model1, M, Model).
  370
  371save_stack(Stack) :-
  372    b_setval(scasp_stack, Stack),
  373    justification_tree(Stack, Tree, []),
  374    b_setval(scasp_tree, Tree).
  375
  376%!  scasp_stack(-Stack) is det.
  377%
  378%   True when Stack represents the justification   of  the current sCASP
  379%   answer.
  380
  381scasp_stack(Stack) :-
  382    (   nb_current(scasp_stack, Stack0)
  383    ->  Stack = Stack0
  384    ;   Stack = []
  385    ).
  386
  387%!  scasp_justification(:Tree, +Options) is semidet.
  388%
  389%   Justification for the current sCASP answer.
  390
  391scasp_justification(M:Tree, Options) :-
  392    nb_current(scasp_tree, Tree0),
  393    remove_origins(Tree0, Tree1, Options),
  394    unqualify_justitication_tree(Tree1, M, Tree).
  395
  396remove_origins(Tree0, Tree, Options) :-
  397    option(source(false), Options),
  398    !,
  399    remove_origins(Tree0, Tree).
  400remove_origins(Tree, Tree, _).
  401
  402remove_origins(M:Tree0, Result) =>
  403    Result = M:Tree,
  404    remove_origins(Tree0, Tree).
  405remove_origins(Term0-Children0, Result) =>
  406    Result = Term-Children,
  407    remove_origin(Term0, Term),
  408    maplist(remove_origins, Children0, Children).
  409remove_origins(Nodes0, Nodes), is_list(Nodes0) =>
  410    maplist(remove_origins, Nodes0, Nodes).
  411remove_origins(Node0, Node) =>
  412    remove_origin(Node0, Node).
  413
  414remove_origin(goal_origin(Term, _), Result) =>
  415    Result = Term.
  416remove_origin(Term, Result) =>
  417    Result = Term.
  418
  419
  420%!  scasp_listing(+Unit, +Options)
  421%
  422%   List the transformed program for Unit
  423
  424scasp_listing(Unit, Options) :-
  425    scasp_module(Unit, Module),
  426    scasp_portray_program(Module:Options).
  427
  428:- residual_goals(scasp_residuals).  429
  430%!  scasp_residuals// is det.
  431%
  432%   Hook into the SWI-Prolog toplevel  to   add  additional goals to the
  433%   answer conjunction. Optionally provides the model and justification.
  434
  435scasp_residuals -->
  436    { '$current_typein_module'(TypeIn),
  437      scasp_residual_types(Types)
  438    },
  439    scasp_residuals(Types, TypeIn).
  440
  441scasp_residuals([], _) -->
  442    [].
  443scasp_residuals([model(Options)|T], M) -->
  444    (   {scasp_model(M:Model, Options)}
  445    ->  [ scasp_show_model(Model, Options) ]
  446    ;   []
  447    ),
  448    scasp_residuals(T, M).
  449scasp_residuals([justification(Options)|T], M) -->
  450    (   {scasp_stack(Stack), Stack \== []}
  451    ->  [ scasp_show_stack(M:Stack, Options) ]
  452    ;   []
  453    ),
  454    scasp_residuals(T, M).
  455
  456scasp_residual_types(Types) :-
  457    findall(Type, scasp_residual_type(Type), Types).
  458
  459scasp_residual_type(model(Options)) :-
  460    current_prolog_flag(scasp_show_model, Spec),
  461    Spec \== false,
  462    res_options(Spec, Options).
  463scasp_residual_type(justification(Options)) :-
  464    current_prolog_flag(scasp_show_justification, Spec),
  465    Spec \== false,
  466    res_options(Spec, Options).
  467
  468res_options(List, Options), is_list(List) =>
  469    Options = List.
  470res_options(true, Options) =>
  471    Options = [unicode(true)].
  472res_options(unicode, Options) =>
  473    Options = [unicode(true)].
  474res_options(human, Options) =>
  475    Options = [human(true)].
  476
  477user:portray(scasp_show_model(Model, Options)) :-
  478    ansi_format(comment, '% s(CASP) model~n', []),
  479    print_model(Model, Options).
  480user:portray(scasp_show_stack(M:Stack, Options)) :-
  481    ansi_format(comment, '% s(CASP) justification', []),
  482    justification_tree(Stack, Tree0, Options),
  483    unqualify_justitication_tree(Tree0, M, Tree),
  484    print_justification_tree(Tree, [full_stop(false)|Options]).
  485user:portray('\u2209'(V,S)) :-          % not element of
  486    format('~p \u2209 ~p', [V, S]).
  487
  488
  489		 /*******************************
  490		 *       HIGHLIGHT SUPPORT	*
  491		 *******************************/
  492
  493:- multifile
  494    prolog:alternate_syntax/4,
  495    prolog:xref_update_syntax/2.  496
  497prolog:alternate_syntax(scasp, Module, Setup, Restore) :-
  498    Setup = scasp_ops:scasp_push_operators(Module),
  499    Restore = scasp_ops:scasp_pop_operators.
  500
  501prolog:xref_update_syntax(begin_scasp(_Unit), Module) :-
  502    scasp_ops:scasp_push_operators(Module).
  503prolog:xref_update_syntax(begin_scasp(_Unit, _Exports), Module) :-
  504    scasp_ops:scasp_push_operators(Module).
  505prolog:xref_update_syntax(end_scasp, _Module) :-
  506    scasp_ops:scasp_pop_operators.
  507
  508:- multifile
  509    prolog_colour:term_colours/2.  510
  511prolog_colour:term_colours(#(Directive),
  512                           expanded - [DirColours]) :-
  513    debug(scasp(highlight), 'Got ~p', [Directive]),
  514    dir_colours(Directive, DirColours).
  515
  516dir_colours(pred(_Head::_Template),
  517            expanded -
  518            [ expanded -
  519              [ body,
  520                comment(_)
  521              ]
  522            ]).
  523dir_colours(show(Preds),
  524            expanded - [Colours]) :-
  525    decl_show_colours(Preds, Colours).
  526dir_colours(include(_Unit),
  527            expanded -
  528            [ classify
  529            ]).
  530dir_colours(discontiguous(_Preds),
  531            expanded -
  532            [ declarations(discontiguous)
  533            ]).
  534
  535decl_show_colours((A,B), Colours) =>
  536    Colours = classify-[CA,CB],
  537    decl_show_colours(A, CA),
  538    decl_show_colours(B, CB).
  539decl_show_colours(not(_A), Colours) =>
  540    Colours = built_in-[declarations(show)].
  541decl_show_colours(_A, Colours) =>
  542    Colours = declarations(show).
  543
  544
  545		 /*******************************
  546		 *          GXREF SUPPORT	*
  547		 *******************************/
  548
  549%!  pce_xref_gui:gxref_called(?Source, ?Callable)
  550%
  551%   Hook into gxref/0 that may  extend   the  notion of predicates being
  552%   called by some infrastructure. Here, do two things:
  553%
  554%     - We silence called s(CASP) hooks
  555%     - If a predicate is defined using scasp_dynamic/1 and either the
  556%       positive or negative version is called, we consider it called.
  557
  558:- multifile pce_xref_gui:gxref_called/2.  559:- autoload(library(prolog_xref), [xref_called/4]).  560
  561pce_xref_gui:gxref_called(Source, Callable) :-
  562    nonvar(Source),
  563    callable(Callable),
  564    !,
  565    (   xref_called_cond(Source, Callable, _)
  566    ->  true
  567    ;   scasp_called(Callable)
  568    ->  true
  569    ;   xref_dynamic(Source, Callable),
  570        scasp_negate(Callable, NegCallable),
  571        xref_dynamic(Source, NegCallable),
  572        xref_called_cond(Source, NegCallable, _)
  573    ).
  574
  575xref_dynamic(Source, Callable) :-
  576    xref_defined(Source, Callable, dynamic(_)), !.
  577xref_dynamic(Source, Callable) :-
  578    xref_defined(Source, Callable, thread_local(_)).
  579
  580xref_called_cond(Source, Callable, Cond) :-
  581    xref_called(Source, Callable, By, Cond),
  582    By \= Callable.                 % recursive calls
  583
  584scasp_negate(Callable, NegCallable) :-
  585    atom(Callable),
  586    !,
  587    scasp_neg_atom(Callable, NegCallable).
  588scasp_negate(Callable, NegCallable) :-
  589    compound_name_arguments(Callable, Name, Args),
  590    scasp_neg_atom(Name, NegName),
  591    compound_name_arguments(NegCallable, NegName, Args).
  592
  593scasp_neg_atom(Neg, Pos) :-
  594    atom_concat(-, Pos, Neg),
  595    !.
  596scasp_neg_atom(Pos, Neg) :-
  597    atom_concat(-, Pos, Neg).
  598
  599scasp_called(pr_pred_predicate(_,_,_,_)).
  600scasp_called(scasp_expand_program(_,_,_,_)).
  601scasp_called(-)