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