1:- module(scasp_modules,
    2          [ scasp_encoded_module_term/2, % ?MTerm, ?QTerm
    3            encoded_module_term/2,       % ?TermIn, ?TermOut
    4            unqualify_model_term/3,      % +Module, +TermIn, -TermOut
    5            model_term_module/2          % :Term, -Module
    6          ]).    7
    8/** <module> Encode modules
    9
   10The sCASP program representation and  solver   are  not module aware. We
   11solve this by encoding the module in  the functor names. The alternative
   12is to make the solver and program representation work with M:Term terms.
   13
   14This current approach  implies  overhead   in  program  preparation  and
   15returning results, but avoids overhead in   the compilation and solving.
   16As notably the solver is the slow part   it is likely that interning the
   17module into the names is both simpler and faster.
   18*/
   19
   20:- meta_predicate
   21    model_term_module(:, -).   22
   23%!  encoded_module_name(?QTerm, ?QName) is det.
   24%
   25%   Encode a module qualification into a name. Also deals with names
   26%   that embed classical negation (-Name).
   27
   28encoded_module_name(M:NName, QName),
   29    atom(M), atom(NName), atom_concat(-,Name, NName) =>
   30    atomic_list_concat([-,M,:,Name], QName).
   31encoded_module_name(M:Name, QName), atom(M), atom(Name) =>
   32    atomic_list_concat([M,:,Name], QName).
   33encoded_module_name(MName, QName), atom(QName) =>
   34    (   sub_atom(QName, B, _, A, :)
   35    ->  MName = M:Name,
   36        sub_atom(QName, _, A, 0, Name0),
   37        sub_atom(QName, 0, B, _, M0),
   38        (   atom_concat(-, M, M0)
   39        ->  atom_concat(-, Name0, Name)
   40        ;   M = M0,
   41            Name = Name0
   42        )
   43    ;   MName = QName
   44    ).
   45
   46%!  encoded_module_term(?TermIn, ?TermOut) is det.
   47
   48encoded_module_term(M:Term0, Term), atom(M) =>
   49    Term0 =.. [Name|Args],
   50    encoded_module_name(M:Name, QName),
   51    Term =.. [QName|Args].
   52encoded_module_term(MTerm, Term), callable(Term) =>
   53    functor(Term, QName, _),
   54    (   encoded_module_name(M:Name, QName)
   55    ->  Term =.. [_|Args],
   56        Term1 =.. [Name|Args],
   57        MTerm = M:Term1
   58    ;   MTerm = Term
   59    ).
   60
   61%!  scasp_encoded_module_term(?MTerm, ?QTerm) is det.
   62%
   63%   Map an explicit Prolog module qualification into one that is encoded
   64%   in the functor name.
   65
   66scasp_encoded_module_term(-Term, QTerm) =>
   67    QTerm = -Term1,
   68    scasp_encoded_module_term(Term, Term1).
   69scasp_encoded_module_term(not(Term), QTerm) =>
   70    QTerm = not(Term1),
   71    scasp_encoded_module_term(Term, Term1).
   72scasp_encoded_module_term(Term, -QTerm) =>
   73    Term = -Term1,
   74    scasp_encoded_module_term(Term1, QTerm).
   75scasp_encoded_module_term(Term, not(QTerm)) =>
   76    Term = not(Term1),
   77    scasp_encoded_module_term(Term1, QTerm).
   78scasp_encoded_module_term(MTerm, QTerm) =>
   79    encoded_module_term(MTerm, QTerm).
   80
   81%!  unqualify_model_term(+Module, +TermIn, -TermOut)
   82
   83unqualify_model_term(M, goal_origin(Term0, O), Term)  =>
   84    unqualify_model_term(M, Term0, Term1),
   85    Term = goal_origin(Term1, O).
   86unqualify_model_term(M, Term0, Term),
   87    functor(Term0, Name, 1), model_wrapper(Name) =>
   88    Term0 =.. [Name,Arg0],
   89    Term  =.. [Name,Arg],
   90    unqualify_model_term(M, Arg0, Arg).
   91unqualify_model_term(M, findall(Templ, Goal0, List), Findall) =>
   92    Findall = findall(Templ, Goal, List),
   93    unqualify_model_term(M, Goal0, Goal).
   94unqualify_model_term(M, Term0, Term) =>
   95    (   encoded_module_term(Q:Term1, Term0)
   96    ->  (   Q == M
   97        ->  Term = Term1
   98        ;   Term = Q:Term1
   99        )
  100    ;   Term0 = Term
  101    ).
  102
  103model_wrapper(-).
  104model_wrapper(not).
  105model_wrapper(chs).
  106model_wrapper(proved).
  107model_wrapper(assume).
  108model_wrapper(abduced).
  109
  110%!  model_term_module(:Term, -Module) is det.
  111
  112:- det(model_term_module/2).  113model_term_module(M0:Term, M) :-
  114    model_term_module(Term, M0, M).
  115
  116model_term_module(Term, M0, M),
  117    functor(Term, Name, 1), model_wrapper(Name) =>
  118    arg(1, Term, A),
  119    model_term_module(A, M0, M).
  120model_term_module(M:_Term, _, Q) =>
  121    Q = M.
  122model_term_module(Term, M0, M) =>
  123    (   encoded_module_term(Q:_, Term)
  124    ->  M = Q
  125    ;   M = M0
  126    )